src/HOL/UNITY/WFair.thy
author paulson
Thu Jan 30 18:08:09 2003 +0100 (2003-01-30)
changeset 13797 baefae13ad37
parent 10834 a7897aebbffc
child 13798 4c1a53627500
permissions -rw-r--r--
conversion of UNITY theories to new-style
paulson@4776
     1
(*  Title:      HOL/UNITY/WFair
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@4776
     6
Weak Fairness versions of transient, ensures, leadsTo.
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming", 1994
paulson@4776
     9
*)
paulson@4776
    10
paulson@13797
    11
theory WFair = UNITY:
paulson@4776
    12
paulson@4776
    13
constdefs
paulson@4776
    14
paulson@5155
    15
  (*This definition specifies weak fairness.  The rest of the theory
paulson@5155
    16
    is generic to all forms of fairness.*)
paulson@5648
    17
  transient :: "'a set => 'a program set"
nipkow@10834
    18
    "transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}"
paulson@4776
    19
paulson@13797
    20
  ensures :: "['a set, 'a set] => 'a program set"       (infixl "ensures" 60)
paulson@8006
    21
    "A ensures B == (A-B co A Un B) Int transient (A-B)"
paulson@8006
    22
paulson@6536
    23
paulson@6536
    24
consts
paulson@6536
    25
paulson@6536
    26
  (*LEADS-TO constant for the inductive definition*)
paulson@6801
    27
  leads :: "'a program => ('a set * 'a set) set"
paulson@5648
    28
paulson@6801
    29
paulson@6801
    30
inductive "leads F"
paulson@13797
    31
  intros 
paulson@4776
    32
paulson@13797
    33
    Basis:  "F : A ensures B ==> (A,B) : leads F"
paulson@4776
    34
paulson@13797
    35
    Trans:  "[| (A,B) : leads F;  (B,C) : leads F |] ==> (A,C) : leads F"
paulson@4776
    36
paulson@13797
    37
    Union:  "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F"
paulson@4776
    38
paulson@5155
    39
paulson@8006
    40
constdefs
paulson@6536
    41
paulson@8006
    42
  (*visible version of the LEADS-TO relation*)
paulson@13797
    43
  leadsTo :: "['a set, 'a set] => 'a program set"    (infixl "leadsTo" 60)
paulson@8006
    44
    "A leadsTo B == {F. (A,B) : leads F}"
paulson@5648
    45
  
paulson@5648
    46
  (*wlt F B is the largest set that leads to B*)
paulson@5648
    47
  wlt :: "['a program, 'a set] => 'a set"
paulson@6536
    48
    "wlt F B == Union {A. F: A leadsTo B}"
paulson@4776
    49
paulson@9685
    50
syntax (xsymbols)
paulson@13797
    51
  "op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
paulson@13797
    52
paulson@13797
    53
paulson@13797
    54
(*** transient ***)
paulson@13797
    55
paulson@13797
    56
lemma stable_transient_empty: 
paulson@13797
    57
    "[| F : stable A; F : transient A |] ==> A = {}"
paulson@13797
    58
paulson@13797
    59
by (unfold stable_def constrains_def transient_def, blast)
paulson@13797
    60
paulson@13797
    61
lemma transient_strengthen: 
paulson@13797
    62
    "[| F : transient A; B<=A |] ==> F : transient B"
paulson@13797
    63
apply (unfold transient_def, clarify)
paulson@13797
    64
apply (blast intro!: rev_bexI)
paulson@13797
    65
done
paulson@13797
    66
paulson@13797
    67
lemma transientI: 
paulson@13797
    68
    "[| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> F : transient A"
paulson@13797
    69
by (unfold transient_def, blast)
paulson@13797
    70
paulson@13797
    71
lemma transientE: 
paulson@13797
    72
    "[| F : transient A;   
paulson@13797
    73
        !!act. [| act: Acts F;  A <= Domain act;  act``A <= -A |] ==> P |]  
paulson@13797
    74
     ==> P"
paulson@13797
    75
by (unfold transient_def, blast)
paulson@13797
    76
paulson@13797
    77
