# HG changeset patch
# User haftmann
# Date 1272956143 -7200
# Node ID 080b755377c0c8738a8456930a67bcf7010a69e1
# Parent  f9b43d197d16b2255116693fcef13ee4e08ae551
locale predicates of classes carry a mandatory "class" prefix

diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Tue May 04 08:55:43 2010 +0200
@@ -9,8 +9,6 @@
 
 section "error free"
  
-hide_const field
-
 lemma error_free_halloc:
   assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
           error_free_s0: "error_free s0"
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Big_Operators.thy	Tue May 04 08:55:43 2010 +0200
@@ -33,7 +33,7 @@
 text {* for ad-hoc proofs for @{const fold_image} *}
 
 lemma (in comm_monoid_add) comm_monoid_mult:
-  "comm_monoid_mult (op +) 0"
+  "class.comm_monoid_mult (op +) 0"
 proof qed (auto intro: add_assoc add_commute)
 
 notation times (infixl "*" 70)
@@ -1200,7 +1200,8 @@
 context semilattice_inf
 begin
 
-lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
+lemma ab_semigroup_idem_mult_inf:
+  "class.ab_semigroup_idem_mult inf"
 proof qed (rule inf_assoc inf_commute inf_idem)+
 
 lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
@@ -1270,7 +1271,7 @@
 context semilattice_sup
 begin
 
-lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
+lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
 by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
 
 lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
@@ -1490,15 +1491,15 @@
   using assms by (rule Max.hom_commute)
 
 lemma ab_semigroup_idem_mult_min:
-  "ab_semigroup_idem_mult min"
+  "class.ab_semigroup_idem_mult min"
   proof qed (auto simp add: min_def)
 
 lemma ab_semigroup_idem_mult_max:
-  "ab_semigroup_idem_mult max"
+  "class.ab_semigroup_idem_mult max"
   proof qed (auto simp add: max_def)
 
 lemma max_lattice:
-  "semilattice_inf (op \<ge>) (op >) max"
+  "class.semilattice_inf (op \<ge>) (op >) max"
   by (fact min_max.dual_semilattice)
 
 lemma dual_max:
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy	Tue May 04 08:55:43 2010 +0200
@@ -33,8 +33,8 @@
 begin
 
 lemma dual_complete_lattice:
-  "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
-  by (auto intro!: complete_lattice.intro dual_bounded_lattice)
+  "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
     (unfold_locales, (fact bot_least top_greatest
         Sup_upper Sup_least Inf_lower Inf_greatest)+)
 
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 04 08:55:43 2010 +0200
@@ -265,7 +265,7 @@
 lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq 
   le_less neq_iff linear less_not_permute
 
-lemma axiom[no_atp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
+lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
 lemma atoms[no_atp]:
   shows "TERM (less :: 'a \<Rightarrow> _)"
     and "TERM (less_eq :: 'a \<Rightarrow> _)"
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Finite_Set.thy	Tue May 04 08:55:43 2010 +0200
@@ -509,13 +509,8 @@
 
 subsection {* Class @{text finite}  *}
 
-setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
 class finite =
   assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
-setup {* Sign.parent_path *}
-hide_const finite
-
-context finite
 begin
 
 lemma finite [simp]: "finite (A \<Colon> 'a set)"
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/HOL.thy	Tue May 04 08:55:43 2010 +0200
@@ -1886,7 +1886,6 @@
 *}
 
 hide_const (open) eq
-hide_const eq
 
 text {* Cases *}
 
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Lattices.thy	Tue May 04 08:55:43 2010 +0200
@@ -67,8 +67,8 @@
 text {* Dual lattice *}
 
 lemma dual_semilattice:
-  "semilattice_inf (op \<ge>) (op >) sup"
-by (rule semilattice_inf.intro, rule dual_order)
+  "class.semilattice_inf (op \<ge>) (op >) sup"
+by (rule class.semilattice_inf.intro, rule dual_order)
   (unfold_locales, simp_all add: sup_least)
 
 end
@@ -235,8 +235,8 @@
 begin
 
 lemma dual_lattice:
-  "lattice (op \<ge>) (op >) sup inf"
-  by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
+  "class.lattice (op \<ge>) (op >) sup inf"
+  by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
     (unfold_locales, auto)
 
 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
@@ -347,8 +347,8 @@
 by(simp add: inf_sup_aci inf_sup_distrib1)
 
 lemma dual_distrib_lattice:
-  "distrib_lattice (op \<ge>) (op >) sup inf"
-  by (rule distrib_lattice.intro, rule dual_lattice)
+  "class.distrib_lattice (op \<ge>) (op >) sup inf"
+  by (rule class.distrib_lattice.intro, rule dual_lattice)
     (unfold_locales, fact inf_sup_distrib1)
 
 lemmas sup_inf_distrib =
@@ -419,7 +419,7 @@
 begin
 
 lemma dual_bounded_lattice:
-  "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
   by unfold_locales (auto simp add: less_le_not_le)
 
 end
