new theory Transformers: Meier-Sanders non-interference theory
authorpaulson
Tue Feb 18 15:09:14 2003 +0100 (2003-02-18)
changeset 138210fd39aa77095
parent 13820 87a8ab465b29
child 13822 bb5eda7416e5
new theory Transformers: Meier-Sanders non-interference theory
src/HOL/IsaMakefile
src/HOL/UNITY/ROOT.ML
src/HOL/UNITY/Transformers.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Feb 17 17:16:07 2003 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Tue Feb 18 15:09:14 2003 +0100
     1.3 @@ -385,7 +385,7 @@
     1.4    UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
     1.5    UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy \
     1.6    UNITY/Guar.thy UNITY/Lift_prog.thy  UNITY/ListOrder.thy  \
     1.7 -  UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy \
     1.8 +  UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy \
     1.9    UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
    1.10    UNITY/Simple/Channel.thy UNITY/Simple/Common.thy  \
    1.11    UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy  \
     2.1 --- a/src/HOL/UNITY/ROOT.ML	Mon Feb 17 17:16:07 2003 +0100
     2.2 +++ b/src/HOL/UNITY/ROOT.ML	Tue Feb 18 15:09:14 2003 +0100
     2.3 @@ -9,6 +9,9 @@
     2.4  (*Basic meta-theory*)
     2.5  time_use_thy "UNITY_Main";
     2.6  
     2.7 +(*New Meier/Sanders composition theory*)
     2.8 +time_use_thy "Transformers";
     2.9 +
    2.10  (*Simple examples: no composition*)
    2.11  time_use_thy "Simple/Deadlock";
    2.12  time_use_thy "Simple/Common";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/UNITY/Transformers.thy	Tue Feb 18 15:09:14 2003 +0100
     3.3 @@ -0,0 +1,263 @@
     3.4 +(*  Title:      HOL/UNITY/Transformers
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   2003  University of Cambridge
     3.8 +
     3.9 +Predicate Transformers from 
    3.10 +
    3.11 +    David Meier and Beverly Sanders,
    3.12 +    Composing Leads-to Properties
    3.13 +    Theoretical Computer Science 243:1-2 (2000), 339-361.
    3.14 +*)
    3.15 +
    3.16 +header{*Predicate Transformers*}
    3.17 +
    3.18 +theory Transformers = Comp:
    3.19 +
    3.20 +subsection{*Defining the Predicate Transformers @{term wp},
    3.21 +   @{term awp} and  @{term wens}*}
    3.22 +
    3.23 +constdefs
    3.24 +  wp :: "[('a*'a) set, 'a set] => 'a set"  
    3.25 +    --{*Dijkstra's weakest-precondition operator*}
    3.26 +    "wp act B == - (act^-1 `` (-B))"
    3.27 +
    3.28 +  awp :: "[ 'a program, 'a set] => 'a set"  
    3.29 +    "awp F B == (\<Inter>act \<in> Acts F. wp act B)"
    3.30 +
    3.31 +  wens :: "[ 'a program, ('a*'a) set, 'a set] => 'a set"  
    3.32 +    "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
    3.33 +
    3.34 +text{*The fundamental theorem for wp*}
    3.35 +theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
    3.36 +by (force simp add: wp_def) 
    3.37 +
    3.38 +lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B"
    3.39 +by (force simp add: wp_def) 
    3.40 +
    3.41 +lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
    3.42 +by (simp add: awp_def wp_def, blast) 
    3.43 +
    3.44 +text{*The fundamental theorem for awp*}
    3.45 +theorem awp_iff: "(A <= awp F B) = (F \<in> A co B)"
    3.46 +by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 
    3.47 +
    3.48 +theorem stable_iff_awp: "(A \<subseteq> awp F A) = (F \<in> stable A)"
    3.49 +by (simp add: awp_iff stable_def) 
    3.50 +
    3.51 +lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B"
    3.52 +by (simp add: awp_def wp_def, blast)
    3.53 +
    3.54 +lemma wens_unfold:
    3.55 +     "wens F act B = (wp act B \<inter> awp F (B \<union> wens F act B)) \<union> B"
    3.56 +apply (simp add: wens_def) 
    3.57 +apply (rule gfp_unfold) 
    3.58 +apply (simp add: mono_def wp_def awp_def, blast) 
    3.59 +done
    3.60 +
    3.61 +text{*These two theorems justify the claim that @{term wens} returns the
    3.62 +weakest assertion satisfying the ensures property*}
    3.63 +lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
    3.64 +apply (simp add: wens_def ensures_def transient_def, clarify) 
    3.65 +apply (rule rev_bexI, assumption) 
    3.66 +apply (rule gfp_upperbound)
    3.67 +apply (simp add: constrains_def awp_def wp_def, blast)
    3.68 +done
    3.69 +
    3.70 +lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
    3.71 +by (simp add: wens_def gfp_def constrains_def awp_def wp_def
    3.72 +              ensures_def transient_def, blast) 
    3.73 +
    3.74 +text{*These two results constitute assertion (4.13) of the thesis*}
    3.75 +lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
    3.76 +apply (simp add: wens_def wp_def awp_def) 
    3.77 +apply (rule gfp_mono, blast) 
    3.78 +done
    3.79 +
    3.80 +lemma wens_weakening: "B \<subseteq> wens F act B"
    3.81 +by (simp add: wens_def gfp_def, blast)
    3.82 +
    3.83 +text{*Assertion (6), or 4.16 in the thesis*}
    3.84 +lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
    3.85 +apply (simp add: wens_def wp_def awp_def) 
    3.86 +apply (rule gfp_upperbound, blast) 
    3.87 +done
    3.88 +
    3.89 +text{*Assertion 4.17 in the thesis*}
    3.90 +lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
    3.91 +by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
    3.92 +
    3.93 +text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
    3.94 +hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}
    3.95 +lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)"
    3.96 +apply (simp add: stable_def)
    3.97 +apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
    3.98 +apply (simp add: Un_Int_distrib2 Compl_partition2) 
    3.99 +apply (erule constrains_weaken) 
   3.100 + apply blast 
   3.101 +apply (simp add: Un_subset_iff wens_weakening) 
   3.102 +done
   3.103 +
   3.104 +text{*Assertion 4.20 in the thesis.*}
   3.105 +lemma wens_Int_eq_lemma:
   3.106 +      "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   3.107 +       ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
   3.108 +apply (rule subset_wens) 
   3.109 +apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold])
   3.110 +apply (simp add: wp_def awp_def, blast)
   3.111 +done
   3.112 +
   3.113 +text{*Assertion (8): 4.21 in the thesis. Here we indeed require
   3.114 +      @{term "act \<in> Acts F"}*}
   3.115 +lemma wens_Int_eq:
   3.116 +      "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   3.117 +       ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
   3.118 +apply (rule equalityI)
   3.119 + apply (simp_all add: Int_lower1 Int_subset_iff) 
   3.120 + apply (rule wens_Int_eq_lemma, assumption+) 
   3.121 +apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
   3.122 +done
   3.123 +
   3.124 +subsection{*Defining the Weakest Ensures Set*}
   3.125 +
   3.126 +consts
   3.127 +  wens_set :: "['a program, 'a set] => 'a set set"
   3.128 +
   3.129 +inductive "wens_set F B"
   3.130 + intros 
   3.131 +
   3.132 +  Basis: "B \<in> wens_set F B"
   3.133 +
   3.134 +  Wens:  "[|X \<in> wens_set F B; act \<in> Acts F|] ==> wens F act X \<in> wens_set F B"
   3.135 +
   3.136 +  Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B"
   3.137 +
   3.138 +lemma wens_set_imp_co: "A \<in> wens_set F B ==> F \<in> (A-B) co A"
   3.139 +apply (erule wens_set.induct) 
   3.140 +  apply (simp add: constrains_def)
   3.141 + apply (drule_tac act1=act and A1=X 
   3.142 +        in constrains_Un [OF Diff_wens_constrains]) 
   3.143 + apply (erule constrains_weaken, blast) 
   3.144 + apply (simp add: Un_subset_iff wens_weakening) 
   3.145 +apply (rule constrains_weaken) 
   3.146 +apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
   3.147 +done
   3.148 +
   3.149 +lemma wens_set_imp_leadsTo: "A \<in> wens_set F B ==> F \<in> A leadsTo B"
   3.150 +apply (erule wens_set.induct)
   3.151 +  apply (rule leadsTo_refl)  
   3.152 + apply (blast intro: wens_ensures leadsTo_Basis leadsTo_Trans ) 
   3.153 +apply (blast intro: leadsTo_Union) 
   3.154 +done
   3.155 +
   3.156 +(*????????????????Set.thy Set.all_not_in_conv*)
   3.157 +lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
   3.158 +by blast
   3.159 +
   3.160 +
   3.161 +lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C"
   3.162 +apply (erule leadsTo_induct_pre)
   3.163 +  apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens)
   3.164 + apply clarify 
   3.165 + apply (drule ensures_weaken_R, assumption)  
   3.166 + apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
   3.167 +apply (case_tac "S={}") 
   3.168 + apply (simp, blast intro: wens_set.Basis)
   3.169 +apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def) 
   3.170 +apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>S. Z = f U}" in exI)
   3.171 +apply (blast intro: wens_set.Union) 
   3.172 +done
   3.173 +
   3.174 +text{*Assertion (9): 4.27 in the thesis.*}
   3.175 +
   3.176 +lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
   3.177 +by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 
   3.178 +
   3.179 +text{*This is the result that requires the definition of @{term wens_set} to
   3.180 +require @{term W} to be non-empty in the Unio case, for otherwise we should
   3.181 +always have @{term "{} \<in> wens_set F B"}.*}
   3.182 +lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
   3.183 +apply (erule wens_set.induct) 
   3.184 +  apply (blast intro: wens_weakening [THEN subsetD])+
   3.185 +done
   3.186 +
   3.187 +
   3.188 +subsection{*Properties Involving Program Union*}
   3.189 +
   3.190 +text{*Assertion (4.30) of thesis, reoriented*}
   3.191 +lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
   3.192 +by (simp add: awp_def wp_def, blast)
   3.193 +
   3.194 +lemma wens_subset: 
   3.195 +     "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
   3.196 +by (subst wens_unfold, fast) 
   3.197 +
   3.198 +text{*Assertion (4.31)*}
   3.199 +lemma subset_wens_Join:
   3.200 +      "[|A = T \<inter> wens F act B;  T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|] 
   3.201 +       ==> A \<subseteq> wens (F\<squnion>G) act B"
   3.202 +apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
   3.203 +                    wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
   3.204 + apply (rule subset_wens) 
   3.205 + apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
   3.206 + apply (simp add: awp_def wp_def, blast) 
   3.207 +apply (insert wens_subset [of F act B], blast) 
   3.208 +done
   3.209 +
   3.210 +text{*Assertion (4.32)*}
   3.211 +lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B"
   3.212 +apply (simp add: wens_def) 
   3.213 +apply (rule gfp_mono)
   3.214 +apply (auto simp add: awp_Join_eq)  
   3.215 +done
   3.216 +
   3.217 +text{*Lemma, because the inductive step is just too messy.*}
   3.218 +lemma wens_Union_inductive_step:
   3.219 +  assumes awpF: "T-B \<subseteq> awp F T"
   3.220 +      and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   3.221 +  shows "[|X \<in> wens_set F B; act \<in> Acts F; Y \<subseteq> X; T\<inter>X = T\<inter>Y|]
   3.222 +         ==> wens (F\<squnion>G) act Y \<subseteq> wens F act X \<and>
   3.223 +             T \<inter> wens F act X = T \<inter> wens (F\<squnion>G) act Y"
   3.224 +apply (subgoal_tac "wens (F\<squnion>G) act Y \<subseteq> wens F act X")  
   3.225 + prefer 2
   3.226 + apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
   3.227 +apply (rule equalityI) 
   3.228 + prefer 2 apply blast
   3.229 +apply (simp add: Int_lower1 Int_subset_iff) 
   3.230 +apply (frule wens_set_imp_subset) 
   3.231 +apply (subgoal_tac "T-X \<subseteq> awp F T")  
   3.232 + prefer 2 apply (blast intro: awpF [THEN subsetD]) 
   3.233 +apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans) 
   3.234 + prefer 2 apply (blast intro!: wens_mono)
   3.235 +apply (subst wens_Int_eq, assumption+) 
   3.236 +apply (rule subset_wens_Join [of _ T])
   3.237 +  apply simp 
   3.238 + apply blast
   3.239 +apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X")
   3.240 + prefer 2
   3.241 + apply (subst wens_Int_eq [symmetric], assumption+) 
   3.242 + apply (blast intro: wens_weakening [THEN subsetD], simp) 
   3.243 +apply (blast intro: awpG [THEN subsetD] wens_set.Wens)
   3.244 +done
   3.245 +
   3.246 +lemma wens_Union:
   3.247 +  assumes awpF: "T-B \<subseteq> awp F T"
   3.248 +      and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   3.249 +      and major: "X \<in> wens_set F B"
   3.250 +  shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y"
   3.251 +apply (rule wens_set.induct [OF major])
   3.252 +  txt{*Basis: trivial*}
   3.253 +  apply (blast intro: wens_set.Basis)
   3.254 + txt{*Inductive step*}
   3.255 + apply clarify 
   3.256 + apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
   3.257 +  apply (force intro: wens_set.Wens)
   3.258 + apply (simp add: wens_Union_inductive_step [OF awpF awpG]) 
   3.259 +txt{*Union: by Axiom of Choice*}
   3.260 +apply (simp add: ball_conj_distrib Bex_def) 
   3.261 +apply (clarify dest!: bchoice) 
   3.262 +apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI)
   3.263 +apply (blast intro: wens_set.Union) 
   3.264 +done
   3.265 +
   3.266 +end