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