# HG changeset patch # User haftmann # Date 1312824071 -7200 # Node ID 81e55342cb86251b7b9bbe1919cd7637fce8c69c # Parent 4588597ba37e90d5d127bda445b643172359bfc5 dropped lemmas (Inf|Sup)_(singleton|binary) diff -r 4588597ba37e -r 81e55342cb86 NEWS --- a/NEWS Mon Aug 08 08:55:49 2011 -0700 +++ b/NEWS Mon Aug 08 19:21:11 2011 +0200 @@ -68,6 +68,8 @@ boolean algebras and complete linear orders. Lemmas Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder. Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply. +Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary and Sup_binary have +been discarded. More consistent and less misunderstandable names: INFI_def ~> INF_def SUPR_def ~> SUP_def diff -r 4588597ba37e -r 81e55342cb86 src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Complete_Lattice.thy Mon Aug 08 19:21:11 2011 +0200 @@ -129,13 +129,13 @@ lemma le_Inf_iff: "b \ \A \ (\a\A. b \ a)" by (auto intro: Inf_greatest dest: Inf_lower) -lemma le_INF_iff: "u \ (\i\A. f i) \ (\i \ A. u \ f i)" +lemma le_INF_iff: "u \ (\i\A. f i) \ (\i\A. u \ f i)" by (auto simp add: INF_def le_Inf_iff) lemma Sup_le_iff: "\A \ b \ (\a\A. a \ b)" by (auto intro: Sup_least dest: Sup_upper) -lemma SUP_le_iff: "(\i\A. f i) \ u \ (\i \ A. f i \ u)" +lemma SUP_le_iff: "(\i\A. f i) \ u \ (\i\A. f i \ u)" by (auto simp add: SUP_def Sup_le_iff) lemma Inf_empty [simp]: @@ -160,13 +160,13 @@ "\UNIV = \" by (auto intro!: antisym Sup_upper) -lemma Inf_insert: "\insert a A = a \ \A" +lemma Inf_insert (*[simp]*): "\insert a A = a \ \A" by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower) lemma INF_insert: "(\x\insert a A. f x) = f a \ INFI A f" by (simp add: INF_def Inf_insert) -lemma Sup_insert: "\insert a A = a \ \A" +lemma Sup_insert (*[simp]*): "\insert a A = a \ \A" by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper) lemma SUP_insert: "(\x\insert a A. f x) = f a \ SUPR A f" @@ -178,22 +178,6 @@ lemma Sup_Inf: "\A = \{b. \a \ A. a \ b}" by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least) -lemma Inf_singleton [simp]: - "\{a} = a" - by (auto intro: antisym Inf_lower Inf_greatest) - -lemma Sup_singleton [simp]: - "\{a} = a" - by (auto intro: antisym Sup_upper Sup_least) - -lemma Inf_binary: - "\{a, b} = a \ b" - by (simp add: Inf_insert) - -lemma Sup_binary: - "\{a, b} = a \ b" - by (simp add: Sup_insert) - lemma Inf_superset_mono: "B \ A \ \A \ \B" by (auto intro: Inf_greatest Inf_lower) @@ -444,7 +428,7 @@ and prove @{text inf_Sup} and @{text sup_Inf} from that? *} fix a b c from sup_Inf have "a \ \{b, c} = (\d\{b, c}. a \ d)" . - then show "a \ b \ c = (a \ b) \ (a \ c)" by (simp add: INF_def Inf_binary) + then show "a \ b \ c = (a \ b) \ (a \ c)" by (simp add: INF_def Inf_insert) qed lemma Inf_sup: @@ -698,7 +682,7 @@ by (fact Inf_greatest) lemma Int_eq_Inter: "A \ B = \{A, B}" - by (fact Inf_binary [symmetric]) + by (simp add: Inf_insert) lemma Inter_empty [simp]: "\{} = UNIV" by (fact Inf_empty) @@ -1206,6 +1190,22 @@ text {* Legacy names *} +lemma Inf_singleton [simp]: + "\{a} = a" + by (auto intro: antisym Inf_lower Inf_greatest) + +lemma Sup_singleton [simp]: + "\{a} = a" + by (auto intro: antisym Sup_upper Sup_least) + +lemma Inf_binary: + "\{a, b} = a \ b" + by (simp add: Inf_insert) + +lemma Sup_binary: + "\{a, b} = a \ b" + by (simp add: Sup_insert) + lemmas (in complete_lattice) INFI_def = INF_def lemmas (in complete_lattice) SUPR_def = SUP_def lemmas (in complete_lattice) le_SUPI = le_SUP_I diff -r 4588597ba37e -r 81e55342cb86 src/HOL/Import/HOLLight/hollight.imp --- a/src/HOL/Import/HOLLight/hollight.imp Mon Aug 08 08:55:49 2011 -0700 +++ b/src/HOL/Import/HOLLight/hollight.imp Mon Aug 08 19:21:11 2011 +0200 @@ -591,7 +591,6 @@ "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE" "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC" "UNIONS_2" > "Complete_Lattice.Un_eq_Union" - "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton" "UNIONS_0" > "Complete_Lattice.Union_empty" "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def" "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace" @@ -1598,7 +1597,6 @@ "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE" "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC" "INTERS_2" > "Complete_Lattice.Int_eq_Inter" - "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton" "INTERS_0" > "Complete_Lattice.Inter_empty" "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV" "INSERT_UNION_EQ" > "Set.Un_insert_left"