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