src/HOL/UNITY/SubstAx.thy
 changeset 13796 19f50fa807ae parent 9685 6d123a7e30bd child 13798 4c1a53627500
```     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Wed Jan 29 17:35:11 2003 +0100
1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Jan 30 10:35:56 2003 +0100
1.3 @@ -6,16 +6,416 @@
1.4  Weak LeadsTo relation (restricted to the set of reachable states)
1.5  *)
1.6
1.7 -SubstAx = WFair + Constrains +
1.8 +theory SubstAx = WFair + Constrains:
1.9
1.10  constdefs
1.11 -   Ensures :: "['a set, 'a set] => 'a program set"            (infixl 60)
1.12 +   Ensures :: "['a set, 'a set] => 'a program set"    (infixl "Ensures" 60)
1.13      "A Ensures B == {F. F : (reachable F Int A) ensures B}"
1.14
1.15 -   LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
1.16 +   LeadsTo :: "['a set, 'a set] => 'a program set"    (infixl "LeadsTo" 60)
1.17      "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
1.18
1.19  syntax (xsymbols)
1.20 -  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60)
1.21 +  "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
1.22 +
1.23 +
1.24 +(*Resembles the previous definition of LeadsTo*)
1.26 +     "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}"
1.28 +apply (blast dest: psp_stable2 intro: leadsTo_weaken)
1.29 +done
1.30 +
1.31 +
1.32 +(*** Specialized laws for handling invariants ***)
1.33 +
1.34 +(** Conjoining an Always property **)
1.35 +
1.37 +     "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')"
1.39 +
1.41 +     "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')"
1.43 +
1.44 +(* [| F : Always C;  F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
1.46 +
1.47 +(* [| F : Always INV;  F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *)
1.49 +
1.50 +
1.51 +(*** Introduction rules: Basis, Trans, Union ***)
1.52 +
1.56 +done
1.57 +
1.59 +     "[| F : A LeadsTo B;  F : B LeadsTo C |] ==> F : A LeadsTo C"
1.62 +done
1.63 +
1.65 +     "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B"
1.67 +apply (subst Int_Union)
1.69 +done
1.70 +
1.71 +
1.72 +(*** Derived rules ***)
1.73 +
1.76 +
1.77 +(*Useful with cancellation, disjunction*)
1.79 +     "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'"
1.81 +
1.83 +     "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)"
1.85 +
1.87 +     "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B"
1.88 +apply (simp only: Union_image_eq [symmetric])
1.90 +done
1.91 +
1.92 +(*Binary union introduction rule*)
1.94 +     "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C"
1.95 +apply (subst Un_eq_Union)
1.97 +done
1.98 +
1.99 +(*Lets us look at the starting state*)
1.101 +     "(!!s. s : A ==> F : {s} LeadsTo B) ==> F : A LeadsTo B"
1.102 +by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
1.103 +
1.104 +lemma subset_imp_LeadsTo: "A <= B ==> F : A LeadsTo B"
1.107 +done
1.108 +
1.110 +
1.112 +     "[| F : A LeadsTo A';  A' <= B' |] ==> F : A LeadsTo B'"
1.115 +done
1.116 +
1.118 +     "[| F : A LeadsTo A';  B <= A |]
1.119 +      ==> F : B LeadsTo A'"
1.122 +done
1.123 +
1.125 +     "[| F : A LeadsTo A';
1.126 +         B  <= A;   A' <= B' |]
1.127 +      ==> F : B LeadsTo B'"
1.129 +
1.131 +     "[| F : Always C;  F : A LeadsTo A';
1.132 +         C Int B <= A;   C Int A' <= B' |]
1.133 +      ==> F : B LeadsTo B'"
1.135 +
1.136 +(** Two theorems for "proof lattices" **)
1.137 +
1.140 +
1.142 +     "[| F : A LeadsTo B;  F : B LeadsTo C |]
1.143 +      ==> F : (A Un B) LeadsTo C"
1.145 +
1.146 +
1.147 +(** Distributive laws **)
1.148 +
1.150 +     "(F : (A Un B) LeadsTo C)  = (F : A LeadsTo C & F : B LeadsTo C)"
1.152 +
1.154 +     "(F : (UN i:I. A i) LeadsTo B)  =  (ALL i : I. F : (A i) LeadsTo B)"
1.156 +
1.158 +     "(F : (Union S) LeadsTo B)  =  (ALL A : S. F : A LeadsTo B)"
1.160 +
1.161 +
1.162 +(** More rules using the premise "Always INV" **)
1.163 +
1.164 +lemma LeadsTo_Basis: "F : A Ensures B ==> F : A LeadsTo B"
1.166 +
1.167 +lemma EnsuresI:
1.168 +     "[| F : (A-B) Co (A Un B);  F : transient (A-B) |]
1.169 +      ==> F : A Ensures B"
1.170 +apply (simp add: Ensures_def Constrains_eq_constrains)
1.171 +apply (blast intro: ensuresI constrains_weaken transient_strengthen)
1.172 +done
1.173 +
1.175 +     "[| F : Always INV;
1.176 +         F : (INV Int (A-A')) Co (A Un A');
1.177 +         F : transient (INV Int (A-A')) |]
1.178 +  ==> F : A LeadsTo A'"
1.180 +apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
1.181 +done
1.182 +
1.183 +(*Set difference: maybe combine with leadsTo_weaken_L??
1.184 +  This is the most useful form of the "disjunction" rule*)
1.186 +     "[| F : (A-B) LeadsTo C;  F : (A Int B) LeadsTo C |]
1.187 +      ==> F : A LeadsTo C"
1.189 +
1.190 +
1.192 +     "(!! i. i:I ==> F : (A i) LeadsTo (A' i))
1.193 +      ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)"
1.194 +apply (simp only: Union_image_eq [symmetric])
1.196 +done
1.197 +
1.198 +
1.199 +(*Version with no index set*)
1.201 +     "(!! i. F : (A i) LeadsTo (A' i))
1.202 +      ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
1.204 +
1.205 +(*Version with no index set*)
1.207 +     "ALL i. F : (A i) LeadsTo (A' i)
1.208 +      ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
1.210 +
1.211 +(*Binary union version*)
1.213 +     "[| F : A LeadsTo A'; F : B LeadsTo B' |]
1.214 +            ==> F : (A Un B) LeadsTo (A' Un B')"
1.216 +
1.217 +
1.218 +(** The cancellation law **)
1.219 +
1.221 +     "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |]
1.222 +      ==> F : A LeadsTo (A' Un B')"
1.224 +
1.226 +     "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |]
1.227 +      ==> F : A LeadsTo (A' Un B')"
1.229 +prefer 2 apply assumption
1.230 +apply (simp_all (no_asm_simp))
1.231 +done
1.232 +
1.234 +     "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |]
1.235 +      ==> F : A LeadsTo (B' Un A')"
1.238 +done
1.239 +
1.241 +     "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |]
1.242 +      ==> F : A LeadsTo (B' Un A')"
1.244 +prefer 2 apply assumption
1.245 +apply (simp_all (no_asm_simp))
1.246 +done
1.247 +
1.248 +
1.249 +(** The impossibility law **)
1.250 +
1.251 +(*The set "A" may be non-empty, but it contains no reachable states*)
1.252 +lemma LeadsTo_empty: "F : A LeadsTo {} ==> F : Always (-A)"
1.255 +done
1.256 +
1.257 +
1.258 +(** PSP: Progress-Safety-Progress **)
1.259 +
1.260 +(*Special case of PSP: Misra's "stable conjunction"*)
1.261 +lemma PSP_Stable:
1.262 +     "[| F : A LeadsTo A';  F : Stable B |]
1.263 +      ==> F : (A Int B) LeadsTo (A' Int B)"
1.265 +apply (drule psp_stable, assumption)
1.267 +done
1.268 +
1.269 +lemma PSP_Stable2:
1.270 +     "[| F : A LeadsTo A'; F : Stable B |]
1.271 +      ==> F : (B Int A) LeadsTo (B Int A')"
1.272 +by (simp add: PSP_Stable Int_ac)
1.273 +
1.274 +lemma PSP:
1.275 +     "[| F : A LeadsTo A'; F : B Co B' |]
1.276 +      ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"
1.278 +apply (blast dest: psp intro: leadsTo_weaken)
1.279 +done
1.280 +
1.281 +lemma PSP2:
1.282 +     "[| F : A LeadsTo A'; F : B Co B' |]
1.283 +      ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))"
1.284 +by (simp add: PSP Int_ac)
1.285 +
1.286 +lemma PSP_Unless:
1.287 +     "[| F : A LeadsTo A'; F : B Unless B' |]
1.288 +      ==> F : (A Int B) LeadsTo ((A' Int B) Un B')"
1.289 +apply (unfold Unless_def)
1.290 +apply (drule PSP, assumption)
1.292 +done
1.293 +
1.294 +
1.296 +     "[| F : Stable A;  F : transient C;
1.297 +         F : Always (-A Un B Un C) |] ==> F : A LeadsTo B"
1.300 +   prefer 2
1.301 +   apply (erule
1.303 +   apply (blast intro: subset_imp_LeadsTo)+
1.304 +done
1.305 +
1.306 +
1.307 +(*** Induction rules ***)
1.308 +
1.309 +(** Meta or object quantifier ????? **)
1.311 +     "[| wf r;
1.312 +         ALL m. F : (A Int f-`{m}) LeadsTo
1.313 +                            ((A Int f-`(r^-1 `` {m})) Un B) |]
1.314 +      ==> F : A LeadsTo B"
1.318 +done
1.319 +
1.320 +
1.321 +lemma Bounded_induct:
1.322 +     "[| wf r;
1.323 +         ALL m:I. F : (A Int f-`{m}) LeadsTo
1.324 +                              ((A Int f-`(r^-1 `` {m})) Un B) |]
1.325 +      ==> F : A LeadsTo ((A - (f-`I)) Un B)"
1.327 +apply (case_tac "m:I")
1.330 +done
1.331 +
1.332 +
1.333 +lemma LessThan_induct:
1.334 +     "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B))
1.335 +      ==> F : A LeadsTo B"
1.336 +apply (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
1.337 +done
1.338 +
1.339 +(*Integer version.  Could generalize from 0 to any lower bound*)
1.340 +lemma integ_0_le_induct:
1.341 +     "[| F : Always {s. (0::int) <= f s};
1.342 +         !! z. F : (A Int {s. f s = z}) LeadsTo
1.343 +                            ((A Int {s. f s < z}) Un B) |]
1.344 +      ==> F : A LeadsTo B"
1.345 +apply (rule_tac f = "nat o f" in LessThan_induct)
1.348 +apply (auto simp add: nat_eq_iff nat_less_iff)
1.349 +done
1.350 +
1.351 +lemma LessThan_bounded_induct:
1.352 +     "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-`{m}) LeadsTo
1.353 +                                         ((A Int f-`(lessThan m)) Un B) |]
1.354 +            ==> F : A LeadsTo ((A Int (f-`(atMost l))) Un B)"
1.355 +apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
1.356 +apply (rule wf_less_than [THEN Bounded_induct])
1.357 +apply (simp (no_asm_simp))
1.358 +done
1.359 +
1.360 +lemma GreaterThan_bounded_induct:
1.361 +     "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-`{m}) LeadsTo
1.362 +                               ((A Int f-`(greaterThan m)) Un B) |]
1.363 +      ==> F : A LeadsTo ((A Int (f-`(atLeast l))) Un B)"
1.364 +apply (rule_tac f = f and f1 = "%k. l - k"
1.365 +       in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
1.366 +apply (simp add: inv_image_def Image_singleton, clarify)
1.367 +apply (case_tac "m<l")
1.368 + prefer 2 apply (blast intro: not_leE subset_imp_LeadsTo)
1.369 +apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
1.370 +done
1.371 +
1.372 +
1.373 +(*** Completion: Binary and General Finite versions ***)
1.374 +
1.375 +lemma Completion:
1.376 +     "[| F : A LeadsTo (A' Un C);  F : A' Co (A' Un C);
1.377 +         F : B LeadsTo (B' Un C);  F : B' Co (B' Un C) |]
1.378 +      ==> F : (A Int B) LeadsTo ((A' Int B') Un C)"
1.380 +apply (blast intro: completion leadsTo_weaken)
1.381 +done
1.382 +
1.383 +lemma Finite_completion_lemma:
1.384 +     "finite I
1.385 +      ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) -->
1.386 +          (ALL i:I. F : (A' i) Co (A' i Un C)) -->
1.387 +          F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
1.388 +apply (erule finite_induct, auto)
1.389 +apply (rule Completion)
1.390 +   prefer 4
1.391 +   apply (simp only: INT_simps [symmetric])
1.392 +   apply (rule Constrains_INT, auto)
1.393 +done
1.394 +
1.395 +lemma Finite_completion:
1.396 +     "[| finite I;
1.397 +         !!i. i:I ==> F : (A i) LeadsTo (A' i Un C);
1.398 +         !!i. i:I ==> F : (A' i) Co (A' i Un C) |]
1.399 +      ==> F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
1.400 +by (blast intro: Finite_completion_lemma [THEN mp, THEN mp])
1.401 +
1.402 +lemma Stable_completion:
1.403 +     "[| F : A LeadsTo A';  F : Stable A';
1.404 +         F : B LeadsTo B';  F : Stable B' |]
1.405 +      ==> F : (A Int B) LeadsTo (A' Int B')"
1.406 +apply (unfold Stable_def)
1.407 +apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R])
1.408 +apply (force+)
1.409 +done
1.410 +
1.411 +lemma Finite_stable_completion:
1.412 +     "[| finite I;
1.413 +         !!i. i:I ==> F : (A i) LeadsTo (A' i);
1.414 +         !!i. i:I ==> F : Stable (A' i) |]
1.415 +      ==> F : (INT i:I. A i) LeadsTo (INT i:I. A' i)"
1.416 +apply (unfold Stable_def)
1.417 +apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R])
1.418 +apply (simp_all (no_asm_simp))
1.419 +apply blast+
1.420 +done
1.421 +
1.422
1.423  end
```