# HG changeset patch # User ballarin # Date 1161158856 -7200 # Node ID 379542c9d951bde88404a4ef2cb710f30893cbcf # Parent e57e91f728314b8d3046cf9bf9a8bd970a0e872f Stylistic improvements. diff -r e57e91f72831 -r 379542c9d951 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Tue Oct 17 09:51:04 2006 +0200 +++ b/src/HOL/Algebra/Lattice.thy Wed Oct 18 10:07:36 2006 +0200 @@ -18,17 +18,12 @@ subsection {* Partial Orders *} -(* -record 'a order = "'a partial_object" + - le :: "['a, 'a] => bool" (infixl "\\" 50) -*) - text {* Locale @{text order_syntax} is required since we want to refer to definitions (and their derived theorems) outside of @{text partial_order}. *} locale order_syntax = - fixes carrier :: "'a set" and le :: "['a, 'a] => bool" (infix "\" 50) + fixes L :: "'a set" and le :: "['a, 'a] => bool" (infix "\" 50) text {* Note that the type constraints above are necessary, because the definition command cannot specialise the types. *} @@ -40,32 +35,30 @@ definition (in order_syntax) Upper where - "Upper A == {u. (ALL x. x \ A \ carrier --> x \ u)} \ - carrier" + "Upper A == {u. (ALL x. x \ A \ L --> x \ u)} \ L" definition (in order_syntax) Lower :: "'a set => 'a set" - "Lower A == {l. (ALL x. x \ A \ carrier --> l \ x)} \ - carrier" + "Lower A == {l. (ALL x. x \ A \ L --> l \ x)} \ L" text {* Least and greatest, as predicate. *} definition (in order_syntax) least :: "['a, 'a set] => bool" - "least l A == A \ carrier & l \ A & (ALL x : A. l \ x)" + "least l A == A \ L & l \ A & (ALL x : A. l \ x)" definition (in order_syntax) greatest :: "['a, 'a set] => bool" - "greatest g A == A \ carrier & g \ A & (ALL x : A. x \ g)" + "greatest g A == A \ L & g \ A & (ALL x : A. x \ g)" text {* Supremum and infimum *} definition (in order_syntax) - sup :: "'a set => 'a" ("\") (* FIXME precedence [90] 90 *) + sup :: "'a set => 'a" ("\_" [90] 90) "\A == THE x. least x (Upper A)" definition (in order_syntax) - inf :: "'a set => 'a" ("\") (* FIXME precedence *) + inf :: "'a set => 'a" ("\_" [90] 90) "\A == THE x. greatest x (Lower A)" definition (in order_syntax) @@ -78,47 +71,45 @@ locale partial_order = order_syntax + assumes refl [intro, simp]: - "x \ carrier ==> x \ x" + "x \ L ==> x \ x" and anti_sym [intro]: - "[| x \ y; y \ x; x \ carrier; y \ carrier |] ==> x = y" + "[| x \ y; y \ x; x \ L; y \ L |] ==> x = y" and trans [trans]: "[| x \ y; y \ z; - x \ carrier; y \ carrier; z \ carrier |] ==> x \ z" + x \ L; y \ L; z \ L |] ==> x \ z" abbreviation (in partial_order) less (infixl "\" 50) "less == order_syntax.less le" abbreviation (in partial_order) - Upper where "Upper == order_syntax.Upper carrier le" + Upper where "Upper == order_syntax.Upper L le" abbreviation (in partial_order) - Lower where "Lower == order_syntax.Lower carrier le" + Lower where "Lower == order_syntax.Lower L le" abbreviation (in partial_order) - least where "least == order_syntax.least carrier le" + least where "least == order_syntax.least L le" abbreviation (in partial_order) - greatest where "greatest == order_syntax.greatest carrier le" + greatest where "greatest == order_syntax.greatest L le" abbreviation (in partial_order) - sup ("\") (* FIXME precedence *) "sup == order_syntax.sup carrier le" + sup ("\_" [90] 90) "sup == order_syntax.sup L le" abbreviation (in partial_order) - inf ("\") (* FIXME precedence *) "inf == order_syntax.inf carrier le" + inf ("\_" [90] 90) "inf == order_syntax.inf L le" abbreviation (in partial_order) - join (infixl "\" 65) "join == order_syntax.join carrier le" + join (infixl "\" 65) "join == order_syntax.join L le" abbreviation (in partial_order) - meet (infixl "\" 70) "meet == order_syntax.meet carrier le" + meet (infixl "\" 70) "meet == order_syntax.meet L le" subsubsection {* Upper *} lemma (in order_syntax) Upper_closed [intro, simp]: - "Upper A \ carrier" + "Upper A \ L" by (unfold Upper_def) clarify lemma (in order_syntax) UpperD [dest]: - fixes L (structure) - shows "[| u \ Upper A; x \ A; A \ carrier |] ==> x \ u" + "[| u \ Upper A; x \ A; A \ L |] ==> x \ u" by (unfold Upper_def) blast lemma (in order_syntax) Upper_memI: - fixes L (structure) - shows "[| !! y. y \ A ==> y \ x; x \ carrier |] ==> x \ Upper A" + "[| !! y. y \ A ==> y \ x; x \ L |] ==> x \ Upper A" by (unfold Upper_def) blast lemma (in order_syntax) Upper_antimono: @@ -129,15 +120,15 @@ subsubsection {* Lower *} lemma (in order_syntax) Lower_closed [intro, simp]: - "Lower A \ carrier" + "Lower A \ L" by (unfold Lower_def) clarify lemma (in order_syntax) LowerD [dest]: - "[| l \ Lower A; x \ A; A \ carrier |] ==> l \ x" + "[| l \ Lower A; x \ A; A \ L |] ==> l \ x" by (unfold Lower_def) blast lemma (in order_syntax) Lower_memI: - "[| !! y. y \ A ==> x \ y; x \ carrier |] ==> x \ Lower A" + "[| !! y. y \ A ==> x \ y; x \ L |] ==> x \ Lower A" by (unfold Lower_def) blast lemma (in order_syntax) Lower_antimono: @@ -147,8 +138,8 @@ subsubsection {* least *} -lemma (in order_syntax) least_carrier [intro, simp]: - "least l A ==> l \ carrier" +lemma (in order_syntax) least_closed [intro, simp]: + "least l A ==> l \ L" by (unfold least_def) fast lemma (in order_syntax) least_mem: @@ -166,10 +157,10 @@ lemma (in order_syntax) least_UpperI: assumes above: "!! x. x \ A ==> x \ s" and below: "!! y. y \ Upper A ==> s \ y" - and L: "A \ carrier" "s \ carrier" + and L: "A \ L" "s \ L" shows "least s (Upper A)" proof - - have "Upper A \ carrier" by simp + have "Upper A \ L" by simp moreover from above L have "s \ Upper A" by (simp add: Upper_def) moreover from below have "ALL x : Upper A. s \ x" by fast ultimately show ?thesis by (simp add: least_def) @@ -178,8 +169,8 @@ subsubsection {* greatest *} -lemma (in order_syntax) greatest_carrier [intro, simp]: - "greatest l A ==> l \ carrier" +lemma (in order_syntax) greatest_closed [intro, simp]: + "greatest l A ==> l \ L" by (unfold greatest_def) fast lemma (in order_syntax) greatest_mem: @@ -197,10 +188,10 @@ lemma (in order_syntax) greatest_LowerI: assumes below: "!! x. x \ A ==> i \ x" and above: "!! y. y \ Lower A ==> y \ i" - and L: "A \ carrier" "i \ carrier" + and L: "A \ L" "i \ L" shows "greatest i (Lower A)" proof - - have "Lower A \ carrier" by simp + have "Lower A \ L" by simp moreover from below L have "i \ Lower A" by (simp add: Lower_def) moreover from above have "ALL x : Lower A. x \ i" by fast ultimately show ?thesis by (simp add: greatest_def) @@ -211,45 +202,45 @@ locale lattice = partial_order + assumes sup_of_two_exists: - "[| x \ carrier; y \ carrier |] ==> EX s. order_syntax.least carrier le s (order_syntax.Upper carrier le {x, y})" + "[| x \ L; y \ L |] ==> EX s. order_syntax.least L le s (order_syntax.Upper L le {x, y})" and inf_of_two_exists: - "[| x \ carrier; y \ carrier |] ==> EX s. order_syntax.greatest carrier le s (order_syntax.Lower carrier le {x, y})" + "[| x \ L; y \ L |] ==> EX s. order_syntax.greatest L le s (order_syntax.Lower L le {x, y})" abbreviation (in lattice) less (infixl "\" 50) "less == order_syntax.less le" abbreviation (in lattice) - Upper where "Upper == order_syntax.Upper carrier le" + Upper where "Upper == order_syntax.Upper L le" abbreviation (in lattice) - Lower where "Lower == order_syntax.Lower carrier le" + Lower where "Lower == order_syntax.Lower L le" abbreviation (in lattice) - least where "least == order_syntax.least carrier le" + least where "least == order_syntax.least L le" abbreviation (in lattice) - greatest where "greatest == order_syntax.greatest carrier le" + greatest where "greatest == order_syntax.greatest L le" abbreviation (in lattice) - sup ("\") (* FIXME precedence *) "sup == order_syntax.sup carrier le" + sup ("\_" [90] 90) "sup == order_syntax.sup L le" abbreviation (in lattice) - inf ("\") (* FIXME precedence *) "inf == order_syntax.inf carrier le" + inf ("\_" [90] 90) "inf == order_syntax.inf L le" abbreviation (in lattice) - join (infixl "\" 65) "join == order_syntax.join carrier le" + join (infixl "\" 65) "join == order_syntax.join L le" abbreviation (in lattice) - meet (infixl "\" 70) "meet == order_syntax.meet carrier le" + meet (infixl "\" 70) "meet == order_syntax.meet L le" lemma (in order_syntax) least_Upper_above: - "[| least s (Upper A); x \ A; A \ carrier |] ==> x \ s" + "[| least s (Upper A); x \ A; A \ L |] ==> x \ s" by (unfold least_def) blast lemma (in order_syntax) greatest_Lower_above: - "[| greatest i (Lower A); x \ A; A \ carrier |] ==> i \ x" + "[| greatest i (Lower A); x \ A; A \ L |] ==> i \ x" by (unfold greatest_def) blast subsubsection {* Supremum *} lemma (in lattice) joinI: - "[| !!l. least l (Upper {x, y}) ==> P l; x \ carrier; y \ carrier |] + "[| !!l. least l (Upper {x, y}) ==> P l; x \ L; y \ L |] ==> P (x \ y)" proof (unfold join_def sup_def) - assume L: "x \ carrier" "y \ carrier" + assume L: "x \ L" "y \ L" and P: "!!l. least l (Upper {x, y}) ==> P l" with sup_of_two_exists obtain s where "least s (Upper {x, y})" by fast with L show "P (THE l. least l (Upper {x, y}))" @@ -257,15 +248,15 @@ qed lemma (in lattice) join_closed [simp]: - "[| x \ carrier; y \ carrier |] ==> x \ y \ carrier" - by (rule joinI) (rule least_carrier) + "[| x \ L; y \ L |] ==> x \ y \ L" + by (rule joinI) (rule least_closed) lemma (in partial_order) sup_of_singletonI: (* only reflexivity needed ? *) - "x \ carrier ==> least x (Upper {x})" + "x \ L ==> least x (Upper {x})" by (rule least_UpperI) fast+ lemma (in partial_order) sup_of_singleton [simp]: - "x \ carrier ==> \{x} = x" + "x \ L ==> \{x} = x" by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI) @@ -273,13 +264,13 @@ lemma (in lattice) sup_insertI: "[| !!s. least s (Upper (insert x A)) ==> P s; - least a (Upper A); x \ carrier; A \ carrier |] + least a (Upper A); x \ L; A \ L |] ==> P (\(insert x A))" proof (unfold sup_def) - assume L: "x \ carrier" "A \ carrier" + assume L: "x \ L" "A \ L" and P: "!!l. least l (Upper (insert x A)) ==> P l" and least_a: "least a (Upper A)" - from least_a have La: "a \ carrier" by simp + from least_a have La: "a \ L" by simp from L sup_of_two_exists least_a obtain s where least_s: "least s (Upper {a, x})" by blast show "P (THE l. least l (Upper (insert x A)))" @@ -318,8 +309,8 @@ qed qed (rule Upper_closed [THEN subsetD]) next - from L show "insert x A \ carrier" by simp - from least_s show "s \ carrier" by simp + from L show "insert x A \ L" by simp + from least_s show "s \ L" by simp qed next fix l @@ -360,15 +351,15 @@ qed qed (rule Upper_closed [THEN subsetD]) next - from L show "insert x A \ carrier" by simp - from least_s show "s \ carrier" by simp + from L show "insert x A \ L" by simp + from least_s show "s \ L" by simp qed qed qed qed lemma (in lattice) finite_sup_least: - "[| finite A; A \ carrier; A ~= {} |] ==> least (\A) (Upper A)" + "[| finite A; A \ L; A ~= {} |] ==> least (\A) (Upper A)" proof (induct set: Finites) case empty then show ?case by simp @@ -388,7 +379,7 @@ lemma (in lattice) finite_sup_insertI: assumes P: "!!l. least l (Upper (insert x A)) ==> P l" - and xA: "finite A" "x \ carrier" "A \ carrier" + and xA: "finite A" "x \ L" "A \ L" shows "P (\ (insert x A))" proof (cases "A = {}") case True with P and xA show ?thesis @@ -399,7 +390,7 @@ qed lemma (in lattice) finite_sup_closed: - "[| finite A; A \ carrier; A ~= {} |] ==> \A \ carrier" + "[| finite A; A \ L; A ~= {} |] ==> \A \ L" proof (induct set: Finites) case empty then show ?case by simp next @@ -408,17 +399,17 @@ qed lemma (in lattice) join_left: - "[| x \ carrier; y \ carrier |] ==> x \ x \ y" + "[| x \ L; y \ L |] ==> x \ x \ y" by (rule joinI [folded join_def]) (blast dest: least_mem) lemma (in lattice) join_right: - "[| x \ carrier; y \ carrier |] ==> y \ x \ y" + "[| x \ L; y \ L |] ==> y \ x \ y" by (rule joinI [folded join_def]) (blast dest: least_mem) lemma (in lattice) sup_of_two_least: - "[| x \ carrier; y \ carrier |] ==> least (\{x, y}) (Upper {x, y})" + "[| x \ L; y \ L |] ==> least (\{x, y}) (Upper {x, y})" proof (unfold sup_def) - assume L: "x \ carrier" "y \ carrier" + assume L: "x \ L" "y \ L" with sup_of_two_exists obtain s where "least s (Upper {x, y})" by fast with L show "least (THE xa. least xa (Upper {x, y})) (Upper {x, y})" by (fast intro: theI2 least_unique) (* blast fails *) @@ -426,7 +417,7 @@ lemma (in lattice) join_le: assumes sub: "x \ z" "y \ z" - and L: "x \ carrier" "y \ carrier" "z \ carrier" + and L: "x \ L" "y \ L" "z \ L" shows "x \ y \ z" proof (rule joinI) fix s @@ -435,7 +426,7 @@ qed lemma (in lattice) join_assoc_lemma: - assumes L: "x \ carrier" "y \ carrier" "z \ carrier" + assumes L: "x \ L" "y \ L" "z \ L" shows "x \ (y \ z) = \{x, y, z}" proof (rule finite_sup_insertI) -- {* The textbook argument in Jacobson I, p 457 *} @@ -449,7 +440,7 @@ from sup L show "s \ x \ (y \ z)" by (erule_tac least_le) (blast intro!: Upper_memI intro: trans join_left join_right join_closed) - qed (simp_all add: L least_carrier [OF sup]) + qed (simp_all add: L least_closed [OF sup]) qed (simp_all add: L) lemma (in order_syntax) join_comm: @@ -457,7 +448,7 @@ by (unfold join_def) (simp add: insert_commute) lemma (in lattice) join_assoc: - assumes L: "x \ carrier" "y \ carrier" "z \ carrier" + assumes L: "x \ L" "y \ L" "z \ L" shows "(x \ y) \ z = x \ (y \ z)" proof - have "(x \ y) \ z = z \ (x \ y)" by (simp only: join_comm) @@ -471,11 +462,10 @@ subsubsection {* Infimum *} lemma (in lattice) meetI: - "[| !!i. greatest i (Lower {x, y}) ==> P i; - x \ carrier; y \ carrier |] + "[| !!i. greatest i (Lower {x, y}) ==> P i; x \ L; y \ L |] ==> P (x \ y)" proof (unfold meet_def inf_def) - assume L: "x \ carrier" "y \ carrier" + assume L: "x \ L" "y \ L" and P: "!!g. greatest g (Lower {x, y}) ==> P g" with inf_of_two_exists obtain i where "greatest i (Lower {x, y})" by fast with L show "P (THE g. greatest g (Lower {x, y}))" @@ -483,28 +473,28 @@ qed lemma (in lattice) meet_closed [simp]: - "[| x \ carrier; y \ carrier |] ==> x \ y \ carrier" - by (rule meetI) (rule greatest_carrier) + "[| x \ L; y \ L |] ==> x \ y \ L" + by (rule meetI) (rule greatest_closed) lemma (in partial_order) inf_of_singletonI: (* only reflexivity needed ? *) - "x \ carrier ==> greatest x (Lower {x})" + "x \ L ==> greatest x (Lower {x})" by (rule greatest_LowerI) fast+ lemma (in partial_order) inf_of_singleton [simp]: - "x \ carrier ==> \ {x} = x" + "x \ L ==> \ {x} = x" by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI) text {* Condition on A: infimum exists. *} lemma (in lattice) inf_insertI: "[| !!i. greatest i (Lower (insert x A)) ==> P i; - greatest a (Lower A); x \ carrier; A \ carrier |] + greatest a (Lower A); x \ L; A \ L |] ==> P (\(insert x A))" proof (unfold inf_def) - assume L: "x \ carrier" "A \ carrier" + assume L: "x \ L" "A \ L" and P: "!!g. greatest g (Lower (insert x A)) ==> P g" and greatest_a: "greatest a (Lower A)" - from greatest_a have La: "a \ carrier" by simp + from greatest_a have La: "a \ L" by simp from L inf_of_two_exists greatest_a obtain i where greatest_i: "greatest i (Lower {a, x})" by blast show "P (THE g. greatest g (Lower (insert x A)))" @@ -543,8 +533,8 @@ qed qed (rule Lower_closed [THEN subsetD]) next - from L show "insert x A \ carrier" by simp - from greatest_i show "i \ carrier" by simp + from L show "insert x A \ L" by simp + from greatest_i show "i \ L" by simp qed next fix g @@ -585,15 +575,15 @@ qed qed (rule Lower_closed [THEN subsetD]) next - from L show "insert x A \ carrier" by simp - from greatest_i show "i \ carrier" by simp + from L show "insert x A \ L" by simp + from greatest_i show "i \ L" by simp qed qed qed qed lemma (in lattice) finite_inf_greatest: - "[| finite A; A \ carrier; A ~= {} |] ==> greatest (\A) (Lower A)" + "[| finite A; A \ L; A ~= {} |] ==> greatest (\A) (Lower A)" proof (induct set: Finites) case empty then show ?case by simp next @@ -613,7 +603,7 @@ lemma (in lattice) finite_inf_insertI: assumes P: "!!i. greatest i (Lower (insert x A)) ==> P i" - and xA: "finite A" "x \ carrier" "A \ carrier" + and xA: "finite A" "x \ L" "A \ L" shows "P (\ (insert x A))" proof (cases "A = {}") case True with P and xA show ?thesis @@ -624,7 +614,7 @@ qed lemma (in lattice) finite_inf_closed: - "[| finite A; A \ carrier; A ~= {} |] ==> \A \ carrier" + "[| finite A; A \ L; A ~= {} |] ==> \A \ L" proof (induct set: Finites) case empty then show ?case by simp next @@ -633,18 +623,17 @@ qed lemma (in lattice) meet_left: - "[| x \ carrier; y \ carrier |] ==> x \ y \ x" + "[| x \ L; y \ L |] ==> x \ y \ x" by (rule meetI [folded meet_def]) (blast dest: greatest_mem) lemma (in lattice) meet_right: - "[| x \ carrier; y \ carrier |] ==> x \ y \ y" + "[| x \ L; y \ L |] ==> x \ y \ y" by (rule meetI [folded meet_def]) (blast dest: greatest_mem) lemma (in lattice) inf_of_two_greatest: - "[| x \ carrier; y \ carrier |] ==> - greatest (\ {x, y}) (Lower {x, y})" + "[| x \ L; y \ L |] ==> greatest (\ {x, y}) (Lower {x, y})" proof (unfold inf_def) - assume L: "x \ carrier" "y \ carrier" + assume L: "x \ L" "y \ L" with inf_of_two_exists obtain s where "greatest s (Lower {x, y})" by fast with L show "greatest (THE xa. greatest xa (Lower {x, y})) (Lower {x, y})" @@ -653,7 +642,7 @@ lemma (in lattice) meet_le: assumes sub: "z \ x" "z \ y" - and L: "x \ carrier" "y \ carrier" "z \ carrier" + and L: "x \ L" "y \ L" "z \ L" shows "z \ x \ y" proof (rule meetI) fix i @@ -662,7 +651,7 @@ qed lemma (in lattice) meet_assoc_lemma: - assumes L: "x \ carrier" "y \ carrier" "z \ carrier" + assumes L: "x \ L" "y \ L" "z \ L" shows "x \ (y \ z) = \{x, y, z}" proof (rule finite_inf_insertI) txt {* The textbook argument in Jacobson I, p 457 *} @@ -676,7 +665,7 @@ from inf L show "x \ (y \ z) \ i" by (erule_tac greatest_le) (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed) - qed (simp_all add: L greatest_carrier [OF inf]) + qed (simp_all add: L greatest_closed [OF inf]) qed (simp_all add: L) lemma (in order_syntax) meet_comm: @@ -684,7 +673,7 @@ by (unfold meet_def) (simp add: insert_commute) lemma (in lattice) meet_assoc: - assumes L: "x \ carrier" "y \ carrier" "z \ carrier" + assumes L: "x \ L" "y \ L" "z \ L" shows "(x \ y) \ z = x \ (y \ z)" proof - have "(x \ y) \ z = z \ (x \ y)" by (simp only: meet_comm) @@ -698,37 +687,37 @@ subsection {* Total Orders *} locale total_order = lattice + - assumes total: "[| x \ carrier; y \ carrier |] ==> x \ y | y \ x" + assumes total: "[| x \ L; y \ L |] ==> x \ y | y \ x" abbreviation (in total_order) less (infixl "\" 50) "less == order_syntax.less le" abbreviation (in total_order) - Upper where "Upper == order_syntax.Upper carrier le" + Upper where "Upper == order_syntax.Upper L le" abbreviation (in total_order) - Lower where "Lower == order_syntax.Lower carrier le" + Lower where "Lower == order_syntax.Lower L le" abbreviation (in total_order) - least where "least == order_syntax.least carrier le" + least where "least == order_syntax.least L le" abbreviation (in total_order) - greatest where "greatest == order_syntax.greatest carrier le" + greatest where "greatest == order_syntax.greatest L le" abbreviation (in total_order) - sup ("\") (* FIXME precedence *) "sup == order_syntax.sup carrier le" + sup ("\_" [90] 90) "sup == order_syntax.sup L le" abbreviation (in total_order) - inf ("\") (* FIXME precedence *) "inf == order_syntax.inf carrier le" + inf ("\_" [90] 90) "inf == order_syntax.inf L le" abbreviation (in total_order) - join (infixl "\" 65) "join == order_syntax.join carrier le" + join (infixl "\" 65) "join == order_syntax.join L le" abbreviation (in total_order) - meet (infixl "\" 70) "meet == order_syntax.meet carrier le" + meet (infixl "\" 70) "meet == order_syntax.meet L le" text {* Introduction rule: the usual definition of total order *} lemma (in partial_order) total_orderI: - assumes total: "!!x y. [| x \ carrier; y \ carrier |] ==> x \ y | y \ x" - shows "total_order carrier le" + assumes total: "!!x y. [| x \ L; y \ L |] ==> x \ y | y \ x" + shows "total_order L le" proof intro_locales - show "lattice_axioms carrier le" + show "lattice_axioms L le" proof (rule lattice_axioms.intro) fix x y - assume L: "x \ carrier" "y \ carrier" + assume L: "x \ L" "y \ L" show "EX s. least s (Upper {x, y})" proof - note total L @@ -748,7 +737,7 @@ qed next fix x y - assume L: "x \ carrier" "y \ carrier" + assume L: "x \ L" "y \ L" show "EX i. greatest i (Lower {x, y})" proof - note total L @@ -774,73 +763,73 @@ locale complete_lattice = lattice + assumes sup_exists: - "[| A \ carrier |] ==> EX s. order_syntax.least carrier le s (order_syntax.Upper carrier le A)" + "[| A \ L |] ==> EX s. order_syntax.least L le s (order_syntax.Upper L le A)" and inf_exists: - "[| A \ carrier |] ==> EX i. order_syntax.greatest carrier le i (order_syntax.Lower carrier le A)" + "[| A \ L |] ==> EX i. order_syntax.greatest L le i (order_syntax.Lower L le A)" abbreviation (in complete_lattice) less (infixl "\" 50) "less == order_syntax.less le" abbreviation (in complete_lattice) - Upper where "Upper == order_syntax.Upper carrier le" + Upper where "Upper == order_syntax.Upper L le" abbreviation (in complete_lattice) - Lower where "Lower == order_syntax.Lower carrier le" + Lower where "Lower == order_syntax.Lower L le" abbreviation (in complete_lattice) - least where "least == order_syntax.least carrier le" + least where "least == order_syntax.least L le" abbreviation (in complete_lattice) - greatest where "greatest == order_syntax.greatest carrier le" + greatest where "greatest == order_syntax.greatest L le" abbreviation (in complete_lattice) - sup ("\") (* FIXME precedence *) "sup == order_syntax.sup carrier le" + sup ("\_" [90] 90) "sup == order_syntax.sup L le" abbreviation (in complete_lattice) - inf ("\") (* FIXME precedence *) "inf == order_syntax.inf carrier le" + inf ("\_" [90] 90) "inf == order_syntax.inf L le" abbreviation (in complete_lattice) - join (infixl "\" 65) "join == order_syntax.join carrier le" + join (infixl "\" 65) "join == order_syntax.join L le" abbreviation (in complete_lattice) - meet (infixl "\" 70) "meet == order_syntax.meet carrier le" + meet (infixl "\" 70) "meet == order_syntax.meet L le" text {* Introduction rule: the usual definition of complete lattice *} lemma (in partial_order) complete_latticeI: assumes sup_exists: - "!!A. [| A \ carrier |] ==> EX s. least s (Upper A)" + "!!A. [| A \ L |] ==> EX s. least s (Upper A)" and inf_exists: - "!!A. [| A \ carrier |] ==> EX i. greatest i (Lower A)" - shows "complete_lattice carrier le" + "!!A. [| A \ L |] ==> EX i. greatest i (Lower A)" + shows "complete_lattice L le" proof intro_locales - show "lattice_axioms carrier le" + show "lattice_axioms L le" by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+ qed (assumption | rule complete_lattice_axioms.intro)+ definition (in order_syntax) top ("\") - "\ == sup carrier" + "\ == sup L" definition (in order_syntax) bottom ("\") - "\ == inf carrier" + "\ == inf L" abbreviation (in partial_order) - top ("\") "top == order_syntax.top carrier le" + top ("\") "top == order_syntax.top L le" abbreviation (in partial_order) - bottom ("\") "bottom == order_syntax.bottom carrier le" + bottom ("\") "bottom == order_syntax.bottom L le" abbreviation (in lattice) - top ("\") "top == order_syntax.top carrier le" + top ("\") "top == order_syntax.top L le" abbreviation (in lattice) - bottom ("\") "bottom == order_syntax.bottom carrier le" + bottom ("\") "bottom == order_syntax.bottom L le" abbreviation (in total_order) - top ("\") "top == order_syntax.top carrier le" + top ("\") "top == order_syntax.top L le" abbreviation (in total_order) - bottom ("\") "bottom == order_syntax.bottom carrier le" + bottom ("\") "bottom == order_syntax.bottom L le" abbreviation (in complete_lattice) - top ("\") "top == order_syntax.top carrier le" + top ("\") "top == order_syntax.top L le" abbreviation (in complete_lattice) - bottom ("\") "bottom == order_syntax.bottom carrier le" + bottom ("\") "bottom == order_syntax.bottom L le" lemma (in complete_lattice) supI: - "[| !!l. least l (Upper A) ==> P l; A \ carrier |] + "[| !!l. least l (Upper A) ==> P l; A \ L |] ==> P (\A)" proof (unfold sup_def) - assume L: "A \ carrier" + assume L: "A \ L" and P: "!!l. least l (Upper A) ==> P l" with sup_exists obtain s where "least s (Upper A)" by blast with L show "P (THE l. least l (Upper A))" @@ -848,18 +837,18 @@ qed lemma (in complete_lattice) sup_closed [simp]: - "A \ carrier ==> \A \ carrier" + "A \ L ==> \A \ L" by (rule supI) simp_all lemma (in complete_lattice) top_closed [simp, intro]: - "\ \ carrier" + "\ \ L" by (unfold top_def) simp lemma (in complete_lattice) infI: - "[| !!i. greatest i (Lower A) ==> P i; A \ carrier |] + "[| !!i. greatest i (Lower A) ==> P i; A \ L |] ==> P (\A)" proof (unfold inf_def) - assume L: "A \ carrier" + assume L: "A \ L" and P: "!!l. greatest l (Lower A) ==> P l" with inf_exists obtain s where "greatest s (Lower A)" by blast with L show "P (THE l. greatest l (Lower A))" @@ -867,36 +856,36 @@ qed lemma (in complete_lattice) inf_closed [simp]: - "A \ carrier ==> \A \ carrier" + "A \ L ==> \A \ L" by (rule infI) simp_all lemma (in complete_lattice) bottom_closed [simp, intro]: - "\ \ carrier" + "\ \ L" by (unfold bottom_def) simp text {* Jacobson: Theorem 8.1 *} lemma (in order_syntax) Lower_empty [simp]: - "Lower {} = carrier" + "Lower {} = L" by (unfold Lower_def) simp lemma (in order_syntax) Upper_empty [simp]: - "Upper {} = carrier" + "Upper {} = L" by (unfold Upper_def) simp theorem (in partial_order) complete_lattice_criterion1: - assumes top_exists: "EX g. greatest g (carrier)" + assumes top_exists: "EX g. greatest g L" and inf_exists: - "!!A. [| A \ carrier; A ~= {} |] ==> EX i. greatest i (Lower A)" - shows "complete_lattice carrier le" + "!!A. [| A \ L; A ~= {} |] ==> EX i. greatest i (Lower A)" + shows "complete_lattice L le" proof (rule complete_latticeI) - from top_exists obtain top where top: "greatest top (carrier)" .. + from top_exists obtain top where top: "greatest top L" .. fix A - assume L: "A \ carrier" + assume L: "A \ L" let ?B = "Upper A" from L top have "top \ ?B" by (fast intro!: Upper_memI intro: greatest_le) then have B_non_empty: "?B ~= {}" by fast - have B_L: "?B \ carrier" by simp + have B_L: "?B \ L" by simp from inf_exists [OF B_L B_non_empty] obtain b where b_inf_B: "greatest b (Lower ?B)" .. have "least b (Upper A)" @@ -911,12 +900,12 @@ apply (erule greatest_Lower_above [OF b_inf_B]) apply simp apply (rule L) -apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *) +apply (rule greatest_closed [OF b_inf_B]) (* rename rule: _closed *) done then show "EX s. least s (Upper A)" .. next fix A - assume L: "A \ carrier" + assume L: "A \ L" show "EX i. greatest i (Lower A)" proof (cases "A = {}") case True then show ?thesis @@ -936,24 +925,24 @@ theorem powerset_is_complete_lattice: "complete_lattice (Pow A) (op \)" - (is "complete_lattice ?car ?le") + (is "complete_lattice ?L ?le") proof (rule partial_order.complete_latticeI) - show "partial_order ?car ?le" + show "partial_order ?L ?le" by (rule partial_order.intro) auto next fix B - assume "B \ ?car" - then have "order_syntax.least ?car ?le (\ B) (order_syntax.Upper ?car ?le B)" + assume "B \ ?L" + then have "order_syntax.least ?L ?le (\ B) (order_syntax.Upper ?L ?le B)" by (fastsimp intro!: order_syntax.least_UpperI simp: order_syntax.Upper_def) - then show "EX s. order_syntax.least ?car ?le s (order_syntax.Upper ?car ?le B)" .. + then show "EX s. order_syntax.least ?L ?le s (order_syntax.Upper ?L ?le B)" .. next fix B - assume "B \ ?car" - then have "order_syntax.greatest ?car ?le (\ B \ A) (order_syntax.Lower ?car ?le B)" + assume "B \ ?L" + then have "order_syntax.greatest ?L ?le (\ B \ A) (order_syntax.Lower ?L ?le B)" txt {* @{term "\ B"} is not the infimum of @{term B}: @{term "\ {} = UNIV"} which is in general bigger than @{term "A"}! *} by (fastsimp intro!: order_syntax.greatest_LowerI simp: order_syntax.Lower_def) - then show "EX i. order_syntax.greatest ?car ?le i (order_syntax.Lower ?car ?le B)" .. + then show "EX i. order_syntax.greatest ?L ?le i (order_syntax.Lower ?L ?le B)" .. qed text {* An other example, that of the lattice of subgroups of a group,