lemma transient_UNIV [simp]: "transient UNIV = {}"
paulson@13797
    78
by (unfold transient_def, blast)
paulson@13797
    79
paulson@13797
    80
lemma transient_empty [simp]: "transient {} = UNIV"
paulson@13797
    81
by (unfold transient_def, auto)
paulson@13797
    82
paulson@13797
    83
paulson@13797
    84
(*** ensures ***)
paulson@13797
    85
paulson@13797
    86
lemma ensuresI: 
paulson@13797
    87
    "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"
paulson@13797
    88
by (unfold ensures_def, blast)
paulson@13797
    89
paulson@13797
    90
lemma ensuresD: 
paulson@13797
    91
    "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"
paulson@13797
    92
by (unfold ensures_def, blast)
paulson@13797
    93
paulson@13797
    94
lemma ensures_weaken_R: 
paulson@13797
    95
    "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"
paulson@13797
    96
apply (unfold ensures_def)
paulson@13797
    97
apply (blast intro: constrains_weaken transient_strengthen)
paulson@13797
    98
done
paulson@13797
    99
paulson@13797
   100
(*The L-version (precondition strengthening) fails, but we have this*)
paulson@13797
   101
lemma stable_ensures_Int: 
paulson@13797
   102
    "[| F : stable C;  F : A ensures B |]    
paulson@13797
   103
    ==> F : (C Int A) ensures (C Int B)"
paulson@13797
   104
apply (unfold ensures_def)
paulson@13797
   105
apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
paulson@13797
   106
prefer 2 apply (blast intro: transient_strengthen)
paulson@13797
   107
apply (blast intro: stable_constrains_Int constrains_weaken)
paulson@13797
   108
done
paulson@13797
   109
paulson@13797
   110
lemma stable_transient_ensures:
paulson@13797
   111
     "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B"
paulson@13797
   112
apply (simp add: ensures_def stable_def)
paulson@13797
   113
apply (blast intro: constrains_weaken transient_strengthen)
paulson@13797
   114
done
paulson@13797
   115
paulson@13797
   116
lemma ensures_eq: "(A ensures B) = (A unless B) Int transient (A-B)"
paulson@13797
   117
by (simp (no_asm) add: ensures_def unless_def)
paulson@13797
   118
paulson@13797
   119
paulson@13797
   120
(*** leadsTo ***)
paulson@13797
   121
paulson@13797
   122
lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B"
paulson@13797
   123
apply (unfold leadsTo_def)
paulson@13797
   124
apply (blast intro: leads.Basis)
paulson@13797
   125
done
paulson@13797
   126
paulson@13797
   127
lemma leadsTo_Trans: 
paulson@13797
   128
     "[| F : A leadsTo B;  F : B leadsTo C |] ==> F : A leadsTo C"
paulson@13797
   129
apply (unfold leadsTo_def)
paulson@13797
   130
apply (blast intro: leads.Trans)
paulson@13797
   131
done
paulson@13797
   132
paulson@13797
   133
lemma transient_imp_leadsTo: "F : transient A ==> F : A leadsTo (-A)"
paulson@13797
   134
by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
paulson@13797
   135
paulson@13797
   136
(*Useful with cancellation, disjunction*)
paulson@13797
   137
lemma leadsTo_Un_duplicate: "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"
paulson@13797
   138
by (simp add: Un_ac)
paulson@13797
   139
paulson@13797
   140
lemma leadsTo_Un_duplicate2:
paulson@13797
   141
     "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"
paulson@13797
   142
by (simp add: Un_ac)
paulson@13797
   143
paulson@13797
   144
(*The Union introduction rule as we should have liked to state it*)
paulson@13797
   145
lemma leadsTo_Union: 
paulson@13797
   146
    "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"
paulson@13797
   147
apply (unfold leadsTo_def)
paulson@13797
   148
apply (blast intro: leads.Union)
paulson@13797
   149
done
paulson@13797
   150
paulson@13797
   151
lemma leadsTo_Union_Int: 
paulson@13797
   152
 "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B"
paulson@13797
   153
apply (unfold leadsTo_def)
paulson@13797
   154
apply (simp only: Int_Union_Union)
paulson@13797
   155
apply (blast intro: leads.Union)
paulson@13797
   156
done
paulson@13797
   157
paulson@13797
   158
lemma leadsTo_UN: 
paulson@13797
   159
    "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"
paulson@13797
   160
apply (subst Union_image_eq [symmetric])
paulson@13797
   161
apply (blast intro: leadsTo_Union)
paulson@13797
   162
done
paulson@13797
   163
paulson@13797
   164
(*Binary union introduction rule*)
paulson@13797
   165
lemma leadsTo_Un:
paulson@13797
   166
     "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C"
paulson@13797
   167
apply (subst Un_eq_Union)
paulson@13797
   168
apply (blast intro: leadsTo_Union)
paulson@13797
   169
done
paulson@13797
   170
paulson@13797
   171
lemma single_leadsTo_I: 
paulson@13797
   172
     "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B"
paulson@13797
   173
by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
paulson@13797
   174
paulson@13797
   175
paulson@13797
   176
(*The INDUCTION rule as we should have liked to state it*)
paulson@13797
   177
lemma leadsTo_induct: 
paulson@13797
   178
  "[| F : za leadsTo zb;   
paulson@13797
   179
      !!A B. F : A ensures B ==> P A B;  
paulson@13797
   180
      !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |]  
paulson@13797
   181
               ==> P A C;  
paulson@13797
   182
      !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B  
paulson@13797
   183
   |] ==> P za zb"
paulson@13797
   184
apply (unfold leadsTo_def)
paulson@13797
   185
apply (drule CollectD, erule leads.induct)
paulson@13797
   186
apply (blast+)
paulson@13797
   187
done
paulson@13797
   188
paulson@13797
   189
paulson@13797
   190
lemma subset_imp_ensures: "A<=B ==> F : A ensures B"
paulson@13797
   191
by (unfold ensures_def constrains_def transient_def, blast)
paulson@13797
   192
paulson@13797
   193
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
paulson@13797
   194
paulson@13797
   195
lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard]
paulson@13797
   196
paulson@13797
   197
lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp]
paulson@13797
   198
paulson@13797
   199
lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp]
paulson@13797
   200
paulson@13797
   201
paulson@13797
   202
paulson@13797
   203
(** Variant induction rule: on the preconditions for B **)
paulson@13797
   204
paulson@13797
   205
(*Lemma is the weak version: can't see how to do it in one step*)
paulson@13797
   206
lemma leadsTo_induct_pre_lemma: 
paulson@13797
   207
  "[| F : za leadsTo zb;   
paulson@13797
   208
      P zb;  
paulson@13797
   209
      !!A B. [| F : A ensures B;  P B |] ==> P A;  
paulson@13797
   210
      !!S. ALL A:S. P A ==> P (Union S)  
paulson@13797
   211
   |] ==> P za"
paulson@13797
   212
(*by induction on this formula*)
paulson@13797
   213
apply (subgoal_tac "P zb --> P za")
paulson@13797
   214
(*now solve first subgoal: this formula is sufficient*)
paulson@13797
   215
apply (blast intro: leadsTo_refl)
paulson@13797
   216
apply (erule leadsTo_induct)
paulson@13797
   217
apply (blast+)
paulson@13797
   218
done
paulson@13797
   219
paulson@13797
   220
lemma leadsTo_induct_pre: 
paulson@13797
   221
  "[| F : za leadsTo zb;   
paulson@13797
   222
      P zb;  
paulson@13797
   223
      !!A B. [| F : A ensures B;  F : B leadsTo zb;  P B |] ==> P A;  
paulson@13797
   224
      !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S)  
paulson@13797
   225
   |] ==> P za"
paulson@13797
   226
apply (subgoal_tac "F : za leadsTo zb & P za")
paulson@13797
   227
apply (erule conjunct2)
paulson@13797
   228
apply (erule leadsTo_induct_pre_lemma)
paulson@13797
   229
prefer 3 apply (blast intro: leadsTo_Union)
paulson@13797
   230
prefer 2 apply (blast intro: leadsTo_Trans)
paulson@13797
   231
