# HG changeset patch
# User ballarin
# Date 1229016845 -3600
# Node ID 5226d990d74b9e5f440b7111cd3793b0f3ca2bda
# Parent  4025459e3f83fcabe2c4cf42ab7e141a353fef01# Parent  e09c532898307cc7c8d49d7c21aa42fb6655db8e
Merged.

diff -r 4025459e3f83 -r 5226d990d74b src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/HOL/Divides.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -639,7 +639,7 @@
 
 text {* @{term "op dvd"} is a partial order *}
 
-interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
+class_interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
   proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
 
 lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
diff -r 4025459e3f83 -r 5226d990d74b src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -750,7 +750,7 @@
 assumes "finite A" and "a \<notin> A"
 shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
 proof -
-  interpret I: fun_left_comm ["%x y. (g x) * y"]
+  interpret I: fun_left_comm "%x y. (g x) * y"
     by unfold_locales (simp add: mult_ac)
   show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
 qed
@@ -798,7 +798,7 @@
     and hyp: "\<And>x y. h (g x y) = times x (h y)"
   shows "h (fold g j w A) = fold times j (h w) A"
 proof -
-  interpret ab_semigroup_mult [g] by fact
+  class_interpret ab_semigroup_mult [g] by fact
   show ?thesis using fin hyp by (induct set: finite) simp_all
 qed
 *)
@@ -873,7 +873,7 @@
 
 subsection {* Generalized summation over a set *}
 
-interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
+class_interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
   proof qed (auto intro: add_assoc add_commute)
 
 definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
@@ -1760,7 +1760,7 @@
 proof (induct rule: finite_induct)
   case empty then show ?case by simp
 next
-  interpret ab_semigroup_mult ["op Un"]
+  class_interpret ab_semigroup_mult ["op Un"]
     proof qed auto
   case insert 
   then show ?case by simp
@@ -1943,7 +1943,7 @@
 assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
 shows "fold_graph times z (insert b A) (z * y)"
 proof -
-  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
+  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
 from assms show ?thesis
 proof (induct rule: fold_graph.induct)
   case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
@@ -1983,7 +1983,7 @@
 lemma fold1_eq_fold:
 assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
 proof -
-  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
+  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
   from assms show ?thesis
 apply (simp add: fold1_def fold_def)
 apply (rule the_equality)
@@ -2010,7 +2010,7 @@
   assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
   shows "fold1 times (insert x A) = x * fold1 times A"
 proof -
-  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
+  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
   from nonempty obtain a A' where "A = insert a A' & a ~: A'"
     by (auto simp add: nonempty_iff)
   with A show ?thesis
@@ -2033,7 +2033,7 @@
   assumes nonempty: "A \<noteq> {}" and A: "finite A" 
   shows "fold1 times (insert x A) = x * fold1 times A"
 proof -
-  interpret fun_left_comm_idem ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"]
+  interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
     by (rule fun_left_comm_idem)
   from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
     by (auto simp add: nonempty_iff)
@@ -2198,7 +2198,7 @@
   assumes "finite A" "A \<noteq> {}"
   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
 proof -
-  interpret ab_semigroup_idem_mult [inf]
+  class_interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
 qed
@@ -2213,7 +2213,7 @@
   proof (induct rule: finite_ne_induct)
     case singleton thus ?case by simp
   next
-    interpret ab_semigroup_idem_mult [inf]
+    class_interpret ab_semigroup_idem_mult [inf]
       by (rule ab_semigroup_idem_mult_inf)
     case (insert x F)
     from insert(5) have "a = x \<or> a \<in> F" by simp
@@ -2288,7 +2288,7 @@
     and "A \<noteq> {}"
   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
 proof -