@@ -431,8 +431,8 @@
 begin
 
 lemma dual_boolean_algebra:
-  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
-  by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
+  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
     (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
 
 lemma compl_inf_bot:
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue May 04 08:55:43 2010 +0200
@@ -1239,7 +1239,7 @@
   qed
   have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
     unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
-  show "order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
+  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
   qed (auto simp add: le_multiset_def irrefl dest: trans)
 qed
 
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Orderings.thy	Tue May 04 08:55:43 2010 +0200
@@ -106,7 +106,7 @@
 text {* Dual order *}
 
 lemma dual_preorder:
-  "preorder (op \<ge>) (op >)"
+  "class.preorder (op \<ge>) (op >)"
 proof qed (auto simp add: less_le_not_le intro: order_trans)
 
 end
@@ -186,7 +186,7 @@
 text {* Dual order *}
 
 lemma dual_order:
-  "order (op \<ge>) (op >)"
+  "class.order (op \<ge>) (op >)"
 by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
 
 end
@@ -257,8 +257,8 @@
 text {* Dual order *}
 
 lemma dual_linorder:
-  "linorder (op \<ge>) (op >)"
-by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
+  "class.linorder (op \<ge>) (op >)"
+by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
 
 
 text {* min/max *}
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Wellfounded.thy	Tue May 04 08:55:43 2010 +0200
@@ -68,7 +68,7 @@
   assumes lin: "OFCLASS('a::ord, linorder_class)"
   shows "OFCLASS('a::ord, wellorder_class)"
 using lin by (rule wellorder_class.intro)
-  (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
+  (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
 
 lemma (in wellorder) wf:
   "wf {(x, y). x < y}"
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Word/WordArith.thy	Tue May 04 08:55:43 2010 +0200
@@ -17,7 +17,7 @@
   by (auto simp del: word_uint.Rep_inject 
            simp: word_uint.Rep_inject [symmetric])
 
-lemma signed_linorder: "linorder word_sle word_sless"
+lemma signed_linorder: "class.linorder word_sle word_sless"
 proof
 qed (unfold word_sle_def word_sless_def, auto)
 
diff -r f9b43d197d16 -r 080b755377c0 src/HOL/ex/Landau.thy
--- a/src/HOL/ex/Landau.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/ex/Landau.thy	Tue May 04 08:55:43 2010 +0200
@@ -187,7 +187,7 @@
 proof -
   interpret preorder_equiv less_eq_fun less_fun proof
   qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
-  show "preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
+  show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
   show "preorder_equiv.equiv less_eq_fun = equiv_fun"
     by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
 qed
diff -r f9b43d197d16 -r 080b755377c0 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOLCF/CompactBasis.thy	Tue May 04 08:55:43 2010 +0200
@@ -237,12 +237,12 @@
   where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
 
 lemma fold_pd_PDUnit:
-  assumes "ab_semigroup_idem_mult f"
+  assumes "class.ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDUnit x) = g x"
 unfolding fold_pd_def Rep_PDUnit by simp
 
 lemma fold_pd_PDPlus:
-  assumes "ab_semigroup_idem_mult f"
+  assumes "class.ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
 proof -
   interpret ab_semigroup_idem_mult f by fact
diff -r f9b43d197d16 -r 080b755377c0 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOLCF/ConvexPD.thy	Tue May 04 08:55:43 2010 +0200
@@ -412,7 +412,7 @@
     (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
 
 lemma ACI_convex_bind:
-  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: convex_plus_assoc)
 apply (simp add: convex_plus_commute)
diff -r f9b43d197d16 -r 080b755377c0 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOLCF/LowerPD.thy	Tue May 04 08:55:43 2010 +0200
@@ -393,7 +393,7 @@
     (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
 
 lemma ACI_lower_bind:
-  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: lower_plus_assoc)
 apply (simp add: lower_plus_commute)
diff -r f9b43d197d16 -r 080b755377c0 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOLCF/UpperPD.thy	Tue May 04 08:55:43 2010 +0200
@@ -388,7 +388,7 @@
     (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
 
 lemma ACI_upper_bind:
-  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
+  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
 apply unfold_locales
 apply (simp add: upper_plus_assoc)
 apply (simp add: upper_plus_commute)
diff -r f9b43d197d16 -r 080b755377c0 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue May 04 08:55:39 2010 +0200
+++ b/src/Pure/Isar/class.ML	Tue May 04 08:55:43 2010 +0200
@@ -276,16 +276,16 @@
     #> pair (param_map, params, assm_axiom)))
   end;
 
-fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
   let
-    val class = Sign.full_name thy bname;
+    val class = Sign.full_name thy b;
     val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
       prep_class_spec thy raw_supclasses raw_elems;
   in
     thy
-    |> Expression.add_locale bname Binding.empty supexpr elems
+    |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
     |> snd |> Local_Theory.exit_global
-    |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
+    |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
     ||> Theory.checkpoint
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)