apply (blast intro: leadsTo_refl)
paulson@13797
   232
done
paulson@13797
   233
paulson@13797
   234
paulson@13797
   235
lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"
paulson@13797
   236
by (blast intro: subset_imp_leadsTo leadsTo_Trans)
paulson@13797
   237
paulson@13797
   238
lemma leadsTo_weaken_L [rule_format (no_asm)]:
paulson@13797
   239
     "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"
paulson@13797
   240
by (blast intro: leadsTo_Trans subset_imp_leadsTo)
paulson@13797
   241
paulson@13797
   242
(*Distributes over binary unions*)
paulson@13797
   243
lemma leadsTo_Un_distrib:
paulson@13797
   244
     "F : (A Un B) leadsTo C  =  (F : A leadsTo C & F : B leadsTo C)"
paulson@13797
   245
by (blast intro: leadsTo_Un leadsTo_weaken_L)
paulson@13797
   246
paulson@13797
   247
lemma leadsTo_UN_distrib:
paulson@13797
   248
     "F : (UN i:I. A i) leadsTo B  =  (ALL i : I. F : (A i) leadsTo B)"
paulson@13797
   249
by (blast intro: leadsTo_UN leadsTo_weaken_L)
paulson@13797
   250
paulson@13797
   251
lemma leadsTo_Union_distrib:
paulson@13797
   252
     "F : (Union S) leadsTo B  =  (ALL A : S. F : A leadsTo B)"
paulson@13797
   253
by (blast intro: leadsTo_Union leadsTo_weaken_L)
paulson@13797
   254
paulson@13797
   255
paulson@13797
   256
lemma leadsTo_weaken:
paulson@13797
   257
     "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'"
paulson@13797
   258
by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
paulson@13797
   259
paulson@13797
   260
paulson@13797
   261
(*Set difference: maybe combine with leadsTo_weaken_L?*)
paulson@13797
   262
lemma leadsTo_Diff:
paulson@13797
   263
     "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C"
paulson@13797
   264
by (blast intro: leadsTo_Un leadsTo_weaken)
paulson@13797
   265
paulson@13797
   266
lemma leadsTo_UN_UN:
paulson@13797
   267
   "(!! i. i:I ==> F : (A i) leadsTo (A' i))  
paulson@13797
   268
    ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"
paulson@13797
   269
apply (simp only: Union_image_eq [symmetric])
paulson@13797
   270
apply (blast intro: leadsTo_Union leadsTo_weaken_R)
paulson@13797
   271
done
paulson@13797
   272
paulson@13797
   273
(*Binary union version*)
paulson@13797
   274
lemma leadsTo_Un_Un:
paulson@13797
   275
     "[| F : A leadsTo A'; F : B leadsTo B' |]  
paulson@13797
   276
      ==> F : (A Un B) leadsTo (A' Un B')"
paulson@13797
   277
by (blast intro: leadsTo_Un leadsTo_weaken_R)
paulson@13797
   278
paulson@13797
   279
paulson@13797
   280
(** The cancellation law **)
paulson@13797
   281
paulson@13797
   282
lemma leadsTo_cancel2:
paulson@13797
   283
     "[| F : A leadsTo (A' Un B); F : B leadsTo B' |]  
paulson@13797
   284
      ==> F : A leadsTo (A' Un B')"
paulson@13797
   285
by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans)
paulson@13797
   286
paulson@13797
   287
lemma leadsTo_cancel_Diff2:
paulson@13797
   288
     "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |]  
paulson@13797
   289
      ==> F : A leadsTo (A' Un B')"
paulson@13797
   290
apply (rule leadsTo_cancel2)
paulson@13797
   291
prefer 2 apply assumption
paulson@13797
   292
apply (simp_all (no_asm_simp))
paulson@13797
   293
done
paulson@13797
   294
paulson@13797
   295
lemma leadsTo_cancel1:
paulson@13797
   296
     "[| F : A leadsTo (B Un A'); F : B leadsTo B' |]  
paulson@13797
   297
    ==> F : A leadsTo (B' Un A')"
paulson@13797
   298
apply (simp add: Un_commute)
paulson@13797
   299
