summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | ballarin |

Wed, 30 Jul 2008 19:03:33 +0200 | |

changeset 27713 | 95b36bfe7fc4 |

parent 27712 | 007a339b9e7d |

child 27714 | 27b4d7c01f8b |

New locales for orders and lattices where the equivalence relation is not restricted to equality.

NEWS | file | annotate | diff | comparison | revisions | |

src/HOL/Algebra/Divisibility.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Algebra/GLattice.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Algebra/Group.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Algebra/IntRing.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Algebra/Lattice.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Algebra/ROOT.ML | file | annotate | diff | comparison | revisions | |

src/HOL/IsaMakefile | file | annotate | diff | comparison | revisions |

--- a/NEWS Wed Jul 30 16:07:00 2008 +0200 +++ b/NEWS Wed Jul 30 19:03:33 2008 +0200 @@ -125,6 +125,13 @@ *** HOL-Algebra *** +* New locales for orders and lattices where the equivalence relation + is not restricted to equality. INCOMPATIBILITY: all order and + lattice locales use a record structure with field eq for the + equivalence. + +* New theory of factorial domains. + * Units_l_inv and Units_r_inv are now simprules by default. INCOMPATIBILITY. Simplifier proof that require deletion of l_inv and/or r_inv will now also require deletion of these lemmas. @@ -136,8 +143,6 @@ greatest_carrier ~> greatest_closed greatest_Lower_above ~> greatest_Lower_below -* New theory of factorial domains. - *** HOL-NSA ***

--- a/src/HOL/Algebra/Divisibility.thy Wed Jul 30 16:07:00 2008 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Wed Jul 30 19:03:33 2008 +0200 @@ -2,11 +2,12 @@ Title: Divisibility in monoids and rings Id: $Id$ Author: Clemens Ballarin, started 18 July 2008 - Copyright: Clemens Ballarin + +Based on work by Stefan Hohe. *) theory Divisibility -imports Permutation Coset Group GLattice +imports Permutation Coset Group begin subsection {* Monoid with cancelation law *} @@ -490,8 +491,8 @@ show "x divides y'" by simp qed -lemma (in monoid) division_gpartial_order [simp, intro!]: - "gpartial_order (division_rel G)" +lemma (in monoid) division_weak_partial_order [simp, intro!]: + "weak_partial_order (division_rel G)" apply unfold_locales apply simp_all apply (simp add: associated_sym) @@ -731,12 +732,12 @@ apply (iprover intro: divides_trans)+ done -lemma properfactor_glless: +lemma properfactor_lless: fixes G (structure) - shows "properfactor G = glless (division_rel G)" + shows "properfactor G = lless (division_rel G)" apply (rule ext) apply (rule ext) apply rule - apply (fastsimp elim: properfactorE2 intro: gllessI) -apply (fastsimp elim: gllessE intro: properfactorI2) + apply (fastsimp elim: properfactorE2 intro: weak_llessI) +apply (fastsimp elim: weak_llessE intro: properfactorI2) done lemma (in monoid) properfactor_cong_l [trans]: @@ -745,9 +746,9 @@ and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" shows "properfactor G x' y" using pf -unfolding properfactor_glless +unfolding properfactor_lless proof - - interpret gpartial_order ["division_rel G"] .. + interpret weak_partial_order ["division_rel G"] .. from x'x have "x' .=\<^bsub>division_rel G\<^esub> x" by simp also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y" @@ -761,9 +762,9 @@ and carr: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" shows "properfactor G x y'" using pf -unfolding properfactor_glless +unfolding properfactor_lless proof - - interpret gpartial_order ["division_rel G"] .. + interpret weak_partial_order ["division_rel G"] .. assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y" also from yy' have "y .=\<^bsub>division_rel G\<^esub> y'" by simp @@ -2630,7 +2631,7 @@ "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof a b" constdefs (structure G) - "SomeGcd G A == ginf (division_rel G) A" + "SomeGcd G A == inf (division_rel G) A" locale gcd_condition_monoid = comm_monoid_cancel + @@ -2648,12 +2649,12 @@ subsubsection {* Connections to \texttt{Lattice.thy} *} -lemma gcdof_ggreatestLower: +lemma gcdof_greatestLower: fixes G (structure) assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G" shows "(x \<in> carrier G \<and> x gcdof a b) = - ggreatest (division_rel G) x (Lower (division_rel G) {a, b})" -unfolding isgcd_def ggreatest_def Lower_def elem_def + greatest (division_rel G) x (Lower (division_rel G) {a, b})" +unfolding isgcd_def greatest_def Lower_def elem_def proof (simp, safe) fix xa assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> xa divides x" @@ -2674,12 +2675,12 @@ by (fast intro: r1) qed (simp, simp) -lemma lcmof_gleastUpper: +lemma lcmof_leastUpper: fixes G (structure) assumes carr[simp]: "a \<in> carrier G" "b \<in> carrier G" shows "(x \<in> carrier G \<and> x lcmof a b) = - gleast (division_rel G) x (Upper (division_rel G) {a, b})" -unfolding islcm_def gleast_def Upper_def elem_def + least (division_rel G) x (Upper (division_rel G) {a, b})" +unfolding islcm_def least_def Upper_def elem_def proof (simp, safe) fix xa assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides xa" @@ -2700,12 +2701,12 @@ by (fast intro: r1) qed (simp, simp) -lemma somegcd_gmeet: +lemma somegcd_meet: fixes G (structure) assumes carr: "a \<in> carrier G" "b \<in> carrier G" - shows "somegcd G a b = gmeet (division_rel G) a b" -unfolding somegcd_def gmeet_def ginf_def -by (simp add: gcdof_ggreatestLower[OF carr]) + shows "somegcd G a b = meet (division_rel G) a b" +unfolding somegcd_def meet_def inf_def +by (simp add: gcdof_greatestLower[OF carr]) lemma (in monoid) isgcd_divides_l: assumes "a divides b" @@ -2910,10 +2911,10 @@ subsubsection {* Gcd condition *} -lemma (in gcd_condition_monoid) division_glower_semilattice [simp]: - shows "glower_semilattice (division_rel G)" +lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]: + shows "weak_lower_semilattice (division_rel G)" proof - - interpret gpartial_order ["division_rel G"] .. + interpret weak_partial_order ["division_rel G"] .. show ?thesis apply (unfold_locales, simp_all) proof - @@ -2925,9 +2926,9 @@ and isgcd: "z gcdof x y" by auto with carr - have "ggreatest (division_rel G) z (Lower (division_rel G) {x, y})" - by (subst gcdof_ggreatestLower[symmetric], simp+) - thus "\<exists>z. ggreatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast + have "greatest (division_rel G) z (Lower (division_rel G) {x, y})" + by (subst gcdof_greatestLower[symmetric], simp+) + thus "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast qed qed @@ -2938,15 +2939,15 @@ shows "a' gcdof b c" proof - note carr = a'carr carr' - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp have "a' \<in> carrier G \<and> a' gcdof b c" - apply (simp add: gcdof_ggreatestLower carr') - apply (subst ggreatest_Lower_cong_l[of _ a]) + apply (simp add: gcdof_greatestLower carr') + apply (subst greatest_Lower_cong_l[of _ a]) apply (simp add: a'a) apply (simp add: carr) apply (simp add: carr) apply (simp add: carr) - apply (simp add: gcdof_ggreatestLower[symmetric] agcd carr) + apply (simp add: gcdof_greatestLower[symmetric] agcd carr) done thus ?thesis .. qed @@ -2955,10 +2956,10 @@ assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "somegcd G a b \<in> carrier G" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp show ?thesis - apply (simp add: somegcd_gmeet[OF carr]) - apply (rule gmeet_closed[simplified], fact+) + apply (simp add: somegcd_meet[OF carr]) + apply (rule meet_closed[simplified], fact+) done qed @@ -2966,12 +2967,12 @@ assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "(somegcd G a b) gcdof a b" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b" - apply (subst gcdof_ggreatestLower, simp, simp) - apply (simp add: somegcd_gmeet[OF carr] gmeet_def) - apply (rule ginf_of_two_ggreatest[simplified], assumption+) + apply (subst gcdof_greatestLower, simp, simp) + apply (simp add: somegcd_meet[OF carr] meet_def) + apply (rule inf_of_two_greatest[simplified], assumption+) done thus "(somegcd G a b) gcdof a b" by simp qed @@ -2980,10 +2981,10 @@ assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "\<exists>x\<in>carrier G. x = somegcd G a b" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp show ?thesis - apply (simp add: somegcd_gmeet[OF carr]) - apply (rule gmeet_closed[simplified], fact+) + apply (simp add: somegcd_meet[OF carr]) + apply (rule meet_closed[simplified], fact+) done qed @@ -2991,10 +2992,10 @@ assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "(somegcd G a b) divides a" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp show ?thesis - apply (simp add: somegcd_gmeet[OF carr]) - apply (rule gmeet_left[simplified], fact+) + apply (simp add: somegcd_meet[OF carr]) + apply (rule meet_left[simplified], fact+) done qed @@ -3002,10 +3003,10 @@ assumes carr: "a \<in> carrier G" "b \<in> carrier G" shows "(somegcd G a b) divides b" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp show ?thesis - apply (simp add: somegcd_gmeet[OF carr]) - apply (rule gmeet_right[simplified], fact+) + apply (simp add: somegcd_meet[OF carr]) + apply (rule meet_right[simplified], fact+) done qed @@ -3014,10 +3015,10 @@ and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" shows "z divides (somegcd G x y)" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp show ?thesis - apply (simp add: somegcd_gmeet L) - apply (rule gmeet_le[simplified], fact+) + apply (simp add: somegcd_meet L) + apply (rule meet_le[simplified], fact+) done qed @@ -3026,10 +3027,10 @@ and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" shows "somegcd G x y \<sim> somegcd G x' y" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp show ?thesis - apply (simp add: somegcd_gmeet carr) - apply (rule gmeet_cong_l[simplified], fact+) + apply (simp add: somegcd_meet carr) + apply (rule meet_cong_l[simplified], fact+) done qed @@ -3038,10 +3039,10 @@ and yy': "y \<sim> y'" shows "somegcd G x y \<sim> somegcd G x y'" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp show ?thesis - apply (simp add: somegcd_gmeet carr) - apply (rule gmeet_cong_r[simplified], fact+) + apply (simp add: somegcd_meet carr) + apply (rule meet_cong_r[simplified], fact+) done qed @@ -3089,10 +3090,10 @@ assumes "finite A" "A \<subseteq> carrier G" "A \<noteq> {}" shows "\<exists>x\<in> carrier G. x = SomeGcd G A" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp show ?thesis apply (simp add: SomeGcd_def) - apply (rule finite_ginf_closed[simplified], fact+) + apply (rule finite_inf_closed[simplified], fact+) done qed @@ -3100,11 +3101,11 @@ assumes carr: "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)" proof - - interpret glower_semilattice ["division_rel G"] by simp + interpret weak_lower_semilattice ["division_rel G"] by simp show ?thesis - apply (subst (2 3) somegcd_gmeet, (simp add: carr)+) - apply (simp add: somegcd_gmeet carr) - apply (rule gmeet_assoc[simplified], fact+) + apply (subst (2 3) somegcd_meet, (simp add: carr)+) + apply (simp add: somegcd_meet carr) + apply (rule weak_meet_assoc[simplified], fact+) done qed @@ -3866,12 +3867,12 @@ interpretation factorial_monoid \<subseteq> gcd_condition_monoid by (unfold_locales, rule gcdof_exists) -lemma (in factorial_monoid) division_glattice [simp]: - shows "glattice (division_rel G)" +lemma (in factorial_monoid) division_weak_lattice [simp]: + shows "weak_lattice (division_rel G)" proof - - interpret glower_semilattice ["division_rel G"] by simp - - show "glattice (division_rel G)" + interpret weak_lower_semilattice ["division_rel G"] by simp + + show "weak_lattice (division_rel G)" apply (unfold_locales, simp_all) proof - fix x y @@ -3883,9 +3884,9 @@ and isgcd: "z lcmof x y" by auto with carr - have "gleast (division_rel G) z (Upper (division_rel G) {x, y})" - by (simp add: lcmof_gleastUpper[symmetric]) - thus "\<exists>z. gleast (division_rel G) z (Upper (division_rel G) {x, y})" by fast + have "least (division_rel G) z (Upper (division_rel G) {x, y})" + by (simp add: lcmof_leastUpper[symmetric]) + thus "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})" by fast qed qed