-  interpret ab_semigroup_idem_mult [inf]
+  class_interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   from assms show ?thesis
     by (simp add: Inf_fin_def image_def
@@ -2303,7 +2303,7 @@
   case singleton thus ?case
     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
 next
-  interpret ab_semigroup_idem_mult [inf]
+  class_interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   case (insert x A)
   have finB: "finite {sup x b |b. b \<in> B}"
@@ -2333,7 +2333,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
 proof -
-  interpret ab_semigroup_idem_mult [sup]
+  class_interpret ab_semigroup_idem_mult [sup]
     by (rule ab_semigroup_idem_mult_sup)
   from assms show ?thesis
     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
@@ -2357,7 +2357,7 @@
     thus ?thesis by(simp add: insert(1) B(1))
   qed
   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
-  interpret ab_semigroup_idem_mult [sup]
+  class_interpret ab_semigroup_idem_mult [sup]
     by (rule ab_semigroup_idem_mult_sup)
   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)"
     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
@@ -2386,7 +2386,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
 proof -
-  interpret ab_semigroup_idem_mult [inf]
+  class_interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   from assms show ?thesis
   unfolding Inf_fin_def by (induct A set: finite)
@@ -2397,7 +2397,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
 proof -
-  interpret ab_semigroup_idem_mult [sup]
+  class_interpret ab_semigroup_idem_mult [sup]
     by (rule ab_semigroup_idem_mult_sup)
   from assms show ?thesis
   unfolding Sup_fin_def by (induct A set: finite)
@@ -2446,7 +2446,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
   by (induct rule: finite_ne_induct)
@@ -2457,7 +2457,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
   by (induct rule: finite_ne_induct)
@@ -2468,7 +2468,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
   by (induct rule: finite_ne_induct)
@@ -2481,7 +2481,7 @@
 proof cases
   assume "A = B" thus ?thesis by simp
 next
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   assume "A \<noteq> B"
   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
@@ -2515,7 +2515,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min (insert x A) = min x (Min A)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
 qed
@@ -2524,7 +2524,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Max (insert x A) = max x (Max A)"
 proof -
-  interpret ab_semigroup_idem_mult [max]
+  class_interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
 qed
@@ -2533,7 +2533,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<in> A"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
 qed
@@ -2542,7 +2542,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<in> A"
 proof -
-  interpret ab_semigroup_idem_mult [max]
+  class_interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
 qed
@@ -2551,7 +2551,7 @@
   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   shows "Min (A \<union> B) = min (Min A) (Min B)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
     by (simp add: Min_def fold1_Un2)
@@ -2561,7 +2561,7 @@
   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   shows "Max (A \<union> B) = max (Max A) (Max B)"
 proof -
-  interpret ab_semigroup_idem_mult [max]
+  class_interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms show ?thesis
     by (simp add: Max_def fold1_Un2)
@@ -2572,7 +2572,7 @@
     and "finite N" and "N \<noteq> {}"
   shows "h (Min N) = Min (h ` N)"
 proof -
-  interpret ab_semigroup_idem_mult [min]
+  class_interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
     by (simp add: Min_def hom_fold1_commute)
@@ -2583,7 +2583,7 @@
     and "finite N" and "N \<noteq> {}"
   shows "h (Max N) = Max (h ` N)"
 proof -
-  interpret ab_semigroup_idem_mult [max]
+  class_interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms show ?thesis
     by (simp add: Max_def hom_fold1_commute [of h])
@@ -2593,7 +2593,7 @@
   assumes "finite A" and "x \<in> A"
   shows "Min A \<le> x"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis by (simp add: Min_def fold1_belowI)
 qed
@@ -2611,7 +2611,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis by (simp add: Min_def below_fold1_iff)
 qed
@@ -2629,7 +2629,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
 qed
@@ -2639,7 +2639,7 @@
   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
 proof -
   note Max = Max_def
-  interpret linorder ["op \<ge>" "op >"]
+  class_interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max strict_below_fold1_iff [folded dual_max])
@@ -2649,7 +2649,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis
     by (simp add: Min_def fold1_below_iff)
@@ -2660,7 +2660,7 @@
   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
 proof -
   note Max = Max_def
