src/ZF/UNITY/SubstAx.thy
author paulson
Mon Mar 28 16:19:56 2005 +0200 (2005-03-28)
changeset 15634 bca33c49b083
parent 12195 ed2893765a08
child 18371 d93fdf00f8a6
permissions -rw-r--r--
conversion of UNITY to Isar scripts
paulson@15634
     1
(*  ID:         $Id$
paulson@11479
     2
    Author:     Sidi O Ehmety, Computer Laboratory
paulson@11479
     3
    Copyright   2001  University of Cambridge
paulson@11479
     4
paulson@11479
     5
Theory ported from HOL.
paulson@11479
     6
*)
paulson@11479
     7
paulson@15634
     8
header{*Weak LeadsTo relation (restricted to the set of reachable states)*}
paulson@15634
     9
paulson@15634
    10
theory SubstAx
paulson@15634
    11
imports WFair Constrains 
paulson@15634
    12
paulson@15634
    13
begin
paulson@11479
    14
paulson@11479
    15
constdefs
ehmety@12195
    16
  (* The definitions below are not `conventional', but yields simpler rules *)
paulson@15634
    17
   Ensures :: "[i,i] => i"            (infixl "Ensures" 60)
ehmety@12195
    18
    "A Ensures B == {F:program. F : (reachable(F) Int A) ensures (reachable(F) Int B) }"
paulson@11479
    19
paulson@15634
    20
  LeadsTo :: "[i, i] => i"            (infixl "LeadsTo" 60)
ehmety@12195
    21
    "A LeadsTo B == {F:program. F:(reachable(F) Int A) leadsTo (reachable(F) Int B)}"
paulson@11479
    22
paulson@11479
    23
syntax (xsymbols)
paulson@15634
    24
  "LeadsTo" :: "[i, i] => i" (infixl " \<longmapsto>w " 60)
paulson@15634
    25
paulson@15634
    26
paulson@15634
    27
paulson@15634
    28
(*Resembles the previous definition of LeadsTo*)
paulson@15634
    29
paulson@15634
    30
(* Equivalence with the HOL-like definition *)
paulson@15634
    31
lemma LeadsTo_eq: 
paulson@15634
    32
"st_set(B)==> A LeadsTo B = {F \<in> program. F:(reachable(F) Int A) leadsTo B}"
paulson@15634
    33
apply (unfold LeadsTo_def)
paulson@15634
    34
apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
paulson@15634
    35
done
paulson@15634
    36
paulson@15634
    37
lemma LeadsTo_type: "A LeadsTo B <=program"
paulson@15634
    38
by (unfold LeadsTo_def, auto)
paulson@15634
    39
paulson@15634
    40
(*** Specialized laws for handling invariants ***)
paulson@15634
    41
paulson@15634
    42
(** Conjoining an Always property **)
paulson@15634
    43
lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I Int A) LeadsTo A') <-> (F \<in> A LeadsTo A')"
paulson@15634
    44
by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
paulson@15634
    45
paulson@15634
    46
lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A LeadsTo (I Int A')) <-> (F \<in> A LeadsTo A')"
paulson@15634
    47
apply (unfold LeadsTo_def)
paulson@15634
    48
apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
paulson@15634
    49
done
paulson@15634
    50
paulson@15634
    51
(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
paulson@15634
    52
lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C Int A) LeadsTo A' |] ==> F \<in> A LeadsTo A'"
paulson@15634
    53
by (blast intro: Always_LeadsTo_pre [THEN iffD1])
paulson@15634
    54
paulson@15634
    55
(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *)
paulson@15634
    56
lemma Always_LeadsToD: "[| F \<in> Always(C);  F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (C Int A')"
paulson@15634
    57
by (blast intro: Always_LeadsTo_post [THEN iffD2])
paulson@15634
    58
paulson@15634
    59
(*** Introduction rules \<in> Basis, Trans, Union ***)
paulson@15634
    60
paulson@15634
    61
lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"
paulson@15634
    62
by (auto simp add: Ensures_def LeadsTo_def)
paulson@15634
    63
paulson@15634
    64
lemma LeadsTo_Trans:
paulson@15634
    65
     "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"
paulson@15634
    66
apply (simp (no_asm_use) add: LeadsTo_def)
paulson@15634
    67
apply (blast intro: leadsTo_Trans)
paulson@15634
    68
done
paulson@15634
    69
paulson@15634
    70
lemma LeadsTo_Union:
paulson@15634
    71
"[|(!!A. A \<in> S ==> F \<in> A LeadsTo B); F \<in> program|]==>F \<in> Union(S) LeadsTo B"
paulson@15634
    72
apply (simp add: LeadsTo_def)
paulson@15634
    73
apply (subst Int_Union_Union2)
paulson@15634
    74
apply (rule leadsTo_UN, auto)
paulson@15634
    75
done
paulson@15634
    76
paulson@15634
    77
(*** Derived rules ***)
paulson@15634
    78
paulson@15634
    79
lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
paulson@15634
    80
apply (frule leadsToD2, clarify)
paulson@15634
    81
apply (simp (no_asm_simp) add: LeadsTo_eq)
paulson@15634
    82
apply (blast intro: leadsTo_weaken_L)
paulson@15634
    83
done
paulson@15634
    84
paulson@15634
    85
(*Useful with cancellation, disjunction*)
paulson@15634
    86
lemma LeadsTo_Un_duplicate: "F \<in> A LeadsTo (A' Un A') ==> F \<in> A LeadsTo A'"
paulson@15634
    87
by (simp add: Un_ac)
paulson@15634
    88
paulson@15634
    89
lemma LeadsTo_Un_duplicate2:
paulson@15634
    90
     "F \<in> A LeadsTo (A' Un C Un C) ==> F \<in> A LeadsTo (A' Un C)"
paulson@15634
    91
by (simp add: Un_ac)
paulson@15634
    92
paulson@15634
    93
lemma LeadsTo_UN:
paulson@15634
    94
    "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo B); F \<in> program|]
paulson@15634
    95
     ==>F:(\<Union>i \<in> I. A(i)) LeadsTo B"
paulson@15634
    96
apply (simp add: LeadsTo_def)
paulson@15634
    97
apply (simp (no_asm_simp) del: UN_simps add: Int_UN_distrib)
paulson@15634
    98
apply (rule leadsTo_UN, auto)
paulson@15634
    99
done
paulson@15634
   100
paulson@15634
   101
(*Binary union introduction rule*)
paulson@15634
   102
lemma LeadsTo_Un:
paulson@15634
   103
     "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A Un B) LeadsTo C"
paulson@15634
   104
apply (subst Un_eq_Union)
paulson@15634
   105
apply (rule LeadsTo_Union)
paulson@15634
   106
apply (auto dest: LeadsTo_type [THEN subsetD])
paulson@15634
   107
done
paulson@15634
   108
paulson@15634
   109
(*Lets us look at the starting state*)
paulson@15634
   110
lemma single_LeadsTo_I: 
paulson@15634
   111
    "[|(!!s. s \<in> A ==> F:{s} LeadsTo B); F \<in> program|]==>F \<in> A LeadsTo B"
paulson@15634
   112
apply (subst UN_singleton [symmetric], rule LeadsTo_UN, auto)
paulson@15634
   113
done
paulson@15634
   114
paulson@15634
   115
lemma subset_imp_LeadsTo: "[| A <= B; F \<in> program |] ==> F \<in> A LeadsTo B"
paulson@15634
   116
apply (simp (no_asm_simp) add: LeadsTo_def)
paulson@15634
   117
apply (blast intro: subset_imp_leadsTo)
paulson@15634
   118
done
paulson@15634
   119
paulson@15634
   120
lemma empty_LeadsTo: "F:0 LeadsTo A <-> F \<in> program"
paulson@15634
   121
by (auto dest: LeadsTo_type [THEN subsetD]
paulson@15634
   122
            intro: empty_subsetI [THEN subset_imp_LeadsTo])
paulson@15634
   123
declare empty_LeadsTo [iff]
paulson@15634
   124
paulson@15634
   125
lemma LeadsTo_state: "F \<in> A LeadsTo state <-> F \<in> program"
paulson@15634
   126
by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq)
paulson@15634
   127
declare LeadsTo_state [iff]
paulson@15634
   128
paulson@15634
   129
lemma LeadsTo_weaken_R: "[| F \<in> A LeadsTo A';  A'<=B'|] ==> F \<in> A LeadsTo B'"
paulson@15634
   130
apply (unfold LeadsTo_def)
paulson@15634
   131
apply (auto intro: leadsTo_weaken_R)
paulson@15634
   132
done
paulson@15634
   133
paulson@15634
   134
lemma LeadsTo_weaken_L: "[| F \<in> A LeadsTo A'; B <= A |] ==> F \<in> B LeadsTo A'"
paulson@15634
   135
apply (unfold LeadsTo_def)
paulson@15634
   136
apply (auto intro: leadsTo_weaken_L)
paulson@15634
   137
done
paulson@15634
   138
paulson@15634
   139
lemma LeadsTo_weaken: "[| F \<in> A LeadsTo A'; B<=A; A'<=B' |] ==> F \<in> B LeadsTo B'"
paulson@15634
   140
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
paulson@15634
   141
paulson@15634
   142
lemma Always_LeadsTo_weaken: 
paulson@15634
   143
"[| F \<in> Always(C);  F \<in> A LeadsTo A'; C Int B <= A;   C Int A' <= B' |]  
paulson@15634
   144
      ==> F \<in> B LeadsTo B'"
paulson@15634
   145
apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD)
paulson@15634
   146
done
paulson@15634
   147
paulson@15634
   148
(** Two theorems for "proof lattices" **)
paulson@15634
   149
paulson@15634
   150
lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F:(A Un B) LeadsTo B"
paulson@15634
   151
by (blast dest: LeadsTo_type [THEN subsetD]
paulson@15634
   152
             intro: LeadsTo_Un subset_imp_LeadsTo)
paulson@15634
   153
paulson@15634
   154
lemma LeadsTo_Trans_Un: "[| F \<in> A LeadsTo B;  F \<in> B LeadsTo C |]  
paulson@15634
   155
      ==> F \<in> (A Un B) LeadsTo C"
paulson@15634
   156
apply (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
paulson@15634
   157
done
paulson@15634
   158
paulson@15634
   159
(** Distributive laws **)
paulson@15634
   160
lemma LeadsTo_Un_distrib: "(F \<in> (A Un B) LeadsTo C)  <-> (F \<in> A LeadsTo C & F \<in> B LeadsTo C)"
paulson@15634
   161
by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
paulson@15634
   162
paulson@15634
   163
lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) LeadsTo B) <->  (\<forall>i \<in> I. F \<in> A(i) LeadsTo B) & F \<in> program"
paulson@15634
   164
by (blast dest: LeadsTo_type [THEN subsetD]
paulson@15634
   165
             intro: LeadsTo_UN LeadsTo_weaken_L)
paulson@15634
   166
paulson@15634
   167
lemma LeadsTo_Union_distrib: "(F \<in> Union(S) LeadsTo B)  <->  (\<forall>A \<in> S. F \<in> A LeadsTo B) & F \<in> program"
paulson@15634
   168
by (blast dest: LeadsTo_type [THEN subsetD]
paulson@15634
   169
             intro: LeadsTo_Union LeadsTo_weaken_L)
paulson@15634
   170
paulson@15634
   171
(** More rules using the premise "Always(I)" **)
paulson@15634
   172
paulson@15634
   173
lemma EnsuresI: "[| F:(A-B) Co (A Un B);  F \<in> transient (A-B) |] ==> F \<in> A Ensures B"
paulson@15634
   174
apply (simp add: Ensures_def Constrains_eq_constrains)
paulson@15634
   175
apply (blast intro: ensuresI constrains_weaken transient_strengthen dest: constrainsD2)
paulson@15634
   176
done
paulson@15634
   177
paulson@15634
   178
lemma Always_LeadsTo_Basis: "[| F \<in> Always(I); F \<in> (I Int (A-A')) Co (A Un A');  
paulson@15634
   179
         F \<in> transient (I Int (A-A')) |]    
paulson@15634
   180
  ==> F \<in> A LeadsTo A'"
paulson@15634
   181
apply (rule Always_LeadsToI, assumption)
paulson@15634
   182
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
paulson@15634
   183
done
paulson@15634
   184
paulson@15634
   185
(*Set difference: maybe combine with leadsTo_weaken_L??
paulson@15634
   186
  This is the most useful form of the "disjunction" rule*)
paulson@15634
   187
lemma LeadsTo_Diff:
paulson@15634
   188
     "[| F \<in> (A-B) LeadsTo C;  F \<in> (A Int B) LeadsTo C |] ==> F \<in> A LeadsTo C"
paulson@15634
   189
by (blast intro: LeadsTo_Un LeadsTo_weaken)
paulson@15634
   190
paulson@15634
   191
lemma LeadsTo_UN_UN:  
paulson@15634
   192
     "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i)); F \<in> program |]  
paulson@15634
   193
      ==> F \<in> (\<Union>i \<in> I. A(i)) LeadsTo (\<Union>i \<in> I. A'(i))"
paulson@15634
   194
apply (rule LeadsTo_Union, auto) 
paulson@15634
   195
apply (blast intro: LeadsTo_weaken_R)
paulson@15634
   196
done
paulson@15634
   197
paulson@15634
   198
(*Binary union version*)
paulson@15634
   199
lemma LeadsTo_Un_Un:
paulson@15634
   200
  "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] ==> F:(A Un B) LeadsTo (A' Un B')"
paulson@15634
   201
by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
paulson@15634
   202
paulson@15634
   203
(** The cancellation law **)
paulson@15634
   204
paulson@15634
   205
lemma LeadsTo_cancel2: "[| F \<in> A LeadsTo(A' Un B); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (A' Un B')"
paulson@15634
   206
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
paulson@15634
   207
paulson@15634
   208
lemma Un_Diff: "A Un (B - A) = A Un B"
paulson@15634
   209
by auto
paulson@15634
   210
paulson@15634
   211
lemma LeadsTo_cancel_Diff2: "[| F \<in> A LeadsTo (A' Un B); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (A' Un B')"
paulson@15634
   212
apply (rule LeadsTo_cancel2)
paulson@15634
   213
prefer 2 apply assumption
paulson@15634
   214
apply (simp (no_asm_simp) add: Un_Diff)
paulson@15634
   215
done
paulson@15634
   216
paulson@15634
   217
lemma LeadsTo_cancel1: "[| F \<in> A LeadsTo (B Un A'); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (B' Un A')"
paulson@15634
   218
apply (simp add: Un_commute)
paulson@15634
   219
apply (blast intro!: LeadsTo_cancel2)
paulson@15634
   220
done
paulson@15634
   221
paulson@15634
   222
lemma Diff_Un2: "(B - A) Un A = B Un A"
paulson@15634
   223
by auto
paulson@15634
   224
paulson@15634
   225
lemma LeadsTo_cancel_Diff1: "[| F \<in> A LeadsTo (B Un A'); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (B' Un A')"
paulson@15634
   226
apply (rule LeadsTo_cancel1)
paulson@15634
   227
prefer 2 apply assumption
paulson@15634
   228
apply (simp (no_asm_simp) add: Diff_Un2)
paulson@15634
   229
done
paulson@15634
   230
paulson@15634
   231
(** The impossibility law **)
paulson@15634
   232
paulson@15634
   233
(*The set "A" may be non-empty, but it contains no reachable states*)
paulson@15634
   234
lemma LeadsTo_empty: "F \<in> A LeadsTo 0 ==> F \<in> Always (state -A)"
paulson@15634
   235
apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
paulson@15634
   236
apply (cut_tac reachable_type)
paulson@15634
   237
apply (auto dest!: leadsTo_empty)
paulson@15634
   238
done
paulson@15634
   239
paulson@15634
   240
(** PSP \<in> Progress-Safety-Progress **)
paulson@15634
   241
paulson@15634
   242
(*Special case of PSP \<in> Misra's "stable conjunction"*)
paulson@15634
   243
lemma PSP_Stable: "[| F \<in> A LeadsTo A';  F \<in> Stable(B) |]==> F:(A Int B) LeadsTo (A' Int B)"
paulson@15634
   244
apply (simp add: LeadsTo_def Stable_eq_stable, clarify)
paulson@15634
   245
apply (drule psp_stable, assumption)
paulson@15634
   246
apply (simp add: Int_ac)
paulson@15634
   247
done
paulson@15634
   248
paulson@15634
   249
lemma PSP_Stable2: "[| F \<in> A LeadsTo A'; F \<in> Stable(B) |] ==> F \<in> (B Int A) LeadsTo (B Int A')"
paulson@15634
   250
apply (simp (no_asm_simp) add: PSP_Stable Int_ac)
paulson@15634
   251
done
paulson@15634
   252
paulson@15634
   253
lemma PSP: "[| F \<in> A LeadsTo A'; F \<in> B Co B'|]==> F \<in> (A Int B') LeadsTo ((A' Int B) Un (B' - B))"
paulson@15634
   254
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
paulson@15634
   255
apply (blast dest: psp intro: leadsTo_weaken)
paulson@15634
   256
done
paulson@15634
   257
paulson@15634
   258
lemma PSP2: "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]==> F:(B' Int A) LeadsTo ((B Int A') Un (B' - B))"
paulson@15634
   259
by (simp (no_asm_simp) add: PSP Int_ac)
paulson@15634
   260
paulson@15634
   261
lemma PSP_Unless: 
paulson@15634
   262
"[| F \<in> A LeadsTo A'; F \<in> B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')"
paulson@15634
   263
apply (unfold Unless_def)
paulson@15634
   264
apply (drule PSP, assumption)
paulson@15634
   265
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
paulson@15634
   266
done
paulson@15634
   267
paulson@15634
   268
(*** Induction rules ***)
paulson@15634
   269
paulson@15634
   270
(** Meta or object quantifier ????? **)
paulson@15634
   271
lemma LeadsTo_wf_induct: "[| wf(r);      
paulson@15634
   272
         \<forall>m \<in> I. F \<in> (A Int f-``{m}) LeadsTo                      
paulson@15634
   273
                            ((A Int f-``(converse(r) `` {m})) Un B);  
paulson@15634
   274
         field(r)<=I; A<=f-``I; F \<in> program |]  
paulson@15634
   275
      ==> F \<in> A LeadsTo B"
paulson@15634
   276
apply (simp (no_asm_use) add: LeadsTo_def)
paulson@15634
   277
apply auto
paulson@15634
   278
apply (erule_tac I = I and f = f in leadsTo_wf_induct, safe)
paulson@15634
   279
apply (drule_tac [2] x = m in bspec, safe)
paulson@15634
   280
apply (rule_tac [2] A' = "reachable (F) Int (A Int f -`` (converse (r) ``{m}) Un B) " in leadsTo_weaken_R)
paulson@15634
   281
apply (auto simp add: Int_assoc) 
paulson@15634
   282
done
paulson@15634
   283
paulson@15634
   284
paulson@15634
   285
lemma LessThan_induct: "[| \<forall>m \<in> nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``m) Un B);  
paulson@15634
   286
      A<=f-``nat; F \<in> program |] ==> F \<in> A LeadsTo B"
paulson@15634
   287
apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN LeadsTo_wf_induct])
paulson@15634
   288
apply (simp_all add: nat_measure_field)
paulson@15634
   289
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
paulson@15634
   290
done
paulson@15634
   291
paulson@15634
   292
paulson@15634
   293
(****** 
paulson@15634
   294
 To be ported ??? I am not sure.
paulson@15634
   295
paulson@15634
   296
  integ_0_le_induct
paulson@15634
   297
  LessThan_bounded_induct
paulson@15634
   298
  GreaterThan_bounded_induct
paulson@15634
   299
paulson@15634
   300
*****)
paulson@15634
   301
paulson@15634
   302
(*** Completion \<in> Binary and General Finite versions ***)
paulson@15634
   303
paulson@15634
   304
lemma Completion: "[| F \<in> A LeadsTo (A' Un C);  F \<in> A' Co (A' Un C);  
paulson@15634
   305
         F \<in> B LeadsTo (B' Un C);  F \<in> B' Co (B' Un C) |]  
paulson@15634
   306
      ==> F \<in> (A Int B) LeadsTo ((A' Int B') Un C)"
paulson@15634
   307
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains Int_Un_distrib)
paulson@15634
   308
apply (blast intro: completion leadsTo_weaken)
paulson@15634
   309
done
paulson@15634
   310
paulson@15634
   311
lemma Finite_completion_aux:
paulson@15634
   312
     "[| I \<in> Fin(X);F \<in> program |]  
paulson@15634
   313
      ==> (\<forall>i \<in> I. F \<in> (A(i)) LeadsTo (A'(i) Un C)) -->   
paulson@15634
   314
          (\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) Un C)) -->  
paulson@15634
   315
          F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) Un C)"
paulson@15634
   316
apply (erule Fin_induct)
paulson@15634
   317
apply (auto simp del: INT_simps simp add: Inter_0)
paulson@15634
   318
apply (rule Completion, auto) 
paulson@15634
   319
apply (simp del: INT_simps add: INT_extend_simps)
paulson@15634
   320
apply (blast intro: Constrains_INT)
paulson@15634
   321
done
paulson@15634
   322
paulson@15634
   323
lemma Finite_completion: 
paulson@15634
   324
     "[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) LeadsTo (A'(i) Un C);  
paulson@15634
   325
         !!i. i \<in> I ==> F \<in> A'(i) Co (A'(i) Un C);  
paulson@15634
   326
         F \<in> program |]    
paulson@15634
   327
      ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) Un C)"
paulson@15634
   328
by (blast intro: Finite_completion_aux [THEN mp, THEN mp])
paulson@15634
   329
paulson@15634
   330
lemma Stable_completion: 
paulson@15634
   331
     "[| F \<in> A LeadsTo A';  F \<in> Stable(A');    
paulson@15634
   332
         F \<in> B LeadsTo B';  F \<in> Stable(B') |]  
paulson@15634
   333
    ==> F \<in> (A Int B) LeadsTo (A' Int B')"
paulson@15634
   334
apply (unfold Stable_def)
paulson@15634
   335
apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
paulson@15634
   336
    prefer 5
paulson@15634
   337
    apply blast 
paulson@15634
   338
apply auto 
paulson@15634
   339
done
paulson@15634
   340
paulson@15634
   341
lemma Finite_stable_completion: 
paulson@15634
   342
     "[| I \<in> Fin(X);  
paulson@15634
   343
         (!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i));  
paulson@15634
   344
         (!!i. i \<in> I ==>F \<in> Stable(A'(i)));   F \<in> program  |]  
paulson@15634
   345
      ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo (\<Inter>i \<in> I. A'(i))"
paulson@15634
   346
apply (unfold Stable_def)
paulson@15634
   347
apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
paulson@15634
   348
apply (rule_tac [3] subset_refl, auto) 
paulson@15634
   349
done
paulson@15634
   350
paulson@15634
   351
ML
paulson@15634
   352
{*
paulson@15634
   353
val LeadsTo_eq = thm "LeadsTo_eq";
paulson@15634
   354
val LeadsTo_type = thm "LeadsTo_type";
paulson@15634
   355
val Always_LeadsTo_pre = thm "Always_LeadsTo_pre";
paulson@15634
   356
val Always_LeadsTo_post = thm "Always_LeadsTo_post";
paulson@15634
   357
val Always_LeadsToI = thm "Always_LeadsToI";
paulson@15634
   358
val Always_LeadsToD = thm "Always_LeadsToD";
paulson@15634
   359
val LeadsTo_Basis = thm "LeadsTo_Basis";
paulson@15634
   360
val LeadsTo_Trans = thm "LeadsTo_Trans";
paulson@15634
   361
val LeadsTo_Union = thm "LeadsTo_Union";
paulson@15634
   362
val leadsTo_imp_LeadsTo = thm "leadsTo_imp_LeadsTo";
paulson@15634
   363
val LeadsTo_Un_duplicate = thm "LeadsTo_Un_duplicate";
paulson@15634
   364
val LeadsTo_Un_duplicate2 = thm "LeadsTo_Un_duplicate2";
paulson@15634
   365
val LeadsTo_UN = thm "LeadsTo_UN";
paulson@15634
   366
val LeadsTo_Un = thm "LeadsTo_Un";
paulson@15634
   367
val single_LeadsTo_I = thm "single_LeadsTo_I";
paulson@15634
   368
val subset_imp_LeadsTo = thm "subset_imp_LeadsTo";
paulson@15634
   369
val empty_LeadsTo = thm "empty_LeadsTo";
paulson@15634
   370
val LeadsTo_state = thm "LeadsTo_state";
paulson@15634
   371
val LeadsTo_weaken_R = thm "LeadsTo_weaken_R";
paulson@15634
   372
val LeadsTo_weaken_L = thm "LeadsTo_weaken_L";
paulson@15634
   373
val LeadsTo_weaken = thm "LeadsTo_weaken";
paulson@15634
   374
val Always_LeadsTo_weaken = thm "Always_LeadsTo_weaken";
paulson@15634
   375
val LeadsTo_Un_post = thm "LeadsTo_Un_post";
paulson@15634
   376
val LeadsTo_Trans_Un = thm "LeadsTo_Trans_Un";
paulson@15634
   377
val LeadsTo_Un_distrib = thm "LeadsTo_Un_distrib";
paulson@15634
   378
val LeadsTo_UN_distrib = thm "LeadsTo_UN_distrib";
paulson@15634
   379
val LeadsTo_Union_distrib = thm "LeadsTo_Union_distrib";
paulson@15634
   380
val EnsuresI = thm "EnsuresI";
paulson@15634
   381
val Always_LeadsTo_Basis = thm "Always_LeadsTo_Basis";
paulson@15634
   382
val LeadsTo_Diff = thm "LeadsTo_Diff";
paulson@15634
   383
val LeadsTo_UN_UN = thm "LeadsTo_UN_UN";
paulson@15634
   384
val LeadsTo_Un_Un = thm "LeadsTo_Un_Un";
paulson@15634
   385
val LeadsTo_cancel2 = thm "LeadsTo_cancel2";
paulson@15634
   386
val Un_Diff = thm "Un_Diff";
paulson@15634
   387
val LeadsTo_cancel_Diff2 = thm "LeadsTo_cancel_Diff2";
paulson@15634
   388
val LeadsTo_cancel1 = thm "LeadsTo_cancel1";
paulson@15634
   389
val Diff_Un2 = thm "Diff_Un2";
paulson@15634
   390
val LeadsTo_cancel_Diff1 = thm "LeadsTo_cancel_Diff1";
paulson@15634
   391
val LeadsTo_empty = thm "LeadsTo_empty";
paulson@15634
   392
val PSP_Stable = thm "PSP_Stable";
paulson@15634
   393
val PSP_Stable2 = thm "PSP_Stable2";
paulson@15634
   394
val PSP = thm "PSP";
paulson@15634
   395
val PSP2 = thm "PSP2";
paulson@15634
   396
val PSP_Unless = thm "PSP_Unless";
paulson@15634
   397
val LeadsTo_wf_induct = thm "LeadsTo_wf_induct";
paulson@15634
   398
val LessThan_induct = thm "LessThan_induct";
paulson@15634
   399
val Completion = thm "Completion";
paulson@15634
   400
val Finite_completion = thm "Finite_completion";
paulson@15634
   401
val Stable_completion = thm "Stable_completion";
paulson@15634
   402
val Finite_stable_completion = thm "Finite_stable_completion";
paulson@15634
   403
paulson@15634
   404
paulson@15634
   405
(*proves "ensures/leadsTo" properties when the program is specified*)
paulson@15634
   406
fun gen_ensures_tac(cs,ss) sact = 
paulson@15634
   407
    SELECT_GOAL
paulson@15634
   408
      (EVERY [REPEAT (Always_Int_tac 1),
paulson@15634
   409
              etac Always_LeadsTo_Basis 1 
paulson@15634
   410
                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
paulson@15634
   411
                  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
paulson@15634
   412
                                    EnsuresI, ensuresI] 1),
paulson@15634
   413
              (*now there are two subgoals: co & transient*)
paulson@15634
   414
              simp_tac (ss addsimps !program_defs_ref) 2,
paulson@15634
   415
              res_inst_tac [("act", sact)] transientI 2,
paulson@15634
   416
                 (*simplify the command's domain*)
paulson@15634
   417
              simp_tac (ss addsimps [domain_def]) 3, 
paulson@15634
   418
              (* proving the domain part *)
paulson@15634
   419
             clarify_tac cs 3, dtac swap 3, force_tac (cs,ss) 4,
paulson@15634
   420
             rtac ReplaceI 3, force_tac (cs,ss) 3, force_tac (cs,ss) 4,
paulson@15634
   421
             asm_full_simp_tac ss 3, rtac conjI 3, simp_tac ss 4,
paulson@15634
   422
             REPEAT (rtac state_update_type 3),
paulson@15634
   423
             gen_constrains_tac (cs,ss) 1,
paulson@15634
   424
             ALLGOALS (clarify_tac cs),
paulson@15634
   425
             ALLGOALS (asm_full_simp_tac (ss addsimps [st_set_def])),
paulson@15634
   426
                        ALLGOALS (clarify_tac cs),
paulson@15634
   427
            ALLGOALS (asm_lr_simp_tac ss)]);
paulson@15634
   428
paulson@15634
   429
fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact;
paulson@15634
   430
*}
paulson@15634
   431
paulson@15634
   432
paulson@15634
   433
method_setup ensures_tac = {*
paulson@15634
   434
    fn args => fn ctxt =>
paulson@15634
   435
        Method.goal_args' (Scan.lift Args.name) 
paulson@15634
   436
           (gen_ensures_tac (local_clasimpset_of ctxt))
paulson@15634
   437
           args ctxt *}
paulson@15634
   438
    "for proving progress properties"
paulson@15634
   439
paulson@11479
   440
paulson@11479
   441
end