--- a/src/HOL/Algebra/GLattice.thy Wed Jul 30 16:07:00 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1181 +0,0 @@ -(* - Title: HOL/Algebra/Lattice.thy - Id: $Id$ - Author: Clemens Ballarin, started 7 November 2003 - Copyright: Clemens Ballarin -*) - -theory GLattice imports Congruence begin - -(* FIXME: unify with Lattice.thy *) - - -section {* Orders and Lattices *} - -subsection {* Partial Orders *} - -record 'a gorder = "'a eq_object" + - le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) - -locale gpartial_order = equivalence L + - assumes le_refl [intro, simp]: - "x \<in> carrier L ==> x \<sqsubseteq> x" - and le_anti_sym [intro]: - "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y" - and le_trans [trans]: - "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z" - and le_cong: - "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w" - -constdefs (structure L) - glless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) - "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y" - - -subsubsection {* The order relation *} - -context gpartial_order begin - -lemma le_cong_l [intro, trans]: - "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" - by (auto intro: le_cong [THEN iffD2]) - -lemma le_cong_r [intro, trans]: - "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" - by (auto intro: le_cong [THEN iffD1]) - -lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y" - by (simp add: le_cong_l) - -end - -lemma gllessI: - fixes R (structure) - assumes "x \<sqsubseteq> y" and "~(x .= y)" - shows "x \<sqsubset> y" - using assms - unfolding glless_def - by simp - -lemma gllessD1: - fixes R (structure) - assumes "x \<sqsubset> y" - shows "x \<sqsubseteq> y" - using assms - unfolding glless_def - by simp - -lemma gllessD2: - fixes R (structure) - assumes "x \<sqsubset> y" - shows "\<not> (x .= y)" - using assms - unfolding glless_def - by simp - -lemma gllessE: - fixes R (structure) - assumes p: "x \<sqsubset> y" - and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P" - shows "P" - using p - by (blast dest: gllessD1 gllessD2 e) - -(* -lemma (in gpartial_order) lless_cong_l [trans]: - assumes xx': "x \<doteq> x'" - and xy: "x' \<sqsubset> y" - and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" - shows "x \<sqsubseteq> y" -using xy -unfolding lless_def -proof clarify - note xx' - also assume "x' \<sqsubseteq> y" - finally show "x \<sqsubseteq> y" by (simp add: carr) -qed -*) - -lemma (in gpartial_order) glless_cong_l [trans]: - assumes xx': "x .= x'" - and xy: "x' \<sqsubset> y" - and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" - shows "x \<sqsubset> y" - using assms - apply (elim gllessE, intro gllessI) - apply (iprover intro: le_cong_l) - apply (iprover intro: trans sym) - done - -(* -lemma (in gpartial_order) lless_cong_r: - assumes xy: "x \<sqsubset> y" - and yy': "y \<doteq> y'" - and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" - shows "x \<sqsubseteq> y'" -using xy -unfolding lless_def -proof clarify - assume "x \<sqsubseteq> y" - also note yy' - finally show "x \<sqsubseteq> y'" by (simp add: carr) -qed -*) - -lemma (in gpartial_order) glless_cong_r [trans]: - assumes xy: "x \<sqsubset> y" - and yy': "y .= y'" - and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" - shows "x \<sqsubset> y'" - using assms - apply (elim gllessE, intro gllessI) - apply (iprover intro: le_cong_r) - apply (iprover intro: trans sym) - done - -(* -lemma (in gpartial_order) glless_antisym: - assumes "a \<in> carrier L" "b \<in> carrier L" - and "a \<sqsubset> b" "b \<sqsubset> a" - shows "a \<doteq> b" - using assms - by (elim gllessE) (rule gle_anti_sym) - -lemma (in gpartial_order) glless_trans [trans]: - assumes "a .\<sqsubset> b" "b .\<sqsubset> c" - and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L" - shows "a .\<sqsubset> c" -using assms -apply (elim gllessE, intro gllessI) - apply (iprover dest: le_trans) -proof (rule ccontr, simp) - assume ab: "a \<sqsubseteq> b" and bc: "b \<sqsubseteq> c" - and ac: "a \<doteq> c" - and nbc: "\<not> b \<doteq> c" - note ac[symmetric] - also note ab - finally have "c \<sqsubseteq> b" by simp - with bc have "b \<doteq> c" by (iprover intro: gle_anti_sym carr) - with nbc - show "False" by simp -qed -*) - -subsubsection {* Upper and lower bounds of a set *} - -constdefs (structure L) - Upper :: "[_, 'a set] => 'a set" - "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L" - - Lower :: "[_, 'a set] => 'a set" - "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L" - -lemma Upper_closed [intro!, simp]: - "Upper L A \<subseteq> carrier L" - by (unfold Upper_def) clarify - -lemma Upper_memD [dest]: - fixes L (structure) - shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L" - by (unfold Upper_def) blast - -lemma (in gpartial_order) Upper_elemD [dest]: - "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u" - unfolding Upper_def elem_def - by (blast dest: sym) - -lemma Upper_memI: - fixes L (structure) - shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A" - by (unfold Upper_def) blast - -lemma (in gpartial_order) Upper_elemI: - "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A" - unfolding Upper_def by blast - -lemma Upper_antimono: - "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A" - by (unfold Upper_def) blast - -lemma (in gpartial_order) Upper_is_closed [simp]: - "A \<subseteq> carrier L ==> is_closed (Upper L A)" - by (rule is_closedI) (blast intro: Upper_memI)+ - -lemma (in gpartial_order) Upper_mem_cong: - assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L" - and aa': "a .= a'" - and aelem: "a \<in> Upper L A" - shows "a' \<in> Upper L A" -proof (rule Upper_memI[OF _ a'carr]) - fix y - assume yA: "y \<in> A" - hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr) - also note aa' - finally - show "y \<sqsubseteq> a'" - by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem]) -qed - -lemma (in gpartial_order) Upper_cong: - assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L" - and AA': "A {.=} A'" - shows "Upper L A = Upper L A'" -unfolding Upper_def -apply rule - apply (rule, clarsimp) defer 1 - apply (rule, clarsimp) defer 1 -proof - - fix x a' - assume carr: "x \<in> carrier L" "a' \<in> carrier L" - and a'A': "a' \<in> A'" - assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x" - - from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2) - from this obtain a - where aA: "a \<in> A" - and a'a: "a' .= a" - by auto - note [simp] = subsetD[OF Acarr aA] carr - - note a'a - also have "a \<sqsubseteq> x" by (simp add: aLxCond aA) - finally show "a' \<sqsubseteq> x" by simp -next - fix x a - assume carr: "x \<in> carrier L" "a \<in> carrier L" - and aA: "a \<in> A" - assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x" - - from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1) - from this obtain a' - where a'A': "a' \<in> A'" - and aa': "a .= a'" - by auto - note [simp] = subsetD[OF A'carr a'A'] carr - - note aa' - also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A') - finally show "a \<sqsubseteq> x" by simp -qed - -lemma Lower_closed [intro!, simp]: - "Lower L A \<subseteq> carrier L" - by (unfold Lower_def) clarify - -lemma Lower_memD [dest]: - fixes L (structure) - shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L" - by (unfold Lower_def) blast - -lemma Lower_memI: - fixes L (structure) - shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A" - by (unfold Lower_def) blast - -lemma Lower_antimono: - "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A" - by (unfold Lower_def) blast - -lemma (in gpartial_order) Lower_is_closed [simp]: - "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)" - by (rule is_closedI) (blast intro: Lower_memI dest: sym)+ - -lemma (in gpartial_order) Lower_mem_cong: - assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L" - and aa': "a .= a'" - and aelem: "a \<in> Lower L A" - shows "a' \<in> Lower L A" -using assms Lower_closed[of L A] -by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]]) - -lemma (in gpartial_order) Lower_cong: - assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L" - and AA': "A {.=} A'" - shows "Lower L A = Lower L A'" -using Lower_memD[of y] -unfolding Lower_def -apply safe - apply clarsimp defer 1 - apply clarsimp defer 1 -proof - - fix x a' - assume carr: "x \<in> carrier L" "a' \<in> carrier L" - and a'A': "a' \<in> A'" - assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a" - hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast - - from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2) - from this obtain a - where aA: "a \<in> A" - and a'a: "a' .= a" - by auto - - from aA and subsetD[OF Acarr aA] - have "x \<sqsubseteq> a" by (rule aLxCond) - also note a'a[symmetric] - finally - show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA]) -next - fix x a - assume carr: "x \<in> carrier L" "a \<in> carrier L" - and aA: "a \<in> A" - assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'" - hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+ - - from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1) - from this obtain a' - where a'A': "a' \<in> A'" - and aa': "a .= a'" - by auto - from a'A' and subsetD[OF A'carr a'A'] - have "x \<sqsubseteq> a'" by (rule a'LxCond) - also note aa'[symmetric] - finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A']) -qed - - -subsubsection {* Least and greatest, as predicate *} - -constdefs (structure L) - gleast :: "[_, 'a, 'a set] => bool" - "gleast L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" - - ggreatest :: "[_, 'a, 'a set] => bool" - "ggreatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" - -lemma gleast_closed [intro, simp]: - "gleast L l A ==> l \<in> carrier L" - by (unfold gleast_def) fast - -lemma gleast_mem: - "gleast L l A ==> l \<in> A" - by (unfold gleast_def) fast - -lemma (in gpartial_order) gleast_unique: - "[| gleast L x A; gleast L y A |] ==> x .= y" - by (unfold gleast_def) blast - -lemma gleast_le: - fixes L (structure) - shows "[| gleast L x A; a \<in> A |] ==> x \<sqsubseteq> a" - by (unfold gleast_def) fast - -lemma (in gpartial_order) gleast_cong: - "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> gleast L x A = gleast L x' A" - by (unfold gleast_def) (auto dest: sym) - -text {* @{const gleast} is not congruent in the second parameter for - @{term [locale=gpartial_order] "A {.=} A'"} *} - -lemma (in gpartial_order) gleast_Upper_cong_l: - assumes "x .= x'" - and "x \<in> carrier L" "x' \<in> carrier L" - and "A \<subseteq> carrier L" - shows "gleast L x (Upper L A) = gleast L x' (Upper L A)" - apply (rule gleast_cong) using assms by auto - -lemma (in gpartial_order) gleast_Upper_cong_r: - assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *) - and AA': "A {.=} A'" - shows "gleast L x (Upper L A) = gleast L x (Upper L A')" -apply (subgoal_tac "Upper L A = Upper L A'", simp) -by (rule Upper_cong) fact+ - -lemma gleast_UpperI: - fixes L (structure) - assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" - and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y" - and L: "A \<subseteq> carrier L" "s \<in> carrier L" - shows "gleast L s (Upper L A)" -proof - - have "Upper L A \<subseteq> carrier L" by simp - moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def) - moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast - ultimately show ?thesis by (simp add: gleast_def) -qed - -lemma gleast_Upper_above: - fixes L (structure) - shows "[| gleast L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s" - by (unfold gleast_def) blast - -lemma ggreatest_closed [intro, simp]: - "ggreatest L l A ==> l \<in> carrier L" - by (unfold ggreatest_def) fast - -lemma ggreatest_mem: - "ggreatest L l A ==> l \<in> A" - by (unfold ggreatest_def) fast - -lemma (in gpartial_order) ggreatest_unique: - "[| ggreatest L x A; ggreatest L y A |] ==> x .= y" - by (unfold ggreatest_def) blast - -lemma ggreatest_le: - fixes L (structure) - shows "[| ggreatest L x A; a \<in> A |] ==> a \<sqsubseteq> x" - by (unfold ggreatest_def) fast - -lemma (in gpartial_order) ggreatest_cong: - "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> - ggreatest L x A = ggreatest L x' A" - by (unfold ggreatest_def) (auto dest: sym) - -text {* @{const ggreatest} is not congruent in the second parameter for - @{term [locale=gpartial_order] "A {.=} A'"} *} - -lemma (in gpartial_order) ggreatest_Lower_cong_l: - assumes "x .= x'" - and "x \<in> carrier L" "x' \<in> carrier L" - and "A \<subseteq> carrier L" (* unneccessary with current Lower *) - shows "ggreatest L x (Lower L A) = ggreatest L x' (Lower L A)" - apply (rule ggreatest_cong) using assms by auto - -lemma (in gpartial_order) ggreatest_Lower_cong_r: - assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" - and AA': "A {.=} A'" - shows "ggreatest L x (Lower L A) = ggreatest L x (Lower L A')" -apply (subgoal_tac "Lower L A = Lower L A'", simp) -by (rule Lower_cong) fact+ - -lemma ggreatest_LowerI: - fixes L (structure) - assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" - and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i" - and L: "A \<subseteq> carrier L" "i \<in> carrier L" - shows "ggreatest L i (Lower L A)" -proof - - have "Lower L A \<subseteq> carrier L" by simp - moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def) - moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast - ultimately show ?thesis by (simp add: ggreatest_def) -qed - -lemma ggreatest_Lower_below: - fixes L (structure) - shows "[| ggreatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x" - by (unfold ggreatest_def) blast - -text {* Supremum and infimum *} - -constdefs (structure L) - gsup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) - "\<Squnion>A == SOME x. gleast L x (Upper L A)" - - ginf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) - "\<Sqinter>A == SOME x. ggreatest L x (Lower L A)" - - gjoin :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) - "x \<squnion> y == \<Squnion> {x, y}" - - gmeet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) - "x \<sqinter> y == \<Sqinter> {x, y}" - - -subsection {* Lattices *} - -locale gupper_semilattice = gpartial_order + - assumes gsup_of_two_exists: - "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. gleast L s (Upper L {x, y})" - -locale glower_semilattice = gpartial_order + - assumes ginf_of_two_exists: - "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. ggreatest L s (Lower L {x, y})" - -locale glattice = gupper_semilattice + glower_semilattice - - -subsubsection {* Supremum *} - -lemma (in gupper_semilattice) gjoinI: - "[| !!l. gleast L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |] - ==> P (x \<squnion> y)" -proof (unfold gjoin_def gsup_def) - assume L: "x \<in> carrier L" "y \<in> carrier L" - and P: "!!l. gleast L l (Upper L {x, y}) ==> P l" - with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast - with L show "P (SOME l. gleast L l (Upper L {x, y}))" - by (fast intro: someI2 P) -qed - -lemma (in gupper_semilattice) gjoin_closed [simp]: - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L" - by (rule gjoinI) (rule gleast_closed) - -lemma (in gupper_semilattice) gjoin_cong_l: - assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" - and xx': "x .= x'" - shows "x \<squnion> y .= x' \<squnion> y" -proof (rule gjoinI, rule gjoinI) - fix a b - from xx' carr - have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) - - assume gleasta: "gleast L a (Upper L {x, y})" - assume "gleast L b (Upper L {x', y})" - with carr - have gleastb: "gleast L b (Upper L {x, y})" - by (simp add: gleast_Upper_cong_r[OF _ _ seq]) - - from gleasta gleastb - show "a .= b" by (rule gleast_unique) -qed (rule carr)+ - -lemma (in gupper_semilattice) gjoin_cong_r: - assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" - and yy': "y .= y'" - shows "x \<squnion> y .= x \<squnion> y'" -proof (rule gjoinI, rule gjoinI) - fix a b - have "{x, y} = {y, x}" by fast - also from carr yy' - have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) - also have "{y', x} = {x, y'}" by fast - finally - have seq: "{x, y} {.=} {x, y'}" . - - assume gleasta: "gleast L a (Upper L {x, y})" - assume "gleast L b (Upper L {x, y'})" - with carr - have gleastb: "gleast L b (Upper L {x, y})" - by (simp add: gleast_Upper_cong_r[OF _ _ seq]) - - from gleasta gleastb - show "a .= b" by (rule gleast_unique) -qed (rule carr)+ - -lemma (in gpartial_order) gsup_of_singletonI: (* only reflexivity needed ? *) - "x \<in> carrier L ==> gleast L x (Upper L {x})" - by (rule gleast_UpperI) auto - -lemma (in gpartial_order) gsup_of_singleton [simp]: - "x \<in> carrier L ==> \<Squnion>{x} .= x" - unfolding gsup_def - by (rule someI2) (auto intro: gleast_unique gsup_of_singletonI) - -lemma (in gpartial_order) gsup_of_singleton_closed [simp]: - "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L" - unfolding gsup_def - by (rule someI2) (auto intro: gsup_of_singletonI) - -text {* Condition on @{text A}: supremum exists. *} - -lemma (in gupper_semilattice) gsup_insertI: - "[| !!s. gleast L s (Upper L (insert x A)) ==> P s; - gleast L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |] - ==> P (\<Squnion>(insert x A))" -proof (unfold gsup_def) - assume L: "x \<in> carrier L" "A \<subseteq> carrier L" - and P: "!!l. gleast L l (Upper L (insert x A)) ==> P l" - and gleast_a: "gleast L a (Upper L A)" - from L gleast_a have La: "a \<in> carrier L" by simp - from L gsup_of_two_exists gleast_a - obtain s where gleast_s: "gleast L s (Upper L {a, x})" by blast - show "P (SOME l. gleast L l (Upper L (insert x A)))" - proof (rule someI2) - show "gleast L s (Upper L (insert x A))" - proof (rule gleast_UpperI) - fix z - assume "z \<in> insert x A" - then show "z \<sqsubseteq> s" - proof - assume "z = x" then show ?thesis - by (simp add: gleast_Upper_above [OF gleast_s] L La) - next - assume "z \<in> A" - with L gleast_s gleast_a show ?thesis - by (rule_tac le_trans [where y = a]) (auto dest: gleast_Upper_above) - qed - next - fix y - assume y: "y \<in> Upper L (insert x A)" - show "s \<sqsubseteq> y" - proof (rule gleast_le [OF gleast_s], rule Upper_memI) - fix z - assume z: "z \<in> {a, x}" - then show "z \<sqsubseteq> y" - proof - have y': "y \<in> Upper L A" - apply (rule subsetD [where A = "Upper L (insert x A)"]) - apply (rule Upper_antimono) - apply blast - apply (rule y) - done - assume "z = a" - with y' gleast_a show ?thesis by (fast dest: gleast_le) - next - assume "z \<in> {x}" (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *) - with y L show ?thesis by blast - qed - qed (rule Upper_closed [THEN subsetD, OF y]) - next - from L show "insert x A \<subseteq> carrier L" by simp - from gleast_s show "s \<in> carrier L" by simp - qed - qed (rule P) -qed - -lemma (in gupper_semilattice) finite_gsup_gleast: - "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> gleast L (\<Squnion>A) (Upper L A)" -proof (induct set: finite) - case empty - then show ?case by simp -next - case (insert x A) - show ?case - proof (cases "A = {}") - case True - with insert show ?thesis - by simp (simp add: gleast_cong [OF gsup_of_singleton] - gsup_of_singleton_closed gsup_of_singletonI) - (* The above step is hairy; gleast_cong can make simp loop. - Would want special version of simp to apply gleast_cong. *) - next - case False - with insert have "gleast L (\<Squnion>A) (Upper L A)" by simp - with _ show ?thesis - by (rule gsup_insertI) (simp_all add: insert [simplified]) - qed -qed - -lemma (in gupper_semilattice) finite_gsup_insertI: - assumes P: "!!l. gleast L l (Upper L (insert x A)) ==> P l" - and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" - shows "P (\<Squnion> (insert x A))" -proof (cases "A = {}") - case True with P and xA show ?thesis - by (simp add: finite_gsup_gleast) -next - case False with P and xA show ?thesis - by (simp add: gsup_insertI finite_gsup_gleast) -qed - -lemma (in gupper_semilattice) finite_gsup_closed [simp]: - "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L" -proof (induct set: finite) - case empty then show ?case by simp -next - case insert then show ?case - by - (rule finite_gsup_insertI, simp_all) -qed - -lemma (in gupper_semilattice) gjoin_left: - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" - by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem) - -lemma (in gupper_semilattice) gjoin_right: - "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" - by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem) - -lemma (in gupper_semilattice) gsup_of_two_gleast: - "[| x \<in> carrier L; y \<in> carrier L |] ==> gleast L (\<Squnion>{x, y}) (Upper L {x, y})" -proof (unfold gsup_def) - assume L: "x \<in> carrier L" "y \<in> carrier L" - with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast - with L show "gleast L (SOME z. gleast L z (Upper L {x, y})) (Upper L {x, y})" - by (fast intro: someI2 gleast_unique) (* blast fails *) -qed - -lemma (in gupper_semilattice) gjoin_le: - assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" - and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" - shows "x \<squnion> y \<sqsubseteq> z" -proof (rule gjoinI [OF _ x y]) - fix s - assume "gleast L s (Upper L {x, y})" - with sub z show "s \<sqsubseteq> z" by (fast elim: gleast_le intro: Upper_memI) -qed - -lemma (in gupper_semilattice) gjoin_assoc_lemma: - assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" - shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}" -proof (rule finite_gsup_insertI) - -- {* The textbook argument in Jacobson I, p 457 *} - fix s - assume gsup: "gleast L s (Upper L {x, y, z})" - show "x \<squnion> (y \<squnion> z) .= s" - proof (rule le_anti_sym) - from gsup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" - by (fastsimp intro!: gjoin_le elim: gleast_Upper_above) - next - from gsup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)" - by (erule_tac gleast_le) - (blast intro!: Upper_memI intro: le_trans gjoin_left gjoin_right gjoin_closed) - qed (simp_all add: L gleast_closed [OF gsup]) -qed (simp_all add: L) - -text {* Commutativity holds for @{text "="}. *} - -lemma gjoin_comm: - fixes L (structure) - shows "x \<squnion> y = y \<squnion> x" - by (unfold gjoin_def) (simp add: insert_commute) - -lemma (in gupper_semilattice) gjoin_assoc: - assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" - shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)" -proof - - (* FIXME: could be simplified by improved simp: uniform use of .=, - omit [symmetric] in last step. *) - have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: gjoin_comm) - also from L have "... .= \<Squnion>{z, x, y}" by (simp add: gjoin_assoc_lemma) - also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute) - also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: gjoin_assoc_lemma [symmetric]) - finally show ?thesis by (simp add: L) -qed - - -subsubsection {* Infimum *} - -lemma (in glower_semilattice) gmeetI: - "[| !!i. ggreatest L i (Lower L {x, y}) ==> P i; - x \<in> carrier L; y \<in> carrier L |] - ==> P (x \<sqinter> y)" -proof (unfold gmeet_def ginf_def) - assume L: "x \<in> carrier L" "y \<in> carrier L" - and P: "!!g. ggreatest L g (Lower L {x, y}) ==> P g" - with ginf_of_two_exists obtain i where "ggreatest L i (Lower L {x, y})" by fast - with L show "P (SOME g. ggreatest L g (Lower L {x, y}))" - by (fast intro: someI2 ggreatest_unique P) -qed - -lemma (in glower_semilattice) gmeet_closed [simp]: - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L" - by (rule gmeetI) (rule ggreatest_closed) - -lemma (in glower_semilattice) gmeet_cong_l: - assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" - and xx': "x .= x'" - shows "x \<sqinter> y .= x' \<sqinter> y" -proof (rule gmeetI, rule gmeetI) - fix a b - from xx' carr - have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) - - assume ggreatesta: "ggreatest L a (Lower L {x, y})" - assume "ggreatest L b (Lower L {x', y})" - with carr - have ggreatestb: "ggreatest L b (Lower L {x, y})" - by (simp add: ggreatest_Lower_cong_r[OF _ _ seq]) - - from ggreatesta ggreatestb - show "a .= b" by (rule ggreatest_unique) -qed (rule carr)+ - -lemma (in glower_semilattice) gmeet_cong_r: - assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" - and yy': "y .= y'" - shows "x \<sqinter> y .= x \<sqinter> y'" -proof (rule gmeetI, rule gmeetI) - fix a b - have "{x, y} = {y, x}" by fast - also from carr yy' - have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) - also have "{y', x} = {x, y'}" by fast - finally - have seq: "{x, y} {.=} {x, y'}" . - - assume ggreatesta: "ggreatest L a (Lower L {x, y})" - assume "ggreatest L b (Lower L {x, y'})" - with carr - have ggreatestb: "ggreatest L b (Lower L {x, y})" - by (simp add: ggreatest_Lower_cong_r[OF _ _ seq]) - - from ggreatesta ggreatestb - show "a .= b" by (rule ggreatest_unique) -qed (rule carr)+ - -lemma (in gpartial_order) ginf_of_singletonI: (* only reflexivity needed ? *) - "x \<in> carrier L ==> ggreatest L x (Lower L {x})" - by (rule ggreatest_LowerI) auto - -lemma (in gpartial_order) ginf_of_singleton [simp]: - "x \<in> carrier L ==> \<Sqinter>{x} .= x" - unfolding ginf_def - by (rule someI2) (auto intro: ggreatest_unique ginf_of_singletonI) - -lemma (in gpartial_order) ginf_of_singleton_closed: - "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L" - unfolding ginf_def - by (rule someI2) (auto intro: ginf_of_singletonI) - -text {* Condition on @{text A}: infimum exists. *} - -lemma (in glower_semilattice) ginf_insertI: - "[| !!i. ggreatest L i (Lower L (insert x A)) ==> P i; - ggreatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] - ==> P (\<Sqinter>(insert x A))" -proof (unfold ginf_def) - assume L: "x \<in> carrier L" "A \<subseteq> carrier L" - and P: "!!g. ggreatest L g (Lower L (insert x A)) ==> P g" - and ggreatest_a: "ggreatest L a (Lower L A)" - from L ggreatest_a have La: "a \<in> carrier L" by simp - from L ginf_of_two_exists ggreatest_a - obtain i where ggreatest_i: "ggreatest L i (Lower L {a, x})" by blast - show "P (SOME g. ggreatest L g (Lower L (insert x A)))" - proof (rule someI2) - show "ggreatest L i (Lower L (insert x A))" - proof (rule ggreatest_LowerI) - fix z - assume "z \<in> insert x A" - then show "i \<sqsubseteq> z" - proof - assume "z = x" then show ?thesis - by (simp add: ggreatest_Lower_below [OF ggreatest_i] L La) - next - assume "z \<in> A" - with L ggreatest_i ggreatest_a show ?thesis - by (rule_tac le_trans [where y = a]) (auto dest: ggreatest_Lower_below) - qed - next - fix y - assume y: "y \<in> Lower L (insert x A)" - show "y \<sqsubseteq> i" - proof (rule ggreatest_le [OF ggreatest_i], rule Lower_memI) - fix z - assume z: "z \<in> {a, x}" - then show "y \<sqsubseteq> z" - proof - have y': "y \<in> Lower L A" - apply (rule subsetD [where A = "Lower L (insert x A)"]) - apply (rule Lower_antimono) - apply blast - apply (rule y) - done - assume "z = a" - with y' ggreatest_a show ?thesis by (fast dest: ggreatest_le) - next - assume "z \<in> {x}" - with y L show ?thesis by blast - qed - qed (rule Lower_closed [THEN subsetD, OF y]) - next - from L show "insert x A \<subseteq> carrier L" by simp - from ggreatest_i show "i \<in> carrier L" by simp - qed - qed (rule P) -qed - -lemma (in glower_semilattice) finite_ginf_ggreatest: - "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> ggreatest L (\<Sqinter>A) (Lower L A)" -proof (induct set: finite) - case empty then show ?case by simp -next - case (insert x A) - show ?case - proof (cases "A = {}") - case True - with insert show ?thesis - by simp (simp add: ggreatest_cong [OF ginf_of_singleton] - ginf_of_singleton_closed ginf_of_singletonI) - next - case False - from insert show ?thesis - proof (rule_tac ginf_insertI) - from False insert show "ggreatest L (\<Sqinter>A) (Lower L A)" by simp - qed simp_all - qed -qed - -lemma (in glower_semilattice) finite_ginf_insertI: - assumes P: "!!i. ggreatest L i (Lower L (insert x A)) ==> P i" - and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" - shows "P (\<Sqinter> (insert x A))" -proof (cases "A = {}") - case True with P and xA show ?thesis - by (simp add: finite_ginf_ggreatest) -next - case False with P and xA show ?thesis - by (simp add: ginf_insertI finite_ginf_ggreatest) -qed - -lemma (in glower_semilattice) finite_ginf_closed [simp]: - "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L" -proof (induct set: finite) - case empty then show ?case by simp -next - case insert then show ?case - by (rule_tac finite_ginf_insertI) (simp_all) -qed - -lemma (in glower_semilattice) gmeet_left: - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" - by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem) - -lemma (in glower_semilattice) gmeet_right: - "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" - by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem) - -lemma (in glower_semilattice) ginf_of_two_ggreatest: - "[| x \<in> carrier L; y \<in> carrier L |] ==> - ggreatest L (\<Sqinter> {x, y}) (Lower L {x, y})" -proof (unfold ginf_def) - assume L: "x \<in> carrier L" "y \<in> carrier L" - with ginf_of_two_exists obtain s where "ggreatest L s (Lower L {x, y})" by fast - with L - show "ggreatest L (SOME z. ggreatest L z (Lower L {x, y})) (Lower L {x, y})" - by (fast intro: someI2 ggreatest_unique) (* blast fails *) -qed - -lemma (in glower_semilattice) gmeet_le: - assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" - and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" - shows "z \<sqsubseteq> x \<sqinter> y" -proof (rule gmeetI [OF _ x y]) - fix i - assume "ggreatest L i (Lower L {x, y})" - with sub z show "z \<sqsubseteq> i" by (fast elim: ggreatest_le intro: Lower_memI) -qed - -lemma (in glower_semilattice) gmeet_assoc_lemma: - assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" - shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}" -proof (rule finite_ginf_insertI) - txt {* The textbook argument in Jacobson I, p 457 *} - fix i - assume ginf: "ggreatest L i (Lower L {x, y, z})" - show "x \<sqinter> (y \<sqinter> z) .= i" - proof (rule le_anti_sym) - from ginf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" - by (fastsimp intro!: gmeet_le elim: ggreatest_Lower_below) - next - from ginf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" - by (erule_tac ggreatest_le) - (blast intro!: Lower_memI intro: le_trans gmeet_left gmeet_right gmeet_closed) - qed (simp_all add: L ggreatest_closed [OF ginf]) -qed (simp_all add: L) - -lemma gmeet_comm: - fixes L (structure) - shows "x \<sqinter> y = y \<sqinter> x" - by (unfold gmeet_def) (simp add: insert_commute) - -lemma (in glower_semilattice) gmeet_assoc: - assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" - shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)" -proof - - (* FIXME: improved simp, see gjoin_assoc above *) - have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: gmeet_comm) - also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: gmeet_assoc_lemma) - also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute) - also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: gmeet_assoc_lemma [symmetric]) - finally show ?thesis by (simp add: L) -qed - - -subsection {* Total Orders *} - -locale gtotal_order = gpartial_order + - assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" - -text {* Introduction rule: the usual definition of total order *} - -lemma (in gpartial_order) gtotal_orderI: - assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" - shows "gtotal_order L" - by unfold_locales (rule total) - -text {* Total orders are lattices. *} - -interpretation gtotal_order < glattice -proof unfold_locales - fix x y - assume L: "x \<in> carrier L" "y \<in> carrier L" - show "EX s. gleast L s (Upper L {x, y})" - proof - - note total L - moreover - { - assume "x \<sqsubseteq> y" - with L have "gleast L y (Upper L {x, y})" - by (rule_tac gleast_UpperI) auto - } - moreover - { - assume "y \<sqsubseteq> x" - with L have "gleast L x (Upper L {x, y})" - by (rule_tac gleast_UpperI) auto - } - ultimately show ?thesis by blast - qed -next - fix x y - assume L: "x \<in> carrier L" "y \<in> carrier L" - show "EX i. ggreatest L i (Lower L {x, y})" - proof - - note total L - moreover - { - assume "y \<sqsubseteq> x" - with L have "ggreatest L y (Lower L {x, y})" - by (rule_tac ggreatest_LowerI) auto - } - moreover - { - assume "x \<sqsubseteq> y" - with L have "ggreatest L x (Lower L {x, y})" - by (rule_tac ggreatest_LowerI) auto - } - ultimately show ?thesis by blast - qed -qed - - -subsection {* Complete lattices *} - -locale complete_lattice = glattice + - assumes gsup_exists: - "[| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)" - and ginf_exists: - "[| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)" - -text {* Introduction rule: the usual definition of complete lattice *} - -lemma (in gpartial_order) complete_latticeI: - assumes gsup_exists: - "!!A. [| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)" - and ginf_exists: - "!!A. [| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)" - shows "complete_lattice L" - by unfold_locales (auto intro: gsup_exists ginf_exists) - -constdefs (structure L) - top :: "_ => 'a" ("\<top>\<index>") - "\<top> == gsup L (carrier L)" - - bottom :: "_ => 'a" ("\<bottom>\<index>") - "\<bottom> == ginf L (carrier L)" - - -lemma (in complete_lattice) gsupI: - "[| !!l. gleast L l (Upper L A) ==> P l; A \<subseteq> carrier L |] - ==> P (\<Squnion>A)" -proof (unfold gsup_def) - assume L: "A \<subseteq> carrier L" - and P: "!!l. gleast L l (Upper L A) ==> P l" - with gsup_exists obtain s where "gleast L s (Upper L A)" by blast - with L show "P (SOME l. gleast L l (Upper L A))" - by (fast intro: someI2 gleast_unique P) -qed - -lemma (in complete_lattice) gsup_closed [simp]: - "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" - by (rule gsupI) simp_all - -lemma (in complete_lattice) top_closed [simp, intro]: - "\<top> \<in> carrier L" - by (unfold top_def) simp - -lemma (in complete_lattice) ginfI: - "[| !!i. ggreatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |] - ==> P (\<Sqinter>A)" -proof (unfold ginf_def) - assume L: "A \<subseteq> carrier L" - and P: "!!l. ggreatest L l (Lower L A) ==> P l" - with ginf_exists obtain s where "ggreatest L s (Lower L A)" by blast - with L show "P (SOME l. ggreatest L l (Lower L A))" - by (fast intro: someI2 ggreatest_unique P) -qed - -lemma (in complete_lattice) ginf_closed [simp]: - "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" - by (rule ginfI) simp_all - -lemma (in complete_lattice) bottom_closed [simp, intro]: - "\<bottom> \<in> carrier L" - by (unfold bottom_def) simp - -text {* Jacobson: Theorem 8.1 *} - -lemma Lower_empty [simp]: - "Lower L {} = carrier L" - by (unfold Lower_def) simp - -lemma Upper_empty [simp]: - "Upper L {} = carrier L" - by (unfold Upper_def) simp - -theorem (in gpartial_order) complete_lattice_criterion1: - assumes top_exists: "EX g. ggreatest L g (carrier L)" - and ginf_exists: - "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. ggreatest L i (Lower L A)" - shows "complete_lattice L" -proof (rule complete_latticeI) - from top_exists obtain top where top: "ggreatest L top (carrier L)" .. - fix A - assume L: "A \<subseteq> carrier L" - let ?B = "Upper L A" - from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: ggreatest_le) - then have B_non_empty: "?B ~= {}" by fast - have B_L: "?B \<subseteq> carrier L" by simp - from ginf_exists [OF B_L B_non_empty] - obtain b where b_ginf_B: "ggreatest L b (Lower L ?B)" .. - have "gleast L b (Upper L A)" -apply (rule gleast_UpperI) - apply (rule ggreatest_le [where A = "Lower L ?B"]) - apply (rule b_ginf_B) - apply (rule Lower_memI) - apply (erule Upper_memD [THEN conjunct1]) - apply assumption - apply (rule L) - apply (fast intro: L [THEN subsetD]) - apply (erule ggreatest_Lower_below [OF b_ginf_B]) - apply simp - apply (rule L) -apply (rule ggreatest_closed [OF b_ginf_B]) -done - then show "EX s. gleast L s (Upper L A)" .. -next - fix A - assume L: "A \<subseteq> carrier L" - show "EX i. ggreatest L i (Lower L A)" - proof (cases "A = {}") - case True then show ?thesis - by (simp add: top_exists) - next - case False with L show ?thesis - by (rule ginf_exists) - qed -qed - -(* TODO: prove dual version *) - - -subsection {* Examples *} - -(* Not so useful for the generalised version. - -subsubsection {* Powerset of a Set is a Complete Lattice *} - -theorem powerset_is_complete_lattice: - "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)" - (is "complete_lattice ?L") -proof (rule gpartial_order.complete_latticeI) - show "gpartial_order ?L" - by (rule gpartial_order.intro) auto -next - fix B - assume B: "B \<subseteq> carrier ?L" - show "EX s. gleast ?L s (Upper ?L B)" - proof - from B show "gleast ?L (\<Union> B) (Upper ?L B)" - by (fastsimp intro!: gleast_UpperI simp: Upper_def) - qed -next - fix B - assume B: "B \<subseteq> carrier ?L" - show "EX i. ggreatest ?L i (Lower ?L B)" - proof - from B show "ggreatest ?L (\<Inter> B \<inter> A) (Lower ?L B)" - txt {* @{term "\<Inter> B"} is not the infimum of @{term B}: - @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *} - by (fastsimp intro!: ggreatest_LowerI simp: Lower_def) - qed -qed - -text {* An other example, that of the lattice of subgroups of a group, - can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *} - -*) - -end

--- a/src/HOL/Algebra/Group.thy Wed Jul 30 16:07:00 2008 +0200 +++ b/src/HOL/Algebra/Group.thy Wed Jul 30 19:03:33 2008 +0200 @@ -712,8 +712,8 @@ text_raw {* \label{sec:subgroup-lattice} *} theorem (in group) subgroups_partial_order: - "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" - by (rule partial_order.intro) simp_all + "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)" + by unfold_locales simp_all lemma (in group) subgroup_self: "subgroup (carrier G) G" @@ -757,7 +757,7 @@ qed theorem (in group) subgroups_complete_lattice: - "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)" + "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)" (is "complete_lattice ?L") proof (rule partial_order.complete_lattice_criterion1) show "partial_order ?L" by (rule subgroups_partial_order)

--- a/src/HOL/Algebra/IntRing.thy Wed Jul 30 16:07:00 2008 +0200 +++ b/src/HOL/Algebra/IntRing.thy Wed Jul 30 19:03:33 2008 +0200 @@ -208,27 +208,27 @@ by simp_all interpretation int [unfolded UNIV]: - partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"] - where "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV" - and "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)" - and "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)" + partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"] + where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV" + and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)" + and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)" proof - - show "partial_order (| carrier = UNIV::int set, le = op \<le> |)" + show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)" by unfold_locales simp_all - show "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV" + show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV" by simp - show "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)" + show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)" by simp - show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)" + show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)" by (simp add: lless_def) auto qed interpretation int [unfolded UNIV]: - lattice ["(| carrier = UNIV::int set, le = op \<le> |)"] - where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y" - and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y" + lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"] + where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y" + and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y" proof - - let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)" + let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)" show "lattice ?Z" apply unfold_locales apply (simp add: least_def Upper_def) @@ -250,7 +250,7 @@ qed interpretation int [unfolded UNIV]: - total_order ["(| carrier = UNIV::int set, le = op \<le> |)"] + total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"] by unfold_locales clarsimp

--- a/src/HOL/Algebra/Lattice.thy Wed Jul 30 16:07:00 2008 +0200 +++ b/src/HOL/Algebra/Lattice.thy Wed Jul 30 19:03:33 2008 +0200 @@ -1,5 +1,5 @@ (* - Title: HOL/Algebra/Lattice.thy + Title: HOL/Algebra/GLattice.thy Id: $Id$ Author: Clemens Ballarin, started 7 November 2003 Copyright: Clemens Ballarin @@ -7,88 +7,202 @@ theory Lattice imports Congruence begin - section {* Orders and Lattices *} subsection {* Partial Orders *} -record 'a order = "'a partial_object" + +record 'a gorder = "'a eq_object" + le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50) -locale partial_order = - fixes L (structure) - assumes refl [intro, simp]: - "x \<in> carrier L ==> x \<sqsubseteq> x" - and anti_sym [intro]: - "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y" - and trans [trans]: - "[| x \<sqsubseteq> y; y \<sqsubseteq> z; - x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z" +locale weak_partial_order = equivalence L + + assumes le_refl [intro, simp]: + "x \<in> carrier L ==> x \<sqsubseteq> x" + and weak_le_anti_sym [intro]: + "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y" + and le_trans [trans]: + "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z" + and le_cong: + "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w" constdefs (structure L) lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50) - "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y" + "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y" + + +subsubsection {* The order relation *} + +context weak_partial_order begin + +lemma le_cong_l [intro, trans]: + "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" + by (auto intro: le_cong [THEN iffD2]) + +lemma le_cong_r [intro, trans]: + "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z" + by (auto intro: le_cong [THEN iffD1]) + +lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y" + by (simp add: le_cong_l) + +end + +lemma weak_llessI: + fixes R (structure) + assumes "x \<sqsubseteq> y" and "~(x .= y)" + shows "x \<sqsubset> y" + using assms unfolding lless_def by simp + +lemma lless_imp_le: + fixes R (structure) + assumes "x \<sqsubset> y" + shows "x \<sqsubseteq> y" + using assms unfolding lless_def by simp + +lemma weak_lless_imp_not_eq: + fixes R (structure) + assumes "x \<sqsubset> y" + shows "\<not> (x .= y)" + using assms unfolding lless_def by simp - -- {* Upper and lower bounds of a set. *} +lemma weak_llessE: + fixes R (structure) + assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P" + shows "P" + using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e) + +lemma (in weak_partial_order) lless_cong_l [trans]: + assumes xx': "x .= x'" + and xy: "x' \<sqsubset> y" + and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" + shows "x \<sqsubset> y" + using assms unfolding lless_def by (auto intro: trans sym) + +lemma (in weak_partial_order) lless_cong_r [trans]: + assumes xy: "x \<sqsubset> y" + and yy': "y .= y'" + and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" + shows "x \<sqsubset> y'" + using assms unfolding lless_def by (auto intro: trans sym) + + +lemma (in weak_partial_order) lless_antisym: + assumes "a \<in> carrier L" "b \<in> carrier L" + and "a \<sqsubset> b" "b \<sqsubset> a" + shows "P" + using assms + by (elim weak_llessE) auto + +lemma (in weak_partial_order) lless_trans [trans]: + assumes "a \<sqsubset> b" "b \<sqsubset> c" + and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L" + shows "a \<sqsubset> c" + using assms unfolding lless_def by (blast dest: le_trans intro: sym) + + +subsubsection {* Upper and lower bounds of a set *} + +constdefs (structure L) Upper :: "[_, 'a set] => 'a set" - "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> - carrier L" + "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L" Lower :: "[_, 'a set] => 'a set" - "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> - carrier L" - - -- {* Least and greatest, as predicate. *} - least :: "[_, 'a, 'a set] => bool" - "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" - - greatest :: "[_, 'a, 'a set] => bool" - "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" - - -- {* Supremum and infimum *} - sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) - "\<Squnion>A == THE x. least L x (Upper L A)" + "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L" - inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) - "\<Sqinter>A == THE x. greatest L x (Lower L A)" - - join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) - "x \<squnion> y == sup L {x, y}" - - meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) - "x \<sqinter> y == inf L {x, y}" - - -subsubsection {* Upper *} - -lemma Upper_closed [intro, simp]: +lemma Upper_closed [intro!, simp]: "Upper L A \<subseteq> carrier L" by (unfold Upper_def) clarify lemma Upper_memD [dest]: fixes L (structure) - shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u" + shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L" by (unfold Upper_def) blast +lemma (in weak_partial_order) Upper_elemD [dest]: + "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u" + unfolding Upper_def elem_def + by (blast dest: sym) + lemma Upper_memI: fixes L (structure) shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A" by (unfold Upper_def) blast +lemma (in weak_partial_order) Upper_elemI: + "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A" + unfolding Upper_def by blast + lemma Upper_antimono: "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A" by (unfold Upper_def) blast +lemma (in weak_partial_order) Upper_is_closed [simp]: + "A \<subseteq> carrier L ==> is_closed (Upper L A)" + by (rule is_closedI) (blast intro: Upper_memI)+ -subsubsection {* Lower *} +lemma (in weak_partial_order) Upper_mem_cong: + assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L" + and aa': "a .= a'" + and aelem: "a \<in> Upper L A" + shows "a' \<in> Upper L A" +proof (rule Upper_memI[OF _ a'carr]) + fix y + assume yA: "y \<in> A" + hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr) + also note aa' + finally + show "y \<sqsubseteq> a'" + by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem]) +qed + +lemma (in weak_partial_order) Upper_cong: + assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L" + and AA': "A {.=} A'" + shows "Upper L A = Upper L A'" +unfolding Upper_def +apply rule + apply (rule, clarsimp) defer 1 + apply (rule, clarsimp) defer 1 +proof - + fix x a' + assume carr: "x \<in> carrier L" "a' \<in> carrier L" + and a'A': "a' \<in> A'" + assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x" -lemma Lower_closed [intro, simp]: + from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2) + from this obtain a + where aA: "a \<in> A" + and a'a: "a' .= a" + by auto + note [simp] = subsetD[OF Acarr aA] carr + + note a'a + also have "a \<sqsubseteq> x" by (simp add: aLxCond aA) + finally show "a' \<sqsubseteq> x" by simp +next + fix x a + assume carr: "x \<in> carrier L" "a \<in> carrier L" + and aA: "a \<in> A" + assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x" + + from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1) + from this obtain a' + where a'A': "a' \<in> A'" + and aa': "a .= a'" + by auto + note [simp] = subsetD[OF A'carr a'A'] carr + + note aa' + also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A') + finally show "a \<sqsubseteq> x" by simp +qed + +lemma Lower_closed [intro!, simp]: "Lower L A \<subseteq> carrier L" by (unfold Lower_def) clarify lemma Lower_memD [dest]: fixes L (structure) - shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x" + shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L" by (unfold Lower_def) blast lemma Lower_memI: @@ -100,19 +214,86 @@ "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A" by (unfold Lower_def) blast +lemma (in weak_partial_order) Lower_is_closed [simp]: + "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)" + by (rule is_closedI) (blast intro: Lower_memI dest: sym)+ -subsubsection {* least *} +lemma (in weak_partial_order) Lower_mem_cong: + assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L" + and aa': "a .= a'" + and aelem: "a \<in> Lower L A" + shows "a' \<in> Lower L A" +using assms Lower_closed[of L A] +by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]]) + +lemma (in weak_partial_order) Lower_cong: + assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L" + and AA': "A {.=} A'" + shows "Lower L A = Lower L A'" +using Lower_memD[of y] +unfolding Lower_def +apply safe + apply clarsimp defer 1 + apply clarsimp defer 1 +proof - + fix x a' + assume carr: "x \<in> carrier L" "a' \<in> carrier L" + and a'A': "a' \<in> A'" + assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a" + hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast + + from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2) + from this obtain a + where aA: "a \<in> A" + and a'a: "a' .= a" + by auto + + from aA and subsetD[OF Acarr aA] + have "x \<sqsubseteq> a" by (rule aLxCond) + also note a'a[symmetric] + finally + show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA]) +next + fix x a + assume carr: "x \<in> carrier L" "a \<in> carrier L" + and aA: "a \<in> A" + assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'" + hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+ + + from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1) + from this obtain a' + where a'A': "a' \<in> A'" + and aa': "a .= a'" + by auto + from a'A' and subsetD[OF A'carr a'A'] + have "x \<sqsubseteq> a'" by (rule a'LxCond) + also note aa'[symmetric] + finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A']) +qed + + +subsubsection {* Least and greatest, as predicate *} + +constdefs (structure L) + least :: "[_, 'a, 'a set] => bool" + "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)" + + greatest :: "[_, 'a, 'a set] => bool" + "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)" + +text {* Could weaken these to @{term [locale=weak_partial_order] "l \<in> carrier L \<and> l + .\<in> A"} and @{term [locale=weak_partial_order] "g \<in> carrier L \<and> g .\<in> A"}. *} lemma least_closed [intro, simp]: - shows "least L l A ==> l \<in> carrier L" + "least L l A ==> l \<in> carrier L" by (unfold least_def) fast lemma least_mem: "least L l A ==> l \<in> A" by (unfold least_def) fast -lemma (in partial_order) least_unique: - "[| least L x A; least L y A |] ==> x = y" +lemma (in weak_partial_order) weak_least_unique: + "[| least L x A; least L y A |] ==> x .= y" by (unfold least_def) blast lemma least_le: @@ -120,6 +301,27 @@ shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a" by (unfold least_def) fast +lemma (in weak_partial_order) least_cong: + "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A" + by (unfold least_def) (auto dest: sym) + +text {* @{const least} is not congruent in the second parameter for + @{term [locale=weak_partial_order] "A {.=} A'"} *} + +lemma (in weak_partial_order) least_Upper_cong_l: + assumes "x .= x'" + and "x \<in> carrier L" "x' \<in> carrier L" + and "A \<subseteq> carrier L" + shows "least L x (Upper L A) = least L x' (Upper L A)" + apply (rule least_cong) using assms by auto + +lemma (in weak_partial_order) least_Upper_cong_r: + assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *) + and AA': "A {.=} A'" + shows "least L x (Upper L A) = least L x (Upper L A')" +apply (subgoal_tac "Upper L A = Upper L A'", simp) +by (rule Upper_cong) fact+ + lemma least_UpperI: fixes L (structure) assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s" @@ -133,19 +335,21 @@ ultimately show ?thesis by (simp add: least_def) qed - -subsubsection {* greatest *} +lemma least_Upper_above: + fixes L (structure) + shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s" + by (unfold least_def) blast lemma greatest_closed [intro, simp]: - shows "greatest L l A ==> l \<in> carrier L" + "greatest L l A ==> l \<in> carrier L" by (unfold greatest_def) fast lemma greatest_mem: "greatest L l A ==> l \<in> A" by (unfold greatest_def) fast -lemma (in partial_order) greatest_unique: - "[| greatest L x A; greatest L y A |] ==> x = y" +lemma (in weak_partial_order) weak_greatest_unique: + "[| greatest L x A; greatest L y A |] ==> x .= y" by (unfold greatest_def) blast lemma greatest_le: @@ -153,6 +357,28 @@ shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x" by (unfold greatest_def) fast +lemma (in weak_partial_order) greatest_cong: + "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> + greatest L x A = greatest L x' A" + by (unfold greatest_def) (auto dest: sym) + +text {* @{const greatest} is not congruent in the second parameter for + @{term [locale=weak_partial_order] "A {.=} A'"} *} + +lemma (in weak_partial_order) greatest_Lower_cong_l: + assumes "x .= x'" + and "x \<in> carrier L" "x' \<in> carrier L" + and "A \<subseteq> carrier L" (* unneccessary with current Lower *) + shows "greatest L x (Lower L A) = greatest L x' (Lower L A)" + apply (rule greatest_cong) using assms by auto + +lemma (in weak_partial_order) greatest_Lower_cong_r: + assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" + and AA': "A {.=} A'" + shows "greatest L x (Lower L A) = greatest L x (Lower L A')" +apply (subgoal_tac "Lower L A = Lower L A'", simp) +by (rule Lower_cong) fact+ + lemma greatest_LowerI: fixes L (structure) assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x" @@ -166,55 +392,116 @@ ultimately show ?thesis by (simp add: greatest_def) qed - -subsection {* Lattices *} - -locale lattice = partial_order + - assumes sup_of_two_exists: - "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" - and inf_of_two_exists: - "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" - -lemma least_Upper_above: - fixes L (structure) - shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s" - by (unfold least_def) blast - lemma greatest_Lower_below: fixes L (structure) shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x" by (unfold greatest_def) blast +text {* Supremum and infimum *} + +constdefs (structure L) + sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90) + "\<Squnion>A == SOME x. least L x (Upper L A)" + + inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90) + "\<Sqinter>A == SOME x. greatest L x (Lower L A)" + + join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65) + "x \<squnion> y == \<Squnion> {x, y}" + + meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70) + "x \<sqinter> y == \<Sqinter> {x, y}" + + +subsection {* Lattices *} + +locale weak_upper_semilattice = weak_partial_order + + assumes sup_of_two_exists: + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" + +locale weak_lower_semilattice = weak_partial_order + + assumes inf_of_two_exists: + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" + +locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice + subsubsection {* Supremum *} -lemma (in lattice) joinI: +lemma (in weak_upper_semilattice) joinI: "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |] ==> P (x \<squnion> y)" proof (unfold join_def sup_def) assume L: "x \<in> carrier L" "y \<in> carrier L" and P: "!!l. least L l (Upper L {x, y}) ==> P l" with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast - with L show "P (THE l. least L l (Upper L {x, y}))" - by (fast intro: theI2 least_unique P) + with L show "P (SOME l. least L l (Upper L {x, y}))" + by (fast intro: someI2 P) qed -lemma (in lattice) join_closed [simp]: +lemma (in weak_upper_semilattice) join_closed [simp]: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L" by (rule joinI) (rule least_closed) -lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) - "x \<in> carrier L ==> least L x (Upper L {x})" - by (rule least_UpperI) fast+ +lemma (in weak_upper_semilattice) join_cong_l: + assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" + and xx': "x .= x'" + shows "x \<squnion> y .= x' \<squnion> y" +proof (rule joinI, rule joinI) + fix a b + from xx' carr + have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) + + assume leasta: "least L a (Upper L {x, y})" + assume "least L b (Upper L {x', y})" + with carr + have leastb: "least L b (Upper L {x, y})" + by (simp add: least_Upper_cong_r[OF _ _ seq]) + + from leasta leastb + show "a .= b" by (rule weak_least_unique) +qed (rule carr)+ -lemma (in partial_order) sup_of_singleton [simp]: - "x \<in> carrier L ==> \<Squnion>{x} = x" - by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) +lemma (in weak_upper_semilattice) join_cong_r: + assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" + and yy': "y .= y'" + shows "x \<squnion> y .= x \<squnion> y'" +proof (rule joinI, rule joinI) + fix a b + have "{x, y} = {y, x}" by fast + also from carr yy' + have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) + also have "{y', x} = {x, y'}" by fast + finally + have seq: "{x, y} {.=} {x, y'}" . + assume leasta: "least L a (Upper L {x, y})" + assume "least L b (Upper L {x, y'})" + with carr + have leastb: "least L b (Upper L {x, y})" + by (simp add: least_Upper_cong_r[OF _ _ seq]) + + from leasta leastb + show "a .= b" by (rule weak_least_unique) +qed (rule carr)+ + +lemma (in weak_partial_order) sup_of_singletonI: (* only reflexivity needed ? *) + "x \<in> carrier L ==> least L x (Upper L {x})" + by (rule least_UpperI) auto + +lemma (in weak_partial_order) weak_sup_of_singleton [simp]: + "x \<in> carrier L ==> \<Squnion>{x} .= x" + unfolding sup_def + by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI) + +lemma (in weak_partial_order) sup_of_singleton_closed [simp]: + "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L" + unfolding sup_def + by (rule someI2) (auto intro: sup_of_singletonI) text {* Condition on @{text A}: supremum exists. *} -lemma (in lattice) sup_insertI: +lemma (in weak_upper_semilattice) sup_insertI: "[| !!s. least L s (Upper L (insert x A)) ==> P s; least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |] ==> P (\<Squnion>(insert x A))" @@ -225,8 +512,8 @@ from L least_a have La: "a \<in> carrier L" by simp from L sup_of_two_exists least_a obtain s where least_s: "least L s (Upper L {a, x})" by blast - show "P (THE l. least L l (Upper L (insert x A)))" - proof (rule theI2) + show "P (SOME l. least L l (Upper L (insert x A)))" + proof (rule someI2) show "least L s (Upper L (insert x A))" proof (rule least_UpperI) fix z @@ -238,7 +525,7 @@ next assume "z \<in> A" with L least_s least_a show ?thesis - by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) + by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above) qed next fix y @@ -266,55 +553,10 @@ from L show "insert x A \<subseteq> carrier L" by simp from least_s show "s \<in> carrier L" by simp qed - next - fix l - assume least_l: "least L l (Upper L (insert x A))" - show "l = s" - proof (rule least_unique) - show "least L s (Upper L (insert x A))" - proof (rule least_UpperI) - fix z - assume "z \<in> insert x A" - then show "z \<sqsubseteq> s" - proof - assume "z = x" then show ?thesis - by (simp add: least_Upper_above [OF least_s] L La) - next - assume "z \<in> A" - with L least_s least_a show ?thesis - by (rule_tac trans [where y = a]) (auto dest: least_Upper_above) - qed - next - fix y - assume y: "y \<in> Upper L (insert x A)" - show "s \<sqsubseteq> y" - proof (rule least_le [OF least_s], rule Upper_memI) - fix z - assume z: "z \<in> {a, x}" - then show "z \<sqsubseteq> y" - proof - have y': "y \<in> Upper L A" - apply (rule subsetD [where A = "Upper L (insert x A)"]) - apply (rule Upper_antimono) - apply blast - apply (rule y) - done - assume "z = a" - with y' least_a show ?thesis by (fast dest: least_le) - next - assume "z \<in> {x}" - with y L show ?thesis by blast - qed - qed (rule Upper_closed [THEN subsetD, OF y]) - next - from L show "insert x A \<subseteq> carrier L" by simp - from least_s show "s \<in> carrier L" by simp - qed - qed (rule least_l) qed (rule P) qed -lemma (in lattice) finite_sup_least: +lemma (in weak_upper_semilattice) finite_sup_least: "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)" proof (induct set: finite) case empty @@ -324,7 +566,11 @@ show ?case proof (cases "A = {}") case True - with insert show ?thesis by (simp add: sup_of_singletonI) + with insert show ?thesis + by simp (simp add: least_cong [OF weak_sup_of_singleton] + sup_of_singleton_closed sup_of_singletonI) + (* The above step is hairy; least_cong can make simp loop. + Would want special version of simp to apply least_cong. *) next case False with insert have "least L (\<Squnion>A) (Upper L A)" by simp @@ -333,19 +579,19 @@ qed qed -lemma (in lattice) finite_sup_insertI: +lemma (in weak_upper_semilattice) finite_sup_insertI: assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l" and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" shows "P (\<Squnion> (insert x A))" proof (cases "A = {}") case True with P and xA show ?thesis - by (simp add: sup_of_singletonI) + by (simp add: finite_sup_least) next case False with P and xA show ?thesis by (simp add: sup_insertI finite_sup_least) qed -lemma (in lattice) finite_sup_closed: +lemma (in weak_upper_semilattice) finite_sup_closed [simp]: "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L" proof (induct set: finite) case empty then show ?case by simp @@ -354,24 +600,24 @@ by - (rule finite_sup_insertI, simp_all) qed -lemma (in lattice) join_left: +lemma (in weak_upper_semilattice) join_left: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y" by (rule joinI [folded join_def]) (blast dest: least_mem) -lemma (in lattice) join_right: +lemma (in weak_upper_semilattice) join_right: "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y" by (rule joinI [folded join_def]) (blast dest: least_mem) -lemma (in lattice) sup_of_two_least: +lemma (in weak_upper_semilattice) sup_of_two_least: "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})" proof (unfold sup_def) assume L: "x \<in> carrier L" "y \<in> carrier L" with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast - with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})" - by (fast intro: theI2 least_unique) (* blast fails *) + with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})" + by (fast intro: someI2 weak_least_unique) (* blast fails *) qed -lemma (in lattice) join_le: +lemma (in weak_upper_semilattice) join_le: assumes sub: "x \<sqsubseteq> z" "y \<sqsubseteq> z" and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" shows "x \<squnion> y \<sqsubseteq> z" @@ -381,44 +627,48 @@ with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI) qed -lemma (in lattice) join_assoc_lemma: +lemma (in weak_upper_semilattice) weak_join_assoc_lemma: assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" - shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" + shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}" proof (rule finite_sup_insertI) -- {* The textbook argument in Jacobson I, p 457 *} fix s assume sup: "least L s (Upper L {x, y, z})" - show "x \<squnion> (y \<squnion> z) = s" - proof (rule anti_sym) + show "x \<squnion> (y \<squnion> z) .= s" + proof (rule weak_le_anti_sym) from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s" by (fastsimp intro!: join_le elim: least_Upper_above) next from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)" by (erule_tac least_le) - (blast intro!: Upper_memI intro: trans join_left join_right join_closed) + (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed) qed (simp_all add: L least_closed [OF sup]) qed (simp_all add: L) +text {* Commutativity holds for @{text "="}. *} + lemma join_comm: fixes L (structure) shows "x \<squnion> y = y \<squnion> x" by (unfold join_def) (simp add: insert_commute) -lemma (in lattice) join_assoc: +lemma (in weak_upper_semilattice) weak_join_assoc: assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" - shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" + shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)" proof - + (* FIXME: could be simplified by improved simp: uniform use of .=, + omit [symmetric] in last step. *) have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm) - also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma) + also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma) also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute) - also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma) - finally show ?thesis . + also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric]) + finally show ?thesis by (simp add: L) qed subsubsection {* Infimum *} -lemma (in lattice) meetI: +lemma (in weak_lower_semilattice) meetI: "[| !!i. greatest L i (Lower L {x, y}) ==> P i; x \<in> carrier L; y \<in> carrier L |] ==> P (x \<sqinter> y)" @@ -426,25 +676,73 @@ assume L: "x \<in> carrier L" "y \<in> carrier L" and P: "!!g. greatest L g (Lower L {x, y}) ==> P g" with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast - with L show "P (THE g. greatest L g (Lower L {x, y}))" - by (fast intro: theI2 greatest_unique P) + with L show "P (SOME g. greatest L g (Lower L {x, y}))" + by (fast intro: someI2 weak_greatest_unique P) qed -lemma (in lattice) meet_closed [simp]: +lemma (in weak_lower_semilattice) meet_closed [simp]: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L" by (rule meetI) (rule greatest_closed) -lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) - "x \<in> carrier L ==> greatest L x (Lower L {x})" - by (rule greatest_LowerI) fast+ +lemma (in weak_lower_semilattice) meet_cong_l: + assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L" + and xx': "x .= x'" + shows "x \<sqinter> y .= x' \<sqinter> y" +proof (rule meetI, rule meetI) + fix a b + from xx' carr + have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI) + + assume greatesta: "greatest L a (Lower L {x, y})" + assume "greatest L b (Lower L {x', y})" + with carr + have greatestb: "greatest L b (Lower L {x, y})" + by (simp add: greatest_Lower_cong_r[OF _ _ seq]) + + from greatesta greatestb + show "a .= b" by (rule weak_greatest_unique) +qed (rule carr)+ -lemma (in partial_order) inf_of_singleton [simp]: - "x \<in> carrier L ==> \<Sqinter> {x} = x" - by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) +lemma (in weak_lower_semilattice) meet_cong_r: + assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L" + and yy': "y .= y'" + shows "x \<sqinter> y .= x \<sqinter> y'" +proof (rule meetI, rule meetI) + fix a b + have "{x, y} = {y, x}" by fast + also from carr yy' + have "{y, x} {.=} {y', x}" by (intro set_eq_pairI) + also have "{y', x} = {x, y'}" by fast + finally + have seq: "{x, y} {.=} {x, y'}" . + + assume greatesta: "greatest L a (Lower L {x, y})" + assume "greatest L b (Lower L {x, y'})" + with carr + have greatestb: "greatest L b (Lower L {x, y})" + by (simp add: greatest_Lower_cong_r[OF _ _ seq]) -text {* Condition on A: infimum exists. *} + from greatesta greatestb + show "a .= b" by (rule weak_greatest_unique) +qed (rule carr)+ + +lemma (in weak_partial_order) inf_of_singletonI: (* only reflexivity needed ? *) + "x \<in> carrier L ==> greatest L x (Lower L {x})" + by (rule greatest_LowerI) auto -lemma (in lattice) inf_insertI: +lemma (in weak_partial_order) weak_inf_of_singleton [simp]: + "x \<in> carrier L ==> \<Sqinter>{x} .= x" + unfolding inf_def + by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI) + +lemma (in weak_partial_order) inf_of_singleton_closed: + "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L" + unfolding inf_def + by (rule someI2) (auto intro: inf_of_singletonI) + +text {* Condition on @{text A}: infimum exists. *} + +lemma (in weak_lower_semilattice) inf_insertI: "[| !!i. greatest L i (Lower L (insert x A)) ==> P i; greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |] ==> P (\<Sqinter>(insert x A))" @@ -455,8 +753,8 @@ from L greatest_a have La: "a \<in> carrier L" by simp from L inf_of_two_exists greatest_a obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast - show "P (THE g. greatest L g (Lower L (insert x A)))" - proof (rule theI2) + show "P (SOME g. greatest L g (Lower L (insert x A)))" + proof (rule someI2) show "greatest L i (Lower L (insert x A))" proof (rule greatest_LowerI) fix z @@ -468,7 +766,7 @@ next assume "z \<in> A" with L greatest_i greatest_a show ?thesis - by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below) + by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below) qed next fix y @@ -496,55 +794,10 @@ from L show "insert x A \<subseteq> carrier L" by simp from greatest_i show "i \<in> carrier L" by simp qed - next - fix g - assume greatest_g: "greatest L g (Lower L (insert x A))" - show "g = i" - proof (rule greatest_unique) - show "greatest L i (Lower L (insert x A))" - proof (rule greatest_LowerI) - fix z - assume "z \<in> insert x A" - then show "i \<sqsubseteq> z" - proof - assume "z = x" then show ?thesis - by (simp add: greatest_Lower_below [OF greatest_i] L La) - next - assume "z \<in> A" - with L greatest_i greatest_a show ?thesis - by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below) - qed - next - fix y - assume y: "y \<in> Lower L (insert x A)" - show "y \<sqsubseteq> i" - proof (rule greatest_le [OF greatest_i], rule Lower_memI) - fix z - assume z: "z \<in> {a, x}" - then show "y \<sqsubseteq> z" - proof - have y': "y \<in> Lower L A" - apply (rule subsetD [where A = "Lower L (insert x A)"]) - apply (rule Lower_antimono) - apply blast - apply (rule y) - done - assume "z = a" - with y' greatest_a show ?thesis by (fast dest: greatest_le) - next - assume "z \<in> {x}" - with y L show ?thesis by blast - qed - qed (rule Lower_closed [THEN subsetD, OF y]) - next - from L show "insert x A \<subseteq> carrier L" by simp - from greatest_i show "i \<in> carrier L" by simp - qed - qed (rule greatest_g) qed (rule P) qed -lemma (in lattice) finite_inf_greatest: +lemma (in weak_lower_semilattice) finite_inf_greatest: "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)" proof (induct set: finite) case empty then show ?case by simp @@ -553,7 +806,9 @@ show ?case proof (cases "A = {}") case True - with insert show ?thesis by (simp add: inf_of_singletonI) + with insert show ?thesis + by simp (simp add: greatest_cong [OF weak_inf_of_singleton] + inf_of_singleton_closed inf_of_singletonI) next case False from insert show ?thesis @@ -563,19 +818,19 @@ qed qed -lemma (in lattice) finite_inf_insertI: +lemma (in weak_lower_semilattice) finite_inf_insertI: assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i" and xA: "finite A" "x \<in> carrier L" "A \<subseteq> carrier L" shows "P (\<Sqinter> (insert x A))" proof (cases "A = {}") case True with P and xA show ?thesis - by (simp add: inf_of_singletonI) + by (simp add: finite_inf_greatest) next case False with P and xA show ?thesis by (simp add: inf_insertI finite_inf_greatest) qed -lemma (in lattice) finite_inf_closed: +lemma (in weak_lower_semilattice) finite_inf_closed [simp]: "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L" proof (induct set: finite) case empty then show ?case by simp @@ -584,26 +839,26 @@ by (rule_tac finite_inf_insertI) (simp_all) qed -lemma (in lattice) meet_left: +lemma (in weak_lower_semilattice) meet_left: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x" by (rule meetI [folded meet_def]) (blast dest: greatest_mem) -lemma (in lattice) meet_right: +lemma (in weak_lower_semilattice) meet_right: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y" by (rule meetI [folded meet_def]) (blast dest: greatest_mem) -lemma (in lattice) inf_of_two_greatest: +lemma (in weak_lower_semilattice) inf_of_two_greatest: "[| x \<in> carrier L; y \<in> carrier L |] ==> greatest L (\<Sqinter> {x, y}) (Lower L {x, y})" proof (unfold inf_def) assume L: "x \<in> carrier L" "y \<in> carrier L" with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast with L - show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})" - by (fast intro: theI2 greatest_unique) (* blast fails *) + show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})" + by (fast intro: someI2 weak_greatest_unique) (* blast fails *) qed -lemma (in lattice) meet_le: +lemma (in weak_lower_semilattice) meet_le: assumes sub: "z \<sqsubseteq> x" "z \<sqsubseteq> y" and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L" shows "z \<sqsubseteq> x \<sqinter> y" @@ -613,21 +868,21 @@ with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI) qed -lemma (in lattice) meet_assoc_lemma: +lemma (in weak_lower_semilattice) weak_meet_assoc_lemma: assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" - shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" + shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}" proof (rule finite_inf_insertI) txt {* The textbook argument in Jacobson I, p 457 *} fix i assume inf: "greatest L i (Lower L {x, y, z})" - show "x \<sqinter> (y \<sqinter> z) = i" - proof (rule anti_sym) + show "x \<sqinter> (y \<sqinter> z) .= i" + proof (rule weak_le_anti_sym) from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)" by (fastsimp intro!: meet_le elim: greatest_Lower_below) next from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i" by (erule_tac greatest_le) - (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed) + (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed) qed (simp_all add: L greatest_closed [OF inf]) qed (simp_all add: L) @@ -636,33 +891,34 @@ shows "x \<sqinter> y = y \<sqinter> x" by (unfold meet_def) (simp add: insert_commute) -lemma (in lattice) meet_assoc: +lemma (in weak_lower_semilattice) weak_meet_assoc: assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" - shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" + shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)" proof - + (* FIXME: improved simp, see weak_join_assoc above *) have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm) - also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma) + also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma) also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute) - also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma) - finally show ?thesis . + also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric]) + finally show ?thesis by (simp add: L) qed subsection {* Total Orders *} -locale total_order = partial_order + +locale weak_total_order = weak_partial_order + assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" text {* Introduction rule: the usual definition of total order *} -lemma (in partial_order) total_orderI: +lemma (in weak_partial_order) weak_total_orderI: assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" - shows "total_order L" + shows "weak_total_order L" by unfold_locales (rule total) text {* Total orders are lattices. *} -interpretation total_order < lattice +interpretation weak_total_order < weak_lattice proof unfold_locales fix x y assume L: "x \<in> carrier L" "y \<in> carrier L" @@ -708,7 +964,7 @@ subsection {* Complete lattices *} -locale complete_lattice = lattice + +locale weak_complete_lattice = weak_lattice + assumes sup_exists: "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" and inf_exists: @@ -716,16 +972,13 @@ text {* Introduction rule: the usual definition of complete lattice *} -lemma (in partial_order) complete_latticeI: +lemma (in weak_partial_order) weak_complete_latticeI: assumes sup_exists: "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" and inf_exists: "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" - shows "complete_lattice L" -proof intro_locales - show "lattice_axioms L" - by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ -qed (rule complete_lattice_axioms.intro sup_exists inf_exists | assumption)+ + shows "weak_complete_lattice L" + by unfold_locales (auto intro: sup_exists inf_exists) constdefs (structure L) top :: "_ => 'a" ("\<top>\<index>") @@ -735,41 +988,41 @@ "\<bottom> == inf L (carrier L)" -lemma (in complete_lattice) supI: +lemma (in weak_complete_lattice) supI: "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |] ==> P (\<Squnion>A)" proof (unfold sup_def) assume L: "A \<subseteq> carrier L" and P: "!!l. least L l (Upper L A) ==> P l" with sup_exists obtain s where "least L s (Upper L A)" by blast - with L show "P (THE l. least L l (Upper L A))" - by (fast intro: theI2 least_unique P) + with L show "P (SOME l. least L l (Upper L A))" + by (fast intro: someI2 weak_least_unique P) qed -lemma (in complete_lattice) sup_closed [simp]: +lemma (in weak_complete_lattice) sup_closed [simp]: "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L" by (rule supI) simp_all -lemma (in complete_lattice) top_closed [simp, intro]: +lemma (in weak_complete_lattice) top_closed [simp, intro]: "\<top> \<in> carrier L" by (unfold top_def) simp -lemma (in complete_lattice) infI: +lemma (in weak_complete_lattice) infI: "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |] ==> P (\<Sqinter>A)" proof (unfold inf_def) assume L: "A \<subseteq> carrier L" and P: "!!l. greatest L l (Lower L A) ==> P l" with inf_exists obtain s where "greatest L s (Lower L A)" by blast - with L show "P (THE l. greatest L l (Lower L A))" - by (fast intro: theI2 greatest_unique P) + with L show "P (SOME l. greatest L l (Lower L A))" + by (fast intro: someI2 weak_greatest_unique P) qed -lemma (in complete_lattice) inf_closed [simp]: +lemma (in weak_complete_lattice) inf_closed [simp]: "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L" by (rule infI) simp_all -lemma (in complete_lattice) bottom_closed [simp, intro]: +lemma (in weak_complete_lattice) bottom_closed [simp, intro]: "\<bottom> \<in> carrier L" by (unfold bottom_def) simp @@ -783,6 +1036,216 @@ "Upper L {} = carrier L" by (unfold Upper_def) simp +theorem (in weak_partial_order) weak_complete_lattice_criterion1: + assumes top_exists: "EX g. greatest L g (carrier L)" + and inf_exists: + "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)" + shows "weak_complete_lattice L" +proof (rule weak_complete_latticeI) + from top_exists obtain top where top: "greatest L top (carrier L)" .. + fix A + assume L: "A \<subseteq> carrier L" + let ?B = "Upper L A" + from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le) + then have B_non_empty: "?B ~= {}" by fast + have B_L: "?B \<subseteq> carrier L" by simp + from inf_exists [OF B_L B_non_empty] + obtain b where b_inf_B: "greatest L b (Lower L ?B)" .. + have "least L b (Upper L A)" +apply (rule least_UpperI) + apply (rule greatest_le [where A = "Lower L ?B"]) + apply (rule b_inf_B) + apply (rule Lower_memI) + apply (erule Upper_memD [THEN conjunct1]) + apply assumption + apply (rule L) + apply (fast intro: L [THEN subsetD]) + apply (erule greatest_Lower_below [OF b_inf_B]) + apply simp + apply (rule L) +apply (rule greatest_closed [OF b_inf_B]) +done + then show "EX s. least L s (Upper L A)" .. +next + fix A + assume L: "A \<subseteq> carrier L" + show "EX i. greatest L i (Lower L A)" + proof (cases "A = {}") + case True then show ?thesis + by (simp add: top_exists) + next + case False with L show ?thesis + by (rule inf_exists) + qed +qed + +(* TODO: prove dual version *) + + +subsection {* Orders and Lattices where @{text eq} is the Equality *} + +locale partial_order = weak_partial_order + + assumes eq_is_equal: "op .= = op =" +begin + +declare weak_le_anti_sym [rule del] + +lemma le_anti_sym [intro]: + "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y" + using weak_le_anti_sym unfolding eq_is_equal . + +lemma lless_eq: + "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y" + unfolding lless_def by (simp add: eq_is_equal) + +lemma lless_asym: + assumes "a \<in> carrier L" "b \<in> carrier L" + and "a \<sqsubset> b" "b \<sqsubset> a" + shows "P" + using assms unfolding lless_eq by auto + +lemma lless_trans [trans]: + assumes "a \<sqsubset> b" "b \<sqsubset> c" + and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L" + shows "a \<sqsubset> c" + using assms unfolding lless_eq by (blast dest: le_trans intro: sym) + +end + + +subsubsection {* Upper and lower bounds of a set *} + +(* all relevant lemmas are global and already proved above *) + + +subsubsection {* Least and greatest, as predicate *} + +lemma (in partial_order) least_unique: + "[| least L x A; least L y A |] ==> x = y" + using weak_least_unique unfolding eq_is_equal . + +lemma (in partial_order) greatest_unique: + "[| greatest L x A; greatest L y A |] ==> x = y" + using weak_greatest_unique unfolding eq_is_equal . + + +subsection {* Lattices *} + +locale upper_semilattice = partial_order + + assumes sup_of_two_exists: + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})" + +interpretation upper_semilattice < weak_upper_semilattice + by unfold_locales (rule sup_of_two_exists) + +locale lower_semilattice = partial_order + + assumes inf_of_two_exists: + "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})" + +interpretation lower_semilattice < weak_lower_semilattice + by unfold_locales (rule inf_of_two_exists) + +locale lattice = upper_semilattice + lower_semilattice + + +subsubsection {* Supremum *} + +context partial_order begin + +declare weak_sup_of_singleton [simp del] + +lemma sup_of_singleton [simp]: + "x \<in> carrier L ==> \<Squnion>{x} = x" + using weak_sup_of_singleton unfolding eq_is_equal . + +end + +context upper_semilattice begin + +lemma join_assoc_lemma: + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" + shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}" + using weak_join_assoc_lemma unfolding eq_is_equal . + +end + +lemma (in upper_semilattice) join_assoc: + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" + shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" + using weak_join_assoc unfolding eq_is_equal . + + +subsubsection {* Infimum *} + +context partial_order begin + +declare weak_inf_of_singleton [simp del] + +lemma inf_of_singleton [simp]: + "x \<in> carrier L ==> \<Sqinter>{x} = x" + using weak_inf_of_singleton unfolding eq_is_equal . + +end + +context lower_semilattice begin + +text {* Condition on @{text A}: infimum exists. *} + +lemma meet_assoc_lemma: + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" + shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}" + using weak_meet_assoc_lemma unfolding eq_is_equal . + +end + +lemma (in lower_semilattice) meet_assoc: + assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L" + shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" + using weak_meet_assoc unfolding eq_is_equal . + + +subsection {* Total Orders *} + +locale total_order = partial_order + + assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" + +interpretation total_order < weak_total_order + by unfold_locales (rule total) + +text {* Introduction rule: the usual definition of total order *} + +lemma (in partial_order) total_orderI: + assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x" + shows "total_order L" + by unfold_locales (rule total) + +text {* Total orders are lattices. *} + +interpretation total_order < lattice + by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists) + + +subsection {* Complete lattices *} + +locale complete_lattice = lattice + + assumes sup_exists: + "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" + and inf_exists: + "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" + +interpretation complete_lattice < weak_complete_lattice + by unfold_locales (auto intro: sup_exists inf_exists) + +text {* Introduction rule: the usual definition of complete lattice *} + +lemma (in partial_order) complete_latticeI: + assumes sup_exists: + "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)" + and inf_exists: + "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)" + shows "complete_lattice L" + by unfold_locales (auto intro: sup_exists inf_exists) + theorem (in partial_order) complete_lattice_criterion1: assumes top_exists: "EX g. greatest L g (carrier L)" and inf_exists: @@ -803,7 +1266,7 @@ apply (rule greatest_le [where A = "Lower L ?B"]) apply (rule b_inf_B) apply (rule Lower_memI) - apply (erule Upper_memD) + apply (erule Upper_memD [THEN conjunct1]) apply assumption apply (rule L) apply (fast intro: L [THEN subsetD]) @@ -834,11 +1297,11 @@ subsubsection {* Powerset of a Set is a Complete Lattice *} theorem powerset_is_complete_lattice: - "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)" + "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)" (is "complete_lattice ?L") proof (rule partial_order.complete_latticeI) show "partial_order ?L" - by (rule partial_order.intro) auto + by unfold_locales auto next fix B assume B: "B \<subseteq> carrier ?L"

--- a/src/HOL/Algebra/ROOT.ML Wed Jul 30 16:07:00 2008 +0200 +++ b/src/HOL/Algebra/ROOT.ML Wed Jul 30 19:03:33 2008 +0200 @@ -5,7 +5,7 @@ *) (* Preliminaries from set and number theory *) -no_document use_thys ["FuncSet", "Primes", "Binomial"]; +no_document use_thys ["FuncSet", "Primes", "Binomial", "Permutation"]; (*** New development, based on explicit structures ***) @@ -17,8 +17,9 @@ "Bij", (* Automorphism Groups *) (* Rings *) - "UnivPoly", (* Rings and polynomials *) - "IntRing" (* Ideals and residue classes *) + "Divisibility", (* Rings *) + "IntRing", (* Ideals and residue classes *) + "UnivPoly" (* Polynomials *) ];

--- a/src/HOL/IsaMakefile Wed Jul 30 16:07:00 2008 +0200 +++ b/src/HOL/IsaMakefile Wed Jul 30 19:03:33 2008 +0200 @@ -509,7 +509,7 @@ Library/Multiset.thy Library/Permutation.thy Library/Primes.thy \ Algebra/AbelCoset.thy Algebra/Bij.thy Algebra/Congruence.thy \ Algebra/Coset.thy Algebra/Divisibility.thy Algebra/Exponent.thy \ - Algebra/FiniteProduct.thy Algebra/GLattice.thy \ + Algebra/FiniteProduct.thy \ Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy \ Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy \ Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy \