src/HOL/UNITY/Transformers.thy
author paulson
Wed Feb 26 10:48:00 2003 +0100 (2003-02-26)
changeset 13832 e7649436869c
parent 13821 0fd39aa77095
child 13851 f6923453953a
permissions -rw-r--r--
completed proofs for programs consisting of a single assignment
     1 (*  Title:      HOL/UNITY/Transformers
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   2003  University of Cambridge
     5 
     6 Predicate Transformers from 
     7 
     8     David Meier and Beverly Sanders,
     9     Composing Leads-to Properties
    10     Theoretical Computer Science 243:1-2 (2000), 339-361.
    11 *)
    12 
    13 header{*Predicate Transformers*}
    14 
    15 theory Transformers = Comp:
    16 
    17 subsection{*Defining the Predicate Transformers @{term wp},
    18    @{term awp} and  @{term wens}*}
    19 
    20 constdefs
    21   wp :: "[('a*'a) set, 'a set] => 'a set"  
    22     --{*Dijkstra's weakest-precondition operator (for an individual command)*}
    23     "wp act B == - (act^-1 `` (-B))"
    24 
    25   awp :: "['a program, 'a set] => 'a set"  
    26     --{*Dijkstra's weakest-precondition operator (for a program)*}
    27     "awp F B == (\<Inter>act \<in> Acts F. wp act B)"
    28 
    29   wens :: "['a program, ('a*'a) set, 'a set] => 'a set"  
    30     --{*The weakest-ensures transformer*}
    31     "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
    32 
    33 text{*The fundamental theorem for wp*}
    34 theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
    35 by (force simp add: wp_def) 
    36 
    37 lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B"
    38 by (force simp add: wp_def) 
    39 
    40 lemma wp_empty [simp]: "wp act {} = - (Domain act)"
    41 by (force simp add: wp_def)
    42 
    43 text{*The identity relation is the skip action*}
    44 lemma wp_Id [simp]: "wp Id B = B"
    45 by (simp add: wp_def) 
    46 
    47 lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
    48 by (simp add: awp_def wp_def, blast) 
    49 
    50 text{*The fundamental theorem for awp*}
    51 theorem awp_iff: "(A <= awp F B) = (F \<in> A co B)"
    52 by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 
    53 
    54 theorem stable_iff_awp: "(A \<subseteq> awp F A) = (F \<in> stable A)"
    55 by (simp add: awp_iff stable_def) 
    56 
    57 lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B"
    58 by (simp add: awp_def wp_def, blast)
    59 
    60 lemma wens_unfold:
    61      "wens F act B = (wp act B \<inter> awp F (B \<union> wens F act B)) \<union> B"
    62 apply (simp add: wens_def) 
    63 apply (rule gfp_unfold) 
    64 apply (simp add: mono_def wp_def awp_def, blast) 
    65 done
    66 
    67 lemma wens_Id [simp]: "wens F Id B = B"
    68 by (simp add: wens_def gfp_def wp_def awp_def, blast)
    69 
    70 text{*These two theorems justify the claim that @{term wens} returns the
    71 weakest assertion satisfying the ensures property*}
    72 lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
    73 apply (simp add: wens_def ensures_def transient_def, clarify) 
    74 apply (rule rev_bexI, assumption) 
    75 apply (rule gfp_upperbound)
    76 apply (simp add: constrains_def awp_def wp_def, blast)
    77 done
    78 
    79 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
    80 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
    81               ensures_def transient_def, blast) 
    82 
    83 text{*These two results constitute assertion (4.13) of the thesis*}
    84 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
    85 apply (simp add: wens_def wp_def awp_def) 
    86 apply (rule gfp_mono, blast) 
    87 done
    88 
    89 lemma wens_weakening: "B \<subseteq> wens F act B"
    90 by (simp add: wens_def gfp_def, blast)
    91 
    92 text{*Assertion (6), or 4.16 in the thesis*}
    93 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
    94 apply (simp add: wens_def wp_def awp_def) 
    95 apply (rule gfp_upperbound, blast) 
    96 done
    97 
    98 text{*Assertion 4.17 in the thesis*}
    99 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
   100 by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
   101 
   102 text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
   103 hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}
   104 lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)"
   105 apply (simp add: stable_def)
   106 apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
   107 apply (simp add: Un_Int_distrib2 Compl_partition2) 
   108 apply (erule constrains_weaken, blast) 
   109 apply (simp add: Un_subset_iff wens_weakening) 
   110 done
   111 
   112 text{*Assertion 4.20 in the thesis.*}
   113 lemma wens_Int_eq_lemma:
   114       "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   115        ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
   116 apply (rule subset_wens) 
   117 apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold])
   118 apply (simp add: wp_def awp_def, blast)
   119 done
   120 
   121 text{*Assertion (8): 4.21 in the thesis. Here we indeed require
   122       @{term "act \<in> Acts F"}*}
   123 lemma wens_Int_eq:
   124       "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   125        ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
   126 apply (rule equalityI)
   127  apply (simp_all add: Int_lower1 Int_subset_iff) 
   128  apply (rule wens_Int_eq_lemma, assumption+) 
   129 apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
   130 done
   131 
   132 
   133 subsection{*Defining the Weakest Ensures Set*}
   134 
   135 consts
   136   wens_set :: "['a program, 'a set] => 'a set set"
   137 
   138 inductive "wens_set F B"
   139  intros 
   140 
   141   Basis: "B \<in> wens_set F B"
   142 
   143   Wens:  "[|X \<in> wens_set F B; act \<in> Acts F|] ==> wens F act X \<in> wens_set F B"
   144 
   145   Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B"
   146 
   147 lemma wens_set_imp_co: "A \<in> wens_set F B ==> F \<in> (A-B) co A"
   148 apply (erule wens_set.induct) 
   149   apply (simp add: constrains_def)
   150  apply (drule_tac act1=act and A1=X 
   151         in constrains_Un [OF Diff_wens_constrains]) 
   152  apply (erule constrains_weaken, blast) 
   153  apply (simp add: Un_subset_iff wens_weakening) 
   154 apply (rule constrains_weaken) 
   155 apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
   156 done
   157 
   158 lemma wens_set_imp_leadsTo: "A \<in> wens_set F B ==> F \<in> A leadsTo B"
   159 apply (erule wens_set.induct)
   160   apply (rule leadsTo_refl)  
   161  apply (blast intro: wens_ensures leadsTo_Trans) 
   162 apply (blast intro: leadsTo_Union) 
   163 done
   164 
   165 lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C"
   166 apply (erule leadsTo_induct_pre)
   167   apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens)
   168  apply clarify 
   169  apply (drule ensures_weaken_R, assumption)  
   170  apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
   171 apply (case_tac "S={}") 
   172  apply (simp, blast intro: wens_set.Basis)
   173 apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def) 
   174 apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>S. Z = f U}" in exI)
   175 apply (blast intro: wens_set.Union) 
   176 done
   177 
   178 text{*Assertion (9): 4.27 in the thesis.*}
   179 lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
   180 by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 
   181 
   182 text{*This is the result that requires the definition of @{term wens_set} to
   183   require @{term W} to be non-empty in the Unio case, for otherwise we should
   184   always have @{term "{} \<in> wens_set F B"}.*}
   185 lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
   186 apply (erule wens_set.induct) 
   187   apply (blast intro: wens_weakening [THEN subsetD])+
   188 done
   189 
   190 
   191 subsection{*Properties Involving Program Union*}
   192 
   193 text{*Assertion (4.30) of thesis, reoriented*}
   194 lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
   195 by (simp add: awp_def wp_def, blast)
   196 
   197 lemma wens_subset: 
   198      "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
   199 by (subst wens_unfold, fast) 
   200 
   201 text{*Assertion (4.31)*}
   202 lemma subset_wens_Join:
   203       "[|A = T \<inter> wens F act B;  T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|] 
   204        ==> A \<subseteq> wens (F\<squnion>G) act B"
   205 apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
   206                     wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
   207  apply (rule subset_wens) 
   208  apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
   209  apply (simp add: awp_def wp_def, blast) 
   210 apply (insert wens_subset [of F act B], blast) 
   211 done
   212 
   213 text{*Assertion (4.32)*}
   214 lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B"
   215 apply (simp add: wens_def) 
   216 apply (rule gfp_mono)
   217 apply (auto simp add: awp_Join_eq)  
   218 done
   219 
   220 text{*Lemma, because the inductive step is just too messy.*}
   221 lemma wens_Union_inductive_step:
   222   assumes awpF: "T-B \<subseteq> awp F T"
   223       and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   224   shows "[|X \<in> wens_set F B; act \<in> Acts F; Y \<subseteq> X; T\<inter>X = T\<inter>Y|]
   225          ==> wens (F\<squnion>G) act Y \<subseteq> wens F act X \<and>
   226              T \<inter> wens F act X = T \<inter> wens (F\<squnion>G) act Y"
   227 apply (subgoal_tac "wens (F\<squnion>G) act Y \<subseteq> wens F act X")  
   228  prefer 2
   229  apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
   230 apply (rule equalityI) 
   231  prefer 2 apply blast
   232 apply (simp add: Int_lower1 Int_subset_iff) 
   233 apply (frule wens_set_imp_subset) 
   234 apply (subgoal_tac "T-X \<subseteq> awp F T")  
   235  prefer 2 apply (blast intro: awpF [THEN subsetD]) 
   236 apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans) 
   237  prefer 2 apply (blast intro!: wens_mono)
   238 apply (subst wens_Int_eq, assumption+) 
   239 apply (rule subset_wens_Join [of _ T])
   240   apply simp 
   241  apply blast
   242 apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X")
   243  prefer 2
   244  apply (subst wens_Int_eq [symmetric], assumption+) 
   245  apply (blast intro: wens_weakening [THEN subsetD], simp) 
   246 apply (blast intro: awpG [THEN subsetD] wens_set.Wens)
   247 done
   248 
   249 theorem wens_Union:
   250   assumes awpF: "T-B \<subseteq> awp F T"
   251       and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   252       and major: "X \<in> wens_set F B"
   253   shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y"
   254 apply (rule wens_set.induct [OF major])
   255   txt{*Basis: trivial*}
   256   apply (blast intro: wens_set.Basis)
   257  txt{*Inductive step*}
   258  apply clarify 
   259  apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
   260   apply (force intro: wens_set.Wens)
   261  apply (simp add: wens_Union_inductive_step [OF awpF awpG]) 
   262 txt{*Union: by Axiom of Choice*}
   263 apply (simp add: ball_conj_distrib Bex_def) 
   264 apply (clarify dest!: bchoice) 
   265 apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI)
   266 apply (blast intro: wens_set.Union) 
   267 done
   268 
   269 theorem leadsTo_Union:
   270   assumes awpF: "T-B \<subseteq> awp F T"
   271       and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   272       and leadsTo: "F \<in> A leadsTo B"
   273   shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
   274 apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) 
   275 apply (rule wens_Union [THEN bexE]) 
   276    apply (rule awpF) 
   277   apply (erule awpG) 
   278  apply assumption
   279 apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L])  
   280 done
   281 
   282 
   283 subsection {*The Set @{term "wens_set F B"} for a Single-Assignment Program*}
   284 text{*Thesis Section 4.3.3*}
   285 
   286 text{*We start by proving laws about single-assignment programs*}
   287 lemma awp_single_eq [simp]:
   288      "awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B"
   289 by (force simp add: awp_def wp_def) 
   290 
   291 lemma wp_Un_subset: "wp act A \<union> wp act B \<subseteq> wp act (A \<union> B)"
   292 by (force simp add: wp_def)
   293 
   294 lemma wp_Un_eq: "single_valued act ==> wp act (A \<union> B) = wp act A \<union> wp act B"
   295 apply (rule equalityI)
   296  apply (force simp add: wp_def single_valued_def) 
   297 apply (rule wp_Un_subset) 
   298 done
   299 
   300 lemma wp_UN_subset: "(\<Union>i\<in>I. wp act (A i)) \<subseteq> wp act (\<Union>i\<in>I. A i)"
   301 by (force simp add: wp_def)
   302 
   303 lemma wp_UN_eq:
   304      "[|single_valued act; I\<noteq>{}|]
   305       ==> wp act (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. wp act (A i))"
   306 apply (rule equalityI)
   307  prefer 2 apply (rule wp_UN_subset) 
   308  apply (simp add: wp_def Image_INT_eq) 
   309 done
   310 
   311 lemma wens_single_eq:
   312      "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
   313 by (simp add: wens_def gfp_def wp_def, blast)
   314 
   315 
   316 text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
   317 
   318 constdefs
   319   wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set"  
   320     "wens_single_finite act B k == \<Union>i \<in> atMost k. ((wp act)^i) B"
   321 
   322   wens_single :: "[('a*'a) set, 'a set] => 'a set"  
   323     "wens_single act B == \<Union>i. ((wp act)^i) B"
   324 
   325 lemma wens_single_Un_eq:
   326       "single_valued act
   327        ==> wens_single act B \<union> wp act (wens_single act B) = wens_single act B"
   328 apply (rule equalityI)
   329  apply (simp_all add: Un_upper1 Un_subset_iff) 
   330 apply (simp add: wens_single_def wp_UN_eq, clarify) 
   331 apply (rule_tac a="Suc(i)" in UN_I, auto) 
   332 done
   333 
   334 lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}"
   335 by force
   336 
   337 lemma wens_single_finite_Suc:
   338       "single_valued act
   339        ==> wens_single_finite act B (Suc k) =
   340            wens_single_finite act B k \<union> wp act (wens_single_finite act B k) "
   341 apply (simp add: wens_single_finite_def image_def 
   342                  wp_UN_eq [OF _ atMost_nat_nonempty]) 
   343 apply (force elim!: le_SucE)
   344 done
   345 
   346 lemma wens_single_finite_Suc_eq_wens:
   347      "single_valued act
   348        ==> wens_single_finite act B (Suc k) =
   349            wens (mk_program (init, {act}, allowed)) act 
   350                 (wens_single_finite act B k)"
   351 by (simp add: wens_single_finite_Suc wens_single_eq) 
   352 
   353 lemma wens_single_finite_Un_eq:
   354       "single_valued act
   355        ==> wens_single_finite act B k \<union> wp act (wens_single_finite act B k)
   356            \<in> range (wens_single_finite act B)"
   357 by (simp add: wens_single_finite_Suc [symmetric]) 
   358 
   359 lemma wens_single_eq_Union:
   360       "wens_single act B = \<Union>range (wens_single_finite act B)" 
   361 by (simp add: wens_single_finite_def wens_single_def, blast) 
   362 
   363 lemma wens_single_finite_eq_Union:
   364      "wens_single_finite act B n = (\<Union>k\<in>atMost n. wens_single_finite act B k)"
   365 apply (auto simp add: wens_single_finite_def) 
   366 apply (blast intro: le_trans) 
   367 done
   368 
   369 lemma wens_single_finite_mono:
   370      "m \<le> n ==> wens_single_finite act B m \<subseteq> wens_single_finite act B n"
   371 by (force simp add:  wens_single_finite_eq_Union [of act B n]) 
   372 
   373 lemma wens_single_finite_subset_wens_single:
   374       "wens_single_finite act B k \<subseteq> wens_single act B"
   375 by (simp add: wens_single_eq_Union, blast) 
   376 
   377 lemma subset_wens_single_finite:
   378       "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
   379        ==> \<exists>m. \<Union>W = wens_single_finite act B m"
   380 apply (induct k) 
   381  apply (simp, blast) 
   382 apply (auto simp add: atMost_Suc) 
   383 apply (case_tac "wens_single_finite act B (Suc n) \<in> W") 
   384  prefer 2 apply blast 
   385 apply (drule_tac x="Suc n" in spec)
   386 apply (erule notE, rule equalityI)
   387  prefer 2 apply blast 
   388 apply (subst wens_single_finite_eq_Union) 
   389 apply (simp add: atMost_Suc, blast) 
   390 done
   391 
   392 text{*lemma for Union case*}
   393 lemma Union_eq_wens_single:
   394       "\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k};
   395         W \<subseteq> insert (wens_single act B)
   396             (range (wens_single_finite act B))\<rbrakk>
   397        \<Longrightarrow> \<Union>W = wens_single act B"
   398 apply (case_tac "wens_single act B \<in> W")
   399  apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 
   400 apply (simp add: wens_single_eq_Union) 
   401 apply (rule equalityI)
   402  apply blast 
   403 apply (simp add: UN_subset_iff, clarify)
   404 apply (subgoal_tac "\<exists>y\<in>W. \<exists>n. y = wens_single_finite act B n & i\<le>n")  
   405  apply (blast intro: wens_single_finite_mono [THEN subsetD] ) 
   406 apply (drule_tac x=i in spec)
   407 apply (force simp add: atMost_def)
   408 done
   409 
   410 lemma wens_set_subset_single:
   411       "single_valued act
   412        ==> wens_set (mk_program (init, {act}, allowed)) B \<subseteq> 
   413            insert (wens_single act B) (range (wens_single_finite act B))"
   414 apply (rule subsetI)  
   415 apply (erule wens_set.induct)
   416   txt{*Basis*} 
   417   apply (force simp add: wens_single_finite_def)
   418  txt{*Wens inductive step*}
   419  apply (case_tac "acta = Id", simp)   
   420  apply (simp add: wens_single_eq)
   421  apply (elim disjE)   
   422  apply (simp add: wens_single_Un_eq)
   423  apply (force simp add: wens_single_finite_Un_eq)
   424 txt{*Union inductive step*}
   425 apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)")
   426  apply (blast dest!: subset_wens_single_finite, simp) 
   427 apply (rule disjI1 [OF Union_eq_wens_single], blast+)
   428 done
   429 
   430 lemma wens_single_finite_in_wens_set:
   431       "single_valued act \<Longrightarrow>
   432          wens_single_finite act B k
   433          \<in> wens_set (mk_program (init, {act}, allowed)) B"
   434 apply (induct_tac k) 
   435  apply (simp add: wens_single_finite_def wens_set.Basis)
   436 apply (simp add: wens_set.Wens
   437                  wens_single_finite_Suc_eq_wens [of act B _ init allowed]) 
   438 done
   439 
   440 lemma single_subset_wens_set:
   441       "single_valued act
   442        ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
   443            wens_set (mk_program (init, {act}, allowed)) B"
   444 apply (simp add: wens_single_eq_Union UN_eq) 
   445 apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
   446 done
   447 
   448 text{*Theorem (4.29)*}
   449 theorem wens_set_single_eq:
   450       "single_valued act
   451        ==> wens_set (mk_program (init, {act}, allowed)) B =
   452            insert (wens_single act B) (range (wens_single_finite act B))"
   453 apply (rule equalityI)
   454 apply (erule wens_set_subset_single) 
   455 apply (erule single_subset_wens_set) 
   456 done
   457 
   458 end