apply (blast intro!: leadsTo_cancel2)
paulson@13797
   300
done
paulson@13797
   301
paulson@13797
   302
lemma leadsTo_cancel_Diff1:
paulson@13797
   303
     "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |]  
paulson@13797
   304
    ==> F : A leadsTo (B' Un A')"
paulson@13797
   305
apply (rule leadsTo_cancel1)
paulson@13797
   306
prefer 2 apply assumption
paulson@13797
   307
apply (simp_all (no_asm_simp))
paulson@13797
   308
done
paulson@13797
   309
paulson@13797
   310
paulson@13797
   311
paulson@13797
   312
(** The impossibility law **)
paulson@13797
   313
paulson@13797
   314
lemma leadsTo_empty: "F : A leadsTo {} ==> A={}"
paulson@13797
   315
apply (erule leadsTo_induct_pre)
paulson@13797
   316
apply (simp_all add: ensures_def constrains_def transient_def, blast)
paulson@13797
   317
done
paulson@13797
   318
paulson@13797
   319
paulson@13797
   320
(** PSP: Progress-Safety-Progress **)
paulson@13797
   321
paulson@13797
   322
(*Special case of PSP: Misra's "stable conjunction"*)
paulson@13797
   323
lemma psp_stable: 
paulson@13797
   324
   "[| F : A leadsTo A'; F : stable B |]  
paulson@13797
   325
    ==> F : (A Int B) leadsTo (A' Int B)"
paulson@13797
   326
apply (unfold stable_def)
paulson@13797
   327
apply (erule leadsTo_induct)
paulson@13797
   328
prefer 3 apply (blast intro: leadsTo_Union_Int)
paulson@13797
   329
prefer 2 apply (blast intro: leadsTo_Trans)
paulson@13797
   330
apply (rule leadsTo_Basis)
paulson@13797
   331
apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
paulson@13797
   332
apply (blast intro: transient_strengthen constrains_Int)
paulson@13797
   333
done
paulson@13797
   334
paulson@13797
   335
lemma psp_stable2: 
paulson@13797
   336
   "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')"
paulson@13797
   337
by (simp add: psp_stable Int_ac)
paulson@13797
   338
paulson@13797
   339
lemma psp_ensures: 
paulson@13797
   340
   "[| F : A ensures A'; F : B co B' |]  
paulson@13797
   341
    ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))"
paulson@13797
   342
apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*)
paulson@13797
   343
apply (blast intro: transient_strengthen)
paulson@13797
   344
done
paulson@13797
   345
paulson@13797
   346
lemma psp:
paulson@13797
   347
     "[| F : A leadsTo A'; F : B co B' |]  
paulson@13797
   348
      ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))"
paulson@13797
   349
apply (erule leadsTo_induct)
paulson@13797
   350
  prefer 3 apply (blast intro: leadsTo_Union_Int)
paulson@13797
   351
 txt{*Basis case*}
paulson@13797
   352
 apply (blast intro: psp_ensures)
paulson@13797
   353
txt{*Transitivity case has a delicate argument involving "cancellation"*}
paulson@13797
   354
apply (rule leadsTo_Un_duplicate2)
paulson@13797
   355
apply (erule leadsTo_cancel_Diff1)
paulson@13797
   356
apply (simp add: Int_Diff Diff_triv)
paulson@13797
   357
apply (blast intro: leadsTo_weaken_L dest: constrains_imp_subset)
paulson@13797
   358
done
paulson@13797
   359
paulson@13797
   360
lemma psp2:
paulson@13797
   361
     "[| F : A leadsTo A'; F : B co B' |]  
paulson@13797
   362
    ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"
paulson@13797
   363
by (simp (no_asm_simp) add: psp Int_ac)
paulson@13797
   364
paulson@13797
   365
lemma psp_unless: 
paulson@13797
   366
   "[| F : A leadsTo A';  F : B unless B' |]  