-  interpret linorder ["op \<ge>" "op >"]
+  class_interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max fold1_below_iff [folded dual_max])
@@ -2670,7 +2670,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
 proof -
-  interpret lower_semilattice ["op \<le>" "op <" min]
+  class_interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis
     by (simp add: Min_def fold1_strict_below_iff)
@@ -2681,7 +2681,7 @@
   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
 proof -
   note Max = Max_def
-  interpret linorder ["op \<ge>" "op >"]
+  class_interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max fold1_strict_below_iff [folded dual_max])
@@ -2691,7 +2691,7 @@
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Min N \<le> Min M"
 proof -
-  interpret distrib_lattice ["op \<le>" "op <" min max]
+  class_interpret distrib_lattice ["op \<le>" "op <" min max]
     by (rule distrib_lattice_min_max)
   from assms show ?thesis by (simp add: Min_def fold1_antimono)
 qed
@@ -2701,7 +2701,7 @@
   shows "Max M \<le> Max N"
 proof -
   note Max = Max_def
-  interpret linorder ["op \<ge>" "op >"]
+  class_interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max fold1_antimono [folded dual_max])
diff -r 4025459e3f83 -r 5226d990d74b src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Groebner_Basis.thy
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -165,7 +164,7 @@
 end
 
 interpretation class_semiring: gb_semiring
-    ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
+    "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
   proof qed (auto simp add: ring_simps power_Suc)
 
 lemmas nat_arith =
@@ -242,8 +241,8 @@
 end
 
 
-interpretation class_ring: gb_ring ["op +" "op *" "op ^"
-    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
+interpretation class_ring: gb_ring "op +" "op *" "op ^"
+    "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
   proof qed simp_all
 
 
@@ -344,7 +343,7 @@
 qed
 
 interpretation class_ringb: ringb
-  ["op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"]
+  "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
 proof(unfold_locales, simp add: ring_simps power_Suc, auto)
   fix w x y z ::"'a::{idom,recpower,number_ring}"
   assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
@@ -360,7 +359,7 @@
 declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
 
 interpretation natgb: semiringb
-  ["op +" "op *" "op ^" "0::nat" "1"]
+  "op +" "op *" "op ^" "0::nat" "1"
 proof (unfold_locales, simp add: ring_simps power_Suc)
   fix w x y z ::"nat"
   { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
@@ -465,7 +464,7 @@
 subsection{* Groebner Bases for fields *}
 
 interpretation class_fieldgb:
-  fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse)
+  fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
 
 lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
 lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0"
diff -r 4025459e3f83 -r 5226d990d74b src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/HOL/Lattices.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -300,7 +300,7 @@
   by auto
 qed (auto simp add: min_def max_def not_le less_imp_le)
 
-interpretation min_max:
+class_interpretation min_max:
   distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
   by (rule distrib_lattice_min_max)
 
diff -r 4025459e3f83 -r 5226d990d74b src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/HOL/List.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -548,9 +548,9 @@
 lemma append_Nil2 [simp]: "xs @ [] = xs"
 by (induct xs) auto
 
-interpretation semigroup_append: semigroup_add ["op @"]
+class_interpretation semigroup_append: semigroup_add ["op @"]
   proof qed simp
-interpretation monoid_append: monoid_add ["[]" "op @"]
+class_interpretation monoid_append: monoid_add ["[]" "op @"]
   proof qed simp+
 
 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
diff -r 4025459e3f83 -r 5226d990d74b src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -433,8 +433,7 @@
 end
 
 
-interpretation dlo < dlat
-(* TODO: definition syntax is unavailable *)
+sublocale dlo < dlat
 proof
   fix x y
   from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
@@ -445,7 +444,7 @@
   then show "EX sup. is_sup x y sup" by blast
 qed
 
-interpretation dlo < ddlat
+sublocale dlo < ddlat
 proof
   fix x y z
   show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
diff -r 4025459e3f83 -r 5226d990d74b src/HOL/main.ML
--- a/src/HOL/main.ML	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/HOL/main.ML	Thu Dec 11 18:34:05 2008 +0100
@@ -4,4 +4,5 @@
 Classical Higher-order Logic -- only "Main".
 *)
 
+set new_locales;
 use_thy "Main";
diff -r 4025459e3f83 -r 5226d990d74b src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Dec 11 18:34:05 2008 +0100
@@ -53,8 +53,7 @@
   val print_configs: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
-  val print_locale: bool * (Locale.expr * Element.context list)
-    -> Toplevel.transition -> Toplevel.transition
+  val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
   val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_simpset: Toplevel.transition -> Toplevel.transition
@@ -354,11 +353,11 @@
 val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
 
 val print_locales = Toplevel.unknown_theory o
-  Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
+  Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of);
 
-fun print_locale (show_facts, (imports, body)) = Toplevel.unknown_theory o
+fun print_locale (show_facts, name) = Toplevel.unknown_theory o
   Toplevel.keep (fn state =>
-    Locale.print_locale (Toplevel.theory_of state) show_facts imports body);
+    NewLocale.print_locale (Toplevel.theory_of state) show_facts name);
 
 fun print_registrations show_wits name = Toplevel.unknown_context o
   Toplevel.keep (Toplevel.node_case
diff -r 4025459e3f83 -r 5226d990d74b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Dec 11 18:34:05 2008 +0100
@@ -385,18 +385,18 @@
 (* locales *)
 
 val locale_val =
-  SpecParse.locale_expr --
+  SpecParse.locale_expression --
     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
-  Scan.repeat1 SpecParse.context_element >> pair Locale.empty;
+  Scan.repeat1 SpecParse.context_element >> pair ([], []);
 
 val _ =
   OuterSyntax.command "locale" "define named proof context" K.thy_decl
-    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
+    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
-
-val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
+            (Expression.add_locale_cmd name name expr elems #>
+              (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |>
+                fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes))));
 
 val _ =
   OuterSyntax.command "sublocale"
@@ -407,6 +407,39 @@
 
 val _ =
   OuterSyntax.command "interpretation"
