# HG changeset patch # User haftmann # Date 1253275778 -7200 # Node ID b5c3a8a7577245b91aa805e57c327fef1ed93088 # Parent 43ed78ee285d9d89948b527db334df11d3bc5193 INTER and UNION are mere abbreviations for INFI and SUPR diff -r 43ed78ee285d -r b5c3a8a75772 NEWS --- a/NEWS Fri Sep 18 09:35:23 2009 +0200 +++ b/NEWS Fri Sep 18 14:09:38 2009 +0200 @@ -79,8 +79,8 @@ Set.INTER ~> Complete_Lattice.INTER Set.UNION ~> Complete_Lattice.UNION - more convenient names for set intersection and union: - Set.Int ~> Set.inter - Set.Un ~> Set.union + Set.Int ~> Set.inter + Set.Un ~> Set.union - authentic syntax for Set.Pow Set.image @@ -89,6 +89,8 @@ Set.UNIV (for top) Complete_Lattice.Inter (for Inf) Complete_Lattice.Union (for Sup) + Complete_Lattice.INTER (for INFI) + Complete_Lattice.UNION (for SUPR) - object-logic definitions as far as appropriate INCOMPATIBILITY. diff -r 43ed78ee285d -r b5c3a8a75772 src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Fri Sep 18 09:35:23 2009 +0200 +++ b/src/HOL/Complete_Lattice.thy Fri Sep 18 14:09:38 2009 +0200 @@ -278,8 +278,8 @@ subsection {* Unions of families *} -definition UNION :: "'a set \ ('a \ 'b set) \ 'b set" where - SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)" +abbreviation UNION :: "'a set \ ('a \ 'b set) \ 'b set" where + "UNION \ SUPR" syntax "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10) @@ -314,7 +314,7 @@ lemma UNION_eq_Union_image: "(\x\A. B x) = \(B`A)" - by (simp add: SUPR_def SUPR_set_eq [symmetric]) + by (fact SUPR_def) lemma Union_def: "\S = (\x\S. x)" @@ -351,7 +351,7 @@ by blast lemma UN_upper: "a \ A ==> B a \ (\x\A. B x)" - by blast + by (fact le_SUPI) lemma UN_least: "(!!x. x \ A ==> B x \ C) ==> (\x\A. B x) \ C" by (iprover intro: subsetI elim: UN_E dest: subsetD) @@ -514,8 +514,8 @@ subsection {* Intersections of families *} -definition INTER :: "'a set \ ('a \ 'b set) \ 'b set" where - INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)" +abbreviation INTER :: "'a set \ ('a \ 'b set) \ 'b set" where + "INTER \ INFI" syntax "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10) @@ -541,7 +541,7 @@ lemma INTER_eq_Inter_image: "(\x\A. B x) = \(B`A)" - by (simp add: INFI_def INFI_set_eq [symmetric]) + by (fact INFI_def) lemma Inter_def: "\S = (\x\S. x)" @@ -579,10 +579,10 @@ by blast lemma INT_lower: "a \ A ==> (\x\A. B x) \ B a" - by blast + by (fact INF_leI) lemma INT_greatest: "(!!x. x \ A ==> C \ B x) ==> C \ (\x\A. B x)" - by (iprover intro: INT_I subsetI dest: subsetD) + by (fact le_INFI) lemma INT_empty [simp]: "(\x\{}. B x) = UNIV" by blast diff -r 43ed78ee285d -r b5c3a8a75772 src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Fri Sep 18 09:35:23 2009 +0200 +++ b/src/HOL/Library/Executable_Set.thy Fri Sep 18 14:09:38 2009 +0200 @@ -32,8 +32,8 @@ declare inter [code] -declare Inter_image_eq [symmetric, code] -declare Union_image_eq [symmetric, code] +declare Inter_image_eq [symmetric, code_unfold] +declare Union_image_eq [symmetric, code_unfold] declare List_Set.project_def [symmetric, code_unfold]