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