src/HOL/UNITY/Transformers.thy
changeset 13832 e7649436869c
parent 13821 0fd39aa77095
child 13851 f6923453953a
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Wed Feb 26 10:44:54 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Wed Feb 26 10:48:00 2003 +0100
     1.3 @@ -19,13 +19,15 @@
     1.4  
     1.5  constdefs
     1.6    wp :: "[('a*'a) set, 'a set] => 'a set"  
     1.7 -    --{*Dijkstra's weakest-precondition operator*}
     1.8 +    --{*Dijkstra's weakest-precondition operator (for an individual command)*}
     1.9      "wp act B == - (act^-1 `` (-B))"
    1.10  
    1.11 -  awp :: "[ 'a program, 'a set] => 'a set"  
    1.12 +  awp :: "['a program, 'a set] => 'a set"  
    1.13 +    --{*Dijkstra's weakest-precondition operator (for a program)*}
    1.14      "awp F B == (\<Inter>act \<in> Acts F. wp act B)"
    1.15  
    1.16 -  wens :: "[ 'a program, ('a*'a) set, 'a set] => 'a set"  
    1.17 +  wens :: "['a program, ('a*'a) set, 'a set] => 'a set"  
    1.18 +    --{*The weakest-ensures transformer*}
    1.19      "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
    1.20  
    1.21  text{*The fundamental theorem for wp*}
    1.22 @@ -35,6 +37,13 @@
    1.23  lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B"
    1.24  by (force simp add: wp_def) 
    1.25  
    1.26 +lemma wp_empty [simp]: "wp act {} = - (Domain act)"
    1.27 +by (force simp add: wp_def)
    1.28 +
    1.29 +text{*The identity relation is the skip action*}
    1.30 +lemma wp_Id [simp]: "wp Id B = B"
    1.31 +by (simp add: wp_def) 
    1.32 +
    1.33  lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
    1.34  by (simp add: awp_def wp_def, blast) 
    1.35  
    1.36 @@ -55,6 +64,9 @@
    1.37  apply (simp add: mono_def wp_def awp_def, blast) 
    1.38  done
    1.39  
    1.40 +lemma wens_Id [simp]: "wens F Id B = B"
    1.41 +by (simp add: wens_def gfp_def wp_def awp_def, blast)
    1.42 +
    1.43  text{*These two theorems justify the claim that @{term wens} returns the
    1.44  weakest assertion satisfying the ensures property*}
    1.45  lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
    1.46 @@ -93,8 +105,7 @@
    1.47  apply (simp add: stable_def)
    1.48  apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
    1.49  apply (simp add: Un_Int_distrib2 Compl_partition2) 
    1.50 -apply (erule constrains_weaken) 
    1.51 - apply blast 
    1.52 +apply (erule constrains_weaken, blast) 
    1.53  apply (simp add: Un_subset_iff wens_weakening) 
    1.54  done
    1.55  
    1.56 @@ -118,6 +129,7 @@
    1.57  apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
    1.58  done
    1.59  
    1.60 +
    1.61  subsection{*Defining the Weakest Ensures Set*}
    1.62  
    1.63  consts
    1.64 @@ -146,15 +158,10 @@
    1.65  lemma wens_set_imp_leadsTo: "A \<in> wens_set F B ==> F \<in> A leadsTo B"
    1.66  apply (erule wens_set.induct)
    1.67    apply (rule leadsTo_refl)  
    1.68 - apply (blast intro: wens_ensures leadsTo_Basis leadsTo_Trans ) 
    1.69 + apply (blast intro: wens_ensures leadsTo_Trans) 
    1.70  apply (blast intro: leadsTo_Union) 
    1.71  done
    1.72  
    1.73 -(*????????????????Set.thy Set.all_not_in_conv*)
    1.74 -lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
    1.75 -by blast
    1.76 -
    1.77 -
    1.78  lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C"
    1.79  apply (erule leadsTo_induct_pre)
    1.80    apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens)
    1.81 @@ -169,13 +176,12 @@
    1.82  done
    1.83  
    1.84  text{*Assertion (9): 4.27 in the thesis.*}
    1.85 -
    1.86  lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
    1.87  by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 
    1.88  
    1.89  text{*This is the result that requires the definition of @{term wens_set} to
    1.90 -require @{term W} to be non-empty in the Unio case, for otherwise we should
    1.91 -always have @{term "{} \<in> wens_set F B"}.*}
    1.92 +  require @{term W} to be non-empty in the Unio case, for otherwise we should
    1.93 +  always have @{term "{} \<in> wens_set F B"}.*}
    1.94  lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
    1.95  apply (erule wens_set.induct) 
    1.96    apply (blast intro: wens_weakening [THEN subsetD])+
    1.97 @@ -240,7 +246,7 @@
    1.98  apply (blast intro: awpG [THEN subsetD] wens_set.Wens)
    1.99  done
   1.100  
   1.101 -lemma wens_Union:
   1.102 +theorem wens_Union:
   1.103    assumes awpF: "T-B \<subseteq> awp F T"
   1.104        and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   1.105        and major: "X \<in> wens_set F B"
   1.106 @@ -260,4 +266,193 @@
   1.107  apply (blast intro: wens_set.Union) 
   1.108  done
   1.109  
   1.110 +theorem leadsTo_Union:
   1.111 +  assumes awpF: "T-B \<subseteq> awp F T"
   1.112 +      and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   1.113 +      and leadsTo: "F \<in> A leadsTo B"
   1.114 +  shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
   1.115 +apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) 
   1.116 +apply (rule wens_Union [THEN bexE]) 
   1.117 +   apply (rule awpF) 
   1.118 +  apply (erule awpG) 
   1.119 + apply assumption
   1.120 +apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L])  
   1.121 +done
   1.122 +
   1.123 +
   1.124 +subsection {*The Set @{term "wens_set F B"} for a Single-Assignment Program*}
   1.125 +text{*Thesis Section 4.3.3*}
   1.126 +
   1.127 +text{*We start by proving laws about single-assignment programs*}
   1.128 +lemma awp_single_eq [simp]:
   1.129 +     "awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B"
   1.130 +by (force simp add: awp_def wp_def) 
   1.131 +
   1.132 +lemma wp_Un_subset: "wp act A \<union> wp act B \<subseteq> wp act (A \<union> B)"
   1.133 +by (force simp add: wp_def)
   1.134 +
   1.135 +lemma wp_Un_eq: "single_valued act ==> wp act (A \<union> B) = wp act A \<union> wp act B"
   1.136 +apply (rule equalityI)
   1.137 + apply (force simp add: wp_def single_valued_def) 
   1.138 +apply (rule wp_Un_subset) 
   1.139 +done
   1.140 +
   1.141 +lemma wp_UN_subset: "(\<Union>i\<in>I. wp act (A i)) \<subseteq> wp act (\<Union>i\<in>I. A i)"
   1.142 +by (force simp add: wp_def)
   1.143 +
   1.144 +lemma wp_UN_eq:
   1.145 +     "[|single_valued act; I\<noteq>{}|]
   1.146 +      ==> wp act (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. wp act (A i))"
   1.147 +apply (rule equalityI)
   1.148 + prefer 2 apply (rule wp_UN_subset) 
   1.149 + apply (simp add: wp_def Image_INT_eq) 
   1.150 +done
   1.151 +
   1.152 +lemma wens_single_eq:
   1.153 +     "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
   1.154 +by (simp add: wens_def gfp_def wp_def, blast)
   1.155 +
   1.156 +
   1.157 +text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
   1.158 +
   1.159 +constdefs
   1.160 +  wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"  
   1.161 +    "wens_single_finite act B k == \<Union>i \<in> atMost k. ((wp act)^i) B"
   1.162 +
   1.163 +  wens_single :: "[('a*'a) set, 'a set] => 'a set"  
   1.164 +    "wens_single act B == \<Union>i. ((wp act)^i) B"
   1.165 +
   1.166 +lemma wens_single_Un_eq:
   1.167 +      "single_valued act
   1.168 +       ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
   1.169 +apply (rule equalityI)
   1.170 + apply (simp_all add: Un_upper1 Un_subset_iff) 
   1.171 +apply (simp add: wens_single_def wp_UN_eq, clarify) 
   1.172 +apply (rule_tac a="Suc(i)" in UN_I, auto) 
   1.173 +done
   1.174 +
   1.175 +lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}"
   1.176 +by force
   1.177 +
   1.178 +lemma wens_single_finite_Suc:
   1.179 +      "single_valued act
   1.180 +       ==> wens_single_finite act B (Suc k) =
   1.181 +           wens_single_finite act B k \<union> wp act (wens_single_finite act B k) "
   1.182 +apply (simp add: wens_single_finite_def image_def 
   1.183 +                 wp_UN_eq [OF _ atMost_nat_nonempty]) 
   1.184 +apply (force elim!: le_SucE)
   1.185 +done
   1.186 +
   1.187 +lemma wens_single_finite_Suc_eq_wens:
   1.188 +     "single_valued act
   1.189 +       ==> wens_single_finite act B (Suc k) =
   1.190 +           wens (mk_program (init, {act}, allowed)) act 
   1.191 +                (wens_single_finite act B k)"
   1.192 +by (simp add: wens_single_finite_Suc wens_single_eq) 
   1.193 +
   1.194 +lemma wens_single_finite_Un_eq:
   1.195 +      "single_valued act
   1.196 +       ==> wens_single_finite act B k \<union> wp act (wens_single_finite act B k)
   1.197 +           \<in> range (wens_single_finite act B)"
   1.198 +by (simp add: wens_single_finite_Suc [symmetric]) 
   1.199 +
   1.200 +lemma wens_single_eq_Union:
   1.201 +      "wens_single act B = \<Union>range (wens_single_finite act B)" 
   1.202 +by (simp add: wens_single_finite_def wens_single_def, blast) 
   1.203 +
   1.204 +lemma wens_single_finite_eq_Union:
   1.205 +     "wens_single_finite act B n = (\<Union>k\<in>atMost n. wens_single_finite act B k)"
   1.206 +apply (auto simp add: wens_single_finite_def) 
   1.207 +apply (blast intro: le_trans) 
   1.208 +done
   1.209 +
   1.210 +lemma wens_single_finite_mono:
   1.211 +     "m \<le> n ==> wens_single_finite act B m \<subseteq> wens_single_finite act B n"
   1.212 +by (force simp add:  wens_single_finite_eq_Union [of act B n]) 
   1.213 +
   1.214 +lemma wens_single_finite_subset_wens_single:
   1.215 +      "wens_single_finite act B k \<subseteq> wens_single act B"
   1.216 +by (simp add: wens_single_eq_Union, blast) 
   1.217 +
   1.218 +lemma subset_wens_single_finite:
   1.219 +      "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
   1.220 +       ==> \<exists>m. \<Union>W = wens_single_finite act B m"
   1.221 +apply (induct k) 
   1.222 + apply (simp, blast) 
   1.223 +apply (auto simp add: atMost_Suc) 
   1.224 +apply (case_tac "wens_single_finite act B (Suc n) \<in> W") 
   1.225 + prefer 2 apply blast 
   1.226 +apply (drule_tac x="Suc n" in spec)
   1.227 +apply (erule notE, rule equalityI)
   1.228 + prefer 2 apply blast 
   1.229 +apply (subst wens_single_finite_eq_Union) 
   1.230 +apply (simp add: atMost_Suc, blast) 
   1.231 +done
   1.232 +
   1.233 +text{*lemma for Union case*}
   1.234 +lemma Union_eq_wens_single:
   1.235 +      "\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k};
   1.236 +        W \<subseteq> insert (wens_single act B)
   1.237 +            (range (wens_single_finite act B))\<rbrakk>
   1.238 +       \<Longrightarrow> \<Union>W = wens_single act B"
   1.239 +apply (case_tac "wens_single act B \<in> W")
   1.240 + apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 
   1.241 +apply (simp add: wens_single_eq_Union) 
   1.242 +apply (rule equalityI)
   1.243 + apply blast 
   1.244 +apply (simp add: UN_subset_iff, clarify)
   1.245 +apply (subgoal_tac "\<exists>y\<in>W. \<exists>n. y = wens_single_finite act B n & i\<le>n")  
   1.246 + apply (blast intro: wens_single_finite_mono [THEN subsetD] ) 
   1.247 +apply (drule_tac x=i in spec)
   1.248 +apply (force simp add: atMost_def)
   1.249 +done
   1.250 +
   1.251 +lemma wens_set_subset_single:
   1.252 +      "single_valued act
   1.253 +       ==> wens_set (mk_program (init, {act}, allowed)) B \<subseteq> 
   1.254 +           insert (wens_single act B) (range (wens_single_finite act B))"
   1.255 +apply (rule subsetI)  
   1.256 +apply (erule wens_set.induct)
   1.257 +  txt{*Basis*} 
   1.258 +  apply (force simp add: wens_single_finite_def)
   1.259 + txt{*Wens inductive step*}
   1.260 + apply (case_tac "acta = Id", simp)   
   1.261 + apply (simp add: wens_single_eq)
   1.262 + apply (elim disjE)   
   1.263 + apply (simp add: wens_single_Un_eq)
   1.264 + apply (force simp add: wens_single_finite_Un_eq)
   1.265 +txt{*Union inductive step*}
   1.266 +apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)")
   1.267 + apply (blast dest!: subset_wens_single_finite, simp) 
   1.268 +apply (rule disjI1 [OF Union_eq_wens_single], blast+)
   1.269 +done
   1.270 +
   1.271 +lemma wens_single_finite_in_wens_set:
   1.272 +      "single_valued act \<Longrightarrow>
   1.273 +         wens_single_finite act B k
   1.274 +         \<in> wens_set (mk_program (init, {act}, allowed)) B"
   1.275 +apply (induct_tac k) 
   1.276 + apply (simp add: wens_single_finite_def wens_set.Basis)
   1.277 +apply (simp add: wens_set.Wens
   1.278 +                 wens_single_finite_Suc_eq_wens [of act B _ init allowed]) 
   1.279 +done
   1.280 +
   1.281 +lemma single_subset_wens_set:
   1.282 +      "single_valued act
   1.283 +       ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
   1.284 +           wens_set (mk_program (init, {act}, allowed)) B"
   1.285 +apply (simp add: wens_single_eq_Union UN_eq) 
   1.286 +apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
   1.287 +done
   1.288 +
   1.289 +text{*Theorem (4.29)*}
   1.290 +theorem wens_set_single_eq:
   1.291 +      "single_valued act
   1.292 +       ==> wens_set (mk_program (init, {act}, allowed)) B =
   1.293 +           insert (wens_single act B) (range (wens_single_finite act B))"
   1.294 +apply (rule equalityI)
   1.295 +apply (erule wens_set_subset_single) 
   1.296 +apply (erule single_subset_wens_set) 
   1.297 +done
   1.298 +
   1.299  end