src/HOL/UNITY/Simple/Reachability.thy
author haftmann
Sun Nov 18 18:07:51 2018 +0000 (8 months ago)
changeset 69313 b021008c5397
parent 67613 ce654b0e6d69
permissions -rw-r--r--
removed legacy input syntax
wenzelm@37936
     1
(*  Title:      HOL/UNITY/Simple/Reachability.thy
paulson@11195
     2
    Author:     Tanja Vos, Cambridge University Computer Laboratory
paulson@11195
     3
    Copyright   2000  University of Cambridge
paulson@11195
     4
wenzelm@32960
     5
Reachability in Graphs.
paulson@11195
     6
wenzelm@32960
     7
From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2
wenzelm@32960
     8
and 11.3.
paulson@11195
     9
*)
paulson@11195
    10
berghofe@26826
    11
theory Reachability imports "../Detects" Reach begin
paulson@11195
    12
wenzelm@42463
    13
type_synonym edge = "vertex * vertex"
paulson@11195
    14
paulson@11195
    15
record state =
paulson@13785
    16
  reach :: "vertex => bool"
paulson@13785
    17
  nmsg  :: "edge => nat"
paulson@11195
    18
berghofe@23767
    19
consts root :: "vertex"
paulson@13785
    20
       E :: "edge set"
paulson@13785
    21
       V :: "vertex set"
paulson@11195
    22
berghofe@23767
    23
inductive_set REACHABLE :: "edge set"
berghofe@23767
    24
  where
berghofe@23767
    25
    base: "v \<in> V ==> ((v,v) \<in> REACHABLE)"
berghofe@23767
    26
  | step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)"
paulson@11195
    27
haftmann@35416
    28
definition reachable :: "vertex => state set" where
paulson@11195
    29
  "reachable p == {s. reach s p}"
paulson@11195
    30
haftmann@35416
    31
definition nmsg_eq :: "nat => edge  => state set" where
paulson@11195
    32
  "nmsg_eq k == %e. {s. nmsg s e = k}"
paulson@11195
    33
haftmann@35416
    34
definition nmsg_gt :: "nat => edge  => state set" where
paulson@11195
    35
  "nmsg_gt k  == %e. {s. k < nmsg s e}"
paulson@11195
    36
haftmann@35416
    37
definition nmsg_gte :: "nat => edge => state set" where
paulson@13806
    38
  "nmsg_gte k == %e. {s. k \<le> nmsg s e}"
paulson@11195
    39
haftmann@35416
    40
definition nmsg_lte  :: "nat => edge => state set" where
paulson@13806
    41
  "nmsg_lte k  == %e. {s. nmsg s e \<le> k}"
paulson@11195
    42
haftmann@35416
    43
definition final :: "state set" where
paulson@13806
    44
  "final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter> 
