abandoned attempt to unify sublocale and interpretation into global theories
authorhaftmann
Sat Dec 19 11:05:04 2015 +0100 (2015-12-19)
changeset 61890f6ded81f5690
parent 61857 542f2c6da692
child 61891 76189756ff65
abandoned attempt to unify sublocale and interpretation into global theories
src/HOL/Finite_Set.thy
src/HOL/IMP/Abs_Int1_const.thy
src/HOL/IMP/Abs_Int1_parity.thy
src/HOL/IMP/Abs_Int2_ivl.thy
src/HOL/IMP/Abs_Int3.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy
src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy
src/HOL/IMP/Collecting.thy
src/HOL/Library/Multiset.thy
src/Pure/Isar/class.ML
src/Pure/Isar/interpretation.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/overloading.ML
src/Pure/Pure.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Dec 18 14:23:11 2015 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Sat Dec 19 11:05:04 2015 +0100
     1.3 @@ -1209,7 +1209,7 @@
     1.4    But now that we have @{const fold} things are easy:
     1.5  \<close>
     1.6  
     1.7 -permanent_interpretation card: folding "\<lambda>_. Suc" 0
     1.8 +global_interpretation card: folding "\<lambda>_. Suc" 0
     1.9    defines card = "folding.F (\<lambda>_. Suc) 0"
    1.10    by standard rule
    1.11  
     2.1 --- a/src/HOL/IMP/Abs_Int1_const.thy	Fri Dec 18 14:23:11 2015 +0100
     2.2 +++ b/src/HOL/IMP/Abs_Int1_const.thy	Sat Dec 19 11:05:04 2015 +0100
     2.3 @@ -53,7 +53,7 @@
     2.4  end
     2.5  
     2.6  
     2.7 -permanent_interpretation Val_semilattice
     2.8 +global_interpretation Val_semilattice
     2.9  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
    2.10  proof (standard, goal_cases)
    2.11    case (1 a b) thus ?case
    2.12 @@ -66,7 +66,7 @@
    2.13    case 4 thus ?case by(auto simp: plus_const_cases split: const.split)
    2.14  qed
    2.15  
    2.16 -permanent_interpretation Abs_Int
    2.17 +global_interpretation Abs_Int
    2.18  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
    2.19  defines AI_const = AI and step_const = step' and aval'_const = aval'
    2.20  ..
    2.21 @@ -120,7 +120,7 @@
    2.22  
    2.23  text{* Monotonicity: *}
    2.24  
    2.25 -permanent_interpretation Abs_Int_mono
    2.26 +global_interpretation Abs_Int_mono
    2.27  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
    2.28  proof (standard, goal_cases)
    2.29    case 1 thus ?case by(auto simp: plus_const_cases split: const.split)
    2.30 @@ -131,7 +131,7 @@
    2.31  definition m_const :: "const \<Rightarrow> nat" where
    2.32  "m_const x = (if x = Any then 0 else 1)"
    2.33  
    2.34 -permanent_interpretation Abs_Int_measure
    2.35 +global_interpretation Abs_Int_measure
    2.36  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
    2.37  and m = m_const and h = "1"
    2.38  proof (standard, goal_cases)
     3.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Fri Dec 18 14:23:11 2015 +0100
     3.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Sat Dec 19 11:05:04 2015 +0100
     3.3 @@ -102,7 +102,7 @@
     3.4  text{* First we instantiate the abstract value interface and prove that the
     3.5  functions on type @{typ parity} have all the necessary properties: *}
     3.6  
     3.7 -permanent_interpretation Val_semilattice
     3.8 +global_interpretation Val_semilattice
     3.9  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
    3.10  proof (standard, goal_cases) txt{* subgoals are the locale axioms *}
    3.11    case 1 thus ?case by(auto simp: less_eq_parity_def)
    3.12 @@ -124,7 +124,7 @@
    3.13  proofs (they happened in the instatiation above) but delivers the
    3.14  instantiated abstract interpreter which we call @{text AI_parity}: *}
    3.15  
    3.16 -permanent_interpretation Abs_Int
    3.17 +global_interpretation Abs_Int
    3.18  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
    3.19  defines aval_parity = aval' and step_parity = step' and AI_parity = AI
    3.20  ..
    3.21 @@ -155,7 +155,7 @@
    3.22  
    3.23  subsubsection "Termination"
    3.24  
    3.25 -permanent_interpretation Abs_Int_mono
    3.26 +global_interpretation Abs_Int_mono
    3.27  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
    3.28  proof (standard, goal_cases)
    3.29    case (1 _ a1 _ a2) thus ?case
    3.30 @@ -166,7 +166,7 @@
    3.31  definition m_parity :: "parity \<Rightarrow> nat" where
    3.32  "m_parity x = (if x = Either then 0 else 1)"
    3.33  
    3.34 -permanent_interpretation Abs_Int_measure
    3.35 +global_interpretation Abs_Int_measure
    3.36  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
    3.37  and m = m_parity and h = "1"
    3.38  proof (standard, goal_cases)
     4.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Fri Dec 18 14:23:11 2015 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Sat Dec 19 11:05:04 2015 +0100
     4.3 @@ -302,7 +302,7 @@
     4.4    "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
     4.5  by(drule (1) add_mono) simp
     4.6  
     4.7 -permanent_interpretation Val_semilattice
     4.8 +global_interpretation Val_semilattice
     4.9  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
    4.10  proof (standard, goal_cases)
    4.11    case 1 thus ?case by transfer (simp add: le_iff_subset)
    4.12 @@ -318,7 +318,7 @@
    4.13  qed
    4.14  
    4.15  
    4.16 -permanent_interpretation Val_lattice_gamma
    4.17 +global_interpretation Val_lattice_gamma
    4.18  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
    4.19  defines aval_ivl = aval'
    4.20  proof (standard, goal_cases)
    4.21 @@ -327,7 +327,7 @@
    4.22    case 2 show ?case unfolding bot_ivl_def by transfer simp
    4.23  qed
    4.24  
    4.25 -permanent_interpretation Val_inv
    4.26 +global_interpretation Val_inv
    4.27  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
    4.28  and test_num' = in_ivl
    4.29  and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
    4.30 @@ -350,7 +350,7 @@
    4.31      done
    4.32  qed
    4.33  
    4.34 -permanent_interpretation Abs_Int_inv
    4.35 +global_interpretation Abs_Int_inv
    4.36  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
    4.37  and test_num' = in_ivl
    4.38  and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
    4.39 @@ -384,7 +384,7 @@
    4.40  apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
    4.41  by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
    4.42  
    4.43 -permanent_interpretation Abs_Int_inv_mono
    4.44 +global_interpretation Abs_Int_inv_mono
    4.45  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
    4.46  and test_num' = in_ivl
    4.47  and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
     5.1 --- a/src/HOL/IMP/Abs_Int3.thy	Fri Dec 18 14:23:11 2015 +0100
     5.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Sat Dec 19 11:05:04 2015 +0100
     5.3 @@ -256,7 +256,7 @@
     5.4  
     5.5  end
     5.6  
     5.7 -permanent_interpretation Abs_Int_wn
     5.8 +global_interpretation Abs_Int_wn
     5.9  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
    5.10  and test_num' = in_ivl
    5.11  and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
    5.12 @@ -541,7 +541,7 @@
    5.13           split: prod.splits if_splits extended.split)
    5.14  
    5.15  
    5.16 -permanent_interpretation Abs_Int_wn_measure
    5.17 +global_interpretation Abs_Int_wn_measure
    5.18  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
    5.19  and test_num' = in_ivl
    5.20  and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
     6.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Fri Dec 18 14:23:11 2015 +0100
     6.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Sat Dec 19 11:05:04 2015 +0100
     6.3 @@ -47,13 +47,13 @@
     6.4  
     6.5  end
     6.6  
     6.7 -permanent_interpretation Rep rep_cval
     6.8 +global_interpretation Rep rep_cval
     6.9  proof
    6.10    case goal1 thus ?case
    6.11      by(cases a, cases b, simp, simp, cases b, simp, simp)
    6.12  qed
    6.13  
    6.14 -permanent_interpretation Val_abs rep_cval Const plus_cval
    6.15 +global_interpretation Val_abs rep_cval Const plus_cval
    6.16  proof
    6.17    case goal1 show ?case by simp
    6.18  next
    6.19 @@ -61,7 +61,7 @@
    6.20      by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
    6.21  qed
    6.22  
    6.23 -permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
    6.24 +global_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
    6.25  defines AI_const = AI
    6.26  and aval'_const = aval'
    6.27  proof qed (auto simp: iter'_pfp_above)
     7.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Fri Dec 18 14:23:11 2015 +0100
     7.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Sat Dec 19 11:05:04 2015 +0100
     7.3 @@ -166,13 +166,13 @@
     7.4           I (max_option False (l1 + Some 1) l2) h2)
     7.5     else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
     7.6  
     7.7 -permanent_interpretation Rep rep_ivl
     7.8 +global_interpretation Rep rep_ivl
     7.9  proof
    7.10    case goal1 thus ?case
    7.11      by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
    7.12  qed
    7.13  
    7.14 -permanent_interpretation Val_abs rep_ivl num_ivl plus_ivl
    7.15 +global_interpretation Val_abs rep_ivl num_ivl plus_ivl
    7.16  proof
    7.17    case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
    7.18  next
    7.19 @@ -180,7 +180,7 @@
    7.20      by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
    7.21  qed
    7.22  
    7.23 -permanent_interpretation Rep1 rep_ivl
    7.24 +global_interpretation Rep1 rep_ivl
    7.25  proof
    7.26    case goal1 thus ?case
    7.27      by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
    7.28 @@ -188,7 +188,7 @@
    7.29    case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
    7.30  qed
    7.31  
    7.32 -permanent_interpretation
    7.33 +global_interpretation
    7.34    Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
    7.35  proof
    7.36    case goal1 thus ?case
    7.37 @@ -200,7 +200,7 @@
    7.38        auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
    7.39  qed
    7.40  
    7.41 -permanent_interpretation
    7.42 +global_interpretation
    7.43    Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
    7.44  defines afilter_ivl = afilter
    7.45  and bfilter_ivl = bfilter
     8.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Fri Dec 18 14:23:11 2015 +0100
     8.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Sat Dec 19 11:05:04 2015 +0100
     8.3 @@ -192,7 +192,7 @@
     8.4  
     8.5  end
     8.6  
     8.7 -permanent_interpretation
     8.8 +global_interpretation
     8.9    Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
    8.10  defines afilter_ivl' = afilter
    8.11  and bfilter_ivl' = bfilter
     9.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Fri Dec 18 14:23:11 2015 +0100
     9.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Sat Dec 19 11:05:04 2015 +0100
     9.3 @@ -52,7 +52,7 @@
     9.4  end
     9.5  
     9.6  
     9.7 -permanent_interpretation Val_abs
     9.8 +global_interpretation Val_abs
     9.9  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
    9.10  proof
    9.11    case goal1 thus ?case
    9.12 @@ -66,7 +66,7 @@
    9.13      by(auto simp: plus_const_cases split: const.split)
    9.14  qed
    9.15  
    9.16 -permanent_interpretation Abs_Int
    9.17 +global_interpretation Abs_Int
    9.18  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
    9.19  defines AI_const = AI and step_const = step' and aval'_const = aval'
    9.20  ..
    9.21 @@ -114,7 +114,7 @@
    9.22  
    9.23  text{* Monotonicity: *}
    9.24  
    9.25 -permanent_interpretation Abs_Int_mono
    9.26 +global_interpretation Abs_Int_mono
    9.27  where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
    9.28  proof
    9.29    case goal1 thus ?case
    10.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Fri Dec 18 14:23:11 2015 +0100
    10.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Sat Dec 19 11:05:04 2015 +0100
    10.3 @@ -113,7 +113,7 @@
    10.4  proofs (they happened in the instatiation above) but delivers the
    10.5  instantiated abstract interpreter which we call AI: *}
    10.6  
    10.7 -permanent_interpretation Abs_Int
    10.8 +global_interpretation Abs_Int
    10.9  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
   10.10  defines aval_parity = aval' and step_parity = step' and AI_parity = AI
   10.11  ..
   10.12 @@ -141,7 +141,7 @@
   10.13  
   10.14  subsubsection "Termination"
   10.15  
   10.16 -permanent_interpretation Abs_Int_mono
   10.17 +global_interpretation Abs_Int_mono
   10.18  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
   10.19  proof
   10.20    case goal1 thus ?case
    11.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Fri Dec 18 14:23:11 2015 +0100
    11.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Sat Dec 19 11:05:04 2015 +0100
    11.3 @@ -165,7 +165,7 @@
    11.4           I (max_option False (l1 + Some 1) l2) h2)
    11.5     else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
    11.6  
    11.7 -permanent_interpretation Val_abs
    11.8 +global_interpretation Val_abs
    11.9  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
   11.10  proof
   11.11    case goal1 thus ?case
   11.12 @@ -179,7 +179,7 @@
   11.13      by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
   11.14  qed
   11.15  
   11.16 -permanent_interpretation Val_abs1_gamma
   11.17 +global_interpretation Val_abs1_gamma
   11.18  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
   11.19  defines aval_ivl = aval'
   11.20  proof
   11.21 @@ -198,7 +198,7 @@
   11.22  done
   11.23  
   11.24  
   11.25 -permanent_interpretation Val_abs1
   11.26 +global_interpretation Val_abs1
   11.27  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
   11.28  and test_num' = in_ivl
   11.29  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   11.30 @@ -215,7 +215,7 @@
   11.31        auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
   11.32  qed
   11.33  
   11.34 -permanent_interpretation Abs_Int1
   11.35 +global_interpretation Abs_Int1
   11.36  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
   11.37  and test_num' = in_ivl
   11.38  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   11.39 @@ -229,7 +229,7 @@
   11.40  
   11.41  text{* Monotonicity: *}
   11.42  
   11.43 -permanent_interpretation Abs_Int1_mono
   11.44 +global_interpretation Abs_Int1_mono
   11.45  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
   11.46  and test_num' = in_ivl
   11.47  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
    12.1 --- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Fri Dec 18 14:23:11 2015 +0100
    12.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Sat Dec 19 11:05:04 2015 +0100
    12.3 @@ -225,7 +225,7 @@
    12.4  
    12.5  end
    12.6  
    12.7 -permanent_interpretation Abs_Int2
    12.8 +global_interpretation Abs_Int2
    12.9  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
   12.10  and test_num' = in_ivl
   12.11  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
    13.1 --- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Fri Dec 18 14:23:11 2015 +0100
    13.2 +++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Sat Dec 19 11:05:04 2015 +0100
    13.3 @@ -89,7 +89,7 @@
    13.4   WHILE b DO lift F c (sub\<^sub>1 ` M)
    13.5   {F (post ` M)}"
    13.6  
    13.7 -permanent_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
    13.8 +global_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
    13.9  proof
   13.10    case goal1
   13.11    have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
    14.1 --- a/src/HOL/IMP/Collecting.thy	Fri Dec 18 14:23:11 2015 +0100
    14.2 +++ b/src/HOL/IMP/Collecting.thy	Sat Dec 19 11:05:04 2015 +0100
    14.3 @@ -94,7 +94,7 @@
    14.4  definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
    14.5  "Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
    14.6  
    14.7 -permanent_interpretation
    14.8 +global_interpretation
    14.9    Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
   14.10  proof (standard, goal_cases)
   14.11    case 1 thus ?case
    15.1 --- a/src/HOL/Library/Multiset.thy	Fri Dec 18 14:23:11 2015 +0100
    15.2 +++ b/src/HOL/Library/Multiset.thy	Sat Dec 19 11:05:04 2015 +0100
    15.3 @@ -1054,7 +1054,7 @@
    15.4  lemma mset_map: "mset (map f xs) = image_mset f (mset xs)"
    15.5    by (induct xs) simp_all
    15.6  
    15.7 -permanent_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
    15.8 +global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
    15.9    defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}"
   15.10    by standard (simp add: fun_eq_iff ac_simps)
   15.11  
    16.1 --- a/src/Pure/Isar/class.ML	Fri Dec 18 14:23:11 2015 +0100
    16.2 +++ b/src/Pure/Isar/class.ML	Sat Dec 19 11:05:04 2015 +0100
    16.3 @@ -686,7 +686,8 @@
    16.4          notes = Generic_Target.notes Generic_Target.theory_target_notes,
    16.5          abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
    16.6          declaration = K Generic_Target.theory_declaration,
    16.7 -        subscription = Generic_Target.theory_registration,
    16.8 +        theory_registration = Generic_Target.theory_registration,
    16.9 +        locale_dependency = fn _ => error "Not possible in instantiation target",
   16.10          pretty = pretty,
   16.11          exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   16.12    end;
    17.1 --- a/src/Pure/Isar/interpretation.ML	Fri Dec 18 14:23:11 2015 +0100
    17.2 +++ b/src/Pure/Isar/interpretation.ML	Sat Dec 19 11:05:04 2015 +0100
    17.3 @@ -11,33 +11,38 @@
    17.4    type 'a rewrites = (Attrib.binding * 'a) list
    17.5  
    17.6    (*interpretation in proofs*)
    17.7 -  val interpret: Expression.expression_i -> term rewrites -> bool -> Proof.state -> Proof.state
    17.8 -  val interpret_cmd: Expression.expression -> string rewrites -> bool -> Proof.state -> Proof.state
    17.9 +  val interpret: Expression.expression_i ->
   17.10 +    term rewrites -> bool -> Proof.state -> Proof.state
   17.11 +  val interpret_cmd: Expression.expression ->
   17.12 +    string rewrites -> bool -> Proof.state -> Proof.state
   17.13  
   17.14 -  (*algebraic view*)
   17.15 +  (*interpretation in local theories*)
   17.16 +  val interpretation: Expression.expression_i ->
   17.17 +    term rewrites -> local_theory -> Proof.state
   17.18 +  val interpretation_cmd: Expression.expression ->
   17.19 +    string rewrites -> local_theory -> Proof.state
   17.20 +
   17.21 +  (*interpretation into global theories*)
   17.22    val global_interpretation: Expression.expression_i ->
   17.23 -    term defines -> term rewrites -> theory -> Proof.state
   17.24 -  val global_sublocale: string -> Expression.expression_i ->
   17.25 -    term defines -> term rewrites -> theory -> Proof.state
   17.26 -  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
   17.27 -    string defines -> string rewrites -> theory -> Proof.state
   17.28 +    term defines -> term rewrites -> local_theory -> Proof.state
   17.29 +  val global_interpretation_cmd: Expression.expression ->
   17.30 +    string defines -> string rewrites -> local_theory -> Proof.state
   17.31 +
   17.32 +  (*interpretation between locales*)
   17.33    val sublocale: Expression.expression_i ->
   17.34      term defines -> term rewrites -> local_theory -> Proof.state
   17.35    val sublocale_cmd: Expression.expression ->
   17.36      string defines -> string rewrites -> local_theory -> Proof.state
   17.37 -
   17.38 -  (*local-theory-based view*)
   17.39 -  val ephemeral_interpretation: Expression.expression_i ->
   17.40 -    term rewrites -> local_theory -> Proof.state
   17.41 -  val permanent_interpretation: Expression.expression_i ->
   17.42 -    term defines -> term rewrites -> local_theory -> Proof.state
   17.43 -  val permanent_interpretation_cmd: Expression.expression ->
   17.44 -    string defines -> string rewrites -> local_theory -> Proof.state
   17.45 +  val global_sublocale: string -> Expression.expression_i ->
   17.46 +    term defines -> term rewrites -> theory -> Proof.state
   17.47 +  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
   17.48 +    string defines -> string rewrites -> theory -> Proof.state
   17.49  
   17.50    (*mixed Isar interface*)
   17.51 -  val interpretation: Expression.expression_i -> term rewrites -> local_theory -> Proof.state
   17.52 -  val interpretation_cmd: Expression.expression -> string rewrites ->
   17.53 -    local_theory -> Proof.state
   17.54 +  val isar_interpretation: Expression.expression_i ->
   17.55 +    term rewrites -> local_theory -> Proof.state
   17.56 +  val isar_interpretation_cmd: Expression.expression ->
   17.57 +    string rewrites -> local_theory -> Proof.state
   17.58  end;
   17.59  
   17.60  structure Interpretation : INTERPRETATION =
   17.61 @@ -172,28 +177,46 @@
   17.62  in
   17.63  
   17.64  fun interpret expression = gen_interpret cert_interpretation expression;
   17.65 +
   17.66  fun interpret_cmd raw_expression = gen_interpret read_interpretation raw_expression;
   17.67  
   17.68  end;
   17.69  
   17.70  
   17.71 -(* algebraic view *)
   17.72 +(* interpretation in local theories *)
   17.73 +
   17.74 +fun interpretation expression =
   17.75 +  generic_interpretation cert_interpretation Element.witness_proof_eqs
   17.76 +    Local_Theory.notes_kind Locale.activate_fragment expression;
   17.77 +
   17.78 +fun interpretation_cmd raw_expression =
   17.79 +  generic_interpretation read_interpretation Element.witness_proof_eqs
   17.80 +    Local_Theory.notes_kind Locale.activate_fragment raw_expression;
   17.81 +
   17.82 +
   17.83 +(* interpretation into global theories *)
   17.84 +
   17.85 +fun global_interpretation expression =
   17.86 +  generic_interpretation_with_defs cert_interpretation Element.witness_proof_eqs
   17.87 +    Local_Theory.notes_kind Local_Theory.theory_registration expression;
   17.88 +
   17.89 +fun global_interpretation_cmd raw_expression =
   17.90 +  generic_interpretation_with_defs read_interpretation Element.witness_proof_eqs
   17.91 +    Local_Theory.notes_kind Local_Theory.theory_registration raw_expression;
   17.92 +
   17.93 +
   17.94 +(* interpretation between locales *)
   17.95 +
   17.96 +fun sublocale expression =
   17.97 +  generic_interpretation_with_defs cert_interpretation Element.witness_proof_eqs
   17.98 +    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
   17.99 +
  17.100 +fun sublocale_cmd raw_expression =
  17.101 +  generic_interpretation_with_defs read_interpretation Element.witness_proof_eqs
  17.102 +    Local_Theory.notes_kind Local_Theory.locale_dependency raw_expression;
  17.103  
  17.104  local
  17.105  
  17.106 -fun gen_global_interpretation prep_interpretation expression
  17.107 -    raw_defs raw_eqns thy = 
  17.108 -  let
  17.109 -    val lthy = Named_Target.theory_init thy;
  17.110 -    fun setup_proof after_qed =
  17.111 -      Element.witness_proof_eqs
  17.112 -        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
  17.113 -  in
  17.114 -    lthy |>
  17.115 -      generic_interpretation_with_defs prep_interpretation setup_proof
  17.116 -        Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
  17.117 -  end;
  17.118 -
  17.119  fun gen_global_sublocale prep_loc prep_interpretation
  17.120      raw_locale expression raw_defs raw_eqns thy =
  17.121    let
  17.122 @@ -204,56 +227,16 @@
  17.123    in
  17.124      lthy |>
  17.125        generic_interpretation_with_defs prep_interpretation setup_proof
  17.126 -        Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
  17.127 +        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns
  17.128    end;
  17.129  
  17.130 -fun subscribe_locale_only lthy =
  17.131 -  let
  17.132 -    val _ =
  17.133 -      if Named_Target.is_theory lthy
  17.134 -      then error "Not possible on level of global theory"
  17.135 -      else ();
  17.136 -  in Local_Theory.subscription end;
  17.137 -
  17.138 -fun gen_sublocale prep_interpretation expression raw_defs raw_eqns lthy =
  17.139 -  generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
  17.140 -    Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_defs raw_eqns lthy;
  17.141 -
  17.142  in
  17.143  
  17.144 -fun global_interpretation expression =
  17.145 -  gen_global_interpretation cert_interpretation expression;
  17.146  fun global_sublocale expression =
  17.147    gen_global_sublocale (K I) cert_interpretation expression;
  17.148 +
  17.149  fun global_sublocale_cmd raw_expression =
  17.150    gen_global_sublocale Locale.check read_interpretation raw_expression;
  17.151 -fun sublocale expression =
  17.152 -  gen_sublocale cert_interpretation expression;
  17.153 -fun sublocale_cmd raw_expression =
  17.154 -  gen_sublocale read_interpretation raw_expression;
  17.155 -
  17.156 -end;
  17.157 -
  17.158 -
  17.159 -(* local-theory-based view *)
  17.160 -
  17.161 -local
  17.162 -
  17.163 -fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
  17.164 -  Local_Theory.assert_bottom true
  17.165 -  #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
  17.166 -    Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
  17.167 -
  17.168 -in
  17.169 -
  17.170 -fun ephemeral_interpretation expression =
  17.171 -  generic_interpretation cert_interpretation Element.witness_proof_eqs
  17.172 -    Local_Theory.notes_kind Locale.activate_fragment expression;
  17.173 -
  17.174 -fun permanent_interpretation expression =
  17.175 -  gen_permanent_interpretation cert_interpretation expression;
  17.176 -fun permanent_interpretation_cmd raw_expression =
  17.177 -  gen_permanent_interpretation read_interpretation raw_expression;
  17.178  
  17.179  end;
  17.180  
  17.181 @@ -262,21 +245,21 @@
  17.182  
  17.183  local
  17.184  
  17.185 -fun subscribe_or_activate lthy =
  17.186 +fun register_or_activate lthy =
  17.187    if Named_Target.is_theory lthy
  17.188 -  then Local_Theory.subscription
  17.189 +  then Local_Theory.theory_registration
  17.190    else Locale.activate_fragment;
  17.191  
  17.192 -fun gen_local_theory_interpretation prep_interpretation expression raw_eqns lthy =
  17.193 +fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy =
  17.194    generic_interpretation prep_interpretation Element.witness_proof_eqs
  17.195 -    Local_Theory.notes_kind (subscribe_or_activate lthy) expression raw_eqns lthy;
  17.196 +    Local_Theory.notes_kind (register_or_activate lthy) expression raw_eqns lthy;
  17.197  
  17.198  in
  17.199  
  17.200 -fun interpretation expression =
  17.201 -  gen_local_theory_interpretation cert_interpretation expression;
  17.202 -fun interpretation_cmd raw_expression =
  17.203 -  gen_local_theory_interpretation read_interpretation raw_expression;
  17.204 +fun isar_interpretation expression =
  17.205 +  gen_isar_interpretation cert_interpretation expression;
  17.206 +fun isar_interpretation_cmd raw_expression =
  17.207 +  gen_isar_interpretation read_interpretation raw_expression;
  17.208  
  17.209  end;
  17.210  
    18.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Dec 18 14:23:11 2015 +0100
    18.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 19 11:05:04 2015 +0100
    18.3 @@ -407,6 +407,12 @@
    18.4      Scan.optional
    18.5        (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
    18.6  
    18.7 +val _ =
    18.8 +  Outer_Syntax.command @{command_keyword interpret}
    18.9 +    "prove interpretation of locale expression in proof context"
   18.10 +    (interpretation_args >> (fn (expr, equations) =>
   18.11 +      Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
   18.12 +
   18.13  val interpretation_args_with_defs =
   18.14    Parse.!!! Parse_Spec.locale_expression --
   18.15      (Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
   18.16 @@ -415,6 +421,12 @@
   18.17        (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
   18.18  
   18.19  val _ =
   18.20 +  Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
   18.21 +    "prove interpretation of locale expression into global theory"
   18.22 +    (interpretation_args_with_defs
   18.23 +      >> (fn (expr, (defs, equations)) => Interpretation.global_interpretation_cmd expr defs equations));
   18.24 +
   18.25 +val _ =
   18.26    Outer_Syntax.command @{command_keyword sublocale}
   18.27      "prove sublocale relation between a locale and a locale expression"
   18.28      ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
   18.29 @@ -424,22 +436,11 @@
   18.30          Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
   18.31  
   18.32  val _ =
   18.33 -  Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
   18.34 -    "prove interpretation of locale expression into named theory"
   18.35 -    (interpretation_args_with_defs
   18.36 -      >> (fn (expr, (defs, equations)) => Interpretation.permanent_interpretation_cmd expr defs equations));
   18.37 +  Outer_Syntax.command @{command_keyword interpretation}
   18.38 +    "prove interpretation of locale expression in local theory or into global theory"
   18.39 +    (interpretation_args >> (fn (expr, equations) =>
   18.40 +      Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr equations)));
   18.41  
   18.42 -val _ =
   18.43 -  Outer_Syntax.command @{command_keyword interpretation}
   18.44 -    "prove interpretation of locale expression in local theory"
   18.45 -    (interpretation_args >> (fn (expr, equations) =>
   18.46 -      Toplevel.local_theory_to_proof NONE NONE (Interpretation.interpretation_cmd expr equations)));
   18.47 -
   18.48 -val _ =
   18.49 -  Outer_Syntax.command @{command_keyword interpret}
   18.50 -    "prove interpretation of locale expression in proof context"
   18.51 -    (interpretation_args >> (fn (expr, equations) =>
   18.52 -      Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
   18.53  
   18.54  
   18.55  (* classes *)
    19.1 --- a/src/Pure/Isar/local_theory.ML	Fri Dec 18 14:23:11 2015 +0100
    19.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Dec 19 11:05:04 2015 +0100
    19.3 @@ -52,7 +52,9 @@
    19.4    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    19.5      (term * term) * local_theory
    19.6    val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
    19.7 -  val subscription: string * morphism -> (morphism * bool) option -> morphism ->
    19.8 +  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
    19.9 +    local_theory -> local_theory
   19.10 +  val locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
   19.11      local_theory -> local_theory
   19.12    val pretty: local_theory -> Pretty.T list
   19.13    val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   19.14 @@ -92,7 +94,9 @@
   19.15    abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
   19.16      (term * term) * local_theory,
   19.17    declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
   19.18 -  subscription: string * morphism -> (morphism * bool) option -> morphism ->
   19.19 +  theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
   19.20 +     local_theory -> local_theory,
   19.21 +  locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
   19.22       local_theory -> local_theory,
   19.23    pretty: local_theory -> Pretty.T list,
   19.24    exit: local_theory -> Proof.context};
   19.25 @@ -267,8 +271,10 @@
   19.26  val define_internal = operation2 #define true;
   19.27  val notes_kind = operation2 #notes;
   19.28  val declaration = operation2 #declaration;
   19.29 -fun subscription dep_morph mixin export =
   19.30 -  assert_bottom true #> operation (fn ops => #subscription ops dep_morph mixin export);
   19.31 +fun theory_registration dep_morph mixin export =
   19.32 +  assert_bottom true #> operation (fn ops => #theory_registration ops dep_morph mixin export);
   19.33 +fun locale_dependency dep_morph mixin export =
   19.34 +  assert_bottom true #> operation (fn ops => #locale_dependency ops dep_morph mixin export);
   19.35  
   19.36  
   19.37  (* theorems *)
    20.1 --- a/src/Pure/Isar/named_target.ML	Fri Dec 18 14:23:11 2015 +0100
    20.2 +++ b/src/Pure/Isar/named_target.ML	Sat Dec 19 11:05:04 2015 +0100
    20.3 @@ -89,8 +89,12 @@
    20.4  fun declaration ("", _) flags decl = Generic_Target.theory_declaration decl
    20.5    | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl;
    20.6  
    20.7 -fun subscription ("", _) = Generic_Target.theory_registration
    20.8 -  | subscription (locale, _) = Generic_Target.locale_dependency locale;
    20.9 +fun theory_registration ("", _) = Generic_Target.theory_registration
   20.10 +  | theory_registration _ = (fn _ => error "Not possible in theory target");
   20.11 +
   20.12 +fun locale_dependency ("", false) = (fn _ => error "Not possible in locale target")
   20.13 +  | locale_dependency ("", true) = (fn _ => error "Not possible in class target")
   20.14 +  | locale_dependency (locale, _) = Generic_Target.locale_dependency locale;
   20.15  
   20.16  fun pretty (target, is_class) ctxt =
   20.17    if target = "" then
   20.18 @@ -144,7 +148,8 @@
   20.19          notes = Generic_Target.notes (notes name_data),
   20.20          abbrev = abbrev name_data,
   20.21          declaration = declaration name_data,
   20.22 -        subscription = subscription name_data,
   20.23 +        theory_registration = theory_registration name_data,
   20.24 +        locale_dependency = locale_dependency name_data,
   20.25          pretty = pretty name_data,
   20.26          exit = the_default I before_exit
   20.27            #> Local_Theory.target_of #> Sign.change_end_local}
    21.1 --- a/src/Pure/Isar/overloading.ML	Fri Dec 18 14:23:11 2015 +0100
    21.2 +++ b/src/Pure/Isar/overloading.ML	Sat Dec 19 11:05:04 2015 +0100
    21.3 @@ -204,7 +204,8 @@
    21.4          notes = Generic_Target.notes Generic_Target.theory_target_notes,
    21.5          abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
    21.6          declaration = K Generic_Target.theory_declaration,
    21.7 -        subscription = Generic_Target.theory_registration,
    21.8 +        theory_registration = Generic_Target.theory_registration,
    21.9 +        locale_dependency = fn _ => error "Not possible in overloading target",
   21.10          pretty = pretty,
   21.11          exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   21.12    end;
    22.1 --- a/src/Pure/Pure.thy	Fri Dec 18 14:23:11 2015 +0100
    22.2 +++ b/src/Pure/Pure.thy	Sat Dec 19 11:05:04 2015 +0100
    22.3 @@ -35,8 +35,8 @@
    22.4    and "include" "including" :: prf_decl
    22.5    and "print_bundles" :: diag
    22.6    and "context" "locale" "experiment" :: thy_decl_block
    22.7 -  and "permanent_interpretation" "interpretation" "sublocale" :: thy_goal
    22.8    and "interpret" :: prf_goal % "proof"
    22.9 +  and "interpretation" "global_interpretation" "sublocale" :: thy_goal
   22.10    and "class" :: thy_decl_block
   22.11    and "subclass" :: thy_goal
   22.12    and "instantiation" :: thy_decl_block