paulson@13797
   367
    ==> F : (A Int B) leadsTo ((A' Int B) Un B')"
paulson@13797
   368
paulson@13797
   369
apply (unfold unless_def)
paulson@13797
   370
apply (drule psp, assumption)
paulson@13797
   371
apply (blast intro: leadsTo_weaken)
paulson@13797
   372
done
paulson@13797
   373
paulson@13797
   374
paulson@13797
   375
(*** Proving the induction rules ***)
paulson@13797
   376
paulson@13797
   377
(** The most general rule: r is any wf relation; f is any variant function **)
paulson@13797
   378
paulson@13797
   379
lemma leadsTo_wf_induct_lemma:
paulson@13797
   380
     "[| wf r;      
paulson@13797
   381
         ALL m. F : (A Int f-`{m}) leadsTo                      
paulson@13797
   382
                    ((A Int f-`(r^-1 `` {m})) Un B) |]  
paulson@13797
   383
      ==> F : (A Int f-`{m}) leadsTo B"
paulson@13797
   384
apply (erule_tac a = m in wf_induct)
paulson@13797
   385
apply (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B")
paulson@13797
   386
 apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
paulson@13797
   387
apply (subst vimage_eq_UN)
paulson@13797
   388
apply (simp only: UN_simps [symmetric])
paulson@13797
   389
apply (blast intro: leadsTo_UN)
paulson@13797
   390
done
paulson@13797
   391
paulson@13797
   392
paulson@13797
   393
(** Meta or object quantifier ? **)
paulson@13797
   394
lemma leadsTo_wf_induct:
paulson@13797
   395
     "[| wf r;      
paulson@13797
   396
         ALL m. F : (A Int f-`{m}) leadsTo                      
paulson@13797
   397
                    ((A Int f-`(r^-1 `` {m})) Un B) |]  
paulson@13797
   398
      ==> F : A leadsTo B"
paulson@13797
   399
apply (rule_tac t = A in subst)
paulson@13797
   400
 defer 1
paulson@13797
   401
 apply (rule leadsTo_UN)
paulson@13797
   402
 apply (erule leadsTo_wf_induct_lemma)
paulson@13797
   403
 apply assumption
paulson@13797
   404
apply fast (*Blast_tac: Function unknown's argument not a parameter*)
paulson@13797
   405
done
paulson@13797
   406
paulson@13797
   407
paulson@13797
   408
lemma bounded_induct:
paulson@13797
   409
     "[| wf r;      
paulson@13797
   410
         ALL m:I. F : (A Int f-`{m}) leadsTo                    
paulson@13797
   411
                      ((A Int f-`(r^-1 `` {m})) Un B) |]  
paulson@13797
   412
      ==> F : A leadsTo ((A - (f-`I)) Un B)"
paulson@13797
   413
apply (erule leadsTo_wf_induct, safe)
paulson@13797
   414
apply (case_tac "m:I")
paulson@13797
   415
apply (blast intro: leadsTo_weaken)
paulson@13797
   416
apply (blast intro: subset_imp_leadsTo)
paulson@13797
   417
done
paulson@13797
   418
paulson@13797
   419
paulson@13797
   420
(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
paulson@13797
   421
lemma lessThan_induct: 
paulson@13797
   422
     "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |]  
paulson@13797
   423
      ==> F : A leadsTo B"
paulson@13797
   424
apply (rule wf_less_than [THEN leadsTo_wf_induct])
paulson@13797
   425
apply (simp (no_asm_simp))
paulson@13797
   426
apply blast
paulson@13797
   427
done
paulson@13797
   428
paulson@13797
   429
lemma lessThan_bounded_induct:
paulson@13797
   430
     "!!l::nat. [| ALL m:(greaterThan l).     
paulson@13797
   431
            F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |]  
paulson@13797
   432
      ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)"
paulson@13797
   433
apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
paulson@13797
   434
apply (rule wf_less_than [THEN bounded_induct])
paulson@13797
   435
apply (simp (no_asm_simp))
paulson@13797
   436
done
paulson@13797
   437
paulson@13797
   438
lemma greaterThan_bounded_induct:
paulson@13797
   439
     "!!l::nat. [| ALL m:(lessThan l).     
paulson@13797
   440
            F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |]  
paulson@13797
   441
      ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)"
paulson@13797
   442
