--- a/src/HOL/Finite_Set.thy Sat May 19 11:33:21 2007 +0200
+++ b/src/HOL/Finite_Set.thy Sat May 19 11:33:22 2007 +0200
@@ -2432,53 +2432,53 @@
lemma ACIf_min: "ACIf min"
by (rule lower_semilattice.ACIf_inf,
- rule lattice_pred.axioms,
- rule distrib_lattice_pred.axioms,
+ rule lattice.axioms,
+ rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
lemma ACf_min: "ACf min"
by (rule lower_semilattice.ACf_inf,
- rule lattice_pred.axioms,
- rule distrib_lattice_pred.axioms,
+ rule lattice.axioms,
+ rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
lemma ACIfSL_min: "ACIfSL (op \<^loc>\<le>) (op \<^loc><) min"
by (rule lower_semilattice.ACIfSL_inf,
- rule lattice_pred.axioms,
- rule distrib_lattice_pred.axioms,
+ rule lattice.axioms,
+ rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
lemma ACIfSLlin_min: "ACIfSLlin (op \<^loc>\<le>) (op \<^loc><) min"
by (rule ACIfSLlin.intro,
rule lower_semilattice.ACIfSL_inf,
- rule lattice_pred.axioms,
- rule distrib_lattice_pred.axioms,
+ rule lattice.axioms,
+ rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
(unfold_locales, simp add: min_def)
lemma ACIf_max: "ACIf max"
by (rule upper_semilattice.ACIf_sup,
- rule lattice_pred.axioms,
- rule distrib_lattice_pred.axioms,
+ rule lattice.axioms,
+ rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
lemma ACf_max: "ACf max"
by (rule upper_semilattice.ACf_sup,
- rule lattice_pred.axioms,
- rule distrib_lattice_pred.axioms,
+ rule lattice.axioms,
+ rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
lemma ACIfSL_max: "ACIfSL (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
by (rule upper_semilattice.ACIfSL_sup,
- rule lattice_pred.axioms,
- rule distrib_lattice_pred.axioms,
+ rule lattice.axioms,
+ rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
lemma ACIfSLlin_max: "ACIfSLlin (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x) max"
by (rule ACIfSLlin.intro,
rule upper_semilattice.ACIfSL_sup,
- rule lattice_pred.axioms,
- rule distrib_lattice_pred.axioms,
+ rule lattice.axioms,
+ rule distrib_lattice.axioms,
rule distrib_lattice_min_max)
(unfold_locales, simp add: max_def)
@@ -2601,7 +2601,7 @@
proof
fix A :: "'a set"
show "Linorder.Min (op \<le>) A = Min A"
- by (simp add: Min_def Linorder.Min_def [OF Linorder.intro, OF linorder_pred_axioms]
+ by (simp add: Min_def Linorder.Min_def [OF Linorder.intro, OF linorder_axioms]
linorder_class_min)
qed
@@ -2610,19 +2610,19 @@
proof
fix A :: "'a set"
show "Linorder.Max (op \<le>) A = Max A"
- by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_pred_axioms]
+ by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_axioms]
linorder_class_max)
qed
interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"]
by (rule Linorder_ab_semigroup_add.intro,
- rule Linorder.intro, rule linorder_pred_axioms, rule pordered_ab_semigroup_add_pred_axioms)
+ rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms)
hide const Min Max
interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"]
- by (rule Linorder.intro, rule linorder_pred_axioms)
+ by (rule Linorder.intro, rule linorder_axioms)
declare Min_singleton [simp]
declare Max_singleton [simp]
declare Min_insert [simp]
@@ -2640,8 +2640,11 @@
subsection {* Class @{text finite} *}
+setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
class finite (attach UNIV) = type +
assumes finite: "finite UNIV"
+setup {* Sign.parent_path *}
+hide const finite
lemma finite_set: "finite (A::'a::finite set)"
by (rule finite_subset [OF subset_UNIV finite])
--- a/src/HOL/Lattices.thy Sat May 19 11:33:21 2007 +0200
+++ b/src/HOL/Lattices.thy Sat May 19 11:33:22 2007 +0200
@@ -282,7 +282,7 @@
special case of @{const inf}/@{const sup} *}
lemma (in linorder) distrib_lattice_min_max:
- "distrib_lattice_pred (op \<^loc>\<le>) (op \<^loc><) min max"
+ "distrib_lattice (op \<^loc>\<le>) (op \<^loc><) min max"
proof unfold_locales
have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y"
by (auto simp add: less_le antisym)
--- a/src/HOL/Orderings.thy Sat May 19 11:33:21 2007 +0200
+++ b/src/HOL/Orderings.thy Sat May 19 11:33:22 2007 +0200
@@ -199,7 +199,7 @@
text {* Reverse order *}
lemma order_reverse:
- "order_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+ "order (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
by unfold_locales
(simp add: less_le, auto intro: antisym order_trans)
@@ -266,7 +266,7 @@
text {* Reverse order *}
lemma linorder_reverse:
- "linorder_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
+ "linorder (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
by unfold_locales
(simp add: less_le, auto intro: antisym order_trans simp add: linear)
--- a/src/Pure/Tools/class_package.ML Sat May 19 11:33:21 2007 +0200
+++ b/src/Pure/Tools/class_package.ML Sat May 19 11:33:22 2007 +0200
@@ -561,7 +561,7 @@
#> snd
in
thy
- |> add_locale (SOME (bname ^ "_pred")) bname supexpr ((*elems_constrains @*) elems)
+ |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
|-> (fn name_locale => ProofContext.theory_result (
`(fn thy => extract_params thy name_locale)
#-> (fn (param_names, params) =>