# HG changeset patch
# User nipkow
# Date 1107533682 -3600
# Node ID 53bca254719adc8fcd32451c9e84af2cfb148fa2
# Parent  3263daa9616705c9470e8d81ac831f432c0e5596
Added semi-lattice locales and reorganized fold1 lemmas

diff -r 3263daa96167 -r 53bca254719a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Feb 03 16:45:59 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Feb 04 17:14:42 2005 +0100
@@ -487,6 +487,15 @@
   thus ?thesis by (subst commute)
 qed
 
+lemma (in ACIf) idem2: "x \<cdot> (x \<cdot> y) = x \<cdot> y"
+proof -
+  have "x \<cdot> (x \<cdot> y) = (x \<cdot> x) \<cdot> y" by(simp add:assoc)
+  also have "\<dots> = x \<cdot> y" by(simp add:idem)
+  finally show ?thesis .
+qed
+
+lemmas (in ACIf) ACI = AC idem idem2
+
 text{* Instantiation of locales: *}
 
 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)"
@@ -1913,6 +1922,74 @@
 by(simp add:fold1_insert2)
 
 
+subsubsection{* Semi-Lattices *}
+
+locale ACIfSL = ACIf +
+  fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<preceq>" 50)
+  assumes below_def: "x \<preceq> y = (x\<cdot>y = x)"
+
+locale ACIfSLlin = ACIfSL +
+  assumes lin: "x\<cdot>y \<in> {x,y}"
+
+lemma (in ACIfSL) below_refl[simp]: "x \<preceq> x"
+by(simp add: below_def idem)
+
+lemma (in ACIfSL) below_f_conv[simp]: "x \<preceq> y \<cdot> z = (x \<preceq> y \<and> x \<preceq> z)"
+proof
+  assume "x \<preceq> y \<cdot> z"
+  hence xyzx: "x \<cdot> (y \<cdot> z) = x"  by(simp add: below_def)
+  have "x \<cdot> y = x"
+  proof -
+    have "x \<cdot> y = (x \<cdot> (y \<cdot> z)) \<cdot> y" by(rule subst[OF xyzx], rule refl)
+    also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
+    also have "\<dots> = x" by(rule xyzx)
+    finally show ?thesis .
+  qed
+  moreover have "x \<cdot> z = x"
+  proof -
+    have "x \<cdot> z = (x \<cdot> (y \<cdot> z)) \<cdot> z" by(rule subst[OF xyzx], rule refl)
+    also have "\<dots> = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
+    also have "\<dots> = x" by(rule xyzx)
+    finally show ?thesis .
+  qed
+  ultimately show "x \<preceq> y \<and> x \<preceq> z" by(simp add: below_def)
+next
+  assume a: "x \<preceq> y \<and> x \<preceq> z"
+  hence y: "x \<cdot> y = x" and z: "x \<cdot> z = x" by(simp_all add: below_def)
+  have "x \<cdot> (y \<cdot> z) = (x \<cdot> y) \<cdot> z" by(simp add:assoc)
+  also have "x \<cdot> y = x" using a by(simp_all add: below_def)
+  also have "x \<cdot> z = x" using a by(simp_all add: below_def)
+  finally show "x \<preceq> y \<cdot> z" by(simp_all add: below_def)
+qed
+
+lemma (in ACIfSLlin) above_f_conv:
+ "x \<cdot> y \<preceq> z = (x \<preceq> z \<or> y \<preceq> z)"
+proof
+  assume a: "x \<cdot> y \<preceq> z"
+  have "x \<cdot> y = x \<or> x \<cdot> y = y" using lin[of x y] by simp
+  thus "x \<preceq> z \<or> y \<preceq> z"
+  proof
+    assume "x \<cdot> y = x" hence "x \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
+  next
+    assume "x \<cdot> y = y" hence "y \<preceq> z" by(rule subst)(rule a) thus ?thesis ..
+  qed
+next
+  assume "x \<preceq> z \<or> y \<preceq> z"
+  thus "x \<cdot> y \<preceq> z"
+  proof
+    assume a: "x \<preceq> z"
+    have "(x \<cdot> y) \<cdot> z = (x \<cdot> z) \<cdot> y" by(simp add:ACI)
+    also have "x \<cdot> z = x" using a by(simp add:below_def)
+    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
+  next
+    assume a: "y \<preceq> z"
+    have "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" by(simp add:ACI)
+    also have "y \<cdot> z = y" using a by(simp add:below_def)
+    finally show "x \<cdot> y \<preceq> z" by(simp add:below_def)
+  qed
+qed
+
+
 subsubsection{* Lemmas about {@text fold1} *}
 
 lemma (in ACf) fold1_Un:
@@ -1947,38 +2024,59 @@
   case insert thus ?case using elem by (force simp add:fold1_insert)
 qed
 
-lemma fold1_le:
-  assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
-  and A: "finite (A)" "A \<noteq> {}" and le: "\<And>x y. f x y \<le> x"
-  shows "a \<in> A \<Longrightarrow> fold1 f A \<le> a"
+lemma (in ACIfSL) below_fold1_iff:
+assumes A: "finite A" "A \<noteq> {}"
+shows "x \<preceq> fold1 f A = (\<forall>a\<in>A. x \<preceq> a)"
+using 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 \<preceq> a"
 using A
 proof (induct rule:finite_ne_induct)