apply (rule_tac f = f and f1 = "%k. l - k" 
paulson@13797
   443
       in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
paulson@13797
   444
apply (simp (no_asm) add: inv_image_def Image_singleton)
paulson@13797
   445
apply clarify
paulson@13797
   446
apply (case_tac "m<l")
paulson@13797
   447
prefer 2 apply (blast intro: not_leE subset_imp_leadsTo)
paulson@13797
   448
apply (blast intro: leadsTo_weaken_R diff_less_mono2)
paulson@13797
   449
done
paulson@13797
   450
paulson@13797
   451
paulson@13797
   452
(*** wlt ****)
paulson@13797
   453
paulson@13797
   454
(*Misra's property W3*)
paulson@13797
   455
lemma wlt_leadsTo: "F : (wlt F B) leadsTo B"
paulson@13797
   456
apply (unfold wlt_def)
paulson@13797
   457
apply (blast intro!: leadsTo_Union)
paulson@13797
   458
done
paulson@13797
   459
paulson@13797
   460
lemma leadsTo_subset: "F : A leadsTo B ==> A <= wlt F B"
paulson@13797
   461
apply (unfold wlt_def)
paulson@13797
   462
apply (blast intro!: leadsTo_Union)
paulson@13797
   463
done
paulson@13797
   464
paulson@13797
   465
(*Misra's property W2*)
paulson@13797
   466
lemma leadsTo_eq_subset_wlt: "F : A leadsTo B = (A <= wlt F B)"
paulson@13797
   467
by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
paulson@13797
   468
paulson@13797
   469
(*Misra's property W4*)
paulson@13797
   470
lemma wlt_increasing: "B <= wlt F B"
paulson@13797
   471
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
paulson@13797
   472
done
paulson@13797
   473
paulson@13797
   474
paulson@13797
   475
(*Used in the Trans case below*)
paulson@13797
   476
lemma lemma1: 
paulson@13797
   477
   "[| B <= A2;   
paulson@13797
   478
       F : (A1 - B) co (A1 Un B);  
paulson@13797
   479
       F : (A2 - C) co (A2 Un C) |]  
paulson@13797
   480
    ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"
paulson@13797
   481
by (unfold constrains_def, clarify,  blast)
paulson@13797
   482
paulson@13797
   483
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
paulson@13797
   484
lemma leadsTo_123:
paulson@13797
   485
     "F : A leadsTo A'  
paulson@13797
   486
      ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')"
paulson@13797
   487
apply (erule leadsTo_induct)
paulson@13797
   488
(*Basis*)
paulson@13797
   489
apply (blast dest: ensuresD)
paulson@13797
   490
(*Trans*)
paulson@13797
   491
apply clarify
paulson@13797
   492
apply (rule_tac x = "Ba Un Bb" in exI)
paulson@13797
   493
apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
paulson@13797
   494
(*Union*)
paulson@13797
   495
apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
paulson@13797
   496
apply (rule_tac x = "UN A:S. f A" in exI)
paulson@13797
   497
apply (auto intro: leadsTo_UN)
paulson@13797
   498
(*Blast_tac says PROOF FAILED*)
paulson@13797
   499
apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B" 
paulson@13797
   500
       in constrains_UN [THEN constrains_weaken])
paulson@13797
   501
apply (auto ); 
paulson@13797
   502
done
paulson@13797
   503
paulson@13797
   504
paulson@13797
   505
(*Misra's property W5*)
paulson@13797
   506
lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)"
paulson@13797
   507
apply (cut_tac F = F in wlt_leadsTo [THEN leadsTo_123], clarify)
paulson@13797
   508
apply (subgoal_tac "Ba = wlt F B")
paulson@13797
   509
prefer 2 apply (blast dest: leadsTo_eq_subset_wlt [THEN iffD1], clarify)
paulson@13797
   510
apply (simp add: wlt_increasing Un_absorb2)
paulson@13797
   511
done
paulson@13797
   512
paulson@13797
   513
paulson@13797
   514
(*** Completion: Binary and General Finite versions ***)
paulson@13797
   515
paulson@13797
   516
lemma completion_lemma :
paulson@13797
   517
     "[| W = wlt F (B' Un C);      
paulson@13797
   518
       F : A leadsTo (A' Un C);  F : A' co (A' Un C);    
paulson@13797
   519
       F : B leadsTo (B' Un C);  F : B' co (B' Un C) |]  
paulson@13797
   520
    ==> F : (A Int B) leadsTo ((A' Int B') Un C)"
paulson@13797
   521
apply (subgoal_tac "F : (W-C) co (W Un B' Un C) ")
paulson@13797
   522
 prefer 2
paulson@13797
   523
 apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un, 
paulson@13797
   524
                                         THEN constrains_weaken])
paulson@13797
   525
apply (subgoal_tac "F : (W-C) co W")
paulson@13797
   526
 prefer 2
paulson@13797
   527
 apply (simp add: wlt_increasing Un_assoc Un_absorb2)
paulson@13797
   528
apply (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C) ")
paulson@13797
   529
 prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
paulson@13797
   530
(** LEVEL 6 **)
paulson@13797
   531
apply (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C) ")
paulson@13797
   532
 prefer 2
paulson@13797
   533
 apply (rule leadsTo_Un_duplicate2)
paulson@13797
   534
 apply (blast intro: leadsTo_Un_Un wlt_leadsTo
paulson@13797
   535
                         [THEN psp2, THEN leadsTo_weaken] leadsTo_refl)
paulson@13797
   536
apply (drule leadsTo_Diff)
paulson@13797
   537
apply (blast intro: subset_imp_leadsTo)
paulson@13797
   538
apply (subgoal_tac "A Int B <= A Int W")
paulson@13797
   539
 prefer 2
paulson@13797
   540
 apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
paulson@13797
   541
apply (blast intro: leadsTo_Trans subset_imp_leadsTo)
paulson@13797
   542
done
paulson@13797
   543
paulson@13797
   544
lemmas completion = completion_lemma [OF refl]
paulson@13797
   545
paulson@13797
   546
lemma finite_completion_lemma:
paulson@13797
   547
     "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) -->   
paulson@13797
   548
                   (ALL i:I. F : (A' i) co (A' i Un C)) -->  
paulson@13797
   549
                   F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
paulson@13797
   550
apply (erule finite_induct, auto)
paulson@13797
   551
apply (rule completion)
paulson@13797
   552
   prefer 4
paulson@13797
   553
   apply (simp only: INT_simps [symmetric])
paulson@13797
   554
   apply (rule constrains_INT, auto)
paulson@13797
   555
done
paulson@13797
   556
paulson@13797
   557
lemma finite_completion: 
paulson@13797
   558
     "[| finite I;   
paulson@13797
   559
         !!i. i:I ==> F : (A i) leadsTo (A' i Un C);  
paulson@13797
   560
         !!i. i:I ==> F : (A' i) co (A' i Un C) |]    
paulson@13797
   561
      ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
paulson@13797
   562
by (blast intro: finite_completion_lemma [THEN mp, THEN mp])
paulson@13797
   563
paulson@13797
   564
lemma stable_completion: 
paulson@13797
   565
     "[| F : A leadsTo A';  F : stable A';    
paulson@13797
   566
         F : B leadsTo B';  F : stable B' |]  
paulson@13797
   567
    ==> F : (A Int B) leadsTo (A' Int B')"
paulson@13797
   568
apply (unfold stable_def)
paulson@13797
   569
apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R])
paulson@13797
   570
apply (force+)
paulson@13797
   571
done
paulson@13797
   572
paulson@13797
   573
lemma finite_stable_completion: 
paulson@13797
   574
     "[| finite I;   
paulson@13797
   575
         !!i. i:I ==> F : (A i) leadsTo (A' i);  
paulson@13797
   576
         !!i. i:I ==> F : stable (A' i) |]    
paulson@13797
   577
      ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"
paulson@13797
   578
apply (unfold stable_def)
paulson@13797
   579
apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R])
paulson@13797
   580
apply (simp_all (no_asm_simp))
paulson@13797
   581
apply blast+
paulson@13797
   582
done
paulson@9685
   583
paulson@4776
   584
end