src/HOL/UNITY/SubstAx.thy
changeset 13805 3786b2fd6808
parent 13798 4c1a53627500
child 13812 91713a1915ee
     1.1 --- a/src/HOL/UNITY/SubstAx.thy	Mon Feb 03 11:45:05 2003 +0100
     1.2 +++ b/src/HOL/UNITY/SubstAx.thy	Tue Feb 04 18:12:40 2003 +0100
     1.3 @@ -12,10 +12,10 @@
     1.4  
     1.5  constdefs
     1.6     Ensures :: "['a set, 'a set] => 'a program set"    (infixl "Ensures" 60)
     1.7 -    "A Ensures B == {F. F : (reachable F Int A) ensures B}"
     1.8 +    "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}"
     1.9  
    1.10     LeadsTo :: "['a set, 'a set] => 'a program set"    (infixl "LeadsTo" 60)
    1.11 -    "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
    1.12 +    "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
    1.13  
    1.14  syntax (xsymbols)
    1.15    "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
    1.16 @@ -23,7 +23,7 @@
    1.17  
    1.18  (*Resembles the previous definition of LeadsTo*)
    1.19  lemma LeadsTo_eq_leadsTo: 
    1.20 -     "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}"
    1.21 +     "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}"
    1.22  apply (unfold LeadsTo_def)
    1.23  apply (blast dest: psp_stable2 intro: leadsTo_weaken)
    1.24  done
    1.25 @@ -34,35 +34,37 @@
    1.26  (** Conjoining an Always property **)
    1.27  
    1.28  lemma Always_LeadsTo_pre:
    1.29 -     "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')"
    1.30 -by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
    1.31 +     "F \<in> Always INV ==> (F \<in> (INV \<inter> A) LeadsTo A') = (F \<in> A LeadsTo A')"
    1.32 +by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 
    1.33 +              Int_assoc [symmetric])
    1.34  
    1.35  lemma Always_LeadsTo_post:
    1.36 -     "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')"
    1.37 -by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
    1.38 +     "F \<in> Always INV ==> (F \<in> A LeadsTo (INV \<inter> A')) = (F \<in> A LeadsTo A')"
    1.39 +by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 
    1.40 +              Int_assoc [symmetric])
    1.41  
    1.42 -(* [| F : Always C;  F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
    1.43 +(* [| F \<in> Always C;  F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *)
    1.44  lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
    1.45  
    1.46 -(* [| F : Always INV;  F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *)
    1.47 +(* [| F \<in> Always INV;  F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *)
    1.48  lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
    1.49  
    1.50  
    1.51  subsection{*Introduction rules: Basis, Trans, Union*}
    1.52  
    1.53 -lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B"
    1.54 +lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
    1.55  apply (simp add: LeadsTo_def)
    1.56  apply (blast intro: leadsTo_weaken_L)
    1.57  done
    1.58  
    1.59  lemma LeadsTo_Trans:
    1.60 -     "[| F : A LeadsTo B;  F : B LeadsTo C |] ==> F : A LeadsTo C"
    1.61 +     "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"
    1.62  apply (simp add: LeadsTo_eq_leadsTo)
    1.63  apply (blast intro: leadsTo_Trans)
    1.64  done
    1.65  
    1.66  lemma LeadsTo_Union: 
    1.67 -     "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B"
    1.68 +     "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (Union S) LeadsTo B"
    1.69  apply (simp add: LeadsTo_def)
    1.70  apply (subst Int_Union)
    1.71  apply (blast intro: leadsTo_UN)
    1.72 @@ -71,37 +73,37 @@
    1.73  
    1.74  subsection{*Derived rules*}
    1.75  
    1.76 -lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV"
    1.77 +lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV"
    1.78  by (simp add: LeadsTo_def)
    1.79  
    1.80  (*Useful with cancellation, disjunction*)
    1.81  lemma LeadsTo_Un_duplicate:
    1.82 -     "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'"
    1.83 +     "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
    1.84  by (simp add: Un_ac)
    1.85  
    1.86  lemma LeadsTo_Un_duplicate2:
    1.87 -     "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)"
    1.88 +     "F \<in> A LeadsTo (A' \<union> C \<union> C) ==> F \<in> A LeadsTo (A' \<union> C)"
    1.89  by (simp add: Un_ac)
    1.90  
    1.91  lemma LeadsTo_UN: 
    1.92 -     "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B"
    1.93 +     "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
    1.94  apply (simp only: Union_image_eq [symmetric])
    1.95  apply (blast intro: LeadsTo_Union)
    1.96  done
    1.97  
    1.98  (*Binary union introduction rule*)
    1.99  lemma LeadsTo_Un:
   1.100 -     "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C"
   1.101 +     "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
   1.102  apply (subst Un_eq_Union)
   1.103  apply (blast intro: LeadsTo_Union)
   1.104  done
   1.105  
   1.106  (*Lets us look at the starting state*)
   1.107  lemma single_LeadsTo_I:
   1.108 -     "(!!s. s : A ==> F : {s} LeadsTo B) ==> F : A LeadsTo B"
   1.109 +     "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B"
   1.110  by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
   1.111  
   1.112 -lemma subset_imp_LeadsTo: "A <= B ==> F : A LeadsTo B"
   1.113 +lemma subset_imp_LeadsTo: "A \<subseteq> B ==> F \<in> A LeadsTo B"
   1.114  apply (simp add: LeadsTo_def)
   1.115  apply (blast intro: subset_imp_leadsTo)
   1.116  done
   1.117 @@ -109,73 +111,73 @@
   1.118  lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
   1.119  
   1.120  lemma LeadsTo_weaken_R [rule_format]:
   1.121 -     "[| F : A LeadsTo A';  A' <= B' |] ==> F : A LeadsTo B'"
   1.122 -apply (simp (no_asm_use) add: LeadsTo_def)
   1.123 +     "[| F \<in> A LeadsTo A';  A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"
   1.124 +apply (simp add: LeadsTo_def)
   1.125  apply (blast intro: leadsTo_weaken_R)
   1.126  done
   1.127  
   1.128  lemma LeadsTo_weaken_L [rule_format]:
   1.129 -     "[| F : A LeadsTo A';  B <= A |]   
   1.130 -      ==> F : B LeadsTo A'"
   1.131 -apply (simp (no_asm_use) add: LeadsTo_def)
   1.132 +     "[| F \<in> A LeadsTo A';  B \<subseteq> A |]   
   1.133 +      ==> F \<in> B LeadsTo A'"
   1.134 +apply (simp add: LeadsTo_def)
   1.135  apply (blast intro: leadsTo_weaken_L)
   1.136  done
   1.137  
   1.138  lemma LeadsTo_weaken:
   1.139 -     "[| F : A LeadsTo A';    
   1.140 -         B  <= A;   A' <= B' |]  
   1.141 -      ==> F : B LeadsTo B'"
   1.142 +     "[| F \<in> A LeadsTo A';    
   1.143 +         B  \<subseteq> A;   A' \<subseteq> B' |]  
   1.144 +      ==> F \<in> B LeadsTo B'"
   1.145  by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
   1.146  
   1.147  lemma Always_LeadsTo_weaken:
   1.148 -     "[| F : Always C;  F : A LeadsTo A';    
   1.149 -         C Int B <= A;   C Int A' <= B' |]  
   1.150 -      ==> F : B LeadsTo B'"
   1.151 +     "[| F \<in> Always C;  F \<in> A LeadsTo A';    
   1.152 +         C \<inter> B \<subseteq> A;   C \<inter> A' \<subseteq> B' |]  
   1.153 +      ==> F \<in> B LeadsTo B'"
   1.154  by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD)
   1.155  
   1.156  (** Two theorems for "proof lattices" **)
   1.157  
   1.158 -lemma LeadsTo_Un_post: "F : A LeadsTo B ==> F : (A Un B) LeadsTo B"
   1.159 +lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F \<in> (A \<union> B) LeadsTo B"
   1.160  by (blast intro: LeadsTo_Un subset_imp_LeadsTo)
   1.161  
   1.162  lemma LeadsTo_Trans_Un:
   1.163 -     "[| F : A LeadsTo B;  F : B LeadsTo C |]  
   1.164 -      ==> F : (A Un B) LeadsTo C"
   1.165 +     "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |]  
   1.166 +      ==> F \<in> (A \<union> B) LeadsTo C"
   1.167  by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans)
   1.168  
   1.169  
   1.170  (** Distributive laws **)
   1.171  
   1.172  lemma LeadsTo_Un_distrib:
   1.173 -     "(F : (A Un B) LeadsTo C)  = (F : A LeadsTo C & F : B LeadsTo C)"
   1.174 +     "(F \<in> (A \<union> B) LeadsTo C)  = (F \<in> A LeadsTo C & F \<in> B LeadsTo C)"
   1.175  by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
   1.176  
   1.177  lemma LeadsTo_UN_distrib:
   1.178 -     "(F : (UN i:I. A i) LeadsTo B)  =  (ALL i : I. F : (A i) LeadsTo B)"
   1.179 +     "(F \<in> (\<Union>i \<in> I. A i) LeadsTo B)  =  (\<forall>i \<in> I. F \<in> (A i) LeadsTo B)"
   1.180  by (blast intro: LeadsTo_UN LeadsTo_weaken_L)
   1.181  
   1.182  lemma LeadsTo_Union_distrib:
   1.183 -     "(F : (Union S) LeadsTo B)  =  (ALL A : S. F : A LeadsTo B)"
   1.184 +     "(F \<in> (Union S) LeadsTo B)  =  (\<forall>A \<in> S. F \<in> A LeadsTo B)"
   1.185  by (blast intro: LeadsTo_Union LeadsTo_weaken_L)
   1.186  
   1.187  
   1.188  (** More rules using the premise "Always INV" **)
   1.189  
   1.190 -lemma LeadsTo_Basis: "F : A Ensures B ==> F : A LeadsTo B"
   1.191 +lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"
   1.192  by (simp add: Ensures_def LeadsTo_def leadsTo_Basis)
   1.193  
   1.194  lemma EnsuresI:
   1.195 -     "[| F : (A-B) Co (A Un B);  F : transient (A-B) |]    
   1.196 -      ==> F : A Ensures B"
   1.197 +     "[| F \<in> (A-B) Co (A \<union> B);  F \<in> transient (A-B) |]    
   1.198 +      ==> F \<in> A Ensures B"
   1.199  apply (simp add: Ensures_def Constrains_eq_constrains)
   1.200  apply (blast intro: ensuresI constrains_weaken transient_strengthen)
   1.201  done
   1.202  
   1.203  lemma Always_LeadsTo_Basis:
   1.204 -     "[| F : Always INV;       
   1.205 -         F : (INV Int (A-A')) Co (A Un A');  
   1.206 -         F : transient (INV Int (A-A')) |]    
   1.207 -  ==> F : A LeadsTo A'"
   1.208 +     "[| F \<in> Always INV;       
   1.209 +         F \<in> (INV \<inter> (A-A')) Co (A \<union> A');  
   1.210 +         F \<in> transient (INV \<inter> (A-A')) |]    
   1.211 +  ==> F \<in> A LeadsTo A'"
   1.212  apply (rule Always_LeadsToI, assumption)
   1.213  apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
   1.214  done
   1.215 @@ -183,14 +185,14 @@
   1.216  (*Set difference: maybe combine with leadsTo_weaken_L??
   1.217    This is the most useful form of the "disjunction" rule*)
   1.218  lemma LeadsTo_Diff:
   1.219 -     "[| F : (A-B) LeadsTo C;  F : (A Int B) LeadsTo C |]  
   1.220 -      ==> F : A LeadsTo C"
   1.221 +     "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |]  
   1.222 +      ==> F \<in> A LeadsTo C"
   1.223  by (blast intro: LeadsTo_Un LeadsTo_weaken)
   1.224  
   1.225  
   1.226  lemma LeadsTo_UN_UN: 
   1.227 -     "(!! i. i:I ==> F : (A i) LeadsTo (A' i))  
   1.228 -      ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)"
   1.229 +     "(!! i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i))  
   1.230 +      ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo (\<Union>i \<in> I. A' i)"
   1.231  apply (simp only: Union_image_eq [symmetric])
   1.232  apply (blast intro: LeadsTo_Union LeadsTo_weaken_R)
   1.233  done
   1.234 @@ -198,48 +200,47 @@
   1.235  
   1.236  (*Version with no index set*)
   1.237  lemma LeadsTo_UN_UN_noindex: 
   1.238 -     "(!! i. F : (A i) LeadsTo (A' i))  
   1.239 -      ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
   1.240 +     "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
   1.241  by (blast intro: LeadsTo_UN_UN)
   1.242  
   1.243  (*Version with no index set*)
   1.244  lemma all_LeadsTo_UN_UN:
   1.245 -     "ALL i. F : (A i) LeadsTo (A' i)  
   1.246 -      ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
   1.247 +     "\<forall>i. F \<in> (A i) LeadsTo (A' i)  
   1.248 +      ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
   1.249  by (blast intro: LeadsTo_UN_UN)
   1.250  
   1.251  (*Binary union version*)
   1.252  lemma LeadsTo_Un_Un:
   1.253 -     "[| F : A LeadsTo A'; F : B LeadsTo B' |]  
   1.254 -            ==> F : (A Un B) LeadsTo (A' Un B')"
   1.255 +     "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |]  
   1.256 +            ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')"
   1.257  by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
   1.258  
   1.259  
   1.260  (** The cancellation law **)
   1.261  
   1.262  lemma LeadsTo_cancel2:
   1.263 -     "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |]     
   1.264 -      ==> F : A LeadsTo (A' Un B')"
   1.265 +     "[| F \<in> A LeadsTo (A' \<union> B); F \<in> B LeadsTo B' |]     
   1.266 +      ==> F \<in> A LeadsTo (A' \<union> B')"
   1.267  by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans)
   1.268  
   1.269  lemma LeadsTo_cancel_Diff2:
   1.270 -     "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |]  
   1.271 -      ==> F : A LeadsTo (A' Un B')"
   1.272 +     "[| F \<in> A LeadsTo (A' \<union> B); F \<in> (B-A') LeadsTo B' |]  
   1.273 +      ==> F \<in> A LeadsTo (A' \<union> B')"
   1.274  apply (rule LeadsTo_cancel2)
   1.275  prefer 2 apply assumption
   1.276  apply (simp_all (no_asm_simp))
   1.277  done
   1.278  
   1.279  lemma LeadsTo_cancel1:
   1.280 -     "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |]  
   1.281 -      ==> F : A LeadsTo (B' Un A')"
   1.282 +     "[| F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' |]  
   1.283 +      ==> F \<in> A LeadsTo (B' \<union> A')"
   1.284  apply (simp add: Un_commute)
   1.285  apply (blast intro!: LeadsTo_cancel2)
   1.286  done
   1.287  
   1.288  lemma LeadsTo_cancel_Diff1:
   1.289 -     "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |]  
   1.290 -      ==> F : A LeadsTo (B' Un A')"
   1.291 +     "[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |]  
   1.292 +      ==> F \<in> A LeadsTo (B' \<union> A')"
   1.293  apply (rule LeadsTo_cancel1)
   1.294  prefer 2 apply assumption
   1.295  apply (simp_all (no_asm_simp))
   1.296 @@ -249,8 +250,8 @@
   1.297  (** The impossibility law **)
   1.298  
   1.299  (*The set "A" may be non-empty, but it contains no reachable states*)
   1.300 -lemma LeadsTo_empty: "F : A LeadsTo {} ==> F : Always (-A)"
   1.301 -apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
   1.302 +lemma LeadsTo_empty: "F \<in> A LeadsTo {} ==> F \<in> Always (-A)"
   1.303 +apply (simp add: LeadsTo_def Always_eq_includes_reachable)
   1.304  apply (drule leadsTo_empty, auto)
   1.305  done
   1.306  
   1.307 @@ -259,33 +260,33 @@
   1.308  
   1.309  (*Special case of PSP: Misra's "stable conjunction"*)
   1.310  lemma PSP_Stable:
   1.311 -     "[| F : A LeadsTo A';  F : Stable B |]  
   1.312 -      ==> F : (A Int B) LeadsTo (A' Int B)"
   1.313 -apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Stable_eq_stable)
   1.314 +     "[| F \<in> A LeadsTo A';  F \<in> Stable B |]  
   1.315 +      ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)"
   1.316 +apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable)
   1.317  apply (drule psp_stable, assumption)
   1.318  apply (simp add: Int_ac)
   1.319  done
   1.320  
   1.321  lemma PSP_Stable2:
   1.322 -     "[| F : A LeadsTo A'; F : Stable B |]  
   1.323 -      ==> F : (B Int A) LeadsTo (B Int A')"
   1.324 +     "[| F \<in> A LeadsTo A'; F \<in> Stable B |]  
   1.325 +      ==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')"
   1.326  by (simp add: PSP_Stable Int_ac)
   1.327  
   1.328  lemma PSP:
   1.329 -     "[| F : A LeadsTo A'; F : B Co B' |]  
   1.330 -      ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"
   1.331 -apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
   1.332 +     "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]  
   1.333 +      ==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))"
   1.334 +apply (simp add: LeadsTo_def Constrains_eq_constrains)
   1.335  apply (blast dest: psp intro: leadsTo_weaken)
   1.336  done
   1.337  
   1.338  lemma PSP2:
   1.339 -     "[| F : A LeadsTo A'; F : B Co B' |]  
   1.340 -      ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))"
   1.341 +     "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]  
   1.342 +      ==> F \<in> (B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))"
   1.343  by (simp add: PSP Int_ac)
   1.344  
   1.345  lemma PSP_Unless: 
   1.346 -     "[| F : A LeadsTo A'; F : B Unless B' |]  
   1.347 -      ==> F : (A Int B) LeadsTo ((A' Int B) Un B')"
   1.348 +     "[| F \<in> A LeadsTo A'; F \<in> B Unless B' |]  
   1.349 +      ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')"
   1.350  apply (unfold Unless_def)
   1.351  apply (drule PSP, assumption)
   1.352  apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
   1.353 @@ -293,8 +294,8 @@
   1.354  
   1.355  
   1.356  lemma Stable_transient_Always_LeadsTo:
   1.357 -     "[| F : Stable A;  F : transient C;   
   1.358 -         F : Always (-A Un B Un C) |] ==> F : A LeadsTo B"
   1.359 +     "[| F \<in> Stable A;  F \<in> transient C;   
   1.360 +         F \<in> Always (-A \<union> B \<union> C) |] ==> F \<in> A LeadsTo B"
   1.361  apply (erule Always_LeadsTo_weaken)
   1.362  apply (rule LeadsTo_Diff)
   1.363     prefer 2
   1.364 @@ -309,10 +310,10 @@
   1.365  (** Meta or object quantifier ????? **)
   1.366  lemma LeadsTo_wf_induct:
   1.367       "[| wf r;      
   1.368 -         ALL m. F : (A Int f-`{m}) LeadsTo                      
   1.369 -                            ((A Int f-`(r^-1 `` {m})) Un B) |]  
   1.370 -      ==> F : A LeadsTo B"
   1.371 -apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo)
   1.372 +         \<forall>m. F \<in> (A \<inter> f-`{m}) LeadsTo                      
   1.373 +                    ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
   1.374 +      ==> F \<in> A LeadsTo B"
   1.375 +apply (simp add: LeadsTo_eq_leadsTo)
   1.376  apply (erule leadsTo_wf_induct)
   1.377  apply (blast intro: leadsTo_weaken)
   1.378  done
   1.379 @@ -320,28 +321,27 @@
   1.380  
   1.381  lemma Bounded_induct:
   1.382       "[| wf r;      
   1.383 -         ALL m:I. F : (A Int f-`{m}) LeadsTo                    
   1.384 -                              ((A Int f-`(r^-1 `` {m})) Un B) |]  
   1.385 -      ==> F : A LeadsTo ((A - (f-`I)) Un B)"
   1.386 +         \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) LeadsTo                    
   1.387 +                      ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]  
   1.388 +      ==> F \<in> A LeadsTo ((A - (f-`I)) \<union> B)"
   1.389  apply (erule LeadsTo_wf_induct, safe)
   1.390 -apply (case_tac "m:I")
   1.391 +apply (case_tac "m \<in> I")
   1.392  apply (blast intro: LeadsTo_weaken)
   1.393  apply (blast intro: subset_imp_LeadsTo)
   1.394  done
   1.395  
   1.396  
   1.397  lemma LessThan_induct:
   1.398 -     "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B))  
   1.399 -      ==> F : A LeadsTo B"
   1.400 -apply (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
   1.401 -done
   1.402 +     "(!!m::nat. F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B))
   1.403 +      ==> F \<in> A LeadsTo B"
   1.404 +by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
   1.405  
   1.406  (*Integer version.  Could generalize from 0 to any lower bound*)
   1.407  lemma integ_0_le_induct:
   1.408 -     "[| F : Always {s. (0::int) <= f s};   
   1.409 -         !! z. F : (A Int {s. f s = z}) LeadsTo                      
   1.410 -                            ((A Int {s. f s < z}) Un B) |]  
   1.411 -      ==> F : A LeadsTo B"
   1.412 +     "[| F \<in> Always {s. (0::int) \<le> f s};   
   1.413 +         !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo                      
   1.414 +                   ((A \<inter> {s. f s < z}) \<union> B) |]  
   1.415 +      ==> F \<in> A LeadsTo B"
   1.416  apply (rule_tac f = "nat o f" in LessThan_induct)
   1.417  apply (simp add: vimage_def)
   1.418  apply (rule Always_LeadsTo_weaken, assumption+)
   1.419 @@ -349,42 +349,42 @@
   1.420  done
   1.421  
   1.422  lemma LessThan_bounded_induct:
   1.423 -     "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-`{m}) LeadsTo    
   1.424 -                                         ((A Int f-`(lessThan m)) Un B) |]  
   1.425 -            ==> F : A LeadsTo ((A Int (f-`(atMost l))) Un B)"
   1.426 -apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
   1.427 -apply (rule wf_less_than [THEN Bounded_induct])
   1.428 -apply (simp (no_asm_simp))
   1.429 +     "!!l::nat. \<forall>m \<in> greaterThan l. 
   1.430 +                   F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B)
   1.431 +            ==> F \<in> A LeadsTo ((A \<inter> (f-`(atMost l))) \<union> B)"
   1.432 +apply (simp only: Diff_eq [symmetric] vimage_Compl 
   1.433 +                  Compl_greaterThan [symmetric])
   1.434 +apply (rule wf_less_than [THEN Bounded_induct], simp)
   1.435  done
   1.436  
   1.437  lemma GreaterThan_bounded_induct:
   1.438 -     "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-`{m}) LeadsTo    
   1.439 -                               ((A Int f-`(greaterThan m)) Un B) |]  
   1.440 -      ==> F : A LeadsTo ((A Int (f-`(atLeast l))) Un B)"
   1.441 +     "!!l::nat. \<forall>m \<in> lessThan l. 
   1.442 +                 F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(greaterThan m)) \<union> B)
   1.443 +      ==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
   1.444  apply (rule_tac f = f and f1 = "%k. l - k" 
   1.445         in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
   1.446  apply (simp add: inv_image_def Image_singleton, clarify)
   1.447  apply (case_tac "m<l")
   1.448 - prefer 2 apply (blast intro: not_leE subset_imp_LeadsTo)
   1.449 -apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
   1.450 + apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
   1.451 +apply (blast intro: not_leE subset_imp_LeadsTo)
   1.452  done
   1.453  
   1.454  
   1.455  subsection{*Completion: Binary and General Finite versions*}
   1.456  
   1.457  lemma Completion:
   1.458 -     "[| F : A LeadsTo (A' Un C);  F : A' Co (A' Un C);  
   1.459 -         F : B LeadsTo (B' Un C);  F : B' Co (B' Un C) |]  
   1.460 -      ==> F : (A Int B) LeadsTo ((A' Int B') Un C)"
   1.461 -apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib)
   1.462 +     "[| F \<in> A LeadsTo (A' \<union> C);  F \<in> A' Co (A' \<union> C);  
   1.463 +         F \<in> B LeadsTo (B' \<union> C);  F \<in> B' Co (B' \<union> C) |]  
   1.464 +      ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)"
   1.465 +apply (simp add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib)
   1.466  apply (blast intro: completion leadsTo_weaken)
   1.467  done
   1.468  
   1.469  lemma Finite_completion_lemma:
   1.470       "finite I  
   1.471 -      ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) -->   
   1.472 -          (ALL i:I. F : (A' i) Co (A' i Un C)) -->  
   1.473 -          F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
   1.474 +      ==> (\<forall>i \<in> I. F \<in> (A i) LeadsTo (A' i \<union> C)) -->   
   1.475 +          (\<forall>i \<in> I. F \<in> (A' i) Co (A' i \<union> C)) -->  
   1.476 +          F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
   1.477  apply (erule finite_induct, auto)
   1.478  apply (rule Completion)
   1.479     prefer 4
   1.480 @@ -394,15 +394,15 @@
   1.481  
   1.482  lemma Finite_completion: 
   1.483       "[| finite I;   
   1.484 -         !!i. i:I ==> F : (A i) LeadsTo (A' i Un C);  
   1.485 -         !!i. i:I ==> F : (A' i) Co (A' i Un C) |]    
   1.486 -      ==> F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
   1.487 +         !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i \<union> C);  
   1.488 +         !!i. i \<in> I ==> F \<in> (A' i) Co (A' i \<union> C) |]    
   1.489 +      ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
   1.490  by (blast intro: Finite_completion_lemma [THEN mp, THEN mp])
   1.491  
   1.492  lemma Stable_completion: 
   1.493 -     "[| F : A LeadsTo A';  F : Stable A';    
   1.494 -         F : B LeadsTo B';  F : Stable B' |]  
   1.495 -      ==> F : (A Int B) LeadsTo (A' Int B')"
   1.496 +     "[| F \<in> A LeadsTo A';  F \<in> Stable A';    
   1.497 +         F \<in> B LeadsTo B';  F \<in> Stable B' |]  
   1.498 +      ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')"
   1.499  apply (unfold Stable_def)
   1.500  apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R])
   1.501  apply (force+)
   1.502 @@ -410,14 +410,12 @@
   1.503  
   1.504  lemma Finite_stable_completion: 
   1.505       "[| finite I;   
   1.506 -         !!i. i:I ==> F : (A i) LeadsTo (A' i);  
   1.507 -         !!i. i:I ==> F : Stable (A' i) |]    
   1.508 -      ==> F : (INT i:I. A i) LeadsTo (INT i:I. A' i)"
   1.509 +         !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i);  
   1.510 +         !!i. i \<in> I ==> F \<in> Stable (A' i) |]    
   1.511 +      ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo (\<Inter>i \<in> I. A' i)"
   1.512  apply (unfold Stable_def)
   1.513  apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R])
   1.514 -apply (simp_all (no_asm_simp))
   1.515 -apply blast+
   1.516 +apply (simp_all, blast+)
   1.517  done
   1.518  
   1.519 -
   1.520  end