# HG changeset patch
# User haftmann
# Date 1253101385 -7200
# Node ID caa5ada96a0012b04a1758658cad075042d2c424
# Parent  89b1f0cd9180491e431941ed447dbdc9aed2af0a
Inter and Union are mere abbreviations for Inf and Sup

diff -r 89b1f0cd9180 -r caa5ada96a00 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Wed Sep 16 09:04:41 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy	Wed Sep 16 13:43:05 2009 +0200
@@ -203,8 +203,8 @@
 
 subsection {* Union *}
 
-definition Union :: "'a set set \<Rightarrow> 'a set" where
-  Sup_set_eq [symmetric]: "Union S = \<Squnion>S"
+abbreviation Union :: "'a set set \<Rightarrow> 'a set" where
+  "Union S \<equiv> \<Squnion>S"
 
 notation (xsymbols)
   Union  ("\<Union>_" [90] 90)
@@ -216,7 +216,7 @@
   have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
     by auto
   then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
-    by (simp add: Sup_set_eq [symmetric] Sup_fun_def Sup_bool_def) (simp add: mem_def)
+    by (simp add: Sup_fun_def Sup_bool_def) (simp add: mem_def)
 qed
 
 lemma Union_iff [simp, noatp]:
@@ -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] Sup_set_eq)
+  by (simp add: SUPR_def SUPR_set_eq [symmetric])
 
 lemma Union_def:
   "\<Union>S = (\<Union>x\<in>S. x)"
@@ -439,8 +439,8 @@
 
 subsection {* Inter *}
 
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
-  Inf_set_eq [symmetric]: "Inter S = \<Sqinter>S"
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" where
+  "Inter S \<equiv> \<Sqinter>S"
   
 notation (xsymbols)
   Inter  ("\<Inter>_" [90] 90)
@@ -452,7 +452,7 @@
   have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
     by auto
   then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
-    by (simp add: Inf_fun_def Inf_bool_def Inf_set_eq [symmetric]) (simp add: mem_def)
+    by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
 qed
 
 lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)"
@@ -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] Inf_set_eq)
+  by (simp add: INFI_def INFI_set_eq [symmetric])
   
 lemma Inter_def:
   "\<Inter>S = (\<Inter>x\<in>S. x)"
diff -r 89b1f0cd9180 -r caa5ada96a00 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Sep 16 09:04:41 2009 +0200
+++ b/src/HOL/Inductive.thy	Wed Sep 16 13:43:05 2009 +0200
@@ -111,8 +111,7 @@
   and P_f: "!!S. P S ==> P(f S)"
   and P_Union: "!!M. !S:M. P S ==> P(Union M)"
   shows "P(lfp f)"
-  using assms unfolding Sup_set_eq [symmetric]
-  by (rule lfp_ordinal_induct [where P=P])
+  using assms by (rule lfp_ordinal_induct [where P=P])
 
 
 text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
diff -r 89b1f0cd9180 -r caa5ada96a00 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Wed Sep 16 09:04:41 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Wed Sep 16 13:43:05 2009 +0200
@@ -8,7 +8,7 @@
 imports Main Fset
 begin
 
-subsection {* Derived set operations *}
+subsection {* Preprocessor setup *}
 
 declare member [code] 
 
@@ -24,9 +24,7 @@
 definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   [code del]: "eq_set = op ="
 
-(* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code_unfold]
-*)
+(*declare eq_set_def [symmetric, code_unfold]*)
 
 lemma [code]:
   "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
@@ -37,13 +35,20 @@
 declare Inter_image_eq [symmetric, code]
 declare Union_image_eq [symmetric, code]
 
-
-subsection {* Rewrites for primitive operations *}
-
 declare List_Set.project_def [symmetric, code_unfold]
 
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+  "Inter = Complete_Lattice.Inter"
 
-subsection {* code generator setup *}
+declare Inter_def [symmetric, code_unfold]
+
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+  "Union = Complete_Lattice.Union"
+
+declare Union_def [symmetric, code_unfold]
+
+
+subsection {* Code generator setup *}
 
 ML {*
 nonfix inter;
@@ -75,8 +80,8 @@
   "op \<union>"              ("{*Fset.union*}")
   "op \<inter>"              ("{*Fset.inter*}")
   "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
-  "Complete_Lattice.Union" ("{*Fset.Union*}")
-  "Complete_Lattice.Inter" ("{*Fset.Inter*}")
+  "Union"             ("{*Fset.Union*}")
+  "Inter"             ("{*Fset.Inter*}")
   card                ("{*Fset.card*}")
   fold                ("{*foldl o flip*}")
 
diff -r 89b1f0cd9180 -r caa5ada96a00 src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Wed Sep 16 09:04:41 2009 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Wed Sep 16 13:43:05 2009 +0200
@@ -11134,7 +11134,6 @@
   shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
   and   "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
 apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
 apply(simp add: big_inter_eqvt)
 apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
 apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
@@ -11146,7 +11145,6 @@
 apply(drule subseteq_eqvt(1)[THEN iffD2])
 apply(simp add: perm_bool)
 apply(simp add: lfp_def)
-apply(simp add: Inf_set_eq)
 apply(simp add: big_inter_eqvt)
 apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
 apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
diff -r 89b1f0cd9180 -r caa5ada96a00 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Wed Sep 16 09:04:41 2009 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Wed Sep 16 13:43:05 2009 +0200
@@ -88,7 +88,7 @@
 done
 
 lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def, blast)
 
 text{*These two theorems justify the claim that @{term wens} returns the
 weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
 
 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
-              ensures_def transient_def Sup_set_eq, blast)
+              ensures_def transient_def, blast)
 
 text{*These two results constitute assertion (4.13) of the thesis*}
 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
 done
 
 lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def, blast)
 
 text{*Assertion (6), or 4.16 in the thesis*}
 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
@@ -120,7 +120,7 @@
 
 text{*Assertion 4.17 in the thesis*}
 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
   --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
       is declared as an iff-rule, then it's almost impossible to prove. 
       One proof is via @{text meson} after expanding all definitions, but it's
@@ -331,7 +331,7 @@
 
 lemma wens_single_eq:
      "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
+by (simp add: wens_def gfp_def wp_def, blast)
 
 
 text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
diff -r 89b1f0cd9180 -r caa5ada96a00 src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Wed Sep 16 09:04:41 2009 +0200
+++ b/src/HOL/ex/CTL.thy	Wed Sep 16 13:43:05 2009 +0200
@@ -95,7 +95,7 @@
     proof
       assume "x \<in> gfp (\<lambda>s. - f (- s))"
       then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
-	by (auto simp add: gfp_def Sup_set_eq)
+        by (auto simp add: gfp_def)
       then have "f (- u) \<subseteq> - u" by auto
       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
       from l and this have "x \<notin> u" by auto