+    "prove interpretation of locale expression in theory" K.thy_goal
+    (P.!!! SpecParse.locale_expression
+        >> (fn expr => Toplevel.print o
+            Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
+
+val _ =
+  OuterSyntax.command "interpret"
+    "prove interpretation of locale expression in proof context"
+    (K.tag_proof K.prf_goal)
+    (P.!!! SpecParse.locale_expression
+        >> (fn expr => Toplevel.print o
+            Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
+
+local
+
+val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
+
+in
+
+val locale_val =
+  SpecParse.locale_expr --
+    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
+  Scan.repeat1 SpecParse.context_element >> pair Locale.empty;
+
+val _ =
+  OuterSyntax.command "class_locale" "define named proof context based on classes" K.thy_decl
+    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
+      >> (fn ((name, (expr, elems)), begin) =>
+          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
+            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
+
+val _ =
+  OuterSyntax.command "class_interpretation"
     "prove and register interpretation of locale expression in theory or locale" K.thy_goal
     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
       >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
@@ -416,7 +449,7 @@
               (Locale.interpretation_cmd (Binding.base_name name) expr insts)));
 
 val _ =
-  OuterSyntax.command "interpret"
+  OuterSyntax.command "class_interpret"
     "prove and register interpretation of locale expression in proof context"
     (K.tag_proof K.prf_goal)
     (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
@@ -424,6 +457,8 @@
           Toplevel.proof'
             (fn int => Locale.interpret_cmd (Binding.base_name name) expr insts int)));
 
+end;
+
 
 (* classes *)
 
@@ -817,7 +852,7 @@
 
 val _ =
   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
-    (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
+    (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
 
 val _ =
   OuterSyntax.improper_command "print_interps"
diff -r 4025459e3f83 -r 5226d990d74b src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Dec 11 18:34:05 2008 +0100
@@ -24,13 +24,20 @@
 
 (* new locales *)
 
-fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x;
-fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
-fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
-fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
-fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
-fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x;
-fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x;
+fun locale_extern is_class x = 
+  if !new_locales andalso not is_class then NewLocale.extern x else Locale.extern x;
+fun locale_add_type_syntax is_class x =
+  if !new_locales andalso not is_class then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
+fun locale_add_term_syntax is_class x =
+  if !new_locales andalso not is_class then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
+fun locale_add_declaration is_class x =
+  if !new_locales andalso not is_class then NewLocale.add_declaration x else Locale.add_declaration x;
+fun locale_add_thmss is_class x =
+  if !new_locales andalso not is_class then NewLocale.add_thmss x else Locale.add_thmss x;
+fun locale_init x =
+  if !new_locales then NewLocale.init x else Locale.init x;
+fun locale_intern is_class x =
+  if !new_locales andalso not is_class then NewLocale.intern x else Locale.intern x;
 
 (* context data *)
 
@@ -58,7 +65,7 @@
 fun pretty_thy ctxt target is_locale is_class =
   let
     val thy = ProofContext.theory_of ctxt;
-    val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
+    val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target;
     val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
       (#1 (ProofContext.inferred_fixes ctxt));
     val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
@@ -94,7 +101,7 @@
       |> LocalTheory.target (Context.proof_map d0)
     else
       lthy
-      |> LocalTheory.target (add target d')
+      |> LocalTheory.target (add is_class target d')
   end;
 
 val type_syntax = target_decl locale_add_type_syntax;
@@ -179,7 +186,7 @@
         #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
         #> Sign.restore_naming thy)
     |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
-    |> is_locale ? LocalTheory.target (locale_add_thmss target kind target_facts)
+    |> is_locale ? LocalTheory.target (locale_add_thmss is_class target kind target_facts)
     |> note_local kind local_facts
   end;
 
@@ -367,7 +374,8 @@
 fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
 
 fun context "-" thy = init NONE thy
-  | context target thy = init (SOME (locale_intern thy target)) thy;
+  | context target thy = init (SOME (locale_intern
+      (not (NewLocale.test_locale thy (NewLocale.intern thy target))) thy target)) thy;
 
 fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
 
diff -r 4025459e3f83 -r 5226d990d74b src/ZF/Constructible/L_axioms.thy
--- a/src/ZF/Constructible/L_axioms.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/ZF/Constructible/L_axioms.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Constructible/L_axioms.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
@@ -100,7 +99,7 @@
   apply (rule L_nat)
   done
 
-interpretation M_trivial ["L"] by (rule M_trivial_L)
+interpretation L: M_trivial L by (rule M_trivial_L)
 
 (* Replaces the following declarations...
 lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
diff -r 4025459e3f83 -r 5226d990d74b src/ZF/Constructible/Rec_Separation.thy
--- a/src/ZF/Constructible/Rec_Separation.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Constructible/Rec_Separation.thy
-    ID:   $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
@@ -186,7 +185,7 @@
 theorem M_trancl_L: "PROP M_trancl(L)"
 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
 
-interpretation M_trancl [L] by (rule M_trancl_L)
+interpretation L: M_trancl L by (rule M_trancl_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term list}*}
@@ -373,7 +372,7 @@
   apply (rule M_datatypes_axioms_L) 
   done
 
-interpretation M_datatypes [L] by (rule M_datatypes_L)
+interpretation L: M_datatypes L by (rule M_datatypes_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
@@ -436,7 +435,7 @@
   apply (rule M_eclose_axioms_L)
   done
 
-interpretation M_eclose [L] by (rule M_eclose_L)
+interpretation L: M_eclose L by (rule M_eclose_L)
 
 
 end
diff -r 4025459e3f83 -r 5226d990d74b src/ZF/Constructible/Separation.thy
--- a/src/ZF/Constructible/Separation.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/ZF/Constructible/Separation.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -305,7 +305,7 @@
 theorem M_basic_L: "PROP M_basic(L)"
 by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
 
-interpretation M_basic [L] by (rule M_basic_L)
+interpretation L: M_basic L by (rule M_basic_L)
 
 
 end
diff -r 4025459e3f83 -r 5226d990d74b src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/ZF/ROOT.ML	Thu Dec 11 18:34:05 2008 +0100
@@ -8,5 +8,6 @@
 Paulson.
 *)
 
+set new_locales;
 use_thys ["Main", "Main_ZFC"];
 
diff -r 4025459e3f83 -r 5226d990d74b src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/ZF/ex/Group.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -1,5 +1,4 @@
 (* Title:  ZF/ex/Group.thy
-  Id:     $Id$
 
 *)
 
@@ -40,7 +39,7 @@
   m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where
   "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>)"
 
-locale monoid = struct G +
+locale monoid = fixes G (structure)
   assumes m_closed [intro, simp]:
          "\<lbrakk>x \<in> carrier(G); y \<in> carrier(G)\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> carrier(G)"
       and m_assoc:
@@ -242,7 +241,7 @@
 
 subsection {* Substructures *}
 
-locale subgroup = var H + struct G + 
+locale subgroup = fixes H and G (structure)
   assumes subset: "H \<subseteq> carrier(G)"
     and m_closed [intro, simp]: "\<lbrakk>x \<in> H; y \<in> H\<rbrakk> \<Longrightarrow> x \<cdot> y \<in> H"
     and  one_closed [simp]: "\<one> \<in> H"
@@ -262,7 +261,7 @@
   assumes "group(G)"
   shows "group_axioms (update_carrier(G,H))"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis by (force intro: group_axioms.intro l_inv r_inv)
 qed
 
@@ -270,7 +269,7 @@
   assumes "group(G)"
   shows "group (update_carrier(G,H))"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis
   by (rule groupI) (auto intro: m_assoc l_inv mem_carrier)
 qed
@@ -316,8 +315,8 @@
   assumes "group(G)" and "group(H)"
   shows "group (G \<Otimes> H)"
 proof -
-  interpret G: group [G] by fact
-  interpret H: group [H] by fact
+  interpret G: group G by fact
+  interpret H: group H by fact
   show ?thesis by (force intro!: groupI G.m_assoc H.m_assoc G.l_inv H.l_inv
           simp add: DirProdGroup_def)
 qed
@@ -397,8 +396,8 @@
   assumes "group(G)" and "group(H)"
   shows "(\<lambda><x,y> \<in> carrier(G \<Otimes> H). <y,x>) \<in> (G \<Otimes> H) \<cong> (H \<Otimes> G)"
 proof -
-  interpret group [G] by fact
-  interpret group [H] by fact
+  interpret group G by fact
+  interpret group H by fact
   show ?thesis by (auto simp add: iso_def hom_def inj_def surj_def bij_def)
 qed
 
@@ -407,16 +406,17 @@
   shows "(\<lambda><<x,y>,z> \<in> carrier((G \<Otimes> H) \<Otimes> I). <x,<y,z>>)
           \<in> ((G \<Otimes> H) \<Otimes> I) \<cong> (G \<Otimes> (H \<Otimes> I))"
 proof -
-  interpret group [G] by fact
-  interpret group [H] by fact
-  interpret group [I] by fact
+  interpret group G by fact
+  interpret group H by fact
+  interpret group I by fact
   show ?thesis
     by (auto intro: lam_type simp add: iso_def hom_def inj_def surj_def bij_def) 
 qed
 
 text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   @term{H}, with a homomorphism @{term h} between them*}
-locale group_hom = group G + group H + var h +
+locale group_hom = G: group G + H: group H
+  for G (structure) and H (structure) and h +
   assumes homh: "h \<in> hom(G,H)"
   notes hom_mult [simp] = hom_mult [OF homh]
     and hom_closed [simp] = hom_closed [OF homh]
@@ -870,7 +870,7 @@
    assumes "group(G)"
    shows "equiv (carrier(G), rcong H)"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis proof (simp add: equiv_def, intro conjI)
     show "rcong H \<subseteq> carrier(G) \<times> carrier(G)"
       by (auto simp add: r_congruent_def) 
@@ -907,7 +907,7 @@
   assumes a: "a \<in> carrier(G)"
   shows "a <# H = (rcong H) `` {a}" 
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   show ?thesis
     by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a
       Collect_image_eq) 
@@ -920,7 +920,7 @@
         h \<in> H;  ha \<in> H;  hb \<in> H\<rbrakk>
       \<Longrightarrow> hb \<cdot> a \<in> (\<Union>h\<in>H. {h \<cdot> b})" (is "PROP ?P")
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show "PROP ?P"
     apply (rule UN_I [of "hb \<cdot> ((inv ha) \<cdot> h)"], simp)
     apply (simp add: m_assoc transpose_inv)
@@ -931,7 +931,7 @@
   assumes "subgroup(H, G)"
   shows "\<lbrakk>a \<in> rcosets H; b \<in> rcosets H; a\<noteq>b\<rbrakk> \<Longrightarrow> a \<inter> b = 0" (is "PROP ?P")
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show "PROP ?P"
     apply (simp add: RCOSETS_def r_coset_def)
     apply (blast intro: rcos_equation prems sym)
@@ -949,7 +949,7 @@
   assumes "subgroup(H, G)"
   shows "x \<in> carrier(G) \<Longrightarrow> x \<in> H #> x" (is "PROP ?P")
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show "PROP ?P"
     apply (simp add: r_coset_def)
     apply (rule_tac x="\<one>" in bexI) apply (auto)
@@ -960,7 +960,7 @@
   assumes "subgroup(H, G)"
   shows "\<Union>(rcosets H) = carrier(G)"
 proof -
-  interpret subgroup [H G] by fact
+  interpret subgroup H G by fact
   show ?thesis
     apply (rule equalityI)
     apply (force simp add: RCOSETS_def r_coset_def)
@@ -1044,7 +1044,7 @@
   assumes "group(G)"
   shows "H \<in> rcosets H"
 proof -
-  interpret group [G] by fact
+  interpret group G by fact
   have "H #> \<one> = H"
     using _ subgroup_axioms by (rule coset_join2) simp_all
   then show ?thesis
diff -r 4025459e3f83 -r 5226d990d74b src/ZF/ex/Ring.thy
--- a/src/ZF/ex/Ring.thy	Thu Dec 11 17:56:34 2008 +0100
+++ b/src/ZF/ex/Ring.thy	Thu Dec 11 18:34:05 2008 +0100
@@ -45,7 +45,7 @@
   minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65) where
   "\<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)"
 
-locale abelian_monoid = struct G +
+locale abelian_monoid = fixes G (structure)
   assumes a_comm_monoid: 
     "comm_monoid (<carrier(G), add_field(G), zero(G), 0>)"
 
@@ -57,7 +57,7 @@
   assumes a_comm_group: 
     "comm_group (<carrier(G), add_field(G), zero(G), 0>)"
 
-locale ring = abelian_group R + monoid R +
+locale ring = abelian_group R + monoid R for R (structure) +
   assumes l_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
       \<Longrightarrow> (x \<oplus> y) \<cdot> z = x \<cdot> z \<oplus> y \<cdot> z"
     and r_distr: "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R); z \<in> carrier(R)\<rbrakk>
@@ -262,7 +262,8 @@
 lemma ring_hom_one: "h \<in> ring_hom(R,S) \<Longrightarrow> h ` \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>"
 by (simp add: ring_hom_def)
 
-locale ring_hom_cring = cring R + cring S + var h +
+locale ring_hom_cring = R: cring R + S: cring S
+  for R (structure) and S (structure) and h +
   assumes homh [simp, intro]: "h \<in> ring_hom(R,S)"
   notes hom_closed [simp, intro] = ring_hom_closed [OF homh]
     and hom_mult [simp] = ring_hom_mult [OF homh]