src/HOL/Finite_Set.thy

 
 subsubsection{* Semi-Lattices *}
 
 locale ACIfSL = ACIf +
   fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubseteq>" 50)
+  and strict_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sqsubset>" 50)
   assumes below_def: "(x \<sqsubseteq> y) = (x\<cdot>y = x)"
+  defines strict_below_def:  "(x \<sqsubset> y) \<equiv> (x \<sqsubseteq> y \<and> x \<noteq> y)"
 
 locale ACIfSLlin = ACIfSL +
   assumes lin: "x\<cdot>y \<in> {x,y}"
 
 lemma (in ACIfSL) below_refl[simp]: "x \<sqsubseteq> x"

     finally show "x \<cdot> y \<sqsubseteq> z" by(simp add:below_def)
   qed
 qed
 
 
+lemma (in ACIfSLlin) strict_below_f_conv[simp]: "x \<sqsubset> y \<cdot> z = (x \<sqsubset> y \<and> x \<sqsubset> z)"
+apply(simp add: strict_below_def)
+using lin[of y z] by (auto simp:below_def ACI)
+
+
+lemma (in ACIfSLlin) strict_above_f_conv:
+ "x \<cdot> y \<sqsubset> z = (x \<sqsubset> z \<or> y \<sqsubset> z)"
+apply(simp add: strict_below_def above_f_conv)
+using lin[of y z] lin[of x z] by (auto simp:below_def ACI)
+
+
 subsubsection{* Lemmas about @{text fold1} *}
 
 lemma (in ACf) fold1_Un:
 assumes A: "finite A" "A \<noteq> {}"
 shows "finite B \<Longrightarrow> B \<noteq> {} \<Longrightarrow> A Int B = {} \<Longrightarrow>

 lemma (in ACIfSL) below_fold1_iff:
 assumes A: "finite A" "A \<noteq> {}"
 shows "x \<sqsubseteq> fold1 f A = (\<forall>a\<in>A. x \<sqsubseteq> a)"
 using A
 by(induct rule:finite_ne_induct) simp_all
+
+lemma (in ACIfSLlin) strict_below_fold1_iff:
+  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> x \<sqsubset> fold1 f A = (\<forall>a\<in>A. x \<sqsubset> a)"
+by(induct rule:finite_ne_induct) simp_all
+
 
 lemma (in ACIfSL) fold1_belowI:
 assumes A: "finite A" "A \<noteq> {}"
 shows "a \<in> A \<Longrightarrow> fold1 f A \<sqsubseteq> a"
 using A

       using insert by(simp add:below_def ACI)
     finally show ?thesis  by(simp add:below_def)
   qed
 qed
 
+
 lemma (in ACIfSLlin) fold1_below_iff:
 assumes A: "finite A" "A \<noteq> {}"
 shows "fold1 f A \<sqsubseteq> x = (\<exists>a\<in>A. a \<sqsubseteq> x)"
 using A
 by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
+
+lemma (in ACIfSLlin) fold1_strict_below_iff:
+assumes A: "finite A" "A \<noteq> {}"
+shows "fold1 f A \<sqsubset> x = (\<exists>a\<in>A. a \<sqsubset> x)"
+using A
+by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv)
 
 
 lemma (in ACIfSLlin) fold1_antimono:
 assumes "A \<noteq> {}" and "A \<subseteq> B" and "finite B"
 shows "fold1 f B \<sqsubseteq> fold1 f A"

   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
   have "fold1 f B = fold1 f (A \<union> (B-A))" by(subst B)(rule refl)
   also have "\<dots> = f (fold1 f A) (fold1 f (B-A))"
   proof -
     have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
-    moreover have "finite(B-A)" by(blast intro:finite_Diff prems)
+    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
     moreover have "(B-A) \<noteq> {}" using prems by blast
     moreover have "A Int (B-A) = {}" using prems by blast
     ultimately show ?thesis using `A \<noteq> {}` by(rule_tac fold1_Un)
   qed
   also have "\<dots> \<sqsubseteq> fold1 f A" by(simp add: above_f_conv)
   finally show ?thesis .
 qed
+
 
 
 subsubsection{* Lattices *}
 
 locale Lattice = lattice +

 apply(rule ACIf_axioms.intro)
 apply(auto simp:max_def)
 done
 
 interpretation min:
-  ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
+  ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
+apply(simp add:order_less_le)
 apply(rule ACIfSL_axioms.intro)
 apply(auto simp:min_def)
 done
 
 interpretation min:
-  ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
+  ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>" "op <"]
 apply(rule ACIfSLlin_axioms.intro)
 apply(auto simp:min_def)
 done
 
 interpretation max:
-  ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
+  ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
+apply(simp add:order_less_le eq_sym_conv)
 apply(rule ACIfSL_axioms.intro)
 apply(auto simp:max_def)
 done
 
 interpretation max:
-  ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
+  ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x" "%x y. y<x"]
 apply(rule ACIfSLlin_axioms.intro)
 apply(auto simp:max_def)
 done
 
 interpretation min_max:

 
 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 max.below_fold1_iff)
 
+lemma Min_gr_iff[simp]:
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x < Min A) = (\<forall>a\<in>A. x < a)"
+by(simp add: Min_def min.strict_below_fold1_iff)
+
+lemma Max_less_iff[simp]:
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A < x) = (\<forall>a\<in>A. a < x)"
+by(simp add: Max_def max.strict_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 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 max.fold1_below_iff)
+
+lemma Min_le_iff:
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A < x) = (\<exists>a\<in>A. a < x)"
+by(simp add: Min_def min.fold1_strict_below_iff)
+
+lemma Max_ge_iff:
+  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x < Max A) = (\<exists>a\<in>A. x < a)"
+by(simp add: Max_def max.fold1_strict_below_iff)
 
 lemma Min_Un: "\<lbrakk>finite A; A \<noteq> {}; finite B; B \<noteq> {}\<rbrakk>
   \<Longrightarrow> Min (A \<union> B) = min (Min A) (Min B)"
 by(simp add:Min_def min.f.fold1_Un2)