[isabelle-dev] Example for global interpretation into instantiation [was: Future of permanent_interpretation]
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Thu Dec 17 17:49:53 CET 2015
Hi Clemens,
I have found a potential example for global interpretation into
instantiation in the existing Isabelle sources.
The example is presented in the attached patches, which can be applied
in alphabetical order on top of 32a530a5c54c.
The first patch experimentally introduces a global_interpretation
keyword, which is then used in theory src/HOL/Library/Saturated.thy:
instantiation sat :: (len) "{Inf, Sup}"
begin
global_interpretation Inf_sat: semilattice_neutr_set min "top :: 'a sat"
defines Inf_sat = Inf_sat.F
by standard (simp add: min_def)
global_interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a sat"
defines Sup_sat = Sup_sat.F
by standard (simp add: max_def bot.extremum_unique)
end
Here we have a clear distinction between interpretation, which would
only last until the closing end, and the explicitly permanent global
interpretation which provides the necessary instance definitions.
This pattern, which uses interpretation as a kind of simple definitional
package, is very common nowadays, as can be seen in theories like
src/HOL/Groups_Big.thy, src/HOL/Groups_List.thy,
src/HOL/Lattices_Big.thy or src/HOL/Library/Multiset.thy.
I have prepared this to give some evidence that my insistence on proper
distinction between (confined) interpretation and (permanent) global
interpretation has significant practical implications (although the
experimental nature of the patches exhibits some issues in the internal
machinery which would have to worked out properly first). So, it is
really a good idea to have a separate keyword »global_interpretation«.
Hence, before letting »permanent_interpretation« stand as it is, I would
really prefer to replace the existing occurrences by
»global_interpretation«, to avoid confusion in the long run.
So, my minimal plan for the upcoming release would be:
* Provide »global_interpretation« as separate keyword.
* Discontinue »permanent_interpretation« entirely – remaining
occurrences are suitable for »global_interpretation«.
* »interpretation« retains its current traditional semantics. No
systematic replacement by »global_interpretation«.
* Polish the documentation accordingly.
I have no idea whether you have a time slot to consider and give
feedback on this; anyway this plan is quite minimal invasive wrt.
existing sources, so I am confident that it is appropriate for the
upcoming release.
All the best,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
# HG changeset patch
# Parent 32a530a5c54cfa3bd5263600e3bdfae87153627e
diff -r 32a530a5c54c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/Finite_Set.thy Thu Dec 17 17:34:35 2015 +0100
@@ -1209,7 +1209,7 @@
But now that we have @{const fold} things are easy:
\<close>
-permanent_interpretation card: folding "\<lambda>_. Suc" 0
+global_interpretation card: folding "\<lambda>_. Suc" 0
defines card = "folding.F (\<lambda>_. Suc) 0"
by standard rule
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy Thu Dec 17 17:34:35 2015 +0100
@@ -53,7 +53,7 @@
end
-permanent_interpretation Val_semilattice
+global_interpretation Val_semilattice
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof (standard, goal_cases)
case (1 a b) thus ?case
@@ -66,7 +66,7 @@
case 4 thus ?case by(auto simp: plus_const_cases split: const.split)
qed
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
defines AI_const = AI and step_const = step' and aval'_const = aval'
..
@@ -120,7 +120,7 @@
text{* Monotonicity: *}
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof (standard, goal_cases)
case 1 thus ?case by(auto simp: plus_const_cases split: const.split)
@@ -131,7 +131,7 @@
definition m_const :: "const \<Rightarrow> nat" where
"m_const x = (if x = Any then 0 else 1)"
-permanent_interpretation Abs_Int_measure
+global_interpretation Abs_Int_measure
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
and m = m_const and h = "1"
proof (standard, goal_cases)
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Thu Dec 17 17:34:35 2015 +0100
@@ -102,7 +102,7 @@
text{* First we instantiate the abstract value interface and prove that the
functions on type @{typ parity} have all the necessary properties: *}
-permanent_interpretation Val_semilattice
+global_interpretation Val_semilattice
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof (standard, goal_cases) txt{* subgoals are the locale axioms *}
case 1 thus ?case by(auto simp: less_eq_parity_def)
@@ -124,7 +124,7 @@
proofs (they happened in the instatiation above) but delivers the
instantiated abstract interpreter which we call @{text AI_parity}: *}
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
defines aval_parity = aval' and step_parity = step' and AI_parity = AI
..
@@ -155,7 +155,7 @@
subsubsection "Termination"
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof (standard, goal_cases)
case (1 _ a1 _ a2) thus ?case
@@ -166,7 +166,7 @@
definition m_parity :: "parity \<Rightarrow> nat" where
"m_parity x = (if x = Either then 0 else 1)"
-permanent_interpretation Abs_Int_measure
+global_interpretation Abs_Int_measure
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
and m = m_parity and h = "1"
proof (standard, goal_cases)
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Thu Dec 17 17:34:35 2015 +0100
@@ -302,7 +302,7 @@
"\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
by(drule (1) add_mono) simp
-permanent_interpretation Val_semilattice
+global_interpretation Val_semilattice
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
proof (standard, goal_cases)
case 1 thus ?case by transfer (simp add: le_iff_subset)
@@ -318,7 +318,7 @@
qed
-permanent_interpretation Val_lattice_gamma
+global_interpretation Val_lattice_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
defines aval_ivl = aval'
proof (standard, goal_cases)
@@ -327,7 +327,7 @@
case 2 show ?case unfolding bot_ivl_def by transfer simp
qed
-permanent_interpretation Val_inv
+global_interpretation Val_inv
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -350,7 +350,7 @@
done
qed
-permanent_interpretation Abs_Int_inv
+global_interpretation Abs_Int_inv
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -384,7 +384,7 @@
apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
-permanent_interpretation Abs_Int_inv_mono
+global_interpretation Abs_Int_inv_mono
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Thu Dec 17 17:34:35 2015 +0100
@@ -256,7 +256,7 @@
end
-permanent_interpretation Abs_Int_wn
+global_interpretation Abs_Int_wn
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -541,7 +541,7 @@
split: prod.splits if_splits extended.split)
-permanent_interpretation Abs_Int_wn_measure
+global_interpretation Abs_Int_wn_measure
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Thu Dec 17 17:34:35 2015 +0100
@@ -47,13 +47,13 @@
end
-permanent_interpretation Rep rep_cval
+global_interpretation Rep rep_cval
proof
case goal1 thus ?case
by(cases a, cases b, simp, simp, cases b, simp, simp)
qed
-permanent_interpretation Val_abs rep_cval Const plus_cval
+global_interpretation Val_abs rep_cval Const plus_cval
proof
case goal1 show ?case by simp
next
@@ -61,7 +61,7 @@
by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
qed
-permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
+global_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
defines AI_const = AI
and aval'_const = aval'
proof qed (auto simp: iter'_pfp_above)
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Thu Dec 17 17:34:35 2015 +0100
@@ -166,13 +166,13 @@
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
-permanent_interpretation Rep rep_ivl
+global_interpretation Rep rep_ivl
proof
case goal1 thus ?case
by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
qed
-permanent_interpretation Val_abs rep_ivl num_ivl plus_ivl
+global_interpretation Val_abs rep_ivl num_ivl plus_ivl
proof
case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
next
@@ -180,7 +180,7 @@
by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
qed
-permanent_interpretation Rep1 rep_ivl
+global_interpretation Rep1 rep_ivl
proof
case goal1 thus ?case
by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -188,7 +188,7 @@
case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
qed
-permanent_interpretation
+global_interpretation
Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
proof
case goal1 thus ?case
@@ -200,7 +200,7 @@
auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
qed
-permanent_interpretation
+global_interpretation
Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
defines afilter_ivl = afilter
and bfilter_ivl = bfilter
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Thu Dec 17 17:34:35 2015 +0100
@@ -192,7 +192,7 @@
end
-permanent_interpretation
+global_interpretation
Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
defines afilter_ivl' = afilter
and bfilter_ivl' = bfilter
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Thu Dec 17 17:34:35 2015 +0100
@@ -52,7 +52,7 @@
end
-permanent_interpretation Val_abs
+global_interpretation Val_abs
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof
case goal1 thus ?case
@@ -66,7 +66,7 @@
by(auto simp: plus_const_cases split: const.split)
qed
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
defines AI_const = AI and step_const = step' and aval'_const = aval'
..
@@ -114,7 +114,7 @@
text{* Monotonicity: *}
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
proof
case goal1 thus ?case
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Thu Dec 17 17:34:35 2015 +0100
@@ -113,7 +113,7 @@
proofs (they happened in the instatiation above) but delivers the
instantiated abstract interpreter which we call AI: *}
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
defines aval_parity = aval' and step_parity = step' and AI_parity = AI
..
@@ -141,7 +141,7 @@
subsubsection "Termination"
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
proof
case goal1 thus ?case
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Thu Dec 17 17:34:35 2015 +0100
@@ -165,7 +165,7 @@
I (max_option False (l1 + Some 1) l2) h2)
else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
-permanent_interpretation Val_abs
+global_interpretation Val_abs
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
proof
case goal1 thus ?case
@@ -179,7 +179,7 @@
by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
qed
-permanent_interpretation Val_abs1_gamma
+global_interpretation Val_abs1_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
defines aval_ivl = aval'
proof
@@ -198,7 +198,7 @@
done
-permanent_interpretation Val_abs1
+global_interpretation Val_abs1
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
@@ -215,7 +215,7 @@
auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
qed
-permanent_interpretation Abs_Int1
+global_interpretation Abs_Int1
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
@@ -229,7 +229,7 @@
text{* Monotonicity: *}
-permanent_interpretation Abs_Int1_mono
+global_interpretation Abs_Int1_mono
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Thu Dec 17 17:34:35 2015 +0100
@@ -225,7 +225,7 @@
end
-permanent_interpretation Abs_Int2
+global_interpretation Abs_Int2
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
and test_num' = in_ivl
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
diff -r 32a530a5c54c src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Thu Dec 17 17:34:35 2015 +0100
@@ -89,7 +89,7 @@
WHILE b DO lift F c (sub\<^sub>1 ` M)
{F (post ` M)}"
-permanent_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
+global_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
proof
case goal1
have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
diff -r 32a530a5c54c src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/IMP/Collecting.thy Thu Dec 17 17:34:35 2015 +0100
@@ -94,7 +94,7 @@
definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
"Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
-permanent_interpretation
+global_interpretation
Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
proof (standard, goal_cases)
case 1 thus ?case
diff -r 32a530a5c54c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Dec 17 17:34:35 2015 +0100
@@ -1054,7 +1054,7 @@
lemma mset_map: "mset (map f xs) = image_mset f (mset xs)"
by (induct xs) simp_all
-permanent_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
+global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}"
by standard (simp add: fun_eq_iff ac_simps)
diff -r 32a530a5c54c src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML Wed Dec 16 17:30:30 2015 +0100
+++ b/src/Pure/Isar/class.ML Thu Dec 17 17:34:35 2015 +0100
@@ -686,7 +686,8 @@
notes = Generic_Target.notes Generic_Target.theory_target_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
declaration = K Generic_Target.theory_declaration,
- subscription = Generic_Target.theory_registration,
+ theory_registration = Generic_Target.theory_registration,
+ locale_dependency = fn _ => error "Not possible in instantiation target",
pretty = pretty,
exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
end;
diff -r 32a530a5c54c src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML Wed Dec 16 17:30:30 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML Thu Dec 17 17:34:35 2015 +0100
@@ -11,33 +11,38 @@
type 'a rewrites = (Attrib.binding * 'a) list
(*interpretation in proofs*)
- val interpret: Expression.expression_i -> term rewrites -> bool -> Proof.state -> Proof.state
- val interpret_cmd: Expression.expression -> string rewrites -> bool -> Proof.state -> Proof.state
+ val interpret: Expression.expression_i ->
+ term rewrites -> bool -> Proof.state -> Proof.state
+ val interpret_cmd: Expression.expression ->
+ string rewrites -> bool -> Proof.state -> Proof.state
- (*algebraic view*)
+ (*interpretation in local theories*)
+ val interpretation: Expression.expression_i ->
+ term rewrites -> local_theory -> Proof.state
+ val interpretation_cmd: Expression.expression ->
+ string rewrites -> local_theory -> Proof.state
+
+ (*interpretation into global theories*)
val global_interpretation: Expression.expression_i ->
- term defines -> term rewrites -> theory -> Proof.state
+ term defines -> term rewrites -> local_theory -> Proof.state
+ val global_interpretation_cmd: Expression.expression ->
+ string defines -> string rewrites -> local_theory -> Proof.state
+
+ (*interpretation between locales*)
+ val sublocale: Expression.expression_i ->
+ term defines -> term rewrites -> local_theory -> Proof.state
+ val sublocale_cmd: Expression.expression ->
+ string defines -> string rewrites -> local_theory -> Proof.state
val global_sublocale: string -> Expression.expression_i ->
term defines -> term rewrites -> theory -> Proof.state
val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
string defines -> string rewrites -> theory -> Proof.state
- val sublocale: Expression.expression_i ->
- term defines -> term rewrites -> local_theory -> Proof.state
- val sublocale_cmd: Expression.expression ->
- string defines -> string rewrites -> local_theory -> Proof.state
-
- (*local-theory-based view*)
- val ephemeral_interpretation: Expression.expression_i ->
- term rewrites -> local_theory -> Proof.state
- val permanent_interpretation: Expression.expression_i ->
- term defines -> term rewrites -> local_theory -> Proof.state
- val permanent_interpretation_cmd: Expression.expression ->
- string defines -> string rewrites -> local_theory -> Proof.state
(*mixed Isar interface*)
- val interpretation: Expression.expression_i -> term rewrites -> local_theory -> Proof.state
- val interpretation_cmd: Expression.expression -> string rewrites ->
- local_theory -> Proof.state
+ val isar_interpretation: Expression.expression_i ->
+ term rewrites -> local_theory -> Proof.state
+ val isar_interpretation_cmd: Expression.expression ->
+ string rewrites -> local_theory -> Proof.state
end;
structure Interpretation : INTERPRETATION =
@@ -172,28 +177,46 @@
in
fun interpret expression = gen_interpret cert_interpretation expression;
+
fun interpret_cmd raw_expression = gen_interpret read_interpretation raw_expression;
end;
-(* algebraic view *)
+(* interpretation in local theories *)
+
+fun interpretation expression =
+ generic_interpretation cert_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Locale.activate_fragment expression;
+
+fun interpretation_cmd raw_expression =
+ generic_interpretation read_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Locale.activate_fragment raw_expression;
+
+
+(* interpretation into global theories *)
+
+fun global_interpretation expression =
+ generic_interpretation_with_defs cert_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Local_Theory.theory_registration expression;
+
+fun global_interpretation_cmd raw_expression =
+ generic_interpretation_with_defs read_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Local_Theory.theory_registration raw_expression;
+
+
+(* interpretation between locales *)
+
+fun sublocale expression =
+ generic_interpretation_with_defs cert_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Local_Theory.locale_dependency expression;
+
+fun sublocale_cmd raw_expression =
+ generic_interpretation_with_defs read_interpretation Element.witness_proof_eqs
+ Local_Theory.notes_kind Local_Theory.locale_dependency raw_expression;
local
-fun gen_global_interpretation prep_interpretation expression
- raw_defs raw_eqns thy =
- let
- val lthy = Named_Target.theory_init thy;
- fun setup_proof after_qed =
- Element.witness_proof_eqs
- (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
- in
- lthy |>
- generic_interpretation_with_defs prep_interpretation setup_proof
- Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
- end;
-
fun gen_global_sublocale prep_loc prep_interpretation
raw_locale expression raw_defs raw_eqns thy =
let
@@ -204,56 +227,16 @@
in
lthy |>
generic_interpretation_with_defs prep_interpretation setup_proof
- Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
+ Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns
end;
-fun subscribe_locale_only lthy =
- let
- val _ =
- if Named_Target.is_theory lthy
- then error "Not possible on level of global theory"
- else ();
- in Local_Theory.subscription end;
-
-fun gen_sublocale prep_interpretation expression raw_defs raw_eqns lthy =
- generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_defs raw_eqns lthy;
-
in
-fun global_interpretation expression =
- gen_global_interpretation cert_interpretation expression;
fun global_sublocale expression =
gen_global_sublocale (K I) cert_interpretation expression;
+
fun global_sublocale_cmd raw_expression =
gen_global_sublocale Locale.check read_interpretation raw_expression;
-fun sublocale expression =
- gen_sublocale cert_interpretation expression;
-fun sublocale_cmd raw_expression =
- gen_sublocale read_interpretation raw_expression;
-
-end;
-
-
-(* local-theory-based view *)
-
-local
-
-fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
- Local_Theory.assert_bottom true
- #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
-
-in
-
-fun ephemeral_interpretation expression =
- generic_interpretation cert_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind Locale.activate_fragment expression;
-
-fun permanent_interpretation expression =
- gen_permanent_interpretation cert_interpretation expression;
-fun permanent_interpretation_cmd raw_expression =
- gen_permanent_interpretation read_interpretation raw_expression;
end;
@@ -262,21 +245,21 @@
local
-fun subscribe_or_activate lthy =
+fun register_or_activate lthy =
if Named_Target.is_theory lthy
- then Local_Theory.subscription
+ then Local_Theory.theory_registration
else Locale.activate_fragment;
-fun gen_local_theory_interpretation prep_interpretation expression raw_eqns lthy =
+fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy =
generic_interpretation prep_interpretation Element.witness_proof_eqs
- Local_Theory.notes_kind (subscribe_or_activate lthy) expression raw_eqns lthy;
+ Local_Theory.notes_kind (register_or_activate lthy) expression raw_eqns lthy;
in
-fun interpretation expression =
- gen_local_theory_interpretation cert_interpretation expression;
-fun interpretation_cmd raw_expression =
- gen_local_theory_interpretation read_interpretation raw_expression;
+fun isar_interpretation expression =
+ gen_isar_interpretation cert_interpretation expression;
+fun isar_interpretation_cmd raw_expression =
+ gen_isar_interpretation read_interpretation raw_expression;
end;
diff -r 32a530a5c54c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML Wed Dec 16 17:30:30 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Dec 17 17:34:35 2015 +0100
@@ -407,6 +407,12 @@
Scan.optional
(@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
+val _ =
+ Outer_Syntax.command @{command_keyword interpret}
+ "prove interpretation of locale expression in proof context"
+ (interpretation_args >> (fn (expr, equations) =>
+ Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
+
val interpretation_args_with_defs =
Parse.!!! Parse_Spec.locale_expression --
(Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
@@ -415,6 +421,12 @@
(@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
val _ =
+ Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
+ "prove interpretation of locale expression into global theory"
+ (interpretation_args_with_defs
+ >> (fn (expr, (defs, equations)) => Interpretation.global_interpretation_cmd expr defs equations));
+
+val _ =
Outer_Syntax.command @{command_keyword sublocale}
"prove sublocale relation between a locale and a locale expression"
((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
@@ -424,22 +436,11 @@
Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
val _ =
- Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
- "prove interpretation of locale expression into named theory"
- (interpretation_args_with_defs
- >> (fn (expr, (defs, equations)) => Interpretation.permanent_interpretation_cmd expr defs equations));
+ Outer_Syntax.command @{command_keyword interpretation}
+ "prove interpretation of locale expression in local theory or into global theory"
+ (interpretation_args >> (fn (expr, equations) =>
+ Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr equations)));
-val _ =
- Outer_Syntax.command @{command_keyword interpretation}
- "prove interpretation of locale expression in local theory"
- (interpretation_args >> (fn (expr, equations) =>
- Toplevel.local_theory_to_proof NONE NONE (Interpretation.interpretation_cmd expr equations)));
-
-val _ =
- Outer_Syntax.command @{command_keyword interpret}
- "prove interpretation of locale expression in proof context"
- (interpretation_args >> (fn (expr, equations) =>
- Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
(* classes *)
diff -r 32a530a5c54c src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML Wed Dec 16 17:30:30 2015 +0100
+++ b/src/Pure/Isar/local_theory.ML Thu Dec 17 17:34:35 2015 +0100
@@ -52,7 +52,9 @@
val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
- val subscription: string * morphism -> (morphism * bool) option -> morphism ->
+ val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
+ local_theory -> local_theory
+ val locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
local_theory -> local_theory
val pretty: local_theory -> Pretty.T list
val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
@@ -92,7 +94,9 @@
abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory,
declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
- subscription: string * morphism -> (morphism * bool) option -> morphism ->
+ theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
+ local_theory -> local_theory,
+ locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
local_theory -> local_theory,
pretty: local_theory -> Pretty.T list,
exit: local_theory -> Proof.context};
@@ -267,8 +271,10 @@
val define_internal = operation2 #define true;
val notes_kind = operation2 #notes;
val declaration = operation2 #declaration;
-fun subscription dep_morph mixin export =
- assert_bottom true #> operation (fn ops => #subscription ops dep_morph mixin export);
+fun theory_registration dep_morph mixin export =
+ assert_bottom true #> operation (fn ops => #theory_registration ops dep_morph mixin export);
+fun locale_dependency dep_morph mixin export =
+ assert_bottom true #> operation (fn ops => #locale_dependency ops dep_morph mixin export);
(* theorems *)
diff -r 32a530a5c54c src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML Wed Dec 16 17:30:30 2015 +0100
+++ b/src/Pure/Isar/named_target.ML Thu Dec 17 17:34:35 2015 +0100
@@ -89,8 +89,12 @@
fun declaration ("", _) flags decl = Generic_Target.theory_declaration decl
| declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl;
-fun subscription ("", _) = Generic_Target.theory_registration
- | subscription (locale, _) = Generic_Target.locale_dependency locale;
+fun theory_registration ("", _) = Generic_Target.theory_registration
+ | theory_registration _ = (fn _ => error "Not possible in theory target");
+
+fun locale_dependency ("", false) = (fn _ => error "Not possible in locale target")
+ | locale_dependency ("", true) = (fn _ => error "Not possible in class target")
+ | locale_dependency (locale, _) = Generic_Target.locale_dependency locale;
fun pretty (target, is_class) ctxt =
if target = "" then
@@ -144,7 +148,8 @@
notes = Generic_Target.notes (notes name_data),
abbrev = abbrev name_data,
declaration = declaration name_data,
- subscription = subscription name_data,
+ theory_registration = theory_registration name_data,
+ locale_dependency = locale_dependency name_data,
pretty = pretty name_data,
exit = the_default I before_exit
#> Local_Theory.target_of #> Sign.change_end_local}
diff -r 32a530a5c54c src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML Wed Dec 16 17:30:30 2015 +0100
+++ b/src/Pure/Isar/overloading.ML Thu Dec 17 17:34:35 2015 +0100
@@ -204,7 +204,8 @@
notes = Generic_Target.notes Generic_Target.theory_target_notes,
abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
declaration = K Generic_Target.theory_declaration,
- subscription = Generic_Target.theory_registration,
+ theory_registration = Generic_Target.theory_registration,
+ locale_dependency = fn _ => error "Not possible in overloading target",
pretty = pretty,
exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
end;
diff -r 32a530a5c54c src/Pure/Pure.thy
--- a/src/Pure/Pure.thy Wed Dec 16 17:30:30 2015 +0100
+++ b/src/Pure/Pure.thy Thu Dec 17 17:34:35 2015 +0100
@@ -35,8 +35,8 @@
and "include" "including" :: prf_decl
and "print_bundles" :: diag
and "context" "locale" "experiment" :: thy_decl_block
- and "permanent_interpretation" "interpretation" "sublocale" :: thy_goal
and "interpret" :: prf_goal % "proof"
+ and "interpretation" "global_interpretation" "sublocale" :: thy_goal
and "class" :: thy_decl_block
and "subclass" :: thy_goal
and "instantiation" :: thy_decl_block
-------------- next part --------------
# HG changeset patch
# Parent 822a55ffb5aa3dd06fbdb5b72203a0feb14e857f
diff -r 822a55ffb5aa src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy Thu Dec 03 18:52:26 2015 +0100
+++ b/src/HOL/Library/Saturated.thy Thu Dec 03 18:52:51 2015 +0100
@@ -207,33 +207,18 @@
instantiation sat :: (len) "{Inf, Sup}"
begin
-definition "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
-definition "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
+global_interpretation Inf_sat: semilattice_neutr_set min "top :: 'a sat"
+ defines Inf_sat = Inf_sat.F
+ by standard (simp add: min_def)
+
+global_interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a sat"
+ defines Sup_sat = Sup_sat.F
+ by standard (simp add: max_def bot.extremum_unique)
instance ..
end
-interpretation Inf_sat: semilattice_neutr_set min "top :: 'a::len sat"
-rewrites
- "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
-proof -
- show "semilattice_neutr_set min (top :: 'a sat)"
- by standard (simp add: min_def)
- show "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
- by (simp add: Inf_sat_def)
-qed
-
-interpretation Sup_sat: semilattice_neutr_set max "bot :: 'a::len sat"
-rewrites
- "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
-proof -
- show "semilattice_neutr_set max (bot :: 'a sat)"
- by standard (simp add: max_def bot.extremum_unique)
- show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
- by (simp add: Sup_sat_def)
-qed
-
instance sat :: (len) complete_lattice
proof
fix x :: "'a sat"
diff -r 822a55ffb5aa src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML Thu Dec 03 18:52:26 2015 +0100
+++ b/src/Pure/Isar/generic_target.ML Thu Dec 03 18:52:51 2015 +0100
@@ -137,6 +137,10 @@
end
| _ => NONE)
else NONE;
+ fun perhaps_try f x =
+ case try f x of
+ SOME (y, x') => (SOME y, x')
+ | NONE => (NONE, x);
in
(case const_alias of
SOME c =>
@@ -145,10 +149,11 @@
|> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)])
| NONE =>
context
- |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs')
- |-> (fn (const as Const (c, _), _) => same_stem ?
+ |> perhaps_try (Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs'))
+ |-> (fn SOME (const as Const (c, _), _) => same_stem ?
(Proof_Context.generic_revert_abbrev (#1 prmode) c #>
- same_shape ? Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
+ same_shape ? Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))
+ | NONE => I))
end
else context;
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20151217/83e96a89/attachment-0001.asc>
More information about the isabelle-dev
mailing list