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