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