haftmann@69313
    45
            (\<Inter>((nmsg_eq 0) ` E))"
paulson@11195
    46
wenzelm@45827
    47
axiomatization
wenzelm@45827
    48
where
wenzelm@45827
    49
    Graph1: "root \<in> V" and
paulson@13785
    50
wenzelm@45827
    51
    Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)" and
paulson@13785
    52
wenzelm@45827
    53
    MA1:  "F \<in> Always (reachable root)" and
paulson@13785
    54
wenzelm@45827
    55
    MA2:  "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})" and
paulson@13785
    56
wenzelm@45827
    57
    MA3:  "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))" and
paulson@13785
    58
paulson@13806
    59
    MA4:  "(v,w) \<in> E ==> 
wenzelm@45827
    60
           F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))" and
paulson@13785
    61
paulson@13806
    62
    MA5:  "[|v \<in> V; w \<in> V|] 
wenzelm@45827
    63
           ==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))" and
paulson@13785
    64
wenzelm@45827
    65
    MA6:  "[|v \<in> V|] ==> F \<in> Stable (reachable v)" and
paulson@13785
    66
wenzelm@45827
    67
    MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))" and
paulson@13785
    68
paulson@13806
    69
    MA7:  "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)"
paulson@13785
    70
paulson@13785
    71
wenzelm@45605
    72
lemmas E_imp_in_V_L = Graph2 [THEN conjunct1]
wenzelm@45605
    73
lemmas E_imp_in_V_R = Graph2 [THEN conjunct2]
paulson@13785
    74
paulson@13785
    75
lemma lemma2:
paulson@13806
    76
     "(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v"
paulson@13785
    77
apply (rule MA7 [THEN PSP_Stable, THEN LeadsTo_weaken_L])
paulson@13785
    78
apply (rule_tac [3] MA6)
paulson@13785
    79
apply (auto simp add: E_imp_in_V_L E_imp_in_V_R)
paulson@13785
    80
done
paulson@13785
    81
paulson@13806
    82
lemma Induction_base: "(v,w) \<in> E ==> F \<in> reachable v LeadsTo reachable w"
paulson@13785
    83
apply (rule MA4 [THEN Always_LeadsTo_weaken])
paulson@13785
    84
apply (rule_tac [2] lemma2)
paulson@13785
    85
apply (auto simp add: nmsg_eq_def nmsg_gt_def)
paulson@13785
    86
done
paulson@13785
    87
paulson@13785
    88
lemma REACHABLE_LeadsTo_reachable:
paulson@13806
    89
     "(v,w) \<in> REACHABLE ==> F \<in> reachable v LeadsTo reachable w"
paulson@13785
    90
apply (erule REACHABLE.induct)
paulson@13785
    91
apply (rule subset_imp_LeadsTo, blast)
paulson@13785
    92
apply (blast intro: LeadsTo_Trans Induction_base)
paulson@13785
    93
done
paulson@13785
    94
paulson@13806
    95
lemma Detects_part1: "F \<in> {s. (root,v) \<in> REACHABLE} LeadsTo reachable v"
paulson@13785
    96
apply (rule single_LeadsTo_I)
nipkow@63648
    97
apply (simp split: if_split_asm)
paulson@13785
    98
apply (rule MA1 [THEN Always_LeadsToI])
paulson@13785
    99
apply (erule REACHABLE_LeadsTo_reachable [THEN LeadsTo_weaken_L], auto)
paulson@13785
   100
done
paulson@13785
   101
paulson@13785
   102
paulson@13785
   103
lemma Reachability_Detected: 
paulson@13806
   104
     "v \<in> V ==> F \<in> (reachable v) Detects {s. (root,v) \<in> REACHABLE}"
paulson@13785
   105
apply (unfold Detects_def, auto)
paulson@13785
   106
 prefer 2 apply (blast intro: MA2 [THEN Always_weaken])
paulson@13785
   107
apply (rule Detects_part1 [THEN LeadsTo_weaken_L], blast)
paulson@13785
   108
done
paulson@13785
   109
paulson@13785
   110
paulson@13785
   111
lemma LeadsTo_Reachability:
paulson@13806
   112
     "v \<in> V ==> F \<in> UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE})"
paulson@13785
   113
by (erule Reachability_Detected [THEN Detects_Imp_LeadstoEQ])
paulson@13785
   114
paulson@13785
   115
paulson@13785
   116
(* ------------------------------------ *)
paulson@13785
   117
paulson@13785
   118
(* Some lemmas about <==> *)
paulson@13785
   119
paulson@13785
   120
lemma Eq_lemma1: 
paulson@13806
   121
     "(reachable v <==> {s. (root,v) \<in> REACHABLE}) =  
paulson@13806
   122
      {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
paulson@13806
   123
by (unfold Equality_def, blast)
paulson@13785
   124
paulson@11195
   125
paulson@13785
   126
lemma Eq_lemma2: 
paulson@13806
   127
     "(reachable v <==> (if (root,v) \<in> REACHABLE then UNIV else {})) =  
paulson@13806
   128
      {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
paulson@13806
   129
by (unfold Equality_def, auto)
paulson@13785
   130
paulson@13785
   131
(* ------------------------------------ *)
paulson@13785
   132
paulson@13785
   133
paulson@13785
   134
(* Some lemmas about final (I don't need all of them!)  *)
paulson@13785
   135
paulson@13785
   136
lemma final_lemma1: 
paulson@13806
   137
     "(\<Inter>v \<in> V. \<Inter>w \<in> V. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE)) &  
paulson@13806
   138
                              s \<in> nmsg_eq 0 (v,w)})  
paulson@13806
   139
      \<subseteq> final"
paulson@13785
   140
apply (unfold final_def Equality_def, auto)
paulson@13785
   141
apply (frule E_imp_in_V_R)
paulson@13785
   142
apply (frule E_imp_in_V_L, blast)
paulson@13785
   143
done
paulson@13785
   144
paulson@13785
   145
lemma final_lemma2: 
paulson@13806
   146
 "E\<noteq>{}  
paulson@13806
   147
  ==> (\<Inter>v \<in> V. \<Inter>e \<in> E. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}  
paulson@13806
   148
                           \<inter> nmsg_eq 0 e)    \<subseteq>  final"
paulson@13785
   149
apply (unfold final_def Equality_def)
nipkow@63648
   150
apply (auto split!: if_split)
paulson@13785
   151
apply (frule E_imp_in_V_L, blast)
paulson@13785
   152
done
paulson@13785
   153
paulson@13785
   154
lemma final_lemma3:
paulson@13806
   155
     "E\<noteq>{}  
paulson@13806
   156
      ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.  
paulson@13806
   157
           (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)  
paulson@13806
   158
          \<subseteq> final"
paulson@13785
   159
apply (frule final_lemma2)
paulson@13785
   160
apply (simp (no_asm_use) add: Eq_lemma2)
paulson@13785
   161
done
paulson@13785
   162
paulson@11195
   163
paulson@13785
   164
lemma final_lemma4:
paulson@13806
   165
     "E\<noteq>{}  
paulson@13806
   166
      ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.  
paulson@13806
   167
           {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))} \<inter> nmsg_eq 0 e)  
paulson@13785
   168
          = final"
paulson@13785
   169
apply (rule subset_antisym)
paulson@13785
   170
apply (erule final_lemma2)
paulson@13785
   171
apply (unfold final_def Equality_def, blast)
paulson@13785
   172
done
paulson@13785
   173
paulson@13785
   174
lemma final_lemma5:
paulson@13806
   175
     "E\<noteq>{}  
paulson@13806
   176
      ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.  
paulson@13806
   177
           ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)  
paulson@13785
   178
          = final"
paulson@13785
   179
apply (frule final_lemma4)
paulson@13785
   180
apply (simp (no_asm_use) add: Eq_lemma2)
paulson@13785
   181
done
paulson@13785
   182
paulson@11195
   183
paulson@13785
   184
lemma final_lemma6:
paulson@13806
   185
     "(\<Inter>v \<in> V. \<Inter>w \<in> V.  
paulson@13806
   186
       (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 (v,w))  
paulson@13806
   187
      \<subseteq> final"
paulson@13785
   188
apply (simp (no_asm) add: Eq_lemma2 Int_def)
paulson@13785
   189
apply (rule final_lemma1)
paulson@13785
   190
done
paulson@13785
   191
paulson@13785
   192
paulson@13785
   193
lemma final_lemma7: 
paulson@13785
   194
     "final =  
paulson@13806
   195
      (\<Inter>v \<in> V. \<Inter>w \<in> V.  
paulson@13806
   196
       ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
paulson@13806
   197
       (-{s. (v,w) \<in> E} \<union> (nmsg_eq 0 (v,w))))"
paulson@13785
   198
apply (unfold final_def)
paulson@13785
   199
apply (rule subset_antisym, blast)
nipkow@63648
   200
apply (auto split: if_split_asm)
paulson@13785
   201
apply (blast dest: E_imp_in_V_L E_imp_in_V_R)+
paulson@13785
   202
done
paulson@13785
   203
paulson@13785
   204
(* ------------------------------------ *)
paulson@11195
   205
paulson@13785
   206
paulson@13785
   207
(* ------------------------------------ *)
paulson@13785
   208
paulson@13785
   209
(* Stability theorems *)
paulson@13785
   210
lemma not_REACHABLE_imp_Stable_not_reachable:
paulson@13806
   211
     "[| v \<in> V; (root,v) \<notin> REACHABLE |] ==> F \<in> Stable (- reachable v)"
paulson@13785
   212
apply (drule MA2 [THEN AlwaysD], auto)
paulson@13785
   213
done
paulson@13785
   214
paulson@13785
   215
lemma Stable_reachable_EQ_R:
paulson@13806
   216
     "v \<in> V ==> F \<in> Stable (reachable v <==> {s. (root,v) \<in> REACHABLE})"
paulson@13785
   217
apply (simp (no_asm) add: Equality_def Eq_lemma2)
paulson@13785
   218
apply (blast intro: MA6 not_REACHABLE_imp_Stable_not_reachable)
paulson@13785
   219
done
paulson@13785
   220
paulson@13785
   221
paulson@13785
   222
lemma lemma4: 
paulson@13806
   223
     "((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter> 
paulson@13806
   224
       (- nmsg_gt 0 (v,w) \<union> A))  
paulson@13806
   225
      \<subseteq> A \<union> nmsg_eq 0 (v,w)"
paulson@13785
   226
apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
paulson@13785
   227
done
paulson@13785
   228
paulson@13785
   229
paulson@13785
   230
lemma lemma5: 
paulson@13806
   231
     "reachable v \<inter> nmsg_eq 0 (v,w) =  
paulson@13806
   232
      ((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter> 
paulson@13806
   233
       (reachable v \<inter> nmsg_lte 0 (v,w)))"
paulson@13806
   234
by (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
paulson@13785
   235
paulson@13785
   236
lemma lemma6: 
paulson@13806
   237
     "- nmsg_gt 0 (v,w) \<union> reachable v \<subseteq> nmsg_eq 0 (v,w) \<union> reachable v"
paulson@13785
   238
apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
paulson@13785
   239
done
paulson@11195
   240
paulson@13785
   241
lemma Always_reachable_OR_nmsg_0:
paulson@13806
   242
     "[|v \<in> V; w \<in> V|] ==> F \<in> Always (reachable v \<union> nmsg_eq 0 (v,w))"
paulson@13785
   243
apply (rule Always_Int_I [OF MA5 MA3, THEN Always_weaken])
paulson@13785
   244
apply (rule_tac [5] lemma4, auto)
paulson@13785
   245
done
paulson@13785
   246
paulson@13785
   247
lemma Stable_reachable_AND_nmsg_0:
paulson@13806
   248
     "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (reachable v \<inter> nmsg_eq 0 (v,w))"
paulson@13785
   249
apply (subst lemma5)
paulson@13785
   250
apply (blast intro: MA5 Always_imp_Stable [THEN Stable_Int] MA6b)
paulson@13785
   251
done
paulson@13785
   252
paulson@13785
   253
lemma Stable_nmsg_0_OR_reachable:
paulson@13806
   254
     "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (nmsg_eq 0 (v,w) \<union> reachable v)"
paulson@13785
   255
by (blast intro!: Always_weaken [THEN Always_imp_Stable] lemma6 MA3)
paulson@11195
   256
paulson@13785
   257
lemma not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0:
paulson@13806
   258
     "[| v \<in> V; w \<in> V; (root,v) \<notin> REACHABLE |]  
paulson@13806
   259
      ==> F \<in> Stable (- reachable v \<inter> nmsg_eq 0 (v,w))"
paulson@13785
   260
apply (rule Stable_Int [OF MA2 [THEN Always_imp_Stable] 
paulson@13785
   261
                           Stable_nmsg_0_OR_reachable, 
paulson@13785
   262
            THEN Stable_eq])
paulson@13785
   263
   prefer 4 apply blast
paulson@13785
   264
apply auto
paulson@13785
   265
done
paulson@13785
   266
paulson@13785
   267
lemma Stable_reachable_EQ_R_AND_nmsg_0:
paulson@13806
   268
     "[| v \<in> V; w \<in> V |]  
paulson@13806
   269
      ==> F \<in> Stable ((reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
paulson@13785
   270
                      nmsg_eq 0 (v,w))"
paulson@13785
   271
by (simp add: Equality_def Eq_lemma2  Stable_reachable_AND_nmsg_0
paulson@13785
   272
              not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0)
paulson@13785
   273
paulson@13785
   274
paulson@13785
   275
paulson@13785
   276
(* ------------------------------------ *)
paulson@13785
   277
paulson@13785
   278
paulson@13785
   279
(* LeadsTo final predicate (Exercise 11.2 page 274) *)
paulson@13785
   280
paulson@13806
   281
lemma UNIV_lemma: "UNIV \<subseteq> (\<Inter>v \<in> V. UNIV)"
paulson@13785
   282
by blast
paulson@11195
   283
paulson@13785
   284
lemmas UNIV_LeadsTo_completion = 
paulson@13785
   285
    LeadsTo_weaken_L [OF Finite_stable_completion UNIV_lemma]
paulson@13785
   286
paulson@13806
   287
lemma LeadsTo_final_E_empty: "E={} ==> F \<in> UNIV LeadsTo final"
paulson@13785
   288
apply (unfold final_def, simp)
paulson@13785
   289
apply (rule UNIV_LeadsTo_completion)
paulson@13785
   290
  apply safe
paulson@13785
   291
 apply (erule LeadsTo_Reachability [simplified])
paulson@13785
   292
apply (drule Stable_reachable_EQ_R, simp)
paulson@13785
   293
done
paulson@13785
   294
paulson@13785
   295
paulson@13785
   296
lemma Leadsto_reachability_AND_nmsg_0:
paulson@13806
   297
     "[| v \<in> V; w \<in> V |]  
paulson@13806
   298
      ==> F \<in> UNIV LeadsTo  
wenzelm@67613
   299
             ((reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 (v,w))"
paulson@13785
   300
apply (rule LeadsTo_Reachability [THEN LeadsTo_Trans], blast)
paulson@13785
   301
apply (subgoal_tac
wenzelm@32960
   302
         "F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
paulson@13806
   303
              UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> 
paulson@13785
   304
              nmsg_eq 0 (v,w) ")
paulson@13785
   305
apply simp
paulson@13785
   306
apply (rule PSP_Stable2)
paulson@13785
   307
apply (rule MA7)
paulson@13785
   308
apply (rule_tac [3] Stable_reachable_EQ_R, auto)
paulson@13785
   309
done
paulson@13785
   310
paulson@13806
   311
lemma LeadsTo_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> UNIV LeadsTo final"
paulson@13785
   312
apply (rule LeadsTo_weaken_L [OF LeadsTo_weaken_R UNIV_lemma])
paulson@13785
   313
apply (rule_tac [2] final_lemma6)
paulson@13785
   314
apply (rule Finite_stable_completion)
paulson@13785
   315
  apply blast
paulson@13785
   316
 apply (rule UNIV_LeadsTo_completion)
paulson@13785
   317
   apply (blast intro: Stable_INT Stable_reachable_EQ_R_AND_nmsg_0
paulson@13785
   318
                    Leadsto_reachability_AND_nmsg_0)+
paulson@13785
   319
done
paulson@11195
   320
paulson@13806
   321
lemma LeadsTo_final: "F \<in> UNIV LeadsTo final"
wenzelm@46911
   322
apply (cases "E={}")
paulson@13806
   323
 apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
paulson@13785
   324
apply (rule LeadsTo_final_E_empty, auto)
paulson@13785
   325
done
paulson@13785
   326
paulson@13785
   327
(* ------------------------------------ *)
paulson@13785
   328
paulson@13785
   329
(* Stability of final (Exercise 11.2 page 274) *)
paulson@13785
   330
paulson@13806
   331
lemma Stable_final_E_empty: "E={} ==> F \<in> Stable final"
paulson@13785
   332
apply (unfold final_def, simp)
paulson@13785
   333
apply (rule Stable_INT)
paulson@13785
   334
apply (drule Stable_reachable_EQ_R, simp)
paulson@13785
   335
done
paulson@13785
   336
paulson@11195
   337
paulson@13806
   338
lemma Stable_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> Stable final"
paulson@13785
   339
apply (subst final_lemma7)
paulson@13785
   340
apply (rule Stable_INT)
paulson@13785
   341
apply (rule Stable_INT)
paulson@13785
   342
apply (simp (no_asm) add: Eq_lemma2)
paulson@13785
   343
apply safe
paulson@13785
   344
apply (rule Stable_eq)
paulson@13806
   345
apply (subgoal_tac [2]
paulson@13806
   346
     "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) = 
paulson@13806
   347
      ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))")
wenzelm@46008
   348
prefer 2 apply blast
paulson@13785
   349
prefer 2 apply blast 
paulson@13785
   350
apply (rule Stable_reachable_EQ_R_AND_nmsg_0
paulson@13785
   351
            [simplified Eq_lemma2 Collect_const])
paulson@13785
   352
apply (blast, blast)
paulson@13785
   353
apply (rule Stable_eq)
paulson@13785
   354
 apply (rule Stable_reachable_EQ_R [simplified Eq_lemma2 Collect_const])
paulson@13785
   355
 apply simp
paulson@13785
   356
apply (subgoal_tac 
paulson@13806
   357
        "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) }) = 
wenzelm@67613
   358
         ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter>
paulson@13806
   359
              (- {} \<union> nmsg_eq 0 (v,w)))")
paulson@13785
   360
apply blast+
paulson@13785
   361
done
paulson@13785
   362
paulson@13806
   363
lemma Stable_final: "F \<in> Stable final"
wenzelm@46911
   364
apply (cases "E={}")
paulson@13806
   365
 prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
paulson@13785
   366
apply (blast intro: Stable_final_E_empty)
paulson@13785
   367
done
paulson@11195
   368
paulson@11195
   369
end
paulson@11195
   370