locale predicates of classes carry a mandatory "class" prefix
authorhaftmann
Tue May 04 08:55:43 2010 +0200 (2010-05-04)
changeset 36635080b755377c0
parent 36634 f9b43d197d16
child 36636 7dded80a953f
child 36637 74a5c04bf29d
locale predicates of classes carry a mandatory "class" prefix
src/HOL/Bali/TypeSafe.thy
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattice.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Finite_Set.thy
src/HOL/HOL.thy
src/HOL/Lattices.thy
src/HOL/Library/Multiset.thy
src/HOL/Orderings.thy
src/HOL/Wellfounded.thy
src/HOL/Word/WordArith.thy
src/HOL/ex/Landau.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
src/Pure/Isar/class.ML
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Tue May 04 08:55:39 2010 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Tue May 04 08:55:43 2010 +0200
     1.3 @@ -9,8 +9,6 @@
     1.4  
     1.5  section "error free"
     1.6   
     1.7 -hide_const field
     1.8 -
     1.9  lemma error_free_halloc:
    1.10    assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
    1.11            error_free_s0: "error_free s0"
     2.1 --- a/src/HOL/Big_Operators.thy	Tue May 04 08:55:39 2010 +0200
     2.2 +++ b/src/HOL/Big_Operators.thy	Tue May 04 08:55:43 2010 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4  text {* for ad-hoc proofs for @{const fold_image} *}
     2.5  
     2.6  lemma (in comm_monoid_add) comm_monoid_mult:
     2.7 -  "comm_monoid_mult (op +) 0"
     2.8 +  "class.comm_monoid_mult (op +) 0"
     2.9  proof qed (auto intro: add_assoc add_commute)
    2.10  
    2.11  notation times (infixl "*" 70)
    2.12 @@ -1200,7 +1200,8 @@
    2.13  context semilattice_inf
    2.14  begin
    2.15  
    2.16 -lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
    2.17 +lemma ab_semigroup_idem_mult_inf:
    2.18 +  "class.ab_semigroup_idem_mult inf"
    2.19  proof qed (rule inf_assoc inf_commute inf_idem)+
    2.20  
    2.21  lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
    2.22 @@ -1270,7 +1271,7 @@
    2.23  context semilattice_sup
    2.24  begin
    2.25  
    2.26 -lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
    2.27 +lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
    2.28  by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
    2.29  
    2.30  lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
    2.31 @@ -1490,15 +1491,15 @@
    2.32    using assms by (rule Max.hom_commute)
    2.33  
    2.34  lemma ab_semigroup_idem_mult_min:
    2.35 -  "ab_semigroup_idem_mult min"
    2.36 +  "class.ab_semigroup_idem_mult min"
    2.37    proof qed (auto simp add: min_def)
    2.38  
    2.39  lemma ab_semigroup_idem_mult_max:
    2.40 -  "ab_semigroup_idem_mult max"
    2.41 +  "class.ab_semigroup_idem_mult max"
    2.42    proof qed (auto simp add: max_def)
    2.43  
    2.44  lemma max_lattice:
    2.45 -  "semilattice_inf (op \<ge>) (op >) max"
    2.46 +  "class.semilattice_inf (op \<ge>) (op >) max"
    2.47    by (fact min_max.dual_semilattice)
    2.48  
    2.49  lemma dual_max:
     3.1 --- a/src/HOL/Complete_Lattice.thy	Tue May 04 08:55:39 2010 +0200
     3.2 +++ b/src/HOL/Complete_Lattice.thy	Tue May 04 08:55:43 2010 +0200
     3.3 @@ -33,8 +33,8 @@
     3.4  begin
     3.5  
     3.6  lemma dual_complete_lattice:
     3.7 -  "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
     3.8 -  by (auto intro!: complete_lattice.intro dual_bounded_lattice)
     3.9 +  "class.complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    3.10 +  by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
    3.11      (unfold_locales, (fact bot_least top_greatest
    3.12          Sup_upper Sup_least Inf_lower Inf_greatest)+)
    3.13  
     4.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 04 08:55:39 2010 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Tue May 04 08:55:43 2010 +0200
     4.3 @@ -265,7 +265,7 @@
     4.4  lemmas dlo_simps[no_atp] = order_refl less_irrefl not_less not_le exists_neq 
     4.5    le_less neq_iff linear less_not_permute
     4.6  
     4.7 -lemma axiom[no_atp]: "dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
     4.8 +lemma axiom[no_atp]: "class.dense_linorder (op \<le>) (op <)" by (rule dense_linorder_axioms)
     4.9  lemma atoms[no_atp]:
    4.10    shows "TERM (less :: 'a \<Rightarrow> _)"
    4.11      and "TERM (less_eq :: 'a \<Rightarrow> _)"
     5.1 --- a/src/HOL/Finite_Set.thy	Tue May 04 08:55:39 2010 +0200
     5.2 +++ b/src/HOL/Finite_Set.thy	Tue May 04 08:55:43 2010 +0200
     5.3 @@ -509,13 +509,8 @@
     5.4  
     5.5  subsection {* Class @{text finite}  *}
     5.6  
     5.7 -setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
     5.8  class finite =
     5.9    assumes finite_UNIV: "finite (UNIV \<Colon> 'a set)"
    5.10 -setup {* Sign.parent_path *}
    5.11 -hide_const finite
    5.12 -
    5.13 -context finite
    5.14  begin
    5.15  
    5.16  lemma finite [simp]: "finite (A \<Colon> 'a set)"
     6.1 --- a/src/HOL/HOL.thy	Tue May 04 08:55:39 2010 +0200
     6.2 +++ b/src/HOL/HOL.thy	Tue May 04 08:55:43 2010 +0200
     6.3 @@ -1886,7 +1886,6 @@
     6.4  *}
     6.5  
     6.6  hide_const (open) eq
     6.7 -hide_const eq
     6.8  
     6.9  text {* Cases *}
    6.10  
     7.1 --- a/src/HOL/Lattices.thy	Tue May 04 08:55:39 2010 +0200
     7.2 +++ b/src/HOL/Lattices.thy	Tue May 04 08:55:43 2010 +0200
     7.3 @@ -67,8 +67,8 @@
     7.4  text {* Dual lattice *}
     7.5  
     7.6  lemma dual_semilattice:
     7.7 -  "semilattice_inf (op \<ge>) (op >) sup"
     7.8 -by (rule semilattice_inf.intro, rule dual_order)
     7.9 +  "class.semilattice_inf (op \<ge>) (op >) sup"
    7.10 +by (rule class.semilattice_inf.intro, rule dual_order)
    7.11    (unfold_locales, simp_all add: sup_least)
    7.12  
    7.13  end
    7.14 @@ -235,8 +235,8 @@
    7.15  begin
    7.16  
    7.17  lemma dual_lattice:
    7.18 -  "lattice (op \<ge>) (op >) sup inf"
    7.19 -  by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
    7.20 +  "class.lattice (op \<ge>) (op >) sup inf"
    7.21 +  by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
    7.22      (unfold_locales, auto)
    7.23  
    7.24  lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
    7.25 @@ -347,8 +347,8 @@
    7.26  by(simp add: inf_sup_aci inf_sup_distrib1)
    7.27  
    7.28  lemma dual_distrib_lattice:
    7.29 -  "distrib_lattice (op \<ge>) (op >) sup inf"
    7.30 -  by (rule distrib_lattice.intro, rule dual_lattice)
    7.31 +  "class.distrib_lattice (op \<ge>) (op >) sup inf"
    7.32 +  by (rule class.distrib_lattice.intro, rule dual_lattice)
    7.33      (unfold_locales, fact inf_sup_distrib1)
    7.34  
    7.35  lemmas sup_inf_distrib =
    7.36 @@ -419,7 +419,7 @@
    7.37  begin
    7.38  
    7.39  lemma dual_bounded_lattice:
    7.40 -  "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    7.41 +  "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    7.42    by unfold_locales (auto simp add: less_le_not_le)
    7.43  
    7.44  end
    7.45 @@ -431,8 +431,8 @@
    7.46  begin
    7.47  
    7.48  lemma dual_boolean_algebra:
    7.49 -  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    7.50 -  by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    7.51 +  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    7.52 +  by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    7.53      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    7.54  
    7.55  lemma compl_inf_bot:
     8.1 --- a/src/HOL/Library/Multiset.thy	Tue May 04 08:55:39 2010 +0200
     8.2 +++ b/src/HOL/Library/Multiset.thy	Tue May 04 08:55:43 2010 +0200
     8.3 @@ -1239,7 +1239,7 @@
     8.4    qed
     8.5    have trans: "\<And>K M N :: 'a multiset. K \<subset># M \<Longrightarrow> M \<subset># N \<Longrightarrow> K \<subset># N"
     8.6      unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
     8.7 -  show "order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
     8.8 +  show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset" proof
     8.9    qed (auto simp add: le_multiset_def irrefl dest: trans)
    8.10  qed
    8.11  
     9.1 --- a/src/HOL/Orderings.thy	Tue May 04 08:55:39 2010 +0200
     9.2 +++ b/src/HOL/Orderings.thy	Tue May 04 08:55:43 2010 +0200
     9.3 @@ -106,7 +106,7 @@
     9.4  text {* Dual order *}
     9.5  
     9.6  lemma dual_preorder:
     9.7 -  "preorder (op \<ge>) (op >)"
     9.8 +  "class.preorder (op \<ge>) (op >)"
     9.9  proof qed (auto simp add: less_le_not_le intro: order_trans)
    9.10  
    9.11  end
    9.12 @@ -186,7 +186,7 @@
    9.13  text {* Dual order *}
    9.14  
    9.15  lemma dual_order:
    9.16 -  "order (op \<ge>) (op >)"
    9.17 +  "class.order (op \<ge>) (op >)"
    9.18  by (intro_locales, rule dual_preorder) (unfold_locales, rule antisym)
    9.19  
    9.20  end
    9.21 @@ -257,8 +257,8 @@
    9.22  text {* Dual order *}
    9.23  
    9.24  lemma dual_linorder:
    9.25 -  "linorder (op \<ge>) (op >)"
    9.26 -by (rule linorder.intro, rule dual_order) (unfold_locales, rule linear)
    9.27 +  "class.linorder (op \<ge>) (op >)"
    9.28 +by (rule class.linorder.intro, rule dual_order) (unfold_locales, rule linear)
    9.29  
    9.30  
    9.31  text {* min/max *}
    10.1 --- a/src/HOL/Wellfounded.thy	Tue May 04 08:55:39 2010 +0200
    10.2 +++ b/src/HOL/Wellfounded.thy	Tue May 04 08:55:43 2010 +0200
    10.3 @@ -68,7 +68,7 @@
    10.4    assumes lin: "OFCLASS('a::ord, linorder_class)"
    10.5    shows "OFCLASS('a::ord, wellorder_class)"
    10.6  using lin by (rule wellorder_class.intro)
    10.7 -  (blast intro: wellorder_axioms.intro wf_induct_rule [OF wf])
    10.8 +  (blast intro: class.wellorder_axioms.intro wf_induct_rule [OF wf])
    10.9  
   10.10  lemma (in wellorder) wf:
   10.11    "wf {(x, y). x < y}"
    11.1 --- a/src/HOL/Word/WordArith.thy	Tue May 04 08:55:39 2010 +0200
    11.2 +++ b/src/HOL/Word/WordArith.thy	Tue May 04 08:55:43 2010 +0200
    11.3 @@ -17,7 +17,7 @@
    11.4    by (auto simp del: word_uint.Rep_inject 
    11.5             simp: word_uint.Rep_inject [symmetric])
    11.6  
    11.7 -lemma signed_linorder: "linorder word_sle word_sless"
    11.8 +lemma signed_linorder: "class.linorder word_sle word_sless"
    11.9  proof
   11.10  qed (unfold word_sle_def word_sless_def, auto)
   11.11  
    12.1 --- a/src/HOL/ex/Landau.thy	Tue May 04 08:55:39 2010 +0200
    12.2 +++ b/src/HOL/ex/Landau.thy	Tue May 04 08:55:43 2010 +0200
    12.3 @@ -187,7 +187,7 @@
    12.4  proof -
    12.5    interpret preorder_equiv less_eq_fun less_fun proof
    12.6    qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
    12.7 -  show "preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
    12.8 +  show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
    12.9    show "preorder_equiv.equiv less_eq_fun = equiv_fun"
   12.10      by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
   12.11  qed
    13.1 --- a/src/HOLCF/CompactBasis.thy	Tue May 04 08:55:39 2010 +0200
    13.2 +++ b/src/HOLCF/CompactBasis.thy	Tue May 04 08:55:43 2010 +0200
    13.3 @@ -237,12 +237,12 @@
    13.4    where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
    13.5  
    13.6  lemma fold_pd_PDUnit:
    13.7 -  assumes "ab_semigroup_idem_mult f"
    13.8 +  assumes "class.ab_semigroup_idem_mult f"
    13.9    shows "fold_pd g f (PDUnit x) = g x"
   13.10  unfolding fold_pd_def Rep_PDUnit by simp
   13.11  
   13.12  lemma fold_pd_PDPlus:
   13.13 -  assumes "ab_semigroup_idem_mult f"
   13.14 +  assumes "class.ab_semigroup_idem_mult f"
   13.15    shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
   13.16  proof -
   13.17    interpret ab_semigroup_idem_mult f by fact
    14.1 --- a/src/HOLCF/ConvexPD.thy	Tue May 04 08:55:39 2010 +0200
    14.2 +++ b/src/HOLCF/ConvexPD.thy	Tue May 04 08:55:43 2010 +0200
    14.3 @@ -412,7 +412,7 @@
    14.4      (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
    14.5  
    14.6  lemma ACI_convex_bind:
    14.7 -  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
    14.8 +  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<natural> y\<cdot>f)"
    14.9  apply unfold_locales
   14.10  apply (simp add: convex_plus_assoc)
   14.11  apply (simp add: convex_plus_commute)
    15.1 --- a/src/HOLCF/LowerPD.thy	Tue May 04 08:55:39 2010 +0200
    15.2 +++ b/src/HOLCF/LowerPD.thy	Tue May 04 08:55:43 2010 +0200
    15.3 @@ -393,7 +393,7 @@
    15.4      (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
    15.5  
    15.6  lemma ACI_lower_bind:
    15.7 -  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
    15.8 +  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<flat> y\<cdot>f)"
    15.9  apply unfold_locales
   15.10  apply (simp add: lower_plus_assoc)
   15.11  apply (simp add: lower_plus_commute)
    16.1 --- a/src/HOLCF/UpperPD.thy	Tue May 04 08:55:39 2010 +0200
    16.2 +++ b/src/HOLCF/UpperPD.thy	Tue May 04 08:55:43 2010 +0200
    16.3 @@ -388,7 +388,7 @@
    16.4      (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
    16.5  
    16.6  lemma ACI_upper_bind:
    16.7 -  "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
    16.8 +  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)"
    16.9  apply unfold_locales
   16.10  apply (simp add: upper_plus_assoc)
   16.11  apply (simp add: upper_plus_commute)
    17.1 --- a/src/Pure/Isar/class.ML	Tue May 04 08:55:39 2010 +0200
    17.2 +++ b/src/Pure/Isar/class.ML	Tue May 04 08:55:43 2010 +0200
    17.3 @@ -276,16 +276,16 @@
    17.4      #> pair (param_map, params, assm_axiom)))
    17.5    end;
    17.6  
    17.7 -fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
    17.8 +fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
    17.9    let
   17.10 -    val class = Sign.full_name thy bname;
   17.11 +    val class = Sign.full_name thy b;
   17.12      val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
   17.13        prep_class_spec thy raw_supclasses raw_elems;
   17.14    in
   17.15      thy
   17.16 -    |> Expression.add_locale bname Binding.empty supexpr elems
   17.17 +    |> Expression.add_locale b (Binding.qualify true "class" b) supexpr elems
   17.18      |> snd |> Local_Theory.exit_global
   17.19 -    |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
   17.20 +    |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
   17.21      ||> Theory.checkpoint
   17.22      |-> (fn (param_map, params, assm_axiom) =>
   17.23         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)