src/HOL/TLA/Inc/Inc.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58310 91ea607a34d8
child 60587 0318b43ee95c
permissions -rw-r--r--
modernized header uniformly as section;
wenzelm@41589
     1
(*  Title:      HOL/TLA/Inc/Inc.thy
wenzelm@41589
     2
    Author:     Stephan Merz, University of Munich
wenzelm@3807
     3
*)
wenzelm@3807
     4
wenzelm@58889
     5
section {* Lamport's "increment" example *}
wenzelm@17309
     6
wenzelm@17309
     7
theory Inc
wenzelm@17309
     8
imports TLA
wenzelm@17309
     9
begin
wenzelm@6255
    10
wenzelm@6255
    11
(* program counter as an enumeration type *)
blanchet@58310
    12
datatype pcount = a | b | g
wenzelm@3807
    13
wenzelm@47968
    14
axiomatization
wenzelm@3807
    15
  (* program variables *)
wenzelm@47968
    16
  x :: "nat stfun" and
wenzelm@47968
    17
  y :: "nat stfun" and
wenzelm@47968
    18
  sem :: "nat stfun" and
wenzelm@47968
    19
  pc1 :: "pcount stfun" and
wenzelm@47968
    20
  pc2 :: "pcount stfun" and
wenzelm@3807
    21
wenzelm@3807
    22
  (* names of actions and predicates *)
wenzelm@47968
    23
  M1 :: action and
wenzelm@47968
    24
  M2 :: action and
wenzelm@47968
    25
  N1 :: action and
wenzelm@47968
    26
  N2 :: action and
wenzelm@47968
    27
  alpha1 :: action and
wenzelm@47968
    28
  alpha2 :: action and
wenzelm@47968
    29
  beta1 :: action and
wenzelm@47968
    30
  beta2 :: action and
wenzelm@47968
    31
  gamma1 :: action and
wenzelm@47968
    32
  gamma2 :: action and
wenzelm@47968
    33
  InitPhi :: stpred and
wenzelm@47968
    34
  InitPsi :: stpred and
wenzelm@47968
    35
  PsiInv :: stpred and
wenzelm@47968
    36
  PsiInv1 :: stpred and
wenzelm@47968
    37
  PsiInv2 :: stpred and
wenzelm@47968
    38
  PsiInv3 :: stpred and
wenzelm@3807
    39
wenzelm@3807
    40
  (* temporal formulas *)
wenzelm@47968
    41
  Phi :: temporal and
wenzelm@17309
    42
  Psi :: temporal
wenzelm@47968
    43
where
wenzelm@3807
    44
  (* the "base" variables, required to compute enabledness predicates *)
wenzelm@47968
    45
  Inc_base:      "basevars (x, y, sem, pc1, pc2)" and
wenzelm@3807
    46
wenzelm@3807
    47
  (* definitions for high-level program *)
wenzelm@47968
    48
  InitPhi_def:   "InitPhi == PRED x = # 0 & y = # 0" and
wenzelm@47968
    49
  M1_def:        "M1      == ACT  x$ = Suc<$x> & y$ = $y" and
wenzelm@47968
    50
  M2_def:        "M2      == ACT  y$ = Suc<$y> & x$ = $x" and
wenzelm@17309
    51
  Phi_def:       "Phi     == TEMP Init InitPhi & [][M1 | M2]_(x,y)
wenzelm@47968
    52
                                 & WF(M1)_(x,y) & WF(M2)_(x,y)" and
wenzelm@3807
    53
wenzelm@3807
    54
  (* definitions for low-level program *)
wenzelm@17309
    55
  InitPsi_def:   "InitPsi == PRED pc1 = #a & pc2 = #a
wenzelm@47968
    56
                                 & x = # 0 & y = # 0 & sem = # 1" and
wenzelm@17309
    57
  alpha1_def:    "alpha1  == ACT  $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
wenzelm@47968
    58
                                 & unchanged(x,y,pc2)" and
wenzelm@17309
    59
  alpha2_def:    "alpha2  == ACT  $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
wenzelm@47968
    60
                                 & unchanged(x,y,pc1)" and
wenzelm@17309
    61
  beta1_def:     "beta1   == ACT  $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
wenzelm@47968
    62
                                 & unchanged(y,sem,pc2)" and
wenzelm@17309
    63
  beta2_def:     "beta2   == ACT  $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
wenzelm@47968
    64
                                 & unchanged(x,sem,pc1)" and
wenzelm@17309
    65
  gamma1_def:    "gamma1  == ACT  $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
wenzelm@47968
    66
                                 & unchanged(x,y,pc2)" and
wenzelm@17309
    67
  gamma2_def:    "gamma2  == ACT  $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
wenzelm@47968
    68
                                 & unchanged(x,y,pc1)" and
wenzelm@47968
    69
  N1_def:        "N1      == ACT  (alpha1 | beta1 | gamma1)" and
wenzelm@47968
    70
  N2_def:        "N2      == ACT  (alpha2 | beta2 | gamma2)" and
wenzelm@17309
    71
  Psi_def:       "Psi     == TEMP Init InitPsi
wenzelm@6255
    72
                               & [][N1 | N2]_(x,y,sem,pc1,pc2)
wenzelm@6255
    73
                               & SF(N1)_(x,y,sem,pc1,pc2)
wenzelm@47968
    74
                               & SF(N2)_(x,y,sem,pc1,pc2)" and
wenzelm@3807
    75
wenzelm@47968
    76
  PsiInv1_def:  "PsiInv1  == PRED sem = # 1 & pc1 = #a & pc2 = #a" and
wenzelm@47968
    77
  PsiInv2_def:  "PsiInv2  == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)" and
wenzelm@47968
    78
  PsiInv3_def:  "PsiInv3  == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)" and
wenzelm@17309
    79
  PsiInv_def:   "PsiInv   == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
wenzelm@17309
    80
wenzelm@21624
    81
wenzelm@21624
    82
lemmas PsiInv_defs = PsiInv_def PsiInv1_def PsiInv2_def PsiInv3_def
wenzelm@21624
    83
lemmas Psi_defs = Psi_def InitPsi_def N1_def N2_def alpha1_def alpha2_def
wenzelm@21624
    84
  beta1_def beta2_def gamma1_def gamma2_def
wenzelm@21624
    85
wenzelm@21624
    86
wenzelm@21624
    87
(*** Invariant proof for Psi: "manual" proof proves individual lemmas ***)
wenzelm@21624
    88
wenzelm@21624
    89
lemma PsiInv_Init: "|- InitPsi --> PsiInv"
wenzelm@21624
    90
  by (auto simp: InitPsi_def PsiInv_defs)
wenzelm@21624
    91
wenzelm@21624
    92
lemma PsiInv_alpha1: "|- alpha1 & $PsiInv --> PsiInv$"
wenzelm@21624
    93
  by (auto simp: alpha1_def PsiInv_defs)
wenzelm@21624
    94
wenzelm@21624
    95
lemma PsiInv_alpha2: "|- alpha2 & $PsiInv --> PsiInv$"
wenzelm@21624
    96
  by (auto simp: alpha2_def PsiInv_defs)
wenzelm@21624
    97
wenzelm@21624
    98
lemma PsiInv_beta1: "|- beta1 & $PsiInv --> PsiInv$"
wenzelm@21624
    99
  by (auto simp: beta1_def PsiInv_defs)
wenzelm@21624
   100
wenzelm@21624
   101
lemma PsiInv_beta2: "|- beta2 & $PsiInv --> PsiInv$"
wenzelm@21624
   102
  by (auto simp: beta2_def PsiInv_defs)
wenzelm@21624
   103
wenzelm@21624
   104
lemma PsiInv_gamma1: "|- gamma1 & $PsiInv --> PsiInv$"
wenzelm@21624
   105
  by (auto simp: gamma1_def PsiInv_defs)
wenzelm@21624
   106
wenzelm@21624
   107
lemma PsiInv_gamma2: "|- gamma2 & $PsiInv --> PsiInv$"
wenzelm@21624
   108
  by (auto simp: gamma2_def PsiInv_defs)
wenzelm@21624
   109
wenzelm@21624
   110
lemma PsiInv_stutter: "|- unchanged (x,y,sem,pc1,pc2) & $PsiInv --> PsiInv$"
wenzelm@21624
   111
  by (auto simp: PsiInv_defs)
wenzelm@21624
   112
wenzelm@21624
   113
lemma PsiInv: "|- Psi --> []PsiInv"
wenzelm@42769
   114
  apply (invariant simp: Psi_def)
wenzelm@21624
   115
   apply (force simp: PsiInv_Init [try_rewrite] Init_def)
wenzelm@21624
   116
  apply (auto intro: PsiInv_alpha1 [try_rewrite] PsiInv_alpha2 [try_rewrite]
wenzelm@21624
   117
    PsiInv_beta1 [try_rewrite] PsiInv_beta2 [try_rewrite] PsiInv_gamma1 [try_rewrite]
wenzelm@21624
   118
    PsiInv_gamma2 [try_rewrite] PsiInv_stutter [try_rewrite]
wenzelm@21624
   119
    simp add: square_def N1_def N2_def)
wenzelm@21624
   120
  done
wenzelm@21624
   121
wenzelm@21624
   122
(* Automatic proof works too, but it make take a while on a slow machine.
wenzelm@21624
   123
   More realistic examples require user guidance anyway.
wenzelm@21624
   124
*)
wenzelm@21624
   125
wenzelm@21624
   126
lemma "|- Psi --> []PsiInv"
wenzelm@42769
   127
  by (auto_invariant simp: PsiInv_defs Psi_defs)
wenzelm@21624
   128
wenzelm@21624
   129
wenzelm@21624
   130
(**** Step simulation ****)
wenzelm@21624
   131
wenzelm@21624
   132
lemma Init_sim: "|- Psi --> Init InitPhi"
wenzelm@21624
   133
  by (auto simp: InitPhi_def Psi_def InitPsi_def Init_def)
wenzelm@21624
   134
wenzelm@21624
   135
lemma Step_sim: "|- Psi --> [][M1 | M2]_(x,y)"
wenzelm@21624
   136
  by (auto simp: square_def M1_def M2_def Psi_defs elim!: STL4E [temp_use])
wenzelm@21624
   137
wenzelm@21624
   138
wenzelm@21624
   139
(**** Proof of fairness ****)
wenzelm@21624
   140
wenzelm@21624
   141
(*
wenzelm@21624
   142
   The goal is to prove Fair_M1 far below, which asserts
wenzelm@21624
   143
         |- Psi --> WF(M1)_(x,y)
wenzelm@21624
   144
   (the other fairness condition is symmetrical).
wenzelm@21624
   145
wenzelm@21624
   146
   The strategy is to use WF2 (with beta1 as the helpful action). Proving its
wenzelm@21624
   147
   temporal premise needs two auxiliary lemmas:
wenzelm@21624
   148
   1. Stuck_at_b: control can only proceed at pc1 = b by executing beta1
wenzelm@21624
   149
   2. N1_live: the first component will eventually reach b
wenzelm@21624
   150
wenzelm@21624
   151
   Lemma 1 is easy, lemma 2 relies on the invariant, the strong fairness
wenzelm@21624
   152
   of the semaphore, and needs auxiliary lemmas that ensure that the second
wenzelm@21624
   153
   component will eventually release the semaphore. Most of the proofs of
wenzelm@21624
   154
   the auxiliary lemmas are very similar.
wenzelm@21624
   155
*)
wenzelm@21624
   156
wenzelm@21624
   157
lemma Stuck_at_b: "|- [][(N1 | N2) & ~ beta1]_(x,y,sem,pc1,pc2) --> stable(pc1 = #b)"
wenzelm@21624
   158
  by (auto elim!: Stable squareE simp: Psi_defs)
wenzelm@21624
   159
wenzelm@21624
   160
lemma N1_enabled_at_g: "|- pc1 = #g --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
wenzelm@21624
   161
  apply clarsimp
wenzelm@21624
   162
  apply (rule_tac F = gamma1 in enabled_mono)
wenzelm@42785
   163
   apply (enabled Inc_base)
wenzelm@21624
   164
  apply (force simp: gamma1_def)
wenzelm@21624
   165
  apply (force simp: angle_def gamma1_def N1_def)
wenzelm@21624
   166
  done
wenzelm@21624
   167
wenzelm@21624
   168
lemma g1_leadsto_a1:
wenzelm@21624
   169
  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N1)_(x,y,sem,pc1,pc2) & []#True  
