New theory ProgressSets. Definition of closure sets
authorpaulson
Mon Mar 10 16:21:06 2003 +0100 (2003-03-10)
changeset 1385389131afa9f01
parent 13852 dd2cd94a51e6
child 13854 91c9ab25fece
New theory ProgressSets. Definition of closure sets
src/HOL/IsaMakefile
src/HOL/UNITY/ProgressSets.thy
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Transformers.thy
src/HOL/UNITY/UNITY_Main.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Mar 10 12:53:27 2003 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Mar 10 16:21:06 2003 +0100
     1.3 @@ -383,9 +383,9 @@
     1.4  $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
     1.5    UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
     1.6    UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
     1.7 -  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy \
     1.8 -  UNITY/Guar.thy UNITY/Lift_prog.thy  UNITY/ListOrder.thy  \
     1.9 -  UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy \
    1.10 +  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy\
    1.11 +  UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy\
    1.12 +  UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy\
    1.13    UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
    1.14    UNITY/Simple/Channel.thy UNITY/Simple/Common.thy  \
    1.15    UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy  \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 10 16:21:06 2003 +0100
     2.3 @@ -0,0 +1,116 @@
     2.4 +(*  Title:      HOL/UNITY/ProgressSets
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   2003  University of Cambridge
     2.8 +
     2.9 +Progress Sets.  From 
    2.10 +
    2.11 +    David Meier and Beverly Sanders,
    2.12 +    Composing Leads-to Properties
    2.13 +    Theoretical Computer Science 243:1-2 (2000), 339-361.
    2.14 +*)
    2.15 +
    2.16 +header{*Progress Sets*}
    2.17 +
    2.18 +theory ProgressSets = Transformers:
    2.19 +
    2.20 +constdefs
    2.21 +  closure_set :: "'a set set => bool"
    2.22 +   "closure_set C ==
    2.23 +	 (\<forall>D. D \<subseteq> C --> \<Inter>D \<in> C) & (\<forall>D. D \<subseteq> C --> \<Union>D \<in> C)"
    2.24 +
    2.25 +  cl :: "['a set set, 'a set] => 'a set"
    2.26 +   --{*short for ``closure''*}
    2.27 +   "cl C r == \<Inter>{x. x\<in>C & r \<subseteq> x}"
    2.28 +
    2.29 +lemma UNIV_in_closure_set: "closure_set C ==> UNIV \<in> C"
    2.30 +by (force simp add: closure_set_def)
    2.31 +
    2.32 +lemma empty_in_closure_set: "closure_set C ==> {} \<in> C"
    2.33 +by (force simp add: closure_set_def)
    2.34 +
    2.35 +lemma Union_in_closure_set: "[|D \<subseteq> C; closure_set C|] ==> \<Union>D \<in> C"
    2.36 +by (simp add: closure_set_def)
    2.37 +
    2.38 +lemma Inter_in_closure_set: "[|D \<subseteq> C; closure_set C|] ==> \<Inter>D \<in> C"
    2.39 +by (simp add: closure_set_def)
    2.40 +
    2.41 +lemma UN_in_closure_set:
    2.42 +     "[|closure_set C; !!i. i\<in>I ==> r i \<in> C|] ==> (\<Union>i\<in>I. r i) \<in> C"
    2.43 +apply (simp add: Set.UN_eq) 
    2.44 +apply (blast intro: Union_in_closure_set) 
    2.45 +done
    2.46 +
    2.47 +lemma IN_in_closure_set:
    2.48 +     "[|closure_set C; !!i. i\<in>I ==> r i \<in> C|] ==> (\<Inter>i\<in>I. r i)  \<in> C"
    2.49 +apply (simp add: INT_eq) 
    2.50 +apply (blast intro: Inter_in_closure_set) 
    2.51 +done
    2.52 +
    2.53 +lemma Un_in_closure_set: "[|x\<in>C; y\<in>C; closure_set C|] ==> x\<union>y \<in> C"
    2.54 +apply (simp only: Un_eq_Union) 
    2.55 +apply (blast intro: Union_in_closure_set) 
    2.56 +done
    2.57 +
    2.58 +lemma Int_in_closure_set: "[|x\<in>C; y\<in>C; closure_set C|] ==> x\<inter>y \<in> C"
    2.59 +apply (simp only: Int_eq_Inter) 
    2.60 +apply (blast intro: Inter_in_closure_set) 
    2.61 +done
    2.62 +
    2.63 +lemma closure_set_stable: "closure_set {X. F \<in> stable X}"
    2.64 +by (simp add: closure_set_def stable_def constrains_def, blast)
    2.65 +
    2.66 +text{*The next three results state that @{term "cl C r"} is the minimal
    2.67 + element of @{term C} that includes @{term r}.*}
    2.68 +lemma cl_in_closure_set: "closure_set C ==> cl C r \<in> C"
    2.69 +apply (simp add: closure_set_def cl_def)
    2.70 +apply (erule conjE)  
    2.71 +apply (drule spec, erule mp, blast) 
    2.72 +done
    2.73 +
    2.74 +lemma cl_least: "[|c\<in>C; r\<subseteq>c|] ==> cl C r \<subseteq> c" 
    2.75 +by (force simp add: cl_def)
    2.76 +
    2.77 +text{*The next three lemmas constitute assertion (4.61)*}
    2.78 +lemma cl_mono: "r \<subseteq> r' ==> cl C r \<subseteq> cl C r'"
    2.79 +by (simp add: cl_def, blast)
    2.80 +
    2.81 +lemma subset_cl: "r \<subseteq> cl C r"
    2.82 +by (simp add: cl_def, blast)
    2.83 +
    2.84 +lemma cl_UN_subset: "(\<Union>i\<in>I. cl C (r i)) \<subseteq> cl C (\<Union>i\<in>I. r i)"
    2.85 +by (simp add: cl_def, blast)
    2.86 +
    2.87 +lemma cl_Un: "closure_set C ==> cl C (r\<union>s) = cl C r \<union> cl C s"
    2.88 +apply (rule equalityI) 
    2.89 + prefer 2 
    2.90 +  apply (simp add: cl_def, blast)
    2.91 +apply (rule cl_least)
    2.92 + apply (blast intro: Un_in_closure_set cl_in_closure_set)
    2.93 +apply (blast intro: subset_cl [THEN subsetD])  
    2.94 +done
    2.95 +
    2.96 +lemma cl_UN: "closure_set C ==> cl C (\<Union>i\<in>I. r i) = (\<Union>i\<in>I. cl C (r i))"
    2.97 +apply (rule equalityI) 
    2.98 + prefer 2 
    2.99 +  apply (simp add: cl_def, blast)
   2.100 +apply (rule cl_least)
   2.101 + apply (blast intro: UN_in_closure_set cl_in_closure_set)
   2.102 +apply (blast intro: subset_cl [THEN subsetD])  
   2.103 +done
   2.104 +
   2.105 +lemma cl_idem [simp]: "cl C (cl C r) = cl C r"
   2.106 +by (simp add: cl_def, blast)
   2.107 +
   2.108 +lemma cl_ident: "r\<in>C ==> cl C r = r" 
   2.109 +by (force simp add: cl_def)
   2.110 +
   2.111 +text{*Assertion (4.62)*}
   2.112 +lemma cl_ident_iff: "closure_set C ==> (cl C r = r) = (r\<in>C)" 
   2.113 +apply (rule iffI) 
   2.114 + apply (erule subst)
   2.115 + apply (erule cl_in_closure_set)  
   2.116 +apply (erule cl_ident) 
   2.117 +done
   2.118 +
   2.119 +end
     3.1 --- a/src/HOL/UNITY/ROOT.ML	Mon Mar 10 12:53:27 2003 +0100
     3.2 +++ b/src/HOL/UNITY/ROOT.ML	Mon Mar 10 16:21:06 2003 +0100
     3.3 @@ -9,9 +9,6 @@
     3.4  (*Basic meta-theory*)
     3.5  time_use_thy "UNITY_Main";
     3.6  
     3.7 -(*New Meier/Sanders composition theory*)
     3.8 -time_use_thy "Transformers";
     3.9 -
    3.10  (*Simple examples: no composition*)
    3.11  time_use_thy "Simple/Deadlock";
    3.12  time_use_thy "Simple/Common";
     4.1 --- a/src/HOL/UNITY/Transformers.thy	Mon Mar 10 12:53:27 2003 +0100
     4.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Mar 10 16:21:06 2003 +0100
     4.3 @@ -465,4 +465,15 @@
     4.4  apply (erule ssubst, erule single_subset_wens_set) 
     4.5  done
     4.6  
     4.7 +text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
     4.8 +
     4.9 +lemma fp_leadsTo_Union:
    4.10 +    "[|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"
    4.11 +apply (rule leadsTo_Union) 
    4.12 +apply assumption; 
    4.13 + apply (simp add: FP_def awp_iff stable_def constrains_def) 
    4.14 + apply (blast intro: elim:); 
    4.15 +apply assumption; 
    4.16 +done
    4.17 +
    4.18  end
     5.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Mon Mar 10 12:53:27 2003 +0100
     5.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Mon Mar 10 16:21:06 2003 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  
     5.5  header{*Comprehensive UNITY Theory*}
     5.6  
     5.7 -theory UNITY_Main = Detects + PPROD + Follows + Transformers
     5.8 +theory UNITY_Main = Detects + PPROD + Follows + ProgressSets
     5.9  files "UNITY_tactics.ML":
    5.10  
    5.11  method_setup constrains = {*