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