wenzelm@21624
   170
    --> (pc1 = #g ~> pc1 = #a)"
wenzelm@21624
   171
  apply (rule SF1)
wenzelm@21624
   172
    apply (tactic
wenzelm@51717
   173
      {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
wenzelm@21624
   174
   apply (tactic
wenzelm@51717
   175
      {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
wenzelm@21624
   176
  (* reduce |- []A --> <>Enabled B  to  |- A --> Enabled B *)
wenzelm@21624
   177
  apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
wenzelm@21624
   178
    dest!: STL2_gen [temp_use] simp: Init_def)
wenzelm@21624
   179
  done
wenzelm@21624
   180
wenzelm@21624
   181
(* symmetrical for N2, and similar for beta2 *)
wenzelm@21624
   182
lemma N2_enabled_at_g: "|- pc2 = #g --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
wenzelm@21624
   183
  apply clarsimp
wenzelm@21624
   184
  apply (rule_tac F = gamma2 in enabled_mono)
wenzelm@42785
   185
  apply (enabled Inc_base)
wenzelm@21624
   186
   apply (force simp: gamma2_def)
wenzelm@21624
   187
  apply (force simp: angle_def gamma2_def N2_def)
wenzelm@21624
   188
  done
wenzelm@21624
   189
wenzelm@21624
   190
lemma g2_leadsto_a2:
wenzelm@21624
   191
  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
wenzelm@21624
   192
    --> (pc2 = #g ~> pc2 = #a)"
wenzelm@21624
   193
  apply (rule SF1)
wenzelm@51717
   194
  apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
wenzelm@51717
   195
  apply (tactic {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs})
wenzelm@21624
   196
    [] [] 1 *})
wenzelm@21624
   197
  apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_g [temp_use]
wenzelm@21624
   198
    dest!: STL2_gen [temp_use] simp add: Init_def)
wenzelm@21624
   199
  done
wenzelm@21624
   200
wenzelm@21624
   201
lemma N2_enabled_at_b: "|- pc2 = #b --> Enabled (<N2>_(x,y,sem,pc1,pc2))"
wenzelm@21624
   202
  apply clarsimp
wenzelm@21624
   203
  apply (rule_tac F = beta2 in enabled_mono)
wenzelm@42785
   204
   apply (enabled Inc_base)
wenzelm@21624
   205
   apply (force simp: beta2_def)
wenzelm@21624
   206
  apply (force simp: angle_def beta2_def N2_def)
wenzelm@21624
   207
  done
wenzelm@21624
   208
wenzelm@21624
   209
lemma b2_leadsto_g2:
wenzelm@21624
   210
  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
wenzelm@21624
   211
    --> (pc2 = #b ~> pc2 = #g)"
wenzelm@21624
   212
  apply (rule SF1)
wenzelm@21624
   213
    apply (tactic
wenzelm@51717
   214
      {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
wenzelm@21624
   215
   apply (tactic
wenzelm@51717
   216
     {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
wenzelm@21624
   217
  apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_b [temp_use]
wenzelm@21624
   218
    dest!: STL2_gen [temp_use] simp: Init_def)
wenzelm@21624
   219
  done
wenzelm@21624
   220
wenzelm@21624
   221
(* Combine above lemmas: the second component will eventually reach pc2 = a *)
wenzelm@21624
   222
lemma N2_leadsto_a:
wenzelm@21624
   223
  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True  
wenzelm@21624
   224
    --> (pc2 = #a | pc2 = #b | pc2 = #g ~> pc2 = #a)"
wenzelm@21624
   225
  apply (auto intro!: LatticeDisjunctionIntro [temp_use])
wenzelm@21624
   226
    apply (rule LatticeReflexivity [temp_use])
wenzelm@21624
   227
   apply (rule LatticeTransitivity [temp_use])
wenzelm@21624
   228
  apply (auto intro!: b2_leadsto_g2 [temp_use] g2_leadsto_a2 [temp_use])
wenzelm@21624
   229
  done
wenzelm@21624
   230
wenzelm@21624
   231
(* Get rid of disjunction on the left-hand side of ~> above. *)
wenzelm@21624
   232
lemma N2_live:
wenzelm@21624
   233
  "|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2)  
wenzelm@21624
   234
    --> <>(pc2 = #a)"
wenzelm@21624
   235
  apply (auto simp: Init_defs intro!: N2_leadsto_a [temp_use, THEN [2] leadsto_init [temp_use]])
wenzelm@21624
   236
  apply (case_tac "pc2 (st1 sigma)")
wenzelm@21624
   237
    apply auto
wenzelm@21624
   238
  done
wenzelm@21624
   239
wenzelm@21624
   240
(* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
wenzelm@21624
   241
wenzelm@21624
   242
lemma N1_enabled_at_both_a:
wenzelm@21624
   243
  "|- pc2 = #a & (PsiInv & pc1 = #a) --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
wenzelm@21624
   244
  apply clarsimp
wenzelm@21624
   245
  apply (rule_tac F = alpha1 in enabled_mono)
wenzelm@42785
   246
  apply (enabled Inc_base)
wenzelm@21624
   247
   apply (force simp: alpha1_def PsiInv_defs)
wenzelm@21624
   248
  apply (force simp: angle_def alpha1_def N1_def)
wenzelm@21624
   249
  done
wenzelm@21624
   250
wenzelm@21624
   251
lemma a1_leadsto_b1:
wenzelm@21624
   252
  "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))       
wenzelm@21624
   253
         & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
wenzelm@21624
   254
         --> (pc1 = #a ~> pc1 = #b)"
wenzelm@21624
   255
  apply (rule SF1)
wenzelm@51717
   256
  apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
wenzelm@21624
   257
  apply (tactic
wenzelm@51717
   258
    {* action_simp_tac (@{context} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1 *})
wenzelm@21624
   259
  apply (clarsimp intro!: N1_enabled_at_both_a [THEN DmdImpl [temp_use]])
wenzelm@21624
   260
  apply (auto intro!: BoxDmd2_simple [temp_use] N2_live [temp_use]
wenzelm@21624
   261
    simp: split_box_conj more_temp_simps)
wenzelm@21624
   262
  done
wenzelm@21624
   263
wenzelm@21624
   264
(* Combine the leadsto properties for N1: it will arrive at pc1 = b *)
wenzelm@21624
   265
wenzelm@21624
   266
lemma N1_leadsto_b: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))              
wenzelm@21624
   267
         & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
wenzelm@21624
   268
         --> (pc1 = #b | pc1 = #g | pc1 = #a ~> pc1 = #b)"
wenzelm@21624
   269
  apply (auto intro!: LatticeDisjunctionIntro [temp_use])
wenzelm@21624
   270
    apply (rule LatticeReflexivity [temp_use])
wenzelm@21624
   271
   apply (rule LatticeTransitivity [temp_use])
wenzelm@21624
   272
    apply (auto intro!: a1_leadsto_b1 [temp_use] g1_leadsto_a1 [temp_use]
wenzelm@21624
   273
      simp: split_box_conj)
wenzelm@21624
   274
  done
wenzelm@21624
   275
wenzelm@21624
   276
lemma N1_live: "|- []($PsiInv & [(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2))              
wenzelm@21624
   277
         & SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)   
wenzelm@21624
   278
         --> <>(pc1 = #b)"
wenzelm@21624
   279
  apply (auto simp: Init_defs intro!: N1_leadsto_b [temp_use, THEN [2] leadsto_init [temp_use]])
wenzelm@21624
   280
  apply (case_tac "pc1 (st1 sigma)")
wenzelm@21624
   281
    apply auto
wenzelm@21624
   282
  done
wenzelm@21624
   283
wenzelm@21624
   284
lemma N1_enabled_at_b: "|- pc1 = #b --> Enabled (<N1>_(x,y,sem,pc1,pc2))"
wenzelm@21624
   285
  apply clarsimp
wenzelm@21624
   286
  apply (rule_tac F = beta1 in enabled_mono)
wenzelm@42785
   287
   apply (enabled Inc_base)
wenzelm@21624
   288
   apply (force simp: beta1_def)
wenzelm@21624
   289
  apply (force simp: angle_def beta1_def N1_def)
wenzelm@21624
   290
  done
wenzelm@21624
   291
wenzelm@21624
   292
(* Now assemble the bits and pieces to prove that Psi is fair. *)
wenzelm@21624
   293
wenzelm@21624
   294
lemma Fair_M1_lemma: "|- []($PsiInv & [(N1 | N2)]_(x,y,sem,pc1,pc2))    
wenzelm@21624
   295
         & SF(N1)_(x,y,sem,pc1,pc2) & []SF(N2)_(x,y,sem,pc1,pc2)   
wenzelm@21624
   296
         --> SF(M1)_(x,y)"
wenzelm@21624
   297
  apply (rule_tac B = beta1 and P = "PRED pc1 = #b" in SF2)
wenzelm@21624
   298
   (* action premises *)
wenzelm@21624
   299
     apply (force simp: angle_def M1_def beta1_def)
wenzelm@21624
   300
  apply (force simp: angle_def Psi_defs)
wenzelm@21624
   301
  apply (force elim!: N1_enabled_at_b [temp_use])
wenzelm@21624
   302
    (* temporal premise: use previous lemmas and simple TL *)
wenzelm@21624
   303
  apply (force intro!: DmdStable [temp_use] N1_live [temp_use] Stuck_at_b [temp_use]
wenzelm@21624
   304
    elim: STL4E [temp_use] simp: square_def)
wenzelm@21624
   305
  done
wenzelm@21624
   306
wenzelm@21624
   307
lemma Fair_M1: "|- Psi --> WF(M1)_(x,y)"
wenzelm@21624
   308
  by (auto intro!: SFImplWF [temp_use] Fair_M1_lemma [temp_use] PsiInv [temp_use]
wenzelm@21624
   309
    simp: Psi_def split_box_conj [temp_use] more_temp_simps)
wenzelm@17309
   310
wenzelm@3807
   311
end