author ballarin Thu Dec 11 18:34:05 2008 +0100 (2008-12-11) changeset 29224 5226d990d74b parent 29210 4025459e3f83 parent 29223 e09c53289830 child 29225 cfea1f3719b3
Merged.
1.1 --- a/src/HOL/Divides.thy	Thu Dec 11 17:56:34 2008 +0100
1.2 +++ b/src/HOL/Divides.thy	Thu Dec 11 18:34:05 2008 +0100
1.3 @@ -639,7 +639,7 @@
1.5  text {* @{term "op dvd"} is a partial order *}
1.7 -interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
1.8 +class_interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
1.9    proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
1.11  lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
2.1 --- a/src/HOL/Finite_Set.thy	Thu Dec 11 17:56:34 2008 +0100
2.2 +++ b/src/HOL/Finite_Set.thy	Thu Dec 11 18:34:05 2008 +0100
2.3 @@ -750,7 +750,7 @@
2.4  assumes "finite A" and "a \<notin> A"
2.5  shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
2.6  proof -
2.7 -  interpret I: fun_left_comm ["%x y. (g x) * y"]
2.8 +  interpret I: fun_left_comm "%x y. (g x) * y"
2.9      by unfold_locales (simp add: mult_ac)
2.10    show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
2.11  qed
2.12 @@ -798,7 +798,7 @@
2.13      and hyp: "\<And>x y. h (g x y) = times x (h y)"
2.14    shows "h (fold g j w A) = fold times j (h w) A"
2.15  proof -
2.16 -  interpret ab_semigroup_mult [g] by fact
2.17 +  class_interpret ab_semigroup_mult [g] by fact
2.18    show ?thesis using fin hyp by (induct set: finite) simp_all
2.19  qed
2.20  *)
2.21 @@ -873,7 +873,7 @@
2.23  subsection {* Generalized summation over a set *}
2.25 -interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
2.26 +class_interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
2.27    proof qed (auto intro: add_assoc add_commute)
2.29  definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
2.30 @@ -1760,7 +1760,7 @@
2.31  proof (induct rule: finite_induct)
2.32    case empty then show ?case by simp
2.33  next
2.34 -  interpret ab_semigroup_mult ["op Un"]
2.35 +  class_interpret ab_semigroup_mult ["op Un"]
2.36      proof qed auto
2.37    case insert
2.38    then show ?case by simp
2.39 @@ -1943,7 +1943,7 @@
2.40  assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
2.41  shows "fold_graph times z (insert b A) (z * y)"
2.42  proof -
2.43 -  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
2.44 +  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
2.45  from assms show ?thesis
2.46  proof (induct rule: fold_graph.induct)
2.47    case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
2.48 @@ -1983,7 +1983,7 @@
2.49  lemma fold1_eq_fold:
2.50  assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
2.51  proof -
2.52 -  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
2.53 +  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
2.54    from assms show ?thesis
2.55  apply (simp add: fold1_def fold_def)
2.56  apply (rule the_equality)
2.57 @@ -2010,7 +2010,7 @@
2.58    assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
2.59    shows "fold1 times (insert x A) = x * fold1 times A"
2.60  proof -
2.61 -  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
2.62 +  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
2.63    from nonempty obtain a A' where "A = insert a A' & a ~: A'"
2.64      by (auto simp add: nonempty_iff)
2.65    with A show ?thesis
2.66 @@ -2033,7 +2033,7 @@
2.67    assumes nonempty: "A \<noteq> {}" and A: "finite A"
2.68    shows "fold1 times (insert x A) = x * fold1 times A"
2.69  proof -
2.70 -  interpret fun_left_comm_idem ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"]
2.71 +  interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
2.72      by (rule fun_left_comm_idem)
2.73    from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
2.74      by (auto simp add: nonempty_iff)
2.75 @@ -2198,7 +2198,7 @@
2.76    assumes "finite A" "A \<noteq> {}"
2.77    shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
2.78  proof -
2.79 -  interpret ab_semigroup_idem_mult [inf]
2.80 +  class_interpret ab_semigroup_idem_mult [inf]
2.81      by (rule ab_semigroup_idem_mult_inf)
2.82    show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
2.83  qed
2.84 @@ -2213,7 +2213,7 @@
2.85    proof (induct rule: finite_ne_induct)
2.86      case singleton thus ?case by simp
2.87    next
2.88 -    interpret ab_semigroup_idem_mult [inf]
2.89 +    class_interpret ab_semigroup_idem_mult [inf]
2.90        by (rule ab_semigroup_idem_mult_inf)
2.91      case (insert x F)
2.92      from insert(5) have "a = x \<or> a \<in> F" by simp
2.93 @@ -2288,7 +2288,7 @@
2.94      and "A \<noteq> {}"
2.95    shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
2.96  proof -
2.97 -  interpret ab_semigroup_idem_mult [inf]
2.98 +  class_interpret ab_semigroup_idem_mult [inf]
2.99      by (rule ab_semigroup_idem_mult_inf)
2.100    from assms show ?thesis
2.101      by (simp add: Inf_fin_def image_def
2.102 @@ -2303,7 +2303,7 @@
2.103    case singleton thus ?case
2.104      by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
2.105  next
2.106 -  interpret ab_semigroup_idem_mult [inf]
2.107 +  class_interpret ab_semigroup_idem_mult [inf]
2.108      by (rule ab_semigroup_idem_mult_inf)
2.109    case (insert x A)
2.110    have finB: "finite {sup x b |b. b \<in> B}"
2.111 @@ -2333,7 +2333,7 @@
2.112    assumes "finite A" and "A \<noteq> {}"
2.113    shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
2.114  proof -
2.115 -  interpret ab_semigroup_idem_mult [sup]
2.116 +  class_interpret ab_semigroup_idem_mult [sup]
2.117      by (rule ab_semigroup_idem_mult_sup)
2.118    from assms show ?thesis
2.119      by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
2.120 @@ -2357,7 +2357,7 @@
2.121      thus ?thesis by(simp add: insert(1) B(1))
2.122    qed
2.123    have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
2.124 -  interpret ab_semigroup_idem_mult [sup]
2.125 +  class_interpret ab_semigroup_idem_mult [sup]
2.126      by (rule ab_semigroup_idem_mult_sup)
2.127    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)"
2.128      using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
2.129 @@ -2386,7 +2386,7 @@
2.130    assumes "finite A" and "A \<noteq> {}"
2.131    shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
2.132  proof -
2.133 -  interpret ab_semigroup_idem_mult [inf]
2.134 +  class_interpret ab_semigroup_idem_mult [inf]
2.135      by (rule ab_semigroup_idem_mult_inf)
2.136    from assms show ?thesis
2.137    unfolding Inf_fin_def by (induct A set: finite)
2.138 @@ -2397,7 +2397,7 @@
2.139    assumes "finite A" and "A \<noteq> {}"
2.140    shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
2.141  proof -
2.142 -  interpret ab_semigroup_idem_mult [sup]
2.143 +  class_interpret ab_semigroup_idem_mult [sup]
2.144      by (rule ab_semigroup_idem_mult_sup)
2.145    from assms show ?thesis
2.146    unfolding Sup_fin_def by (induct A set: finite)
2.147 @@ -2446,7 +2446,7 @@
2.148    assumes "finite A" and "A \<noteq> {}"
2.149    shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
2.150  proof -
2.151 -  interpret ab_semigroup_idem_mult [min]
2.152 +  class_interpret ab_semigroup_idem_mult [min]
2.153      by (rule ab_semigroup_idem_mult_min)
2.154    from assms show ?thesis
2.155    by (induct rule: finite_ne_induct)
2.156 @@ -2457,7 +2457,7 @@
2.157    assumes "finite A" and "A \<noteq> {}"
2.158    shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
2.159  proof -
2.160 -  interpret ab_semigroup_idem_mult [min]
2.161 +  class_interpret ab_semigroup_idem_mult [min]
2.162      by (rule ab_semigroup_idem_mult_min)
2.163    from assms show ?thesis
2.164    by (induct rule: finite_ne_induct)
2.165 @@ -2468,7 +2468,7 @@
2.166    assumes "finite A" and "A \<noteq> {}"
2.167    shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
2.168  proof -
2.169 -  interpret ab_semigroup_idem_mult [min]
2.170 +  class_interpret ab_semigroup_idem_mult [min]
2.171      by (rule ab_semigroup_idem_mult_min)
2.172    from assms show ?thesis
2.173    by (induct rule: finite_ne_induct)
2.174 @@ -2481,7 +2481,7 @@
2.175  proof cases
2.176    assume "A = B" thus ?thesis by simp
2.177  next
2.178 -  interpret ab_semigroup_idem_mult [min]
2.179 +  class_interpret ab_semigroup_idem_mult [min]
2.180      by (rule ab_semigroup_idem_mult_min)
2.181    assume "A \<noteq> B"
2.182    have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
2.183 @@ -2515,7 +2515,7 @@
2.184    assumes "finite A" and "A \<noteq> {}"
2.185    shows "Min (insert x A) = min x (Min A)"
2.186  proof -
2.187 -  interpret ab_semigroup_idem_mult [min]
2.188 +  class_interpret ab_semigroup_idem_mult [min]
2.189      by (rule ab_semigroup_idem_mult_min)
2.190    from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
2.191  qed
2.192 @@ -2524,7 +2524,7 @@
2.193    assumes "finite A" and "A \<noteq> {}"
2.194    shows "Max (insert x A) = max x (Max A)"
2.195  proof -
2.196 -  interpret ab_semigroup_idem_mult [max]
2.197 +  class_interpret ab_semigroup_idem_mult [max]
2.198      by (rule ab_semigroup_idem_mult_max)
2.199    from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
2.200  qed
2.201 @@ -2533,7 +2533,7 @@
2.202    assumes "finite A" and "A \<noteq> {}"
2.203    shows "Min A \<in> A"
2.204  proof -
2.205 -  interpret ab_semigroup_idem_mult [min]
2.206 +  class_interpret ab_semigroup_idem_mult [min]
2.207      by (rule ab_semigroup_idem_mult_min)
2.208    from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
2.209  qed
2.210 @@ -2542,7 +2542,7 @@
2.211    assumes "finite A" and "A \<noteq> {}"
2.212    shows "Max A \<in> A"
2.213  proof -
2.214 -  interpret ab_semigroup_idem_mult [max]
2.215 +  class_interpret ab_semigroup_idem_mult [max]
2.216      by (rule ab_semigroup_idem_mult_max)
2.217    from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
2.218  qed
2.219 @@ -2551,7 +2551,7 @@
2.220    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
2.221    shows "Min (A \<union> B) = min (Min A) (Min B)"
2.222  proof -
2.223 -  interpret ab_semigroup_idem_mult [min]
2.224 +  class_interpret ab_semigroup_idem_mult [min]
2.225      by (rule ab_semigroup_idem_mult_min)
2.226    from assms show ?thesis
2.227      by (simp add: Min_def fold1_Un2)
2.228 @@ -2561,7 +2561,7 @@
2.229    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
2.230    shows "Max (A \<union> B) = max (Max A) (Max B)"
2.231  proof -
2.232 -  interpret ab_semigroup_idem_mult [max]
2.233 +  class_interpret ab_semigroup_idem_mult [max]
2.234      by (rule ab_semigroup_idem_mult_max)
2.235    from assms show ?thesis
2.236      by (simp add: Max_def fold1_Un2)
2.237 @@ -2572,7 +2572,7 @@
2.238      and "finite N" and "N \<noteq> {}"
2.239    shows "h (Min N) = Min (h ` N)"
2.240  proof -
2.241 -  interpret ab_semigroup_idem_mult [min]
2.242 +  class_interpret ab_semigroup_idem_mult [min]
2.243      by (rule ab_semigroup_idem_mult_min)
2.244    from assms show ?thesis
2.245      by (simp add: Min_def hom_fold1_commute)
2.246 @@ -2583,7 +2583,7 @@
2.247      and "finite N" and "N \<noteq> {}"
2.248    shows "h (Max N) = Max (h ` N)"
2.249  proof -
2.250 -  interpret ab_semigroup_idem_mult [max]
2.251 +  class_interpret ab_semigroup_idem_mult [max]
2.252      by (rule ab_semigroup_idem_mult_max)
2.253    from assms show ?thesis
2.254      by (simp add: Max_def hom_fold1_commute [of h])
2.255 @@ -2593,7 +2593,7 @@
2.256    assumes "finite A" and "x \<in> A"
2.257    shows "Min A \<le> x"
2.258  proof -
2.259 -  interpret lower_semilattice ["op \<le>" "op <" min]
2.260 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
2.261      by (rule min_lattice)
2.262    from assms show ?thesis by (simp add: Min_def fold1_belowI)
2.263  qed
2.264 @@ -2611,7 +2611,7 @@
2.265    assumes "finite A" and "A \<noteq> {}"
2.266    shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
2.267  proof -
2.268 -  interpret lower_semilattice ["op \<le>" "op <" min]
2.269 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
2.270      by (rule min_lattice)
2.271    from assms show ?thesis by (simp add: Min_def below_fold1_iff)
2.272  qed
2.273 @@ -2629,7 +2629,7 @@
2.274    assumes "finite A" and "A \<noteq> {}"
2.275    shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
2.276  proof -
2.277 -  interpret lower_semilattice ["op \<le>" "op <" min]
2.278 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
2.279      by (rule min_lattice)
2.280    from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
2.281  qed
2.282 @@ -2639,7 +2639,7 @@
2.283    shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
2.284  proof -
2.285    note Max = Max_def
2.286 -  interpret linorder ["op \<ge>" "op >"]
2.287 +  class_interpret linorder ["op \<ge>" "op >"]
2.288      by (rule dual_linorder)
2.289    from assms show ?thesis
2.290      by (simp add: Max strict_below_fold1_iff [folded dual_max])
2.291 @@ -2649,7 +2649,7 @@
2.292    assumes "finite A" and "A \<noteq> {}"
2.293    shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
2.294  proof -
2.295 -  interpret lower_semilattice ["op \<le>" "op <" min]
2.296 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
2.297      by (rule min_lattice)
2.298    from assms show ?thesis
2.299      by (simp add: Min_def fold1_below_iff)
2.300 @@ -2660,7 +2660,7 @@
2.301    shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
2.302  proof -
2.303    note Max = Max_def
2.304 -  interpret linorder ["op \<ge>" "op >"]
2.305 +  class_interpret linorder ["op \<ge>" "op >"]
2.306      by (rule dual_linorder)
2.307    from assms show ?thesis
2.308      by (simp add: Max fold1_below_iff [folded dual_max])
2.309 @@ -2670,7 +2670,7 @@
2.310    assumes "finite A" and "A \<noteq> {}"
2.311    shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
2.312  proof -
2.313 -  interpret lower_semilattice ["op \<le>" "op <" min]
2.314 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
2.315      by (rule min_lattice)
2.316    from assms show ?thesis
2.317      by (simp add: Min_def fold1_strict_below_iff)
2.318 @@ -2681,7 +2681,7 @@
2.319    shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
2.320  proof -
2.321    note Max = Max_def
2.322 -  interpret linorder ["op \<ge>" "op >"]
2.323 +  class_interpret linorder ["op \<ge>" "op >"]
2.324      by (rule dual_linorder)
2.325    from assms show ?thesis
2.326      by (simp add: Max fold1_strict_below_iff [folded dual_max])
2.327 @@ -2691,7 +2691,7 @@
2.328    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
2.329    shows "Min N \<le> Min M"
2.330  proof -
2.331 -  interpret distrib_lattice ["op \<le>" "op <" min max]
2.332 +  class_interpret distrib_lattice ["op \<le>" "op <" min max]
2.333      by (rule distrib_lattice_min_max)
2.334    from assms show ?thesis by (simp add: Min_def fold1_antimono)
2.335  qed
2.336 @@ -2701,7 +2701,7 @@
2.337    shows "Max M \<le> Max N"
2.338  proof -
2.339    note Max = Max_def
2.340 -  interpret linorder ["op \<ge>" "op >"]
2.341 +  class_interpret linorder ["op \<ge>" "op >"]
2.342      by (rule dual_linorder)
2.343    from assms show ?thesis
2.344      by (simp add: Max fold1_antimono [folded dual_max])
3.1 --- a/src/HOL/Groebner_Basis.thy	Thu Dec 11 17:56:34 2008 +0100
3.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Dec 11 18:34:05 2008 +0100
3.3 @@ -1,5 +1,4 @@
3.4  (*  Title:      HOL/Groebner_Basis.thy
3.5 -    ID:         \$Id\$
3.6      Author:     Amine Chaieb, TU Muenchen
3.7  *)
3.9 @@ -165,7 +164,7 @@
3.10  end
3.12  interpretation class_semiring: gb_semiring
3.13 -    ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
3.14 +    "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
3.15    proof qed (auto simp add: ring_simps power_Suc)
3.17  lemmas nat_arith =
3.18 @@ -242,8 +241,8 @@
3.19  end
3.22 -interpretation class_ring: gb_ring ["op +" "op *" "op ^"
3.23 -    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
3.24 +interpretation class_ring: gb_ring "op +" "op *" "op ^"
3.25 +    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
3.26    proof qed simp_all
3.29 @@ -344,7 +343,7 @@
3.30  qed
3.32  interpretation class_ringb: ringb
3.33 -  ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
3.34 +  "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
3.35  proof(unfold_locales, simp add: ring_simps power_Suc, auto)
3.36    fix w x y z ::"'a::{idom,recpower,number_ring}"
3.37    assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
3.38 @@ -360,7 +359,7 @@
3.39  declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
3.41  interpretation natgb: semiringb
3.42 -  ["op +" "op *" "op ^" "0::nat" "1"]
3.43 +  "op +" "op *" "op ^" "0::nat" "1"
3.44  proof (unfold_locales, simp add: ring_simps power_Suc)
3.45    fix w x y z ::"nat"
3.46    { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
3.47 @@ -465,7 +464,7 @@
3.48  subsection{* Groebner Bases for fields *}
3.50  interpretation class_fieldgb:
3.51 -  fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse)
3.52 +  fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
3.54  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
3.55  lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
4.1 --- a/src/HOL/Lattices.thy	Thu Dec 11 17:56:34 2008 +0100
4.2 +++ b/src/HOL/Lattices.thy	Thu Dec 11 18:34:05 2008 +0100
4.3 @@ -300,7 +300,7 @@
4.4    by auto
4.5  qed (auto simp add: min_def max_def not_le less_imp_le)
4.7 -interpretation min_max:
4.8 +class_interpretation min_max:
4.9    distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
4.10    by (rule distrib_lattice_min_max)
5.1 --- a/src/HOL/List.thy	Thu Dec 11 17:56:34 2008 +0100
5.2 +++ b/src/HOL/List.thy	Thu Dec 11 18:34:05 2008 +0100
5.3 @@ -548,9 +548,9 @@
5.4  lemma append_Nil2 [simp]: "xs @ [] = xs"
5.5  by (induct xs) auto
5.7 -interpretation semigroup_append: semigroup_add ["op @"]
5.8 +class_interpretation semigroup_append: semigroup_add ["op @"]
5.9    proof qed simp
5.10 -interpretation monoid_append: monoid_add ["[]" "op @"]
5.11 +class_interpretation monoid_append: monoid_add ["[]" "op @"]
5.12    proof qed simp+
5.14  lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
6.1 --- a/src/HOL/ex/LocaleTest2.thy	Thu Dec 11 17:56:34 2008 +0100
6.2 +++ b/src/HOL/ex/LocaleTest2.thy	Thu Dec 11 18:34:05 2008 +0100
6.3 @@ -433,8 +433,7 @@
6.4  end
6.7 -interpretation dlo < dlat
6.8 -(* TODO: definition syntax is unavailable *)
6.9 +sublocale dlo < dlat
6.10  proof
6.11    fix x y
6.12    from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
6.13 @@ -445,7 +444,7 @@
6.14    then show "EX sup. is_sup x y sup" by blast
6.15  qed
6.17 -interpretation dlo < ddlat
6.18 +sublocale dlo < ddlat
6.19  proof
6.20    fix x y z
6.21    show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
7.1 --- a/src/HOL/main.ML	Thu Dec 11 17:56:34 2008 +0100
7.2 +++ b/src/HOL/main.ML	Thu Dec 11 18:34:05 2008 +0100
7.3 @@ -4,4 +4,5 @@
7.4  Classical Higher-order Logic -- only "Main".
7.5  *)
7.7 +set new_locales;
7.8  use_thy "Main";
8.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Dec 11 17:56:34 2008 +0100
8.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Dec 11 18:34:05 2008 +0100
8.3 @@ -53,8 +53,7 @@
8.4    val print_configs: Toplevel.transition -> Toplevel.transition
8.5    val print_theorems: Toplevel.transition -> Toplevel.transition
8.6    val print_locales: Toplevel.transition -> Toplevel.transition
8.7 -  val print_locale: bool * (Locale.expr * Element.context list)
8.8 -    -> Toplevel.transition -> Toplevel.transition
8.9 +  val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
8.10    val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
8.11    val print_attributes: Toplevel.transition -> Toplevel.transition
8.12    val print_simpset: Toplevel.transition -> Toplevel.transition
8.13 @@ -354,11 +353,11 @@
8.14  val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
8.16  val print_locales = Toplevel.unknown_theory o
8.17 -  Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
8.18 +  Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of);
8.20 -fun print_locale (show_facts, (imports, body)) = Toplevel.unknown_theory o
8.21 +fun print_locale (show_facts, name) = Toplevel.unknown_theory o
8.22    Toplevel.keep (fn state =>
8.23 -    Locale.print_locale (Toplevel.theory_of state) show_facts imports body);
8.24 +    NewLocale.print_locale (Toplevel.theory_of state) show_facts name);
8.26  fun print_registrations show_wits name = Toplevel.unknown_context o
8.27    Toplevel.keep (Toplevel.node_case
9.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Dec 11 17:56:34 2008 +0100
9.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Dec 11 18:34:05 2008 +0100
9.3 @@ -385,18 +385,18 @@
9.4  (* locales *)
9.6  val locale_val =
9.7 -  SpecParse.locale_expr --
9.8 +  SpecParse.locale_expression --
9.9      Scan.optional (P.\$\$\$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
9.10 -  Scan.repeat1 SpecParse.context_element >> pair Locale.empty;
9.11 +  Scan.repeat1 SpecParse.context_element >> pair ([], []);
9.13  val _ =
9.14    OuterSyntax.command "locale" "define named proof context" K.thy_decl
9.15 -    (P.name -- Scan.optional (P.\$\$\$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
9.16 +    (P.name -- Scan.optional (P.\$\$\$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
9.17        >> (fn ((name, (expr, elems)), begin) =>
9.18            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
9.19 -            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
9.20 -
9.21 -val opt_prefix = Scan.optional (P.binding --| P.\$\$\$ ":") Binding.empty;
9.22 +            (Expression.add_locale_cmd name name expr elems #>
9.23 +              (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |>
9.24 +                fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes))));
9.26  val _ =
9.27    OuterSyntax.command "sublocale"
9.28 @@ -407,6 +407,39 @@
9.30  val _ =
9.31    OuterSyntax.command "interpretation"
9.32 +    "prove interpretation of locale expression in theory" K.thy_goal
9.33 +    (P.!!! SpecParse.locale_expression
9.34 +        >> (fn expr => Toplevel.print o
9.35 +            Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
9.36 +
9.37 +val _ =
9.38 +  OuterSyntax.command "interpret"
9.39 +    "prove interpretation of locale expression in proof context"
9.40 +    (K.tag_proof K.prf_goal)
9.41 +    (P.!!! SpecParse.locale_expression
9.42 +        >> (fn expr => Toplevel.print o
9.43 +            Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
9.44 +
9.45 +local
9.46 +
9.47 +val opt_prefix = Scan.optional (P.binding --| P.\$\$\$ ":") Binding.empty;
9.48 +
9.49 +in
9.50 +
9.51 +val locale_val =
9.52 +  SpecParse.locale_expr --
9.53 +    Scan.optional (P.\$\$\$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
9.54 +  Scan.repeat1 SpecParse.context_element >> pair Locale.empty;
9.55 +
9.56 +val _ =
9.57 +  OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl
9.58 +    (P.name -- Scan.optional (P.\$\$\$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
9.59 +      >> (fn ((name, (expr, elems)), begin) =>
9.60 +          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
9.61 +            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
9.62 +
9.63 +val _ =
9.64 +  OuterSyntax.command "class_interpretation"
9.65      "prove and register interpretation of locale expression in theory or locale" K.thy_goal
9.66      (P.xname --| (P.\$\$\$ "\\<subseteq>" || P.\$\$\$ "<") -- P.!!! SpecParse.locale_expr
9.67        >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
9.68 @@ -416,7 +449,7 @@
9.69                (Locale.interpretation_cmd (Binding.base_name name) expr insts)));
9.71  val _ =
9.72 -  OuterSyntax.command "interpret"
9.73 +  OuterSyntax.command "class_interpret"
9.74      "prove and register interpretation of locale expression in proof context"
9.75      (K.tag_proof K.prf_goal)
9.76      (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
9.77 @@ -424,6 +457,8 @@
9.78            Toplevel.proof'
9.79              (fn int => Locale.interpret_cmd (Binding.base_name name) expr insts int)));
9.81 +end;
9.82 +
9.84  (* classes *)
9.86 @@ -817,7 +852,7 @@
9.88  val _ =
9.89    OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
9.90 -    (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
9.91 +    (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
9.93  val _ =
9.94    OuterSyntax.improper_command "print_interps"
10.1 --- a/src/Pure/Isar/theory_target.ML	Thu Dec 11 17:56:34 2008 +0100
10.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Dec 11 18:34:05 2008 +0100
10.3 @@ -24,13 +24,20 @@
10.5  (* new locales *)
10.7 -fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x;
10.8 -fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
10.9 -fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
10.10 -fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
10.11 -fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
10.12 -fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x;
10.13 -fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x;
10.14 +fun locale_extern is_class x =
10.15 +  if !new_locales andalso not is_class then NewLocale.extern x else Locale.extern x;
10.16 +fun locale_add_type_syntax is_class x =
10.17 +  if !new_locales andalso not is_class then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
10.18 +fun locale_add_term_syntax is_class x =
10.19 +  if !new_locales andalso not is_class then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
10.20 +fun locale_add_declaration is_class x =
10.21 +  if !new_locales andalso not is_class then NewLocale.add_declaration x else Locale.add_declaration x;
10.22 +fun locale_add_thmss is_class x =
10.23 +  if !new_locales andalso not is_class then NewLocale.add_thmss x else Locale.add_thmss x;
10.24 +fun locale_init x =
10.25 +  if !new_locales then NewLocale.init x else Locale.init x;
10.26 +fun locale_intern is_class x =
10.27 +  if !new_locales andalso not is_class then NewLocale.intern x else Locale.intern x;
10.29  (* context data *)
10.31 @@ -58,7 +65,7 @@
10.32  fun pretty_thy ctxt target is_locale is_class =
10.33    let
10.34      val thy = ProofContext.theory_of ctxt;
10.35 -    val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
10.36 +    val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target;
10.37      val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
10.38        (#1 (ProofContext.inferred_fixes ctxt));
10.39      val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
10.40 @@ -94,7 +101,7 @@
10.41        |> LocalTheory.target (Context.proof_map d0)
10.42      else
10.43        lthy
10.44 -      |> LocalTheory.target (add target d')
10.45 +      |> LocalTheory.target (add is_class target d')
10.46    end;
10.48  val type_syntax = target_decl locale_add_type_syntax;
10.49 @@ -179,7 +186,7 @@
10.50          #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
10.51          #> Sign.restore_naming thy)
10.52      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
10.53 -    |> is_locale ? LocalTheory.target (locale_add_thmss target kind target_facts)
10.54 +    |> is_locale ? LocalTheory.target (locale_add_thmss is_class target kind target_facts)
10.55      |> note_local kind local_facts
10.56    end;
10.58 @@ -367,7 +374,8 @@
10.59  fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
10.61  fun context "-" thy = init NONE thy
10.62 -  | context target thy = init (SOME (locale_intern thy target)) thy;
10.63 +  | context target thy = init (SOME (locale_intern
10.64 +      (not (NewLocale.test_locale thy (NewLocale.intern thy target))) thy target)) thy;
10.66  fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
11.1 --- a/src/ZF/Constructible/L_axioms.thy	Thu Dec 11 17:56:34 2008 +0100
11.2 +++ b/src/ZF/Constructible/L_axioms.thy	Thu Dec 11 18:34:05 2008 +0100
11.3 @@ -1,5 +1,4 @@
11.4  (*  Title:      ZF/Constructible/L_axioms.thy
11.5 -    ID:         \$Id\$
11.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
11.7  *)
11.9 @@ -100,7 +99,7 @@
11.10    apply (rule L_nat)
11.11    done
11.13 -interpretation M_trivial ["L"] by (rule M_trivial_L)
11.14 +interpretation L: M_trivial L by (rule M_trivial_L)
11.16  (* Replaces the following declarations...
11.17  lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
12.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Thu Dec 11 17:56:34 2008 +0100
12.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Dec 11 18:34:05 2008 +0100
12.3 @@ -1,5 +1,4 @@
12.4  (*  Title:      ZF/Constructible/Rec_Separation.thy
12.5 -    ID:   \$Id\$
12.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
12.7  *)
12.9 @@ -186,7 +185,7 @@
12.10  theorem M_trancl_L: "PROP M_trancl(L)"
12.11  by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
12.13 -interpretation M_trancl [L] by (rule M_trancl_L)
12.14 +interpretation L: M_trancl L by (rule M_trancl_L)
12.17  subsection{*@{term L} is Closed Under the Operator @{term list}*}
12.18 @@ -373,7 +372,7 @@
12.19    apply (rule M_datatypes_axioms_L)
12.20    done
12.22 -interpretation M_datatypes [L] by (rule M_datatypes_L)
12.23 +interpretation L: M_datatypes L by (rule M_datatypes_L)
12.26  subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
12.27 @@ -436,7 +435,7 @@
12.28    apply (rule M_eclose_axioms_L)
12.29    done
12.31 -interpretation M_eclose [L] by (rule M_eclose_L)
12.32 +interpretation L: M_eclose L by (rule M_eclose_L)
12.35  end
13.1 --- a/src/ZF/Constructible/Separation.thy	Thu Dec 11 17:56:34 2008 +0100
13.2 +++ b/src/ZF/Constructible/Separation.thy	Thu Dec 11 18:34:05 2008 +0100
13.3 @@ -305,7 +305,7 @@
13.4  theorem M_basic_L: "PROP M_basic(L)"
13.5  by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
13.7 -interpretation M_basic [L] by (rule M_basic_L)
13.8 +interpretation L: M_basic L by (rule M_basic_L)
13.11  end
14.1 --- a/src/ZF/ROOT.ML	Thu Dec 11 17:56:34 2008 +0100
14.2 +++ b/src/ZF/ROOT.ML	Thu Dec 11 18:34:05 2008 +0100
14.3 @@ -8,5 +8,6 @@
14.4  Paulson.
14.5  *)
14.7 +set new_locales;
14.8  use_thys ["Main", "Main_ZFC"];
15.1 --- a/src/ZF/ex/Group.thy	Thu Dec 11 17:56:34 2008 +0100
15.2 +++ b/src/ZF/ex/Group.thy	Thu Dec 11 18:34:05 2008 +0100
15.3 @@ -1,5 +1,4 @@
15.4  (* Title:  ZF/ex/Group.thy
15.5 -  Id:     \$Id\$
15.7  *)
15.9 @@ -40,7 +39,7 @@
15.10    m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where
15.11    "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"
15.13 -locale monoid = struct G +
15.14 +locale monoid = fixes G (structure)
15.15    assumes m_closed [intro, simp]:
15.16           "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
15.17        and m_assoc:
15.18 @@ -242,7 +241,7 @@
15.20  subsection {* Substructures *}
15.22 -locale subgroup = var H + struct G +
15.23 +locale subgroup = fixes H and G (structure)
15.24    assumes subset: "H \<subseteq> carrier(G)"
15.25      and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H"
15.26      and  one_closed [simp]: "\<one> \<in> H"
15.27 @@ -262,7 +261,7 @@
15.28    assumes "group(G)"
15.29    shows "group_axioms (update_carrier(G,H))"
15.30  proof -
15.31 -  interpret group [G] by fact
15.32 +  interpret group G by fact
15.33    show ?thesis by (force intro: group_axioms.intro l_inv r_inv)
15.34  qed
15.36 @@ -270,7 +269,7 @@
15.37    assumes "group(G)"
15.38    shows "group (update_carrier(G,H))"
15.39  proof -
15.40 -  interpret group [G] by fact
15.41 +  interpret group G by fact
15.42    show ?thesis
15.43    by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
15.44  qed
15.45 @@ -316,8 +315,8 @@
15.46    assumes "group(G)" and "group(H)"
15.47    shows "group (G \<Otimes> H)"
15.48  proof -
15.49 -  interpret G: group [G] by fact
15.50 -  interpret H: group [H] by fact
15.51 +  interpret G: group G by fact
15.52 +  interpret H: group H by fact
15.53    show ?thesis by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
15.54            simp add: DirProdGroup_def)
15.55  qed
15.56 @@ -397,8 +396,8 @@
15.57    assumes "group(G)" and "group(H)"
15.58    shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
15.59  proof -
15.60 -  interpret group [G] by fact
15.61 -  interpret group [H] by fact
15.62 +  interpret group G by fact
15.63 +  interpret group H by fact
15.64    show ?thesis by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
15.65  qed
15.67 @@ -407,16 +406,17 @@
15.68    shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
15.69            \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
15.70  proof -
15.71 -  interpret group [G] by fact
15.72 -  interpret group [H] by fact
15.73 -  interpret group [I] by fact
15.74 +  interpret group G by fact
15.75 +  interpret group H by fact
15.76 +  interpret group I by fact
15.77    show ?thesis
15.78      by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def)
15.79  qed
15.81  text{*Basis for homomorphism proofs: we assume two groups @{term G} and
15.82    @term{H}, with a homomorphism @{term h} between them*}
15.83 -locale group_hom = group G + group H + var h +
15.84 +locale group_hom = G: group G + H: group H
15.85 +  for G (structure) and H (structure) and h +
15.86    assumes homh: "h \<in> hom(G,H)"
15.87    notes hom_mult [simp] = hom_mult [OF homh]
15.88      and hom_closed [simp] = hom_closed [OF homh]
15.89 @@ -870,7 +870,7 @@
15.90     assumes "group(G)"
15.91     shows "equiv (carrier(G), rcong H)"
15.92  proof -
15.93 -  interpret group [G] by fact
15.94 +  interpret group G by fact
15.95    show ?thesis proof (simp add: equiv_def, intro conjI)
15.96      show "rcong H \<subseteq> carrier(G) \<times> carrier(G)"
15.97        by (auto simp add: r_congruent_def)
15.98 @@ -907,7 +907,7 @@
15.99    assumes a: "a \<in> carrier(G)"
15.100    shows "a <# H = (rcong H) `` {a}"
15.101  proof -
15.102 -  interpret group [G] by fact
15.103 +  interpret group G by fact
15.104    show ?thesis
15.105      by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a
15.106        Collect_image_eq)
15.107 @@ -920,7 +920,7 @@
15.108          h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
15.109        \<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})" (is "PROP ?P")
15.110  proof -
15.111 -  interpret subgroup [H G] by fact
15.112 +  interpret subgroup H G by fact
15.113    show "PROP ?P"
15.114      apply (rule UN_I [of "hb \<cdot> ((inv ha) \<cdot> h)"], simp)
15.115      apply (simp add: m_assoc transpose_inv)
15.116 @@ -931,7 +931,7 @@
15.117    assumes "subgroup(H, G)"
15.118    shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = 0" (is "PROP ?P")
15.119  proof -
15.120 -  interpret subgroup [H G] by fact
15.121 +  interpret subgroup H G by fact
15.122    show "PROP ?P"
15.123      apply (simp add: RCOSETS_def r_coset_def)
15.124      apply (blast intro: rcos_equation prems sym)
15.125 @@ -949,7 +949,7 @@
15.126    assumes "subgroup(H, G)"
15.127    shows "x \<in> carrier(G) \<Longrightarrow> x \<in> H #> x" (is "PROP ?P")
15.128  proof -
15.129 -  interpret subgroup [H G] by fact
15.130 +  interpret subgroup H G by fact
15.131    show "PROP ?P"
15.132      apply (simp add: r_coset_def)
15.133      apply (rule_tac x="\<one>" in bexI) apply (auto)
15.134 @@ -960,7 +960,7 @@
15.135    assumes "subgroup(H, G)"
15.136    shows "\<Union>(rcosets H) = carrier(G)"
15.137  proof -
15.138 -  interpret subgroup [H G] by fact
15.139 +  interpret subgroup H G by fact
15.140    show ?thesis
15.141      apply (rule equalityI)
15.142      apply (force simp add: RCOSETS_def r_coset_def)
15.143 @@ -1044,7 +1044,7 @@
15.144    assumes "group(G)"
15.145    shows "H \<in> rcosets H"
15.146  proof -
15.147 -  interpret group [G] by fact
15.148 +  interpret group G by fact
15.149    have "H #> \<one> = H"
15.150      using _ subgroup_axioms by (rule coset_join2) simp_all
15.151    then show ?thesis
16.1 --- a/src/ZF/ex/Ring.thy	Thu Dec 11 17:56:34 2008 +0100
16.2 +++ b/src/ZF/ex/Ring.thy	Thu Dec 11 18:34:05 2008 +0100
16.3 @@ -45,7 +45,7 @@
16.4    minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
16.5    "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
16.7 -locale abelian_monoid = struct G +
16.8 +locale abelian_monoid = fixes G (structure)
16.9    assumes a_comm_monoid:
16.10      "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
16.12 @@ -57,7 +57,7 @@
16.13    assumes a_comm_group:
16.14      "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
16.16 -locale ring = abelian_group R + monoid R +
16.17 +locale ring = abelian_group R + monoid R for R (structure) +
16.18    assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
16.19        \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
16.20      and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
16.21 @@ -262,7 +262,8 @@
16.22  lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
16.23  by (simp add: ring_hom_def)
16.25 -locale ring_hom_cring = cring R + cring S + var h +
16.26 +locale ring_hom_cring = R: cring R + S: cring S
16.27 +  for R (structure) and S (structure) and h +
16.28    assumes homh [simp, intro]: "h \<in> ring_hom(R,S)"
16.29    notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
16.30      and hom_mult [simp] = ring_hom_mult [OF homh]