--- a/src/HOL/Finite_Set.thy Thu Apr 21 15:33:30 2005 +0200
+++ b/src/HOL/Finite_Set.thy Thu Apr 21 17:22:17 2005 +0200
@@ -2227,45 +2227,45 @@
text{* Before we can do anything, we need to show that @{text min} and
@{text max} are ACI and the ordering is linear: *}
-interpretation AC_min [rule del]: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+interpretation min [rule del]: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
apply(rule ACf.intro)
apply(auto simp:min_def)
done
-interpretation AC_min [rule del]: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+interpretation min [rule del]: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
apply(rule ACIf_axioms.intro)
apply(auto simp:min_def)
done
-interpretation AC_max [rule del]: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+interpretation max [rule del]: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
apply(rule ACf.intro)
apply(auto simp:max_def)
done
-interpretation AC_max [rule del]: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+interpretation max [rule del]: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
apply(rule ACIf_axioms.intro)
apply(auto simp:max_def)
done
-interpretation AC_min [rule del]:
+interpretation min [rule del]:
ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
apply(rule ACIfSL_axioms.intro)
apply(auto simp:min_def)
done
-interpretation AC_min [rule del]:
+interpretation min [rule del]:
ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
apply(rule ACIfSLlin_axioms.intro)
apply(auto simp:min_def)
done
-interpretation AC_max [rule del]:
+interpretation max [rule del]:
ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
apply(rule ACIfSL_axioms.intro)
apply(auto simp:max_def)
done
-interpretation AC_max [rule del]:
+interpretation max [rule del]:
ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
apply(rule ACIfSLlin_axioms.intro)
apply(auto simp:max_def)
@@ -2295,42 +2295,42 @@
declare
fold1_singleton_def[OF Min_def, simp]
- AC_min.fold1_insert_idem_def[OF Min_def, simp]
+ min.fold1_insert_idem_def[OF Min_def, simp]
fold1_singleton_def[OF Max_def, simp]
- AC_max.fold1_insert_idem_def[OF Max_def, simp]
+ max.fold1_insert_idem_def[OF Max_def, simp]
text{* Now we instantiate some @{text fold1} properties: *}
lemma Min_in [simp]:
shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
-using AC_min.fold1_in
+using min.fold1_in
by(fastsimp simp: Min_def min_def)
lemma Max_in [simp]:
shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
-using AC_max.fold1_in
+using max.fold1_in
by(fastsimp simp: Max_def max_def)
lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
-by(simp add: Min_def AC_min.fold1_belowI)
+by(simp add: Min_def min.fold1_belowI)
lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
-by(simp add: Max_def AC_max.fold1_belowI)
+by(simp add: Max_def max.fold1_belowI)
lemma Min_ge_iff[simp]:
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
-by(simp add: Min_def AC_min.below_fold1_iff)
+by(simp add: Min_def min.below_fold1_iff)
lemma Max_le_iff[simp]:
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
-by(simp add: Max_def AC_max.below_fold1_iff)
+by(simp add: Max_def max.below_fold1_iff)
lemma Min_le_iff:
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
-by(simp add: Min_def AC_min.fold1_below_iff)
+by(simp add: Min_def min.fold1_below_iff)
lemma Max_ge_iff:
"\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
-by(simp add: Max_def AC_max.fold1_below_iff)
+by(simp add: Max_def max.fold1_below_iff)
end
--- a/src/HOL/Lattice_Locales.thy Thu Apr 21 15:33:30 2005 +0200
+++ b/src/HOL/Lattice_Locales.thy Thu Apr 21 17:22:17 2005 +0200
@@ -52,6 +52,12 @@
lemma (in upper_semilattice) sup_idem[simp]: "x \<squnion> x = x"
by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
+lemma (in lower_semilattice) inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
+by (simp add: inf_assoc[symmetric])
+
+lemma (in upper_semilattice) sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
+by (simp add: sup_assoc[symmetric])
+
lemma (in lattice) inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
by(blast intro: antisym inf_le1 inf_least sup_ge1)
--- a/src/HOL/Orderings.ML Thu Apr 21 15:33:30 2005 +0200
+++ b/src/HOL/Orderings.ML Thu Apr 21 17:22:17 2005 +0200
@@ -33,8 +33,10 @@
val linorder_not_le = thm "linorder_not_le";
val linorder_neq_iff = thm "linorder_neq_iff";
val linorder_neqE = thm "linorder_neqE";
+(*
val min_same = thm "min_same";
val max_same = thm "max_same";
+*)
val le_max_iff_disj = thm "le_max_iff_disj";
val le_maxI1 = thm "le_maxI1";
val le_maxI2 = thm "le_maxI2";
--- a/src/HOL/Orderings.thy Thu Apr 21 15:33:30 2005 +0200
+++ b/src/HOL/Orderings.thy Thu Apr 21 17:22:17 2005 +0200
@@ -390,12 +390,6 @@
subsection "Min and max on (linear) orders"
-lemma min_same [simp]: "min (x::'a::order) x = x"
- by (simp add: min_def)
-
-lemma max_same [simp]: "max (x::'a::order) x = x"
- by (simp add: max_def)
-
text{* Instantiate locales: *}
interpretation min_max [rule del]:
@@ -461,12 +455,7 @@
apply (insert linorder_less_linear)
apply (blast intro: order_less_trans)
done
-(*
-lemma le_min_iff_conj [simp]:
- "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"
- -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *}
-by (rule lower_semilattice.below_inf_conv[OF lower_semilattice_lin_min])
-*)
+
lemma min_less_iff_conj [simp]:
"!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
apply (simp add: order_le_less min_def)
@@ -485,22 +474,10 @@
apply (insert linorder_less_linear)
apply (blast intro: order_less_trans)
done
-(*
-lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
-by (rule upper_semilattice.sup_assoc[OF upper_semilattice_lin_max])
-lemma max_commute: "!!x::'a::linorder. max x y = max y x"
-by (rule upper_semilattice.sup_commute[OF upper_semilattice_lin_max])
-*)
lemmas max_ac = min_max.sup_assoc min_max.sup_commute
mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
-(*
-lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
-by (rule lower_semilattice.inf_assoc[OF lower_semilattice_lin_min])
-lemma min_commute: "!!x::'a::linorder. min x y = min y x"
-by (rule lower_semilattice.inf_commute[OF lower_semilattice_lin_min])
-*)
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]