migrated class package to new locale implementation
authorhaftmann
Fri Jan 16 14:58:11 2009 +0100 (2009-01-16)
changeset 295091ff0f3f08a7b
parent 29505 c6d2d23909d1
child 29510 6fe4200532b7
migrated class package to new locale implementation
src/HOL/Dense_Linear_Order.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/Lattices.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/List.thy
src/HOL/Statespace/StateSpaceEx.thy
src/HOL/Word/WordArith.thy
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
     1.1 --- a/src/HOL/Dense_Linear_Order.thy	Fri Jan 16 08:29:11 2009 +0100
     1.2 +++ b/src/HOL/Dense_Linear_Order.thy	Fri Jan 16 14:58:11 2009 +0100
     1.3 @@ -301,7 +301,7 @@
     1.4  
     1.5  text {* Linear order without upper bounds *}
     1.6  
     1.7 -class_locale linorder_stupid_syntax = linorder
     1.8 +locale linorder_stupid_syntax = linorder
     1.9  begin
    1.10  notation
    1.11    less_eq  ("op \<sqsubseteq>") and
    1.12 @@ -311,7 +311,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -class_locale linorder_no_ub = linorder_stupid_syntax +
    1.17 +locale linorder_no_ub = linorder_stupid_syntax +
    1.18    assumes gt_ex: "\<exists>y. less x y"
    1.19  begin
    1.20  lemma ge_ex: "\<exists>y. x \<sqsubseteq> y" using gt_ex by auto
    1.21 @@ -360,7 +360,7 @@
    1.22  
    1.23  text {* Linear order without upper bounds *}
    1.24  
    1.25 -class_locale linorder_no_lb = linorder_stupid_syntax +
    1.26 +locale linorder_no_lb = linorder_stupid_syntax +
    1.27    assumes lt_ex: "\<exists>y. less y x"
    1.28  begin
    1.29  lemma le_ex: "\<exists>y. y \<sqsubseteq> x" using lt_ex by auto
    1.30 @@ -407,12 +407,12 @@
    1.31  end
    1.32  
    1.33  
    1.34 -class_locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
    1.35 +locale constr_dense_linear_order = linorder_no_lb + linorder_no_ub +
    1.36    fixes between
    1.37    assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
    1.38       and  between_same: "between x x = x"
    1.39  
    1.40 -class_interpretation  constr_dense_linear_order < dense_linear_order 
    1.41 +sublocale  constr_dense_linear_order < dense_linear_order 
    1.42    apply unfold_locales
    1.43    using gt_ex lt_ex between_less
    1.44      by (auto, rule_tac x="between x y" in exI, simp)
    1.45 @@ -635,9 +635,9 @@
    1.46    using eq_diff_eq[where a= x and b=t and c=0] by simp
    1.47  
    1.48  
    1.49 -class_interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order
    1.50 - ["op <=" "op <"
    1.51 -   "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"]
    1.52 +interpretation class_ordered_field_dense_linear_order!: constr_dense_linear_order
    1.53 + "op <=" "op <"
    1.54 +   "\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"
    1.55  proof (unfold_locales, dlo, dlo, auto)
    1.56    fix x y::'a assume lt: "x < y"
    1.57    from  less_half_sum[OF lt] show "x < (x + y) /2" by simp
     2.1 --- a/src/HOL/Divides.thy	Fri Jan 16 08:29:11 2009 +0100
     2.2 +++ b/src/HOL/Divides.thy	Fri Jan 16 14:58:11 2009 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4  
     2.5  subsection {* Abstract division in commutative semirings. *}
     2.6  
     2.7 -class semiring_div = comm_semiring_1_cancel + div + 
     2.8 +class semiring_div = comm_semiring_1_cancel + div +
     2.9    assumes mod_div_equality: "a div b * b + a mod b = a"
    2.10      and div_by_0 [simp]: "a div 0 = 0"
    2.11      and div_0 [simp]: "0 div a = 0"
    2.12 @@ -800,7 +800,7 @@
    2.13  
    2.14  text {* @{term "op dvd"} is a partial order *}
    2.15  
    2.16 -class_interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
    2.17 +interpretation dvd!: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
    2.18    proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
    2.19  
    2.20  lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
     3.1 --- a/src/HOL/Finite_Set.thy	Fri Jan 16 08:29:11 2009 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Fri Jan 16 14:58:11 2009 +0100
     3.3 @@ -873,7 +873,7 @@
     3.4  
     3.5  subsection {* Generalized summation over a set *}
     3.6  
     3.7 -class_interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
     3.8 +interpretation comm_monoid_add!: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
     3.9    proof qed (auto intro: add_assoc add_commute)
    3.10  
    3.11  definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
    3.12 @@ -1760,7 +1760,7 @@
    3.13  proof (induct rule: finite_induct)
    3.14    case empty then show ?case by simp
    3.15  next
    3.16 -  class_interpret ab_semigroup_mult ["op Un"]
    3.17 +  interpret ab_semigroup_mult "op Un"
    3.18      proof qed auto
    3.19    case insert 
    3.20    then show ?case by simp
    3.21 @@ -2198,7 +2198,7 @@
    3.22    assumes "finite A" "A \<noteq> {}"
    3.23    shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
    3.24  proof -
    3.25 -  class_interpret ab_semigroup_idem_mult [inf]
    3.26 +  interpret ab_semigroup_idem_mult inf
    3.27      by (rule ab_semigroup_idem_mult_inf)
    3.28    show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
    3.29  qed
    3.30 @@ -2213,7 +2213,7 @@
    3.31    proof (induct rule: finite_ne_induct)
    3.32      case singleton thus ?case by simp
    3.33    next
    3.34 -    class_interpret ab_semigroup_idem_mult [inf]
    3.35 +    interpret ab_semigroup_idem_mult inf
    3.36        by (rule ab_semigroup_idem_mult_inf)
    3.37      case (insert x F)
    3.38      from insert(5) have "a = x \<or> a \<in> F" by simp
    3.39 @@ -2288,7 +2288,7 @@
    3.40      and "A \<noteq> {}"
    3.41    shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
    3.42  proof -
    3.43 -  class_interpret ab_semigroup_idem_mult [inf]
    3.44 +  interpret ab_semigroup_idem_mult inf
    3.45      by (rule ab_semigroup_idem_mult_inf)
    3.46    from assms show ?thesis
    3.47      by (simp add: Inf_fin_def image_def
    3.48 @@ -2303,7 +2303,7 @@
    3.49    case singleton thus ?case
    3.50      by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
    3.51  next
    3.52 -  class_interpret ab_semigroup_idem_mult [inf]
    3.53 +  interpret ab_semigroup_idem_mult inf
    3.54      by (rule ab_semigroup_idem_mult_inf)
    3.55    case (insert x A)
    3.56    have finB: "finite {sup x b |b. b \<in> B}"
    3.57 @@ -2333,7 +2333,7 @@
    3.58    assumes "finite A" and "A \<noteq> {}"
    3.59    shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
    3.60  proof -
    3.61 -  class_interpret ab_semigroup_idem_mult [sup]
    3.62 +  interpret ab_semigroup_idem_mult sup
    3.63      by (rule ab_semigroup_idem_mult_sup)
    3.64    from assms show ?thesis
    3.65      by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
    3.66 @@ -2357,7 +2357,7 @@
    3.67      thus ?thesis by(simp add: insert(1) B(1))
    3.68    qed
    3.69    have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
    3.70 -  class_interpret ab_semigroup_idem_mult [sup]
    3.71 +  interpret ab_semigroup_idem_mult sup
    3.72      by (rule ab_semigroup_idem_mult_sup)
    3.73    have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
    3.74      using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
    3.75 @@ -2386,7 +2386,7 @@
    3.76    assumes "finite A" and "A \<noteq> {}"
    3.77    shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
    3.78  proof -
    3.79 -  class_interpret ab_semigroup_idem_mult [inf]
    3.80 +    interpret ab_semigroup_idem_mult inf
    3.81      by (rule ab_semigroup_idem_mult_inf)
    3.82    from assms show ?thesis
    3.83    unfolding Inf_fin_def by (induct A set: finite)
    3.84 @@ -2397,7 +2397,7 @@
    3.85    assumes "finite A" and "A \<noteq> {}"
    3.86    shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
    3.87  proof -
    3.88 -  class_interpret ab_semigroup_idem_mult [sup]
    3.89 +  interpret ab_semigroup_idem_mult sup
    3.90      by (rule ab_semigroup_idem_mult_sup)
    3.91    from assms show ?thesis
    3.92    unfolding Sup_fin_def by (induct A set: finite)
    3.93 @@ -2446,7 +2446,7 @@
    3.94    assumes "finite A" and "A \<noteq> {}"
    3.95    shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
    3.96  proof -
    3.97 -  class_interpret ab_semigroup_idem_mult [min]
    3.98 +  interpret ab_semigroup_idem_mult min
    3.99      by (rule ab_semigroup_idem_mult_min)
   3.100    from assms show ?thesis
   3.101    by (induct rule: finite_ne_induct)
   3.102 @@ -2457,7 +2457,7 @@
   3.103    assumes "finite A" and "A \<noteq> {}"
   3.104    shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   3.105  proof -
   3.106 -  class_interpret ab_semigroup_idem_mult [min]
   3.107 +  interpret ab_semigroup_idem_mult min
   3.108      by (rule ab_semigroup_idem_mult_min)
   3.109    from assms show ?thesis
   3.110    by (induct rule: finite_ne_induct)
   3.111 @@ -2468,7 +2468,7 @@
   3.112    assumes "finite A" and "A \<noteq> {}"
   3.113    shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   3.114  proof -
   3.115 -  class_interpret ab_semigroup_idem_mult [min]
   3.116 +  interpret ab_semigroup_idem_mult min
   3.117      by (rule ab_semigroup_idem_mult_min)
   3.118    from assms show ?thesis
   3.119    by (induct rule: finite_ne_induct)
   3.120 @@ -2481,7 +2481,7 @@
   3.121  proof cases
   3.122    assume "A = B" thus ?thesis by simp
   3.123  next
   3.124 -  class_interpret ab_semigroup_idem_mult [min]
   3.125 +  interpret ab_semigroup_idem_mult min
   3.126      by (rule ab_semigroup_idem_mult_min)
   3.127    assume "A \<noteq> B"
   3.128    have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
   3.129 @@ -2515,7 +2515,7 @@
   3.130    assumes "finite A" and "A \<noteq> {}"
   3.131    shows "Min (insert x A) = min x (Min A)"
   3.132  proof -
   3.133 -  class_interpret ab_semigroup_idem_mult [min]
   3.134 +  interpret ab_semigroup_idem_mult min
   3.135      by (rule ab_semigroup_idem_mult_min)
   3.136    from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
   3.137  qed
   3.138 @@ -2524,7 +2524,7 @@
   3.139    assumes "finite A" and "A \<noteq> {}"
   3.140    shows "Max (insert x A) = max x (Max A)"
   3.141  proof -
   3.142 -  class_interpret ab_semigroup_idem_mult [max]
   3.143 +  interpret ab_semigroup_idem_mult max
   3.144      by (rule ab_semigroup_idem_mult_max)
   3.145    from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
   3.146  qed
   3.147 @@ -2533,7 +2533,7 @@
   3.148    assumes "finite A" and "A \<noteq> {}"
   3.149    shows "Min A \<in> A"
   3.150  proof -
   3.151 -  class_interpret ab_semigroup_idem_mult [min]
   3.152 +  interpret ab_semigroup_idem_mult min
   3.153      by (rule ab_semigroup_idem_mult_min)
   3.154    from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
   3.155  qed
   3.156 @@ -2542,7 +2542,7 @@
   3.157    assumes "finite A" and "A \<noteq> {}"
   3.158    shows "Max A \<in> A"
   3.159  proof -
   3.160 -  class_interpret ab_semigroup_idem_mult [max]
   3.161 +  interpret ab_semigroup_idem_mult max
   3.162      by (rule ab_semigroup_idem_mult_max)
   3.163    from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
   3.164  qed
   3.165 @@ -2551,7 +2551,7 @@
   3.166    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   3.167    shows "Min (A \<union> B) = min (Min A) (Min B)"
   3.168  proof -
   3.169 -  class_interpret ab_semigroup_idem_mult [min]
   3.170 +  interpret ab_semigroup_idem_mult min
   3.171      by (rule ab_semigroup_idem_mult_min)
   3.172    from assms show ?thesis
   3.173      by (simp add: Min_def fold1_Un2)
   3.174 @@ -2561,7 +2561,7 @@
   3.175    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   3.176    shows "Max (A \<union> B) = max (Max A) (Max B)"
   3.177  proof -
   3.178 -  class_interpret ab_semigroup_idem_mult [max]
   3.179 +  interpret ab_semigroup_idem_mult max
   3.180      by (rule ab_semigroup_idem_mult_max)
   3.181    from assms show ?thesis
   3.182      by (simp add: Max_def fold1_Un2)
   3.183 @@ -2572,7 +2572,7 @@
   3.184      and "finite N" and "N \<noteq> {}"
   3.185    shows "h (Min N) = Min (h ` N)"
   3.186  proof -
   3.187 -  class_interpret ab_semigroup_idem_mult [min]
   3.188 +  interpret ab_semigroup_idem_mult min
   3.189      by (rule ab_semigroup_idem_mult_min)
   3.190    from assms show ?thesis
   3.191      by (simp add: Min_def hom_fold1_commute)
   3.192 @@ -2583,7 +2583,7 @@
   3.193      and "finite N" and "N \<noteq> {}"
   3.194    shows "h (Max N) = Max (h ` N)"
   3.195  proof -
   3.196 -  class_interpret ab_semigroup_idem_mult [max]
   3.197 +  interpret ab_semigroup_idem_mult max
   3.198      by (rule ab_semigroup_idem_mult_max)
   3.199    from assms show ?thesis
   3.200      by (simp add: Max_def hom_fold1_commute [of h])
   3.201 @@ -2593,7 +2593,7 @@
   3.202    assumes "finite A" and "x \<in> A"
   3.203    shows "Min A \<le> x"
   3.204  proof -
   3.205 -  class_interpret lower_semilattice ["op \<le>" "op <" min]
   3.206 +  interpret lower_semilattice "op \<le>" "op <" min
   3.207      by (rule min_lattice)
   3.208    from assms show ?thesis by (simp add: Min_def fold1_belowI)
   3.209  qed
   3.210 @@ -2602,7 +2602,7 @@
   3.211    assumes "finite A" and "x \<in> A"
   3.212    shows "x \<le> Max A"
   3.213  proof -
   3.214 -  invoke lower_semilattice ["op \<ge>" "op >" max]
   3.215 +  interpret lower_semilattice "op \<ge>" "op >" max
   3.216      by (rule max_lattice)
   3.217    from assms show ?thesis by (simp add: Max_def fold1_belowI)
   3.218  qed
   3.219 @@ -2611,7 +2611,7 @@
   3.220    assumes "finite A" and "A \<noteq> {}"
   3.221    shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   3.222  proof -
   3.223 -  class_interpret lower_semilattice ["op \<le>" "op <" min]
   3.224 +  interpret lower_semilattice "op \<le>" "op <" min
   3.225      by (rule min_lattice)
   3.226    from assms show ?thesis by (simp add: Min_def below_fold1_iff)
   3.227  qed
   3.228 @@ -2620,7 +2620,7 @@
   3.229    assumes "finite A" and "A \<noteq> {}"
   3.230    shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   3.231  proof -
   3.232 -  invoke lower_semilattice ["op \<ge>" "op >" max]
   3.233 +  interpret lower_semilattice "op \<ge>" "op >" max
   3.234      by (rule max_lattice)
   3.235    from assms show ?thesis by (simp add: Max_def below_fold1_iff)
   3.236  qed
   3.237 @@ -2629,7 +2629,7 @@
   3.238    assumes "finite A" and "A \<noteq> {}"
   3.239    shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   3.240  proof -
   3.241 -  class_interpret lower_semilattice ["op \<le>" "op <" min]
   3.242 +  interpret lower_semilattice "op \<le>" "op <" min
   3.243      by (rule min_lattice)
   3.244    from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
   3.245  qed
   3.246 @@ -2639,7 +2639,7 @@
   3.247    shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   3.248  proof -
   3.249    note Max = Max_def
   3.250 -  class_interpret linorder ["op \<ge>" "op >"]
   3.251 +  interpret linorder "op \<ge>" "op >"
   3.252      by (rule dual_linorder)
   3.253    from assms show ?thesis
   3.254      by (simp add: Max strict_below_fold1_iff [folded dual_max])
   3.255 @@ -2649,7 +2649,7 @@
   3.256    assumes "finite A" and "A \<noteq> {}"
   3.257    shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   3.258  proof -
   3.259 -  class_interpret lower_semilattice ["op \<le>" "op <" min]
   3.260 +  interpret lower_semilattice "op \<le>" "op <" min
   3.261      by (rule min_lattice)
   3.262    from assms show ?thesis
   3.263      by (simp add: Min_def fold1_below_iff)
   3.264 @@ -2660,7 +2660,7 @@
   3.265    shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   3.266  proof -
   3.267    note Max = Max_def
   3.268 -  class_interpret linorder ["op \<ge>" "op >"]
   3.269 +  interpret linorder "op \<ge>" "op >"
   3.270      by (rule dual_linorder)
   3.271    from assms show ?thesis
   3.272      by (simp add: Max fold1_below_iff [folded dual_max])
   3.273 @@ -2670,7 +2670,7 @@
   3.274    assumes "finite A" and "A \<noteq> {}"
   3.275    shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   3.276  proof -
   3.277 -  class_interpret lower_semilattice ["op \<le>" "op <" min]
   3.278 +  interpret lower_semilattice "op \<le>" "op <" min
   3.279      by (rule min_lattice)
   3.280    from assms show ?thesis
   3.281      by (simp add: Min_def fold1_strict_below_iff)
   3.282 @@ -2681,7 +2681,7 @@
   3.283    shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   3.284  proof -
   3.285    note Max = Max_def
   3.286 -  class_interpret linorder ["op \<ge>" "op >"]
   3.287 +  interpret linorder "op \<ge>" "op >"
   3.288      by (rule dual_linorder)
   3.289    from assms show ?thesis
   3.290      by (simp add: Max fold1_strict_below_iff [folded dual_max])
   3.291 @@ -2691,7 +2691,7 @@
   3.292    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   3.293    shows "Min N \<le> Min M"
   3.294  proof -
   3.295 -  class_interpret distrib_lattice ["op \<le>" "op <" min max]
   3.296 +  interpret distrib_lattice "op \<le>" "op <" min max
   3.297      by (rule distrib_lattice_min_max)
   3.298    from assms show ?thesis by (simp add: Min_def fold1_antimono)
   3.299  qed
   3.300 @@ -2701,7 +2701,7 @@
   3.301    shows "Max M \<le> Max N"
   3.302  proof -
   3.303    note Max = Max_def
   3.304 -  class_interpret linorder ["op \<ge>" "op >"]
   3.305 +  interpret linorder "op \<ge>" "op >"
   3.306      by (rule dual_linorder)
   3.307    from assms show ?thesis
   3.308      by (simp add: Max fold1_antimono [folded dual_max])
     4.1 --- a/src/HOL/Lattices.thy	Fri Jan 16 08:29:11 2009 +0100
     4.2 +++ b/src/HOL/Lattices.thy	Fri Jan 16 14:58:11 2009 +0100
     4.3 @@ -300,8 +300,7 @@
     4.4    by auto
     4.5  qed (auto simp add: min_def max_def not_le less_imp_le)
     4.6  
     4.7 -class_interpretation min_max:
     4.8 -  distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
     4.9 +interpretation min_max!: distrib_lattice "op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max
    4.10    by (rule distrib_lattice_min_max)
    4.11  
    4.12  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
     5.1 --- a/src/HOL/Library/Multiset.thy	Fri Jan 16 08:29:11 2009 +0100
     5.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jan 16 14:58:11 2009 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Library/Multiset.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
     5.7  *)
     5.8  
     5.9 @@ -1080,16 +1079,16 @@
    5.10  apply simp
    5.11  done
    5.12  
    5.13 -class_interpretation mset_order: order ["op \<le>#" "op <#"]
    5.14 +interpretation mset_order!: order "op \<le>#" "op <#"
    5.15  proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
    5.16    mset_le_trans simp: mset_less_def)
    5.17  
    5.18 -class_interpretation mset_order_cancel_semigroup:
    5.19 -  pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
    5.20 +interpretation mset_order_cancel_semigroup!:
    5.21 +  pordered_cancel_ab_semigroup_add "op +" "op \<le>#" "op <#"
    5.22  proof qed (erule mset_le_mono_add [OF mset_le_refl])
    5.23  
    5.24 -class_interpretation mset_order_semigroup_cancel:
    5.25 -  pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
    5.26 +interpretation mset_order_semigroup_cancel!:
    5.27 +  pordered_ab_semigroup_add_imp_le "op +" "op \<le>#" "op <#"
    5.28  proof qed simp
    5.29  
    5.30  
    5.31 @@ -1156,7 +1155,7 @@
    5.32    then show ?case using T by simp
    5.33  qed
    5.34  
    5.35 -lemmas mset_less_trans = mset_order.less_eq_less.less_trans
    5.36 +lemmas mset_less_trans = mset_order.less_trans
    5.37  
    5.38  lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
    5.39  by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq)
     6.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Fri Jan 16 08:29:11 2009 +0100
     6.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Jan 16 14:58:11 2009 +0100
     6.3 @@ -107,26 +107,26 @@
     6.4    apply simp
     6.5    done
     6.6  
     6.7 -class_interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
     6.8 +interpretation set_semigroup_add!: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
     6.9    apply default
    6.10    apply (unfold set_plus_def)
    6.11    apply (force simp add: add_assoc)
    6.12    done
    6.13  
    6.14 -class_interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
    6.15 +interpretation set_semigroup_mult!: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
    6.16    apply default
    6.17    apply (unfold set_times_def)
    6.18    apply (force simp add: mult_assoc)
    6.19    done
    6.20  
    6.21 -class_interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
    6.22 +interpretation set_comm_monoid_add!: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
    6.23    apply default
    6.24     apply (unfold set_plus_def)
    6.25     apply (force simp add: add_ac)
    6.26    apply force
    6.27    done
    6.28  
    6.29 -class_interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
    6.30 +interpretation set_comm_monoid_mult!: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
    6.31    apply default
    6.32     apply (unfold set_times_def)
    6.33     apply (force simp add: mult_ac)
     7.1 --- a/src/HOL/List.thy	Fri Jan 16 08:29:11 2009 +0100
     7.2 +++ b/src/HOL/List.thy	Fri Jan 16 14:58:11 2009 +0100
     7.3 @@ -547,9 +547,9 @@
     7.4  lemma append_Nil2 [simp]: "xs @ [] = xs"
     7.5  by (induct xs) auto
     7.6  
     7.7 -class_interpretation semigroup_append: semigroup_add ["op @"]
     7.8 +interpretation semigroup_append!: semigroup_add "op @"
     7.9    proof qed simp
    7.10 -class_interpretation monoid_append: monoid_add ["[]" "op @"]
    7.11 +interpretation monoid_append!: monoid_add "[]" "op @"
    7.12    proof qed simp+
    7.13  
    7.14  lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
     8.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Fri Jan 16 08:29:11 2009 +0100
     8.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Fri Jan 16 14:58:11 2009 +0100
     8.3 @@ -41,7 +41,7 @@
     8.4  projection~/ injection functions that convert from abstract values to
     8.5  @{typ "nat"} and @{text "bool"}. The logical content of the locale is: *}
     8.6  
     8.7 -class_locale vars' =
     8.8 +locale vars' =
     8.9    fixes n::'name and b::'name
    8.10    assumes "distinct [n, b]" 
    8.11  
     9.1 --- a/src/HOL/Word/WordArith.thy	Fri Jan 16 08:29:11 2009 +0100
     9.2 +++ b/src/HOL/Word/WordArith.thy	Fri Jan 16 14:58:11 2009 +0100
     9.3 @@ -22,7 +22,7 @@
     9.4  proof
     9.5  qed (unfold word_sle_def word_sless_def, auto)
     9.6  
     9.7 -class_interpretation signed: linorder ["word_sle" "word_sless"] 
     9.8 +interpretation signed!: linorder "word_sle" "word_sless"
     9.9    by (rule signed_linorder)
    9.10  
    9.11  lemmas word_arith_wis = 
    10.1 --- a/src/Pure/Isar/class.ML	Fri Jan 16 08:29:11 2009 +0100
    10.2 +++ b/src/Pure/Isar/class.ML	Fri Jan 16 14:58:11 2009 +0100
    10.3 @@ -27,9 +27,9 @@
    10.4  (** rule calculation **)
    10.5  
    10.6  fun calculate_axiom thy sups base_sort assm_axiom param_map class =
    10.7 -  case Old_Locale.intros thy class
    10.8 -   of (_, []) => assm_axiom
    10.9 -    | (_, [intro]) =>
   10.10 +  case Locale.intros_of thy class
   10.11 +   of (_, NONE) => assm_axiom
   10.12 +    | (_, SOME intro) =>
   10.13        let
   10.14          fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
   10.15            (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
   10.16 @@ -45,23 +45,22 @@
   10.17          |> SOME
   10.18        end;
   10.19  
   10.20 -fun raw_morphism thy class param_map some_axiom =
   10.21 +fun raw_morphism thy class sups param_map some_axiom =
   10.22    let
   10.23      val ctxt = ProofContext.init thy;
   10.24 -    val some_wit = case some_axiom
   10.25 -     of SOME axiom => SOME (Element.prove_witness ctxt
   10.26 -          (Logic.unvarify (Thm.prop_of axiom))
   10.27 -            (ALLGOALS (ProofContext.fact_tac [axiom])))
   10.28 -      | NONE => NONE;
   10.29 -    val instT = Symtab.empty |> Symtab.update ("'a", TFree ("'a", [class]));
   10.30 -    val inst = Symtab.make ((map o apsnd) Const param_map);
   10.31 -  in case some_wit
   10.32 -   of SOME wit => Element.inst_morphism thy (instT, inst)
   10.33 -        $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
   10.34 -        $> Element.satisfy_morphism [wit]
   10.35 -    | NONE => Element.inst_morphism thy (instT, inst)
   10.36 -        $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
   10.37 -  end;
   10.38 +    val (([props], [(_, morph1)], export_morph), _) = ctxt
   10.39 +      |> Expression.cert_goal_expression ([(class, (("", false),
   10.40 +           Expression.Named ((map o apsnd) Const param_map)))], []);
   10.41 +    val morph2 = morph1
   10.42 +      $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class));
   10.43 +    val morph3 = case props
   10.44 +     of [prop] => morph2
   10.45 +          $> Element.satisfy_morphism [(Element.prove_witness ctxt prop
   10.46 +               (ALLGOALS (ProofContext.fact_tac (the_list some_axiom))))]
   10.47 +        | [] => morph2;
   10.48 +    (*FIXME generic amend operation for classes*)
   10.49 +    val morph4 = morph3 $> eq_morph thy (these_defs thy sups);
   10.50 +  in (morph4, export_morph) end;
   10.51  
   10.52  fun calculate_rules thy morph sups base_sort param_map axiom class =
   10.53    let
   10.54 @@ -70,19 +69,18 @@
   10.55          (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
   10.56            Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
   10.57      val defs = these_defs thy sups;
   10.58 -    val assm_intro = Old_Locale.intros thy class
   10.59 +    val assm_intro = Locale.intros_of thy class
   10.60        |> fst
   10.61 -      |> map (instantiate thy base_sort)
   10.62 -      |> map (MetaSimplifier.rewrite_rule defs)
   10.63 -      |> map Thm.close_derivation
   10.64 -      |> try the_single;
   10.65 +      |> Option.map (instantiate thy base_sort)
   10.66 +      |> Option.map (MetaSimplifier.rewrite_rule defs)
   10.67 +      |> Option.map Thm.close_derivation;
   10.68      val fixate = Thm.instantiate
   10.69        (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
   10.70          (TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], [])
   10.71      val of_class_sups = if null sups
   10.72        then map (fixate o Thm.class_triv thy) base_sort
   10.73        else map (fixate o snd o rules thy) sups;
   10.74 -    val locale_dests = map Drule.standard' (Old_Locale.dests thy class);
   10.75 +    val locale_dests = map Drule.standard' (Locale.axioms_of thy class);
   10.76      val num_trivs = case length locale_dests
   10.77       of 0 => if is_none axiom then 0 else 1
   10.78        | n => n;
   10.79 @@ -110,55 +108,54 @@
   10.80  
   10.81  local
   10.82  
   10.83 -fun gen_class_spec prep_class process_expr thy raw_supclasses raw_elems =
   10.84 +fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
   10.85    let
   10.86      val supclasses = map (prep_class thy) raw_supclasses;
   10.87      val supsort = Sign.minimize_sort thy supclasses;
   10.88      val sups = filter (is_class thy) supsort;
   10.89 -    val supparam_names = map fst (these_params thy sups);
   10.90 +    val base_sort = if null sups then supsort else
   10.91 +      foldr1 (Sorts.inter_sort (Sign.classes_of thy))
   10.92 +        (map (base_sort thy) sups);
   10.93 +    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
   10.94 +    val supparam_names = map fst supparams;
   10.95      val _ = if has_duplicates (op =) supparam_names
   10.96        then error ("Duplicate parameter(s) in superclasses: "
   10.97          ^ (commas o map quote o duplicates (op =)) supparam_names)
   10.98        else ();
   10.99 -    val base_sort = if null sups then supsort else
  10.100 -      foldr1 (Sorts.inter_sort (Sign.classes_of thy))
  10.101 -        (map (base_sort thy) sups);
  10.102 -    val suplocales = map Old_Locale.Locale sups;
  10.103 -    val supexpr = Old_Locale.Merge suplocales;
  10.104 -    val supparams = (map fst o Old_Locale.parameters_of_expr thy) supexpr;
  10.105 -    val mergeexpr = Old_Locale.Merge suplocales;
  10.106 +
  10.107 +    val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
  10.108 +      sups, []);
  10.109      val constrain = Element.Constrains ((map o apsnd o map_atyps)
  10.110        (K (TFree (Name.aT, base_sort))) supparams);
  10.111 +      (*FIXME perhaps better: control type variable by explicit
  10.112 +      parameter instantiation of import expression*)
  10.113 +    val begin_ctxt = begin sups base_sort
  10.114 +      #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
  10.115 +          (K (TFree (Name.aT, base_sort))) supparams) (*FIXME
  10.116 +            should constraints be issued in begin?*)
  10.117 +    val ((_, _, syntax_elems), _) = ProofContext.init thy
  10.118 +      |> begin_ctxt
  10.119 +      |> process_decl supexpr raw_elems;
  10.120      fun fork_syn (Element.Fixes xs) =
  10.121            fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
  10.122            #>> Element.Fixes
  10.123        | fork_syn x = pair x;
  10.124 -    fun fork_syntax elems =
  10.125 -      let
  10.126 -        val (elems', global_syntax) = fold_map fork_syn elems [];
  10.127 -      in (constrain :: elems', global_syntax) end;
  10.128 -    val (elems, global_syntax) =
  10.129 -      ProofContext.init thy
  10.130 -      |> Old_Locale.cert_expr supexpr [constrain]
  10.131 -      |> snd
  10.132 -      |> begin sups base_sort
  10.133 -      |> process_expr Old_Locale.empty raw_elems
  10.134 -      |> fst
  10.135 -      |> fork_syntax
  10.136 -  in (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) end;
  10.137 +    val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
  10.138 +  in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
  10.139  
  10.140 -val read_class_spec = gen_class_spec Sign.intern_class Old_Locale.read_expr;
  10.141 -val check_class_spec = gen_class_spec (K I) Old_Locale.cert_expr;
  10.142 +val cert_class_spec = gen_class_spec (K I) Expression.cert_declaration;
  10.143 +val read_class_spec = gen_class_spec Sign.intern_class Expression.cert_read_declaration;
  10.144  
  10.145  fun add_consts bname class base_sort sups supparams global_syntax thy =
  10.146    let
  10.147 -    val supconsts = map fst supparams
  10.148 +    val supconsts = supparams
  10.149        |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
  10.150        |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
  10.151 -    val all_params = map fst (Old_Locale.parameters_of thy class);
  10.152 +    val all_params = Locale.params_of thy class;
  10.153      val raw_params = (snd o chop (length supparams)) all_params;
  10.154 -    fun add_const (v, raw_ty) thy =
  10.155 +    fun add_const (b, SOME raw_ty, _) thy =
  10.156        let
  10.157 +        val v = Binding.base_name b;
  10.158          val c = Sign.full_bname thy v;
  10.159          val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
  10.160          val ty0 = Type.strip_sorts ty;
  10.161 @@ -183,9 +180,9 @@
  10.162      fun globalize param_map = map_aterms
  10.163        (fn Free (v, ty) => Const ((fst o the o AList.lookup (op =) param_map) v, ty)
  10.164          | t => t);
  10.165 -    val raw_pred = Old_Locale.intros thy class
  10.166 +    val raw_pred = Locale.intros_of thy class
  10.167        |> fst
  10.168 -      |> map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
  10.169 +      |> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
  10.170      fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
  10.171       of [] => NONE
  10.172        | [thm] => SOME thm;
  10.173 @@ -194,7 +191,8 @@
  10.174      |> add_consts bname class base_sort sups supparams global_syntax
  10.175      |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
  10.176            (map (fst o snd) params)
  10.177 -          [((Binding.name (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
  10.178 +          [(((*Binding.name (bname ^ "_" ^ AxClass.axiomsN*) Binding.empty, []),
  10.179 +            Option.map (globalize param_map) raw_pred |> the_list)]
  10.180      #> snd
  10.181      #> `get_axiom
  10.182      #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
  10.183 @@ -204,35 +202,42 @@
  10.184  fun gen_class prep_spec bname raw_supclasses raw_elems thy =
  10.185    let
  10.186      val class = Sign.full_bname thy bname;
  10.187 -    val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
  10.188 +    val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
  10.189        prep_spec thy raw_supclasses raw_elems;
  10.190 -    val supconsts = map (apsnd fst o snd) (these_params thy sups);
  10.191 +    (*val export_morph = (*FIXME how canonical is this?*)
  10.192 +      Morphism.morphism { binding = I, var = I,
  10.193 +        typ = Logic.varifyT,
  10.194 +        term = (*map_types Logic.varifyT*) I,
  10.195 +        fact = map Thm.varifyT
  10.196 +      } $> Morphism.morphism { binding = I, var = I,
  10.197 +        typ = Logic.type_map TermSubst.zero_var_indexes,
  10.198 +        term = TermSubst.zero_var_indexes,
  10.199 +        fact = Drule.zero_var_indexes_list o map Thm.strip_shyps
  10.200 +      };*)
  10.201    in
  10.202      thy
  10.203 -    |> Old_Locale.add_locale "" bname mergeexpr elems
  10.204 -    |> snd
  10.205 -    |> ProofContext.theory_of
  10.206 +    |> Expression.add_locale bname "" supexpr elems
  10.207 +    |> snd |> LocalTheory.exit_global
  10.208      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
  10.209      |-> (fn (inst, param_map, params, assm_axiom) =>
  10.210 -        `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
  10.211 +       `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
  10.212      #-> (fn axiom =>
  10.213 -        prove_class_interpretation class inst
  10.214 -          (supconsts @ map (pair class o fst o snd) params) (the_list axiom) []
  10.215 -    #> `(fn thy => raw_morphism thy class param_map axiom)
  10.216 -    #-> (fn morph =>
  10.217 -        `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
  10.218 +       `(fn thy => raw_morphism thy class sups param_map axiom)
  10.219 +    #-> (fn (morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
  10.220 +    #>  Locale.activate_global_facts (class, morph $> export_morph)
  10.221 +    #> `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
  10.222      #-> (fn (assm_intro, of_class) =>
  10.223          register class sups params base_sort inst
  10.224            morph axiom assm_intro of_class
  10.225 -    #> fold (note_assm_intro class) (the_list assm_intro)))))
  10.226 +    (*#> fold (note_assm_intro class) (the_list assm_intro*)))))
  10.227      |> TheoryTarget.init (SOME class)
  10.228      |> pair class
  10.229    end;
  10.230  
  10.231  in
  10.232  
  10.233 +val class = gen_class cert_class_spec;
  10.234  val class_cmd = gen_class read_class_spec;
  10.235 -val class = gen_class check_class_spec;
  10.236  
  10.237  end; (*local*)
  10.238  
  10.239 @@ -241,6 +246,12 @@
  10.240  
  10.241  local
  10.242  
  10.243 +fun prove_sublocale tac (sub, expr) =
  10.244 +  Expression.sublocale sub expr
  10.245 +  #> Proof.global_terminal_proof
  10.246 +      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
  10.247 +  #> ProofContext.theory_of;
  10.248 +
  10.249  fun gen_subclass prep_class do_proof raw_sup lthy =
  10.250    let
  10.251      val thy = ProofContext.theory_of lthy;
  10.252 @@ -258,16 +269,18 @@
  10.253      val _ = if null err_params then [] else
  10.254        error ("Class " ^ Syntax.string_of_sort lthy [sub] ^ " lacks parameter(s) " ^
  10.255          commas_quote err_params ^ " of " ^ Syntax.string_of_sort lthy [sup]);
  10.256 -    val sublocale_prop =
  10.257 -      Old_Locale.global_asms_of thy sup
  10.258 -      |> maps snd
  10.259 -      |> try the_single
  10.260 -      |> Option.map (ObjectLogic.ensure_propT thy);
  10.261 +
  10.262 +    val expr = ([(sup, (("", false), Expression.Positional []))], []);
  10.263 +    val (([props], _, _), goal_ctxt) =
  10.264 +      Expression.cert_goal_expression expr lthy;
  10.265 +    val some_prop = try the_single props; (*FIXME*)
  10.266      fun after_qed some_thm =
  10.267 -      LocalTheory.theory (prove_subclass_relation (sub, sup) some_thm)
  10.268 +      LocalTheory.theory (register_subclass (sub, sup) some_thm)
  10.269 +      #> is_some some_thm ? LocalTheory.theory
  10.270 +        (prove_sublocale (ALLGOALS (ProofContext.fact_tac (the_list some_thm))) (sub, expr))
  10.271        #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
  10.272    in
  10.273 -    do_proof after_qed sublocale_prop lthy
  10.274 +    do_proof after_qed some_prop lthy
  10.275    end;
  10.276  
  10.277  fun user_proof after_qed NONE =
    11.1 --- a/src/Pure/Isar/class_target.ML	Fri Jan 16 08:29:11 2009 +0100
    11.2 +++ b/src/Pure/Isar/class_target.ML	Fri Jan 16 14:58:11 2009 +0100
    11.3 @@ -10,6 +10,8 @@
    11.4    val register: class -> class list -> ((string * typ) * (string * typ)) list
    11.5      -> sort -> term list -> morphism
    11.6      -> thm option -> thm option -> thm -> theory -> theory
    11.7 +  val register_subclass: class * class -> thm option
    11.8 +    -> theory -> theory
    11.9  
   11.10    val begin: class list -> sort -> Proof.context -> Proof.context
   11.11    val init: class -> theory -> Proof.context
   11.12 @@ -21,14 +23,12 @@
   11.13  
   11.14    val intro_classes_tac: thm list -> tactic
   11.15    val default_intro_tac: Proof.context -> thm list -> tactic
   11.16 -  val prove_class_interpretation: class -> term list -> (class * string) list
   11.17 -    -> thm list -> thm list -> theory -> theory
   11.18 -  val prove_subclass_relation: class * class -> thm option -> theory -> theory
   11.19  
   11.20    val class_prefix: string -> string
   11.21    val is_class: theory -> class -> bool
   11.22    val these_params: theory -> sort -> (string * (class * (string * typ))) list
   11.23    val these_defs: theory -> sort -> thm list
   11.24 +  val eq_morph: theory -> thm list -> morphism
   11.25    val base_sort: theory -> class -> sort
   11.26    val rules: theory -> class -> thm option * thm
   11.27    val print_classes: theory -> unit
   11.28 @@ -64,36 +64,6 @@
   11.29  structure Class_Target : CLASS_TARGET =
   11.30  struct
   11.31  
   11.32 -(*temporary adaption code to mediate between old and new locale code*)
   11.33 -
   11.34 -structure Locale_Layer =
   11.35 -struct
   11.36 -
   11.37 -val init = Old_Locale.init;
   11.38 -val parameters_of = Old_Locale.parameters_of;
   11.39 -val intros = Old_Locale.intros;
   11.40 -val dests = Old_Locale.dests;
   11.41 -val get_interpret_morph = Old_Locale.get_interpret_morph;
   11.42 -val Locale = Old_Locale.Locale;
   11.43 -val extern = Old_Locale.extern;
   11.44 -val intro_locales_tac = Old_Locale.intro_locales_tac;
   11.45 -
   11.46 -fun prove_interpretation tac prfx_atts expr inst =
   11.47 -  Old_Locale.interpretation I prfx_atts expr inst
   11.48 -  ##> Proof.global_terminal_proof
   11.49 -      (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
   11.50 -  ##> ProofContext.theory_of;
   11.51 -
   11.52 -fun prove_interpretation_in tac after_qed (name, expr) =
   11.53 -  Old_Locale.interpretation_in_locale
   11.54 -      (ProofContext.theory after_qed) (name, expr)
   11.55 -  #> Proof.global_terminal_proof
   11.56 -      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   11.57 -  #> ProofContext.theory_of;
   11.58 -
   11.59 -end;
   11.60 -
   11.61 -
   11.62  (** primitive axclass and instance commands **)
   11.63  
   11.64  fun axclass_cmd (class, raw_superclasses) raw_specs thy =
   11.65 @@ -201,6 +171,8 @@
   11.66  
   11.67  val ancestry = Graph.all_succs o ClassData.get;
   11.68  
   11.69 +val heritage = Graph.all_preds o ClassData.get;
   11.70 +
   11.71  fun the_inst thy = #inst o the_class_data thy;
   11.72  
   11.73  fun these_params thy =
   11.74 @@ -235,14 +207,14 @@
   11.75  fun class_binding_morph class =
   11.76    Binding.map_prefix (K (Binding.add_prefix false (class_prefix class)));
   11.77  
   11.78 +fun eq_morph thy thms = (*FIXME how general is this?*)
   11.79 +  Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms [])
   11.80 +  $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms);
   11.81 +
   11.82  fun morphism thy class =
   11.83    let
   11.84      val { base_morph, defs, ... } = the_class_data thy class;
   11.85 -  in
   11.86 -    base_morph 
   11.87 -    $> Morphism.term_morphism (MetaSimplifier.rewrite_term thy defs [])
   11.88 -    $> Morphism.thm_morphism (MetaSimplifier.rewrite_rule defs)
   11.89 -  end;
   11.90 +  in base_morph $> eq_morph thy defs end;
   11.91  
   11.92  fun print_classes thy =
   11.93    let
   11.94 @@ -265,7 +237,7 @@
   11.95        (SOME o Pretty.block) [Pretty.str "supersort: ",
   11.96          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
   11.97        if is_class thy class then (SOME o Pretty.str)
   11.98 -        ("locale: " ^ Locale_Layer.extern thy class) else NONE,
   11.99 +        ("locale: " ^ Locale.extern thy class) else NONE,
  11.100        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
  11.101            (Pretty.str "parameters:" :: ps)) o map mk_param
  11.102          o these o Option.map #params o try (AxClass.get_info thy)) class,
  11.103 @@ -312,39 +284,26 @@
  11.104  
  11.105  (** tactics and methods **)
  11.106  
  11.107 -fun prove_class_interpretation class inst consts hyp_facts def_facts thy =
  11.108 -  let
  11.109 -    val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
  11.110 -      [class]))) (Sign.the_const_type thy c)) consts;
  11.111 -    val no_constraints = map (map_atyps (K (TFree (Name.aT, [])))) constraints;
  11.112 -    fun add_constraint c T = Sign.add_const_constraint (c, SOME T);
  11.113 -    fun tac ctxt = ALLGOALS (ProofContext.fact_tac (hyp_facts @ def_facts)
  11.114 -      ORELSE' (fn n => SELECT_GOAL (Locale_Layer.intro_locales_tac false ctxt []) n));
  11.115 -    val prfx = class_prefix class;
  11.116 -  in
  11.117 -    thy
  11.118 -    |> fold2 add_constraint (map snd consts) no_constraints
  11.119 -    |> Locale_Layer.prove_interpretation tac (class_binding_morph class) (Locale_Layer.Locale class)
  11.120 -          (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
  11.121 -    |> snd
  11.122 -    |> fold2 add_constraint (map snd consts) constraints
  11.123 -  end;
  11.124 -
  11.125 -fun prove_subclass_relation (sub, sup) some_thm thy =
  11.126 +fun register_subclass (sub, sup) thms thy =
  11.127    let
  11.128      val of_class = (snd o rules thy) sup;
  11.129 -    val intro = case some_thm
  11.130 +    val intro = case thms
  11.131       of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
  11.132        | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
  11.133            ([], [sub])], []) of_class;
  11.134      val classrel = (intro OF (the_list o fst o rules thy) sub)
  11.135        |> Thm.close_derivation;
  11.136 +    (*FIXME generic amend operation for classes*)
  11.137 +    val amendments = map (fn class => (class, morphism thy class))
  11.138 +      (heritage thy [sub]);
  11.139 +    val diff_sort = Sign.complete_sort thy [sup]
  11.140 +      |> subtract (op =) (Sign.complete_sort thy [sub]);
  11.141 +    val defs_morph = eq_morph thy (these_defs thy diff_sort);
  11.142    in
  11.143      thy
  11.144      |> AxClass.add_classrel classrel
  11.145 -    |> Locale_Layer.prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm)))
  11.146 -         I (sub, Locale_Layer.Locale sup)
  11.147      |> ClassData.map (Graph.add_edge (sub, sup))
  11.148 +    |> fold (Locale.amend_registration defs_morph) amendments
  11.149    end;
  11.150  
  11.151  fun intro_classes_tac facts st =
  11.152 @@ -428,7 +387,7 @@
  11.153  
  11.154  fun init class thy =
  11.155    thy
  11.156 -  |> Locale_Layer.init class
  11.157 +  |> Locale.init class
  11.158    |> begin [class] (base_sort thy class);
  11.159  
  11.160  
  11.161 @@ -441,12 +400,18 @@
  11.162      val morph = morphism thy' class;
  11.163      val inst = the_inst thy' class;
  11.164      val params = map (apsnd fst o snd) (these_params thy' [class]);
  11.165 +    val amendments = map (fn class => (class, morphism thy' class))
  11.166 +      (heritage thy' [class]);
  11.167  
  11.168      val c' = Sign.full_bname thy' c;
  11.169      val dict' = Morphism.term morph dict;
  11.170      val ty' = Term.fastype_of dict';
  11.171      val ty'' = Type.strip_sorts ty';
  11.172      val def_eq = Logic.mk_equals (Const (c', ty'), dict');
  11.173 +    (*FIXME a mess*)
  11.174 +    fun amend def def' (class, morph) thy =
  11.175 +      Locale.amend_registration (eq_morph thy [Thm.varifyT def])
  11.176 +        (class, morph) thy;
  11.177      fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
  11.178    in
  11.179      thy'
  11.180 @@ -454,9 +419,9 @@
  11.181      |> Thm.add_def false false (c, def_eq)
  11.182      |>> Thm.symmetric
  11.183      ||>> get_axiom
  11.184 -    |-> (fn (def, def') => prove_class_interpretation class inst params [] [def]
  11.185 -      #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
  11.186 -      #> PureThy.store_thm (c ^ "_raw", def')
  11.187 +    |-> (fn (def, def') => register_operation class (c', (dict', SOME (Thm.symmetric def')))
  11.188 +      #> fold (amend def def') amendments
  11.189 +      #> PureThy.store_thm (c ^ "_raw", def') (*FIXME name*)
  11.190        #> snd)
  11.191      |> Sign.restore_naming thy
  11.192      |> Sign.add_const_constraint (c', SOME ty')