src/HOL/UNITY/SubstAx.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 14150 9a23e4eb5eb3
child 19769 c40ce2de2020
permissions -rw-r--r--
migrated theory headers to new format
     1 (*  Title:      HOL/UNITY/SubstAx
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Weak LeadsTo relation (restricted to the set of reachable states)
     7 *)
     8 
     9 header{*Weak Progress*}
    10 
    11 theory SubstAx imports WFair Constrains begin
    12 
    13 constdefs
    14    Ensures :: "['a set, 'a set] => 'a program set"    (infixl "Ensures" 60)
    15     "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}"
    16 
    17    LeadsTo :: "['a set, 'a set] => 'a program set"    (infixl "LeadsTo" 60)
    18     "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
    19 
    20 syntax (xsymbols)
    21   "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
    22 
    23 
    24 text{*Resembles the previous definition of LeadsTo*}
    25 lemma LeadsTo_eq_leadsTo: 
    26      "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}"
    27 apply (unfold LeadsTo_def)
    28 apply (blast dest: psp_stable2 intro: leadsTo_weaken)
    29 done
    30 
    31 
    32 subsection{*Specialized laws for handling invariants*}
    33 
    34 (** Conjoining an Always property **)
    35 
    36 lemma Always_LeadsTo_pre:
    37      "F \<in> Always INV ==> (F \<in> (INV \<inter> A) LeadsTo A') = (F \<in> A LeadsTo A')"
    38 by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 
    39               Int_assoc [symmetric])
    40 
    41 lemma Always_LeadsTo_post:
    42      "F \<in> Always INV ==> (F \<in> A LeadsTo (INV \<inter> A')) = (F \<in> A LeadsTo A')"
    43 by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 
    44               Int_assoc [symmetric])
    45 
    46 (* [| F \<in> Always C;  F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *)
    47 lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
    48 
    49 (* [| F \<in> Always INV;  F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *)
    50 lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
    51 
    52 
    53 subsection{*Introduction rules: Basis, Trans, Union*}
    54 
    55 lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
    56 apply (simp add: LeadsTo_def)
    57 apply (blast intro: leadsTo_weaken_L)
    58 done
    59 
    60 lemma LeadsTo_Trans:
    61      "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"
    62 apply (simp add: LeadsTo_eq_leadsTo)
    63 apply (blast intro: leadsTo_Trans)
    64 done
    65 
    66 lemma LeadsTo_Union: 
    67      "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (Union S) LeadsTo B"
    68 apply (simp add: LeadsTo_def)
    69 apply (subst Int_Union)
    70 apply (blast intro: leadsTo_UN)
    71 done
    72 
    73 
    74 subsection{*Derived rules*}
    75 
    76 lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV"
    77 by (simp add: LeadsTo_def)
    78 
    79 text{*Useful with cancellation, disjunction*}
    80 lemma LeadsTo_Un_duplicate:
    81      "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
    82 by (simp add: Un_ac)
    83 
    84 lemma LeadsTo_Un_duplicate2:
    85      "F \<in> A LeadsTo (A' \<union> C \<union> C) ==> F \<in> A LeadsTo (A' \<union> C)"
    86 by (simp add: Un_ac)
    87 
    88 lemma LeadsTo_UN: 
    89      "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
    90 apply (simp only: Union_image_eq [symmetric])
    91 apply (blast intro: LeadsTo_Union)
    92 done
    93 
    94 text{*Binary union introduction rule*}
    95 lemma LeadsTo_Un:
    96      "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
    97 apply (subst Un_eq_Union)
    98 apply (blast intro: LeadsTo_Union)
    99 done
   100 
   101 text{*Lets us look at the starting state*}
   102 lemma single_LeadsTo_I:
   103      "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B"
   104 by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
   105 
   106 lemma subset_imp_LeadsTo: "A \<subseteq> B ==> F \<in> A LeadsTo B"
   107 apply (simp add: LeadsTo_def)
   108 apply (blast intro: subset_imp_leadsTo)
   109 done
   110 
   111 lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
   112 
   113 lemma LeadsTo_weaken_R [rule_format]:
   114      "[| F \<in> A LeadsTo A';  A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"
   115 apply (simp add: LeadsTo_def)
   116 apply (blast intro: leadsTo_weaken_R)
   117 done
   118 
   119 lemma LeadsTo_weaken_L [rule_format]:
   120      "[| F \<in> A LeadsTo A';  B \<subseteq> A |]   
   121       ==> F \<in> B LeadsTo A'"
   122 apply (simp add: LeadsTo_def)
   123 apply (blast intro: leadsTo_weaken_L)
   124 done
   125 
   126 lemma LeadsTo_weaken:
   127      "[| F \<in> A LeadsTo A';    
   128          B  \<subseteq> A;   A' \<subseteq> B' |]  
   129       ==> F \<in> B LeadsTo B'"
   130 by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
   131 
   132 lemma Always_LeadsTo_weaken:
   133      "[| F \<in> Always C;  F \<in> A LeadsTo A';    
   134          C \<inter> B \<subseteq> A;   C \<inter> A' \<subseteq> B' |]  
   135       ==> F \<in> B LeadsTo B'"
   136 by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD)
   137 
   138 (** Two theorems for "proof lattices" **)
   139 
   140 lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F \<in> (A \<union> B) LeadsTo B"
   141 by (blast intro: LeadsTo_Un subset_imp_LeadsTo)
   142 
   143 lemma LeadsTo_Trans_Un:
   144      "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |]  
   145       ==> F \<in> (A \<union> B) LeadsTo C"
   146 by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans)
   147 
   148 
   149 (** Distributive laws **)
   150 
   151 lemma LeadsTo_Un_distrib:
   152      "(F \<in> (A \<union> B) LeadsTo C)  = (F \<in> A LeadsTo C & F \<in> B LeadsTo C)"
   153 by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
   154 
   155 lemma LeadsTo_UN_distrib:
   156      "(F \<in> (\<Union>i \<in> I. A i) LeadsTo B)  =  (\<forall>i \<in> I. F \<in> (A i) LeadsTo B)"
   157 by (blast intro: LeadsTo_UN LeadsTo_weaken_L)
   158 
   159 lemma LeadsTo_Union_distrib:
   160      "(F \<in> (Union S) LeadsTo B)  =  (\<forall>A \<in> S. F \<in> A LeadsTo B)"
   161 by (blast intro: LeadsTo_Union LeadsTo_weaken_L)
   162 
   163 
   164 (** More rules using the premise "Always INV" **)
   165 
   166 lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"
   167 by (simp add: Ensures_def LeadsTo_def leadsTo_Basis)
   168 
   169 lemma EnsuresI:
   170      "[| F \<in> (A-B) Co (A \<union> B);  F \<in> transient (A-B) |]    
   171       ==> F \<in> A Ensures B"
   172 apply (simp add: Ensures_def Constrains_eq_constrains)
   173 apply (blast intro: ensuresI constrains_weaken transient_strengthen)
   174 done
   175 
   176 lemma Always_LeadsTo_Basis:
   177      "[| F \<in> Always INV;       
   178          F \<in> (INV \<inter> (A-A')) Co (A \<union> A');  
   179          F \<in> transient (INV \<inter> (A-A')) |]    
   180   ==> F \<in> A LeadsTo A'"
   181 apply (rule Always_LeadsToI, assumption)
   182 apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
   183 done
   184 
   185 text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??
   186   This is the most useful form of the "disjunction" rule*}
   187 lemma LeadsTo_Diff:
   188      "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |]  
   189       ==> F \<in> A LeadsTo C"
   190 by (blast intro: LeadsTo_Un LeadsTo_weaken)
   191 
   192 
   193 lemma LeadsTo_UN_UN: 
   194      "(!! i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i))  
   195       ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo (\<Union>i \<in> I. A' i)"
   196 apply (simp only: Union_image_eq [symmetric])
   197 apply (blast intro: LeadsTo_Union LeadsTo_weaken_R)
   198 done
   199 
   200 
   201 text{*Version with no index set*}
   202 lemma LeadsTo_UN_UN_noindex: 
   203      "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
   204 by (blast intro: LeadsTo_UN_UN)
   205 
   206 text{*Version with no index set*}
   207 lemma all_LeadsTo_UN_UN:
   208      "\<forall>i. F \<in> (A i) LeadsTo (A' i)  
   209       ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
   210 by (blast intro: LeadsTo_UN_UN)
   211 
   212 text{*Binary union version*}
   213 lemma LeadsTo_Un_Un:
   214      "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |]  
   215             ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')"
   216 by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
   217 
   218 
   219 (** The cancellation law **)
   220 
   221 lemma LeadsTo_cancel2:
   222      "[| F \<in> A LeadsTo (A' \<union> B); F \<in> B LeadsTo B' |]     
   223       ==> F \<in> A LeadsTo (A' \<union> B')"
   224 by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans)
   225 
   226 lemma LeadsTo_cancel_Diff2:
   227      "[| F \<in> A LeadsTo (A' \<union> B); F \<in> (B-A') LeadsTo B' |]  
   228       ==> F \<in> A LeadsTo (A' \<union> B')"
   229 apply (rule LeadsTo_cancel2)
   230 prefer 2 apply assumption
   231 apply (simp_all (no_asm_simp))
   232 done
   233 
   234 lemma LeadsTo_cancel1:
   235      "[| F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' |]  
   236       ==> F \<in> A LeadsTo (B' \<union> A')"
   237 apply (simp add: Un_commute)
   238 apply (blast intro!: LeadsTo_cancel2)
   239 done
   240 
   241 lemma LeadsTo_cancel_Diff1:
   242      "[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |]  
   243       ==> F \<in> A LeadsTo (B' \<union> A')"
   244 apply (rule LeadsTo_cancel1)
   245 prefer 2 apply assumption
   246 apply (simp_all (no_asm_simp))
   247 done
   248 
   249 
   250 text{*The impossibility law*}
   251 
   252 text{*The set "A" may be non-empty, but it contains no reachable states*}
   253 lemma LeadsTo_empty: "[|F \<in> A LeadsTo {}; all_total F|] ==> F \<in> Always (-A)"
   254 apply (simp add: LeadsTo_def Always_eq_includes_reachable)
   255 apply (drule leadsTo_empty, auto)
   256 done
   257 
   258 
   259 subsection{*PSP: Progress-Safety-Progress*}
   260 
   261 text{*Special case of PSP: Misra's "stable conjunction"*}
   262 lemma PSP_Stable:
   263      "[| F \<in> A LeadsTo A';  F \<in> Stable B |]  
   264       ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)"
   265 apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable)
   266 apply (drule psp_stable, assumption)
   267 apply (simp add: Int_ac)
   268 done
   269 
   270 lemma PSP_Stable2:
   271      "[| F \<in> A LeadsTo A'; F \<in> Stable B |]  
   272       ==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')"
   273 by (simp add: PSP_Stable Int_ac)
   274 
   275 lemma PSP:
   276      "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]  
   277       ==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))"
   278 apply (simp add: LeadsTo_def Constrains_eq_constrains)
   279 apply (blast dest: psp intro: leadsTo_weaken)
   280 done
   281 
   282 lemma PSP2:
   283      "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]  
   284       ==> F \<in> (B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))"
   285 by (simp add: PSP Int_ac)
   286 
   287 lemma PSP_Unless: 
   288      "[| F \<in> A LeadsTo A'; F \<in> B Unless B' |]  
   289       ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')"
   290 apply (unfold Unless_def)
   291 apply (drule PSP, assumption)
   292 apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
   293 done
   294 
   295 
   296 lemma Stable_transient_Always_LeadsTo:
   297      "[| F \<in> Stable A;  F \<in> transient C;   
   298          F \<in> Always (-A \<union> B \<union> C) |] ==> F \<in> A LeadsTo B"
   299 apply (erule Always_LeadsTo_weaken)
   300 apply (rule LeadsTo_Diff)
   301    prefer 2
   302    apply (erule
   303           transient_imp_leadsTo [THEN leadsTo_imp_LeadsTo, THEN PSP_Stable2])
   304    apply (blast intro: subset_imp_LeadsTo)+
   305 done
   306 
   307 
   308 subsection{*Induction rules*}
   309 
   310 (** Meta or object quantifier ????? **)
   311 lemma LeadsTo_wf_induct:
   312      "[| wf r;      
   313          \<forall>m. F \<in> (A \<inter> f-`{m}) LeadsTo                      
   314                     ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
   315       ==> F \<in> A LeadsTo B"
   316 apply (simp add: LeadsTo_eq_leadsTo)
   317 apply (erule leadsTo_wf_induct)
   318 apply (blast intro: leadsTo_weaken)
   319 done
   320 
   321 
   322 lemma Bounded_induct:
   323      "[| wf r;      
   324          \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) LeadsTo                    
   325                       ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
   326       ==> F \<in> A LeadsTo ((A - (f-`I)) \<union> B)"
   327 apply (erule LeadsTo_wf_induct, safe)
   328 apply (case_tac "m \<in> I")
   329 apply (blast intro: LeadsTo_weaken)
   330 apply (blast intro: subset_imp_LeadsTo)
   331 done
   332 
   333 
   334 lemma LessThan_induct:
   335      "(!!m::nat. F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B))
   336       ==> F \<in> A LeadsTo B"
   337 by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
   338 
   339 text{*Integer version.  Could generalize from 0 to any lower bound*}
   340 lemma integ_0_le_induct:
   341      "[| F \<in> Always {s. (0::int) \<le> f s};   
   342          !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo                      
   343                    ((A \<inter> {s. f s < z}) \<union> B) |]  
   344       ==> F \<in> A LeadsTo B"
   345 apply (rule_tac f = "nat o f" in LessThan_induct)
   346 apply (simp add: vimage_def)
   347 apply (rule Always_LeadsTo_weaken, assumption+)
   348 apply (auto simp add: nat_eq_iff nat_less_iff)
   349 done
   350 
   351 lemma LessThan_bounded_induct:
   352      "!!l::nat. \<forall>m \<in> greaterThan l. 
   353                    F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B)
   354             ==> F \<in> A LeadsTo ((A \<inter> (f-`(atMost l))) \<union> B)"
   355 apply (simp only: Diff_eq [symmetric] vimage_Compl 
   356                   Compl_greaterThan [symmetric])
   357 apply (rule wf_less_than [THEN Bounded_induct], simp)
   358 done
   359 
   360 lemma GreaterThan_bounded_induct:
   361      "!!l::nat. \<forall>m \<in> lessThan l. 
   362                  F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(greaterThan m)) \<union> B)
   363       ==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
   364 apply (rule_tac f = f and f1 = "%k. l - k" 
   365        in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
   366 apply (simp add: inv_image_def Image_singleton, clarify)
   367 apply (case_tac "m<l")
   368  apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
   369 apply (blast intro: not_leE subset_imp_LeadsTo)
   370 done
   371 
   372 
   373 subsection{*Completion: Binary and General Finite versions*}
   374 
   375 lemma Completion:
   376      "[| F \<in> A LeadsTo (A' \<union> C);  F \<in> A' Co (A' \<union> C);  
   377          F \<in> B LeadsTo (B' \<union> C);  F \<in> B' Co (B' \<union> C) |]  
   378       ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)"
   379 apply (simp add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib)
   380 apply (blast intro: completion leadsTo_weaken)
   381 done
   382 
   383 lemma Finite_completion_lemma:
   384      "finite I  
   385       ==> (\<forall>i \<in> I. F \<in> (A i) LeadsTo (A' i \<union> C)) -->   
   386           (\<forall>i \<in> I. F \<in> (A' i) Co (A' i \<union> C)) -->  
   387           F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
   388 apply (erule finite_induct, auto)
   389 apply (rule Completion)
   390    prefer 4
   391    apply (simp only: INT_simps [symmetric])
   392    apply (rule Constrains_INT, auto)
   393 done
   394 
   395 lemma Finite_completion: 
   396      "[| finite I;   
   397          !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i \<union> C);  
   398          !!i. i \<in> I ==> F \<in> (A' i) Co (A' i \<union> C) |]    
   399       ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
   400 by (blast intro: Finite_completion_lemma [THEN mp, THEN mp])
   401 
   402 lemma Stable_completion: 
   403      "[| F \<in> A LeadsTo A';  F \<in> Stable A';    
   404          F \<in> B LeadsTo B';  F \<in> Stable B' |]  
   405       ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')"
   406 apply (unfold Stable_def)
   407 apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R])
   408 apply (force+)
   409 done
   410 
   411 lemma Finite_stable_completion: 
   412      "[| finite I;   
   413          !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i);  
   414          !!i. i \<in> I ==> F \<in> Stable (A' i) |]    
   415       ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo (\<Inter>i \<in> I. A' i)"
   416 apply (unfold Stable_def)
   417 apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R])
   418 apply (simp_all, blast+)
   419 done
   420 
   421 end