# HG changeset patch # User haftmann # Date 1310848115 -7200 # Node ID f1d23df1adde923277343efc18feabeb275d276b # Parent 020ddc6a95082e826c3655e7a47101d0644a3e8c generalized some lemmas diff -r 020ddc6a9508 -r f1d23df1adde src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Sat Jul 16 22:04:02 2011 +0200 +++ b/src/HOL/Complete_Lattice.thy Sat Jul 16 22:28:35 2011 +0200 @@ -208,6 +208,12 @@ lemma SUP_commute: "(\i\A. \j\B. f i j) = (\j\B. \i\A. f i j)" by (iprover intro: SUP_leI le_SUPI order_trans antisym) +lemma INFI_insert: "(\x\insert a A. B x) = B a \ INFI A B" + by (simp add: INFI_def Inf_insert) + +lemma SUPR_insert: "(\x\insert a A. B x) = B a \ SUPR A B" + by (simp add: SUPR_def Sup_insert) + end lemma Inf_less_iff: @@ -468,9 +474,13 @@ -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\A"}. *} by (unfold INTER_def) blast +lemma (in complete_lattice) INFI_cong: + "A = B \ (\x. x \ B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)" + by (simp add: INFI_def image_def) + lemma INT_cong [cong]: - "A = B \ (\x. x \ B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)" - by (simp add: INTER_def) + "A = B \ (\x. x \ B \ C x = D x) \ (\x\A. C x) = (\x\B. D x)" + by (fact INFI_cong) lemma Collect_ball_eq: "{x. \y\A. P x y} = (\y\A. {x. P x y})" by blast @@ -484,17 +494,31 @@ lemma INT_greatest: "(\x. x \ A \ C \ B x) \ C \ (\x\A. B x)" by (fact le_INFI) +lemma (in complete_lattice) INFI_empty: + "(\x\{}. B x) = \" + by (simp add: INFI_def) + lemma INT_empty [simp]: "(\x\{}. B x) = UNIV" - by blast + by (fact INFI_empty) + +lemma (in complete_lattice) INFI_absorb: + assumes "k \ I" + shows "A k \ (\i\I. A i) = (\i\I. A i)" +proof - + from assms obtain J where "I = insert k J" by blast + then show ?thesis by (simp add: INFI_insert) +qed lemma INT_absorb: "k \ I \ A k \ (\i\I. A i) = (\i\I. A i)" - by blast + by (fact INFI_absorb) -lemma INT_subset_iff: "(B \ (\i\I. A i)) = (\i\I. B \ A i)" +lemma INT_subset_iff: "B \ (\i\I. A i) \ (\i\I. B \ A i)" by (fact le_INF_iff) lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ INTER A B" - by blast + by (fact INFI_insert) + +-- {* continue generalization from here *} lemma INT_Un: "(\i \ A \ B. M i) = (\i \ A. M i) \ (\i\B. M i)" by blast @@ -510,10 +534,10 @@ -- {* Look: it has an \emph{existential} quantifier *} by blast -lemma INTER_UNIV_conv[simp]: +lemma INTER_UNIV_conv [simp]: "(UNIV = (\x\A. B x)) = (\x\A. B x = UNIV)" "((\x\A. B x) = UNIV) = (\x\A. B x = UNIV)" -by blast+ + by blast+ lemma INT_bool_eq: "(\b. A b) = (A True \ A False)" by (auto intro: bool_induct)