Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
INTER and UNION are mere abbreviations for INFI and SUPR
authorhaftmann
Fri, 18 Sep 2009 14:09:38 +0200
changeset 32606 b5c3a8a75772
parent 32605 43ed78ee285d
child 32608 c0056c2c1d17
child 32683 7c1fe854ca6a
INTER and UNION are mere abbreviations for INFI and SUPR
NEWS file | annotate | diff | comparison | revisions
src/HOL/Complete_Lattice.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Executable_Set.thy file | annotate | diff | comparison | revisions 
--- 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.
--- 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 \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  SUPR_set_eq [symmetric]: "UNION S f = (SUP x:S. f x)"
+abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+  "UNION \<equiv> SUPR"
 
 syntax
   "@UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
@@ -314,7 +314,7 @@
 
 lemma UNION_eq_Union_image:
   "(\<Union>x\<in>A. B x) = \<Union>(B`A)"
-  by (simp add: SUPR_def SUPR_set_eq [symmetric])
+  by (fact SUPR_def)
 
 lemma Union_def:
   "\<Union>S = (\<Union>x\<in>S. x)"
@@ -351,7 +351,7 @@
   by blast
 
 lemma UN_upper: "a \<in> A ==> B a \<subseteq> (\<Union>x\<in>A. B x)"
-  by blast
+  by (fact le_SUPI)
 
 lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
   by (iprover intro: subsetI elim: UN_E dest: subsetD)
@@ -514,8 +514,8 @@
 
 subsection {* Intersections of families *}
 
-definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  INFI_set_eq [symmetric]: "INTER S f = (INF x:S. f x)"
+abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+  "INTER \<equiv> INFI"
 
 syntax
   "@INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
@@ -541,7 +541,7 @@
 
 lemma INTER_eq_Inter_image:
   "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
-  by (simp add: INFI_def INFI_set_eq [symmetric])
+  by (fact INFI_def)
   
 lemma Inter_def:
   "\<Inter>S = (\<Inter>x\<in>S. x)"
@@ -579,10 +579,10 @@
   by blast
 
 lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
-  by blast
+  by (fact INF_leI)
 
 lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
-  by (iprover intro: INT_I subsetI dest: subsetD)
+  by (fact le_INFI)
 
 lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
   by blast
--- 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]
isabelle