--- a/src/HOL/Finite_Set.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/Finite_Set.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/IMP/Abs_Int1_const.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy Sat Dec 19 11:05:04 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)
--- a/src/HOL/IMP/Abs_Int1_parity.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy Sat Dec 19 11:05:04 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)
--- a/src/HOL/IMP/Abs_Int2_ivl.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/IMP/Abs_Int3.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Sat Dec 19 11:05:04 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)
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy Sat Dec 19 11:05:04 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"
--- a/src/HOL/IMP/Collecting.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Collecting.thy Sat Dec 19 11:05:04 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
--- a/src/HOL/Library/Multiset.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Dec 19 11:05:04 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)
--- a/src/Pure/Isar/class.ML Fri Dec 18 14:23:11 2015 +0100
+++ b/src/Pure/Isar/class.ML Sat Dec 19 11:05:04 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;
--- a/src/Pure/Isar/interpretation.ML Fri Dec 18 14:23:11 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML Sat Dec 19 11:05:04 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
- 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
+ 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
-
- (*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
+ 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
(*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;
--- a/src/Pure/Isar/isar_syn.ML Fri Dec 18 14:23:11 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Dec 19 11:05:04 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 *)
--- a/src/Pure/Isar/local_theory.ML Fri Dec 18 14:23:11 2015 +0100
+++ b/src/Pure/Isar/local_theory.ML Sat Dec 19 11:05:04 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 *)
--- a/src/Pure/Isar/named_target.ML Fri Dec 18 14:23:11 2015 +0100
+++ b/src/Pure/Isar/named_target.ML Sat Dec 19 11:05:04 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}
--- a/src/Pure/Isar/overloading.ML Fri Dec 18 14:23:11 2015 +0100
+++ b/src/Pure/Isar/overloading.ML Sat Dec 19 11:05:04 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;
--- a/src/Pure/Pure.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/Pure/Pure.thy Sat Dec 19 11:05:04 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