-  case singleton thus ?case by(simp)
+  case singleton thus ?case by simp
 next
-  from le have le2: "\<And>x y. f x y \<le> y" by (fastsimp simp:ACf.commute[OF ACf])
-  case (insert x F) thus ?case using le le2
-    by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: le order_trans)
+  case (insert x F)
+  from insert(4) have "a = x \<or> a \<in> F" by simp
+  thus ?case
+  proof
+    assume "a = x" thus ?thesis using insert by(simp add:below_def ACI)
+  next
+    assume "a \<in> F"
+    hence bel: "fold1 op \<cdot> F \<preceq> a" by(rule insert)
+    have "fold1 op \<cdot> (insert x F) \<cdot> a = x \<cdot> (fold1 op \<cdot> F \<cdot> a)"
+      using insert by(simp add:below_def ACI)
+    also have "fold1 op \<cdot> F \<cdot> a = fold1 op \<cdot> F"
+      using bel  by(simp add:below_def ACI)
+    also have "x \<cdot> \<dots> = fold1 op \<cdot> (insert x F)"
+      using insert by(simp add:below_def ACI)
+    finally show ?thesis  by(simp add:below_def)
+  qed
 qed
 
-lemma fold1_ge:
-  assumes ACf: "ACf(f::'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
-  and A: "finite (A)" "A \<noteq> {}" and ge: "\<And>x y. x \<le> f x y"
-  shows "a \<in> A \<Longrightarrow> a \<le> fold1 f A"
+lemma (in ACIfSLlin) fold1_below_iff:
+assumes A: "finite A" "A \<noteq> {}"
+shows "fold1 f A \<preceq> x = (\<exists>a\<in>A. a \<preceq> x)"
 using A
-proof (induct rule:finite_ne_induct)
-  case singleton thus ?case by(simp)
-next
-  from ge have ge2: "\<And>x y. y \<le> f x y" by (fastsimp simp:ACf.commute[OF ACf])
-  case (insert x F) thus ?case using ge ge2
-    by (simp add:ACf.fold1_insert[OF ACf]) (blast intro: ge order_trans)
-qed
+by(induct rule:finite_ne_induct)(simp_all add:above_f_conv)
 
 
 subsection{*Min and Max*}
 
 text{* As an application of @{text fold1} we define the minimal and
-maximal element of a (non-empty) set over a linear order. First we
-show that @{text min} and @{text max} are ACI: *}
+maximal element of a (non-empty) set over a linear order. *}
+
+constdefs
+  Min :: "('a::linorder)set => 'a"
+  "Min  ==  fold1 min"
+
+  Max :: "('a::linorder)set => 'a"
+  "Max  ==  fold1 max"
+
+
+text{* Before we can do anything, we need to show that @{text min} and
+@{text max} are ACI and the ordering is linear: *}
 
 lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
 apply(rule ACf.intro)
@@ -2002,14 +2100,39 @@
 apply(auto simp:max_def)
 done
 
-text{* Now we make the definitions: *}
+lemma ACIfSL_min: "ACIfSL(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
+apply(rule ACIfSL.intro)
+apply(rule ACf_min)
+apply(rule ACIf.axioms[OF ACIf_min])
+apply(rule ACIfSL_axioms.intro)
+apply(auto simp:min_def)
+done
+
+lemma ACIfSLlin_min: "ACIfSLlin(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
+apply(rule ACIfSLlin.intro)
+apply(rule ACf_min)
+apply(rule ACIf.axioms[OF ACIf_min])
+apply(rule ACIfSL.axioms[OF ACIfSL_min])
+apply(rule ACIfSLlin_axioms.intro)
+apply(auto simp:min_def)
+done
 
-constdefs
-  Min :: "('a::linorder)set => 'a"
-  "Min  ==  fold1 min"
+lemma ACIfSL_max: "ACIfSL(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
+apply(rule ACIfSL.intro)
+apply(rule ACf_max)
+apply(rule ACIf.axioms[OF ACIf_max])
+apply(rule ACIfSL_axioms.intro)
+apply(auto simp:max_def)
+done
 
-  Max :: "('a::linorder)set => 'a"
-  "Max  ==  fold1 max"
+lemma ACIfSLlin_max: "ACIfSLlin(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
+apply(rule ACIfSLlin.intro)
+apply(rule ACf_max)
+apply(rule ACIf.axioms[OF ACIf_max])
+apply(rule ACIfSL.axioms[OF ACIfSL_max])
+apply(rule ACIfSLlin_axioms.intro)
+apply(auto simp:max_def)
+done
 
 text{* Now we instantiate the recursion equations and declare them
 simplification rules: *}
@@ -2033,9 +2156,25 @@
 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 fold1_le[OF ACf_min] min_le_iff_disj)
+by(simp add: Min_def ACIfSL.fold1_belowI[OF ACIfSL_min])
 
 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
-by(simp add: Max_def fold1_ge[OF ACf_max] le_max_iff_disj)
+by(simp add: Max_def ACIfSL.fold1_belowI[OF ACIfSL_max])
+
+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 ACIfSL.below_fold1_iff[OF ACIfSL_min])
+
+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 ACIfSL.below_fold1_iff[OF ACIfSL_max])
+
+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 ACIfSLlin.fold1_below_iff[OF ACIfSLlin_min])
+
+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 ACIfSLlin.fold1_below_iff[OF ACIfSLlin_max])
 
 end