src/HOL/UNITY/Transformers.thy
author paulson
Tue Feb 18 15:09:14 2003 +0100 (2003-02-18)
changeset 13821 0fd39aa77095
child 13832 e7649436869c
permissions -rw-r--r--
new theory Transformers: Meier-Sanders non-interference theory
     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*}
    23     "wp act B == - (act^-1 `` (-B))"
    24 
    25   awp :: "[ 'a program, 'a set] => 'a set"  
    26     "awp F B == (\<Inter>act \<in> Acts F. wp act B)"
    27 
    28   wens :: "[ 'a program, ('a*'a) set, 'a set] => 'a set"  
    29     "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
    30 
    31 text{*The fundamental theorem for wp*}
    32 theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
    33 by (force simp add: wp_def) 
    34 
    35 lemma Compl_Domain_subset_wp: "- (Domain act) \<subseteq> wp act B"
    36 by (force simp add: wp_def) 
    37 
    38 lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
    39 by (simp add: awp_def wp_def, blast) 
    40 
    41 text{*The fundamental theorem for awp*}
    42 theorem awp_iff: "(A <= awp F B) = (F \<in> A co B)"
    43 by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 
    44 
    45 theorem stable_iff_awp: "(A \<subseteq> awp F A) = (F \<in> stable A)"
    46 by (simp add: awp_iff stable_def) 
    47 
    48 lemma awp_mono: "(A \<subseteq> B) ==> awp F A \<subseteq> awp F B"
    49 by (simp add: awp_def wp_def, blast)
    50 
    51 lemma wens_unfold:
    52      "wens F act B = (wp act B \<inter> awp F (B \<union> wens F act B)) \<union> B"
    53 apply (simp add: wens_def) 
    54 apply (rule gfp_unfold) 
    55 apply (simp add: mono_def wp_def awp_def, blast) 
    56 done
    57 
    58 text{*These two theorems justify the claim that @{term wens} returns the
    59 weakest assertion satisfying the ensures property*}
    60 lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
    61 apply (simp add: wens_def ensures_def transient_def, clarify) 
    62 apply (rule rev_bexI, assumption) 
    63 apply (rule gfp_upperbound)
    64 apply (simp add: constrains_def awp_def wp_def, blast)
    65 done
    66 
    67 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
    68 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
    69               ensures_def transient_def, blast) 
    70 
    71 text{*These two results constitute assertion (4.13) of the thesis*}
    72 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
    73 apply (simp add: wens_def wp_def awp_def) 
    74 apply (rule gfp_mono, blast) 
    75 done
    76 
    77 lemma wens_weakening: "B \<subseteq> wens F act B"
    78 by (simp add: wens_def gfp_def, blast)
    79 
    80 text{*Assertion (6), or 4.16 in the thesis*}
    81 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
    82 apply (simp add: wens_def wp_def awp_def) 
    83 apply (rule gfp_upperbound, blast) 
    84 done
    85 
    86 text{*Assertion 4.17 in the thesis*}
    87 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
    88 by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
    89 
    90 text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
    91 hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}
    92 lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)"
    93 apply (simp add: stable_def)
    94 apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
    95 apply (simp add: Un_Int_distrib2 Compl_partition2) 
    96 apply (erule constrains_weaken) 
    97  apply blast 
    98 apply (simp add: Un_subset_iff wens_weakening) 
    99 done
   100 
   101 text{*Assertion 4.20 in the thesis.*}
   102 lemma wens_Int_eq_lemma:
   103       "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   104        ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
   105 apply (rule subset_wens) 
   106 apply (rule_tac P="\<lambda>x. ?f x \<subseteq> ?b" in ssubst [OF wens_unfold])
   107 apply (simp add: wp_def awp_def, blast)
   108 done
   109 
   110 text{*Assertion (8): 4.21 in the thesis. Here we indeed require
   111       @{term "act \<in> Acts F"}*}
   112 lemma wens_Int_eq:
   113       "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
   114        ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
   115 apply (rule equalityI)
   116  apply (simp_all add: Int_lower1 Int_subset_iff) 
   117  apply (rule wens_Int_eq_lemma, assumption+) 
   118 apply (rule subset_trans [OF _ wens_mono [of "T\<inter>B" B]], auto) 
   119 done
   120 
   121 subsection{*Defining the Weakest Ensures Set*}
   122 
   123 consts
   124   wens_set :: "['a program, 'a set] => 'a set set"
   125 
   126 inductive "wens_set F B"
   127  intros 
   128 
   129   Basis: "B \<in> wens_set F B"
   130 
   131   Wens:  "[|X \<in> wens_set F B; act \<in> Acts F|] ==> wens F act X \<in> wens_set F B"
   132 
   133   Union: "W \<noteq> {} ==> \<forall>U \<in> W. U \<in> wens_set F B ==> \<Union>W \<in> wens_set F B"
   134 
   135 lemma wens_set_imp_co: "A \<in> wens_set F B ==> F \<in> (A-B) co A"
   136 apply (erule wens_set.induct) 
   137   apply (simp add: constrains_def)
   138  apply (drule_tac act1=act and A1=X 
   139         in constrains_Un [OF Diff_wens_constrains]) 
   140  apply (erule constrains_weaken, blast) 
   141  apply (simp add: Un_subset_iff wens_weakening) 
   142 apply (rule constrains_weaken) 
   143 apply (rule_tac I=W and A="\<lambda>v. v-B" and A'="\<lambda>v. v" in constrains_UN, blast+)
   144 done
   145 
   146 lemma wens_set_imp_leadsTo: "A \<in> wens_set F B ==> F \<in> A leadsTo B"
   147 apply (erule wens_set.induct)
   148   apply (rule leadsTo_refl)  
   149  apply (blast intro: wens_ensures leadsTo_Basis leadsTo_Trans ) 
   150 apply (blast intro: leadsTo_Union) 
   151 done
   152 
   153 (*????????????????Set.thy Set.all_not_in_conv*)
   154 lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
   155 by blast
   156 
   157 
   158 lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C"
   159 apply (erule leadsTo_induct_pre)
   160   apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens)
   161  apply clarify 
   162  apply (drule ensures_weaken_R, assumption)  
   163  apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
   164 apply (case_tac "S={}") 
   165  apply (simp, blast intro: wens_set.Basis)
   166 apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def) 
   167 apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>S. Z = f U}" in exI)
   168 apply (blast intro: wens_set.Union) 
   169 done
   170 
   171 text{*Assertion (9): 4.27 in the thesis.*}
   172 
   173 lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
   174 by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 
   175 
   176 text{*This is the result that requires the definition of @{term wens_set} to
   177 require @{term W} to be non-empty in the Unio case, for otherwise we should
   178 always have @{term "{} \<in> wens_set F B"}.*}
   179 lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
   180 apply (erule wens_set.induct) 
   181   apply (blast intro: wens_weakening [THEN subsetD])+
   182 done
   183 
   184 
   185 subsection{*Properties Involving Program Union*}
   186 
   187 text{*Assertion (4.30) of thesis, reoriented*}
   188 lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
   189 by (simp add: awp_def wp_def, blast)
   190 
   191 lemma wens_subset: 
   192      "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
   193 by (subst wens_unfold, fast) 
   194 
   195 text{*Assertion (4.31)*}
   196 lemma subset_wens_Join:
   197       "[|A = T \<inter> wens F act B;  T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|] 
   198        ==> A \<subseteq> wens (F\<squnion>G) act B"
   199 apply (subgoal_tac "(T \<inter> wens F act B) - B \<subseteq> 
   200                     wp act B \<inter> awp F (B \<union> wens F act B) \<inter> awp F T") 
   201  apply (rule subset_wens) 
   202  apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute)
   203  apply (simp add: awp_def wp_def, blast) 
   204 apply (insert wens_subset [of F act B], blast) 
   205 done
   206 
   207 text{*Assertion (4.32)*}
   208 lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B"
   209 apply (simp add: wens_def) 
   210 apply (rule gfp_mono)
   211 apply (auto simp add: awp_Join_eq)  
   212 done
   213 
   214 text{*Lemma, because the inductive step is just too messy.*}
   215 lemma wens_Union_inductive_step:
   216   assumes awpF: "T-B \<subseteq> awp F T"
   217       and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   218   shows "[|X \<in> wens_set F B; act \<in> Acts F; Y \<subseteq> X; T\<inter>X = T\<inter>Y|]
   219          ==> wens (F\<squnion>G) act Y \<subseteq> wens F act X \<and>
   220              T \<inter> wens F act X = T \<inter> wens (F\<squnion>G) act Y"
   221 apply (subgoal_tac "wens (F\<squnion>G) act Y \<subseteq> wens F act X")  
   222  prefer 2
   223  apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp)
   224 apply (rule equalityI) 
   225  prefer 2 apply blast
   226 apply (simp add: Int_lower1 Int_subset_iff) 
   227 apply (frule wens_set_imp_subset) 
   228 apply (subgoal_tac "T-X \<subseteq> awp F T")  
   229  prefer 2 apply (blast intro: awpF [THEN subsetD]) 
   230 apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans) 
   231  prefer 2 apply (blast intro!: wens_mono)
   232 apply (subst wens_Int_eq, assumption+) 
   233 apply (rule subset_wens_Join [of _ T])
   234   apply simp 
   235  apply blast
   236 apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X")
   237  prefer 2
   238  apply (subst wens_Int_eq [symmetric], assumption+) 
   239  apply (blast intro: wens_weakening [THEN subsetD], simp) 
   240 apply (blast intro: awpG [THEN subsetD] wens_set.Wens)
   241 done
   242 
   243 lemma wens_Union:
   244   assumes awpF: "T-B \<subseteq> awp F T"
   245       and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
   246       and major: "X \<in> wens_set F B"
   247   shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y"
   248 apply (rule wens_set.induct [OF major])
   249   txt{*Basis: trivial*}
   250   apply (blast intro: wens_set.Basis)
   251  txt{*Inductive step*}
   252  apply clarify 
   253  apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
   254   apply (force intro: wens_set.Wens)
   255  apply (simp add: wens_Union_inductive_step [OF awpF awpG]) 
   256 txt{*Union: by Axiom of Choice*}
   257 apply (simp add: ball_conj_distrib Bex_def) 
   258 apply (clarify dest!: bchoice) 
   259 apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI)
   260 apply (blast intro: wens_set.Union) 
   261 done
   262 
   263 end