New theory ProgressSets. Definition of closure sets

--- a/src/HOL/IsaMakefile	Mon Mar 10 12:53:27 2003 +0100
+++ b/src/HOL/IsaMakefile	Mon Mar 10 16:21:06 2003 +0100
@@ -383,9 +383,9 @@
 $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
   UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
   UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
-  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy \
-  UNITY/Guar.thy UNITY/Lift_prog.thy  UNITY/ListOrder.thy  \
-  UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy \
+  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy\
+  UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy\
+  UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy\
   UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
   UNITY/Simple/Channel.thy UNITY/Simple/Common.thy  \
   UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy  \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 10 16:21:06 2003 +0100
@@ -0,0 +1,116 @@
+(*  Title:      HOL/UNITY/ProgressSets
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2003  University of Cambridge
+
+Progress Sets.  From 
+
+    David Meier and Beverly Sanders,
+    Composing Leads-to Properties
+    Theoretical Computer Science 243:1-2 (2000), 339-361.
+*)
+
+header{*Progress Sets*}
+
+theory ProgressSets = Transformers:
+
+constdefs
+  closure_set :: "'a set set => bool"
+   "closure_set C ==
+	 (\<forall>D. D \<subseteq> C --> \<Inter>D \<in> C) & (\<forall>D. D \<subseteq> C --> \<Union>D \<in> C)"
+
+  cl :: "['a set set, 'a set] => 'a set"
+   --{*short for ``closure''*}
+   "cl C r == \<Inter>{x. x\<in>C & r \<subseteq> x}"
+
+lemma UNIV_in_closure_set: "closure_set C ==> UNIV \<in> C"
+by (force simp add: closure_set_def)
+
+lemma empty_in_closure_set: "closure_set C ==> {} \<in> C"
+by (force simp add: closure_set_def)
+
+lemma Union_in_closure_set: "[|D \<subseteq> C; closure_set C|] ==> \<Union>D \<in> C"
+by (simp add: closure_set_def)
+
+lemma Inter_in_closure_set: "[|D \<subseteq> C; closure_set C|] ==> \<Inter>D \<in> C"
+by (simp add: closure_set_def)
+
+lemma UN_in_closure_set:
+     "[|closure_set C; !!i. i\<in>I ==> r i \<in> C|] ==> (\<Union>i\<in>I. r i) \<in> C"
+apply (simp add: Set.UN_eq) 
+apply (blast intro: Union_in_closure_set) 
+done
+
+lemma IN_in_closure_set:
+     "[|closure_set C; !!i. i\<in>I ==> r i \<in> C|] ==> (\<Inter>i\<in>I. r i)  \<in> C"
+apply (simp add: INT_eq) 
+apply (blast intro: Inter_in_closure_set) 
+done
+
+lemma Un_in_closure_set: "[|x\<in>C; y\<in>C; closure_set C|] ==> x\<union>y \<in> C"
+apply (simp only: Un_eq_Union) 
+apply (blast intro: Union_in_closure_set) 
+done
+
+lemma Int_in_closure_set: "[|x\<in>C; y\<in>C; closure_set C|] ==> x\<inter>y \<in> C"
+apply (simp only: Int_eq_Inter) 
+apply (blast intro: Inter_in_closure_set) 
+done
+
+lemma closure_set_stable: "closure_set {X. F \<in> stable X}"
+by (simp add: closure_set_def stable_def constrains_def, blast)
+
+text{*The next three results state that @{term "cl C r"} is the minimal
+ element of @{term C} that includes @{term r}.*}
+lemma cl_in_closure_set: "closure_set C ==> cl C r \<in> C"
+apply (simp add: closure_set_def cl_def)
+apply (erule conjE)  
+apply (drule spec, erule mp, blast) 
+done
+
+lemma cl_least: "[|c\<in>C; r\<subseteq>c|] ==> cl C r \<subseteq> c" 
+by (force simp add: cl_def)
+
+text{*The next three lemmas constitute assertion (4.61)*}
+lemma cl_mono: "r \<subseteq> r' ==> cl C r \<subseteq> cl C r'"
+by (simp add: cl_def, blast)
+
+lemma subset_cl: "r \<subseteq> cl C r"
+by (simp add: cl_def, blast)
+
+lemma cl_UN_subset: "(\<Union>i\<in>I. cl C (r i)) \<subseteq> cl C (\<Union>i\<in>I. r i)"
+by (simp add: cl_def, blast)
+
+lemma cl_Un: "closure_set C ==> cl C (r\<union>s) = cl C r \<union> cl C s"
+apply (rule equalityI) 
+ prefer 2 
+  apply (simp add: cl_def, blast)
+apply (rule cl_least)
+ apply (blast intro: Un_in_closure_set cl_in_closure_set)
+apply (blast intro: subset_cl [THEN subsetD])  
+done
+
+lemma cl_UN: "closure_set C ==> cl C (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl C (r i))"
+apply (rule equalityI) 
+ prefer 2 
+  apply (simp add: cl_def, blast)
+apply (rule cl_least)
+ apply (blast intro: UN_in_closure_set cl_in_closure_set)
+apply (blast intro: subset_cl [THEN subsetD])  
+done
+
+lemma cl_idem [simp]: "cl C (cl C r) = cl C r"
+by (simp add: cl_def, blast)
+
+lemma cl_ident: "r\<in>C ==> cl C r = r" 
+by (force simp add: cl_def)
+
+text{*Assertion (4.62)*}
+lemma cl_ident_iff: "closure_set C ==> (cl C r = r) = (r\<in>C)" 
+apply (rule iffI) 
+ apply (erule subst)
+ apply (erule cl_in_closure_set)  
+apply (erule cl_ident) 
+done
+
+end

--- a/src/HOL/UNITY/ROOT.ML	Mon Mar 10 12:53:27 2003 +0100
+++ b/src/HOL/UNITY/ROOT.ML	Mon Mar 10 16:21:06 2003 +0100
@@ -9,9 +9,6 @@
 (*Basic meta-theory*)
 time_use_thy "UNITY_Main";
 
-(*New Meier/Sanders composition theory*)
-time_use_thy "Transformers";
-
 (*Simple examples: no composition*)
 time_use_thy "Simple/Deadlock";
 time_use_thy "Simple/Common";

--- a/src/HOL/UNITY/Transformers.thy	Mon Mar 10 12:53:27 2003 +0100
+++ b/src/HOL/UNITY/Transformers.thy	Mon Mar 10 16:21:06 2003 +0100
@@ -465,4 +465,15 @@
 apply (erule ssubst, erule single_subset_wens_set) 
 done
 
+text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
+
+lemma fp_leadsTo_Union:
+    "[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"
+apply (rule leadsTo_Union) 
+apply assumption; 
+ apply (simp add: FP_def awp_iff stable_def constrains_def) 
+ apply (blast intro: elim:); 
+apply assumption; 
+done
+
 end

--- a/src/HOL/UNITY/UNITY_Main.thy	Mon Mar 10 12:53:27 2003 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy	Mon Mar 10 16:21:06 2003 +0100
@@ -6,7 +6,7 @@
 
 header{*Comprehensive UNITY Theory*}
 
-theory UNITY_Main = Detects + PPROD + Follows + Transformers
+theory UNITY_Main = Detects + PPROD + Follows + ProgressSets
 files "UNITY_tactics.ML":
 
 method_setup constrains = {*