no special treatment in naming of locale predicates stemming form classes
authorhaftmann
Sat May 19 11:33:22 2007 +0200 (2007-05-19)
changeset 230181d29bc31b0cb
parent 23017 00c0e4c42396
child 23019 019d44d46834
no special treatment in naming of locale predicates stemming form classes
src/HOL/Finite_Set.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
src/Pure/Tools/class_package.ML
     1.1 --- a/src/HOL/Finite_Set.thy	Sat May 19 11:33:21 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Sat May 19 11:33:22 2007 +0200
     1.3 @@ -2432,53 +2432,53 @@
     1.4  
     1.5  lemma ACIf_min: "ACIf min"
     1.6    by (rule lower_semilattice.ACIf_inf,
     1.7 -    rule lattice_pred.axioms,
     1.8 -    rule distrib_lattice_pred.axioms,
     1.9 +    rule lattice.axioms,
    1.10 +    rule distrib_lattice.axioms,
    1.11      rule distrib_lattice_min_max)
    1.12  
    1.13  lemma ACf_min: "ACf min"
    1.14    by (rule lower_semilattice.ACf_inf,
    1.15 -    rule lattice_pred.axioms,
    1.16 -    rule distrib_lattice_pred.axioms,
    1.17 +    rule lattice.axioms,
    1.18 +    rule distrib_lattice.axioms,
    1.19      rule distrib_lattice_min_max)
    1.20  
    1.21  lemma ACIfSL_min: "ACIfSL (op \<^loc>\<le>) (op \<^loc><) min"
    1.22    by (rule lower_semilattice.ACIfSL_inf,
    1.23 -    rule lattice_pred.axioms,
    1.24 -    rule distrib_lattice_pred.axioms,
    1.25 +    rule lattice.axioms,
    1.26 +    rule distrib_lattice.axioms,
    1.27      rule distrib_lattice_min_max)
    1.28  
    1.29  lemma ACIfSLlin_min: "ACIfSLlin (op \<^loc>\<le>) (op \<^loc><) min"
    1.30    by (rule ACIfSLlin.intro,
    1.31      rule lower_semilattice.ACIfSL_inf,
    1.32 -    rule lattice_pred.axioms,
    1.33 -    rule distrib_lattice_pred.axioms,
    1.34 +    rule lattice.axioms,
    1.35 +    rule distrib_lattice.axioms,
    1.36      rule distrib_lattice_min_max)
    1.37      (unfold_locales, simp add: min_def)
    1.38  
    1.39  lemma ACIf_max: "ACIf max"
    1.40    by (rule upper_semilattice.ACIf_sup,
    1.41 -    rule lattice_pred.axioms,
    1.42 -    rule distrib_lattice_pred.axioms,
    1.43 +    rule lattice.axioms,
    1.44 +    rule distrib_lattice.axioms,
    1.45      rule distrib_lattice_min_max)
    1.46  
    1.47  lemma ACf_max: "ACf max"
    1.48    by (rule upper_semilattice.ACf_sup,
    1.49 -    rule lattice_pred.axioms,
    1.50 -    rule distrib_lattice_pred.axioms,
    1.51 +    rule lattice.axioms,
    1.52 +    rule distrib_lattice.axioms,
    1.53      rule distrib_lattice_min_max)
    1.54  
    1.55  lemma ACIfSL_max: "ACIfSL (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
    1.56    by (rule upper_semilattice.ACIfSL_sup,
    1.57 -    rule lattice_pred.axioms,
    1.58 -    rule distrib_lattice_pred.axioms,
    1.59 +    rule lattice.axioms,
    1.60 +    rule distrib_lattice.axioms,
    1.61      rule distrib_lattice_min_max)
    1.62  
    1.63  lemma ACIfSLlin_max: "ACIfSLlin (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
    1.64    by (rule ACIfSLlin.intro,
    1.65      rule upper_semilattice.ACIfSL_sup,
    1.66 -    rule lattice_pred.axioms,
    1.67 -    rule distrib_lattice_pred.axioms,
    1.68 +    rule lattice.axioms,
    1.69 +    rule distrib_lattice.axioms,
    1.70      rule distrib_lattice_min_max)
    1.71      (unfold_locales, simp add: max_def)
    1.72  
    1.73 @@ -2601,7 +2601,7 @@
    1.74  proof
    1.75    fix A :: "'a set"
    1.76    show "Linorder.Min (op \<le>) A = Min A"
    1.77 -  by (simp add: Min_def Linorder.Min_def [OF Linorder.intro, OF linorder_pred_axioms]
    1.78 +  by (simp add: Min_def Linorder.Min_def [OF Linorder.intro, OF linorder_axioms]
    1.79      linorder_class_min)
    1.80  qed
    1.81  
    1.82 @@ -2610,19 +2610,19 @@
    1.83  proof
    1.84    fix A :: "'a set"
    1.85    show "Linorder.Max (op \<le>) A = Max A"
    1.86 -  by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_pred_axioms]
    1.87 +  by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_axioms]
    1.88      linorder_class_max)
    1.89  qed
    1.90  
    1.91  interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
    1.92    Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"]
    1.93    by (rule Linorder_ab_semigroup_add.intro,
    1.94 -    rule Linorder.intro, rule linorder_pred_axioms, rule pordered_ab_semigroup_add_pred_axioms)
    1.95 +    rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms)
    1.96  hide const Min Max
    1.97  
    1.98  interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
    1.99    Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"]
   1.100 -  by (rule Linorder.intro, rule linorder_pred_axioms)
   1.101 +  by (rule Linorder.intro, rule linorder_axioms)
   1.102  declare Min_singleton [simp]
   1.103  declare Max_singleton [simp]
   1.104  declare Min_insert [simp]
   1.105 @@ -2640,8 +2640,11 @@
   1.106  
   1.107  subsection {* Class @{text finite} *}
   1.108  
   1.109 +setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
   1.110  class finite (attach UNIV) = type +
   1.111    assumes finite: "finite UNIV"
   1.112 +setup {* Sign.parent_path *}
   1.113 +hide const finite
   1.114  
   1.115  lemma finite_set: "finite (A::'a::finite set)"
   1.116    by (rule finite_subset [OF subset_UNIV finite])
     2.1 --- a/src/HOL/Lattices.thy	Sat May 19 11:33:21 2007 +0200
     2.2 +++ b/src/HOL/Lattices.thy	Sat May 19 11:33:22 2007 +0200
     2.3 @@ -282,7 +282,7 @@
     2.4    special case of @{const inf}/@{const sup} *}
     2.5  
     2.6  lemma (in linorder) distrib_lattice_min_max:
     2.7 -  "distrib_lattice_pred (op \<^loc>\<le>) (op \<^loc><) min max"
     2.8 +  "distrib_lattice (op \<^loc>\<le>) (op \<^loc><) min max"
     2.9  proof unfold_locales
    2.10    have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
    2.11      by (auto simp add: less_le antisym)
     3.1 --- a/src/HOL/Orderings.thy	Sat May 19 11:33:21 2007 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Sat May 19 11:33:22 2007 +0200
     3.3 @@ -199,7 +199,7 @@
     3.4  text {* Reverse order *}
     3.5  
     3.6  lemma order_reverse:
     3.7 -  "order_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
     3.8 +  "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
     3.9    by unfold_locales
    3.10      (simp add: less_le, auto intro: antisym order_trans)
    3.11  
    3.12 @@ -266,7 +266,7 @@
    3.13  text {* Reverse order *}
    3.14  
    3.15  lemma linorder_reverse:
    3.16 -  "linorder_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
    3.17 +  "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
    3.18    by unfold_locales
    3.19      (simp add: less_le, auto intro: antisym order_trans simp add: linear)
    3.20  
     4.1 --- a/src/Pure/Tools/class_package.ML	Sat May 19 11:33:21 2007 +0200
     4.2 +++ b/src/Pure/Tools/class_package.ML	Sat May 19 11:33:22 2007 +0200
     4.3 @@ -561,7 +561,7 @@
     4.4        #> snd
     4.5    in
     4.6      thy
     4.7 -    |> add_locale (SOME (bname ^ "_pred")) bname supexpr ((*elems_constrains @*) elems)
     4.8 +    |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
     4.9      |-> (fn name_locale => ProofContext.theory_result (
    4.10        `(fn thy => extract_params thy name_locale)
    4.11        #-> (fn (param_names, params) =>