src/HOL/Hoare_Parallel/Graph.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62042 6c6ccf573479
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@59189
     1
chapter \<open>Case Study: Single and Multi-Mutator Garbage Collection Algorithms\<close>
prensani@13020
     2
wenzelm@59189
     3
section \<open>Formalization of the Memory\<close>
prensani@13020
     4
haftmann@16417
     5
theory Graph imports Main begin
prensani@13020
     6
blanchet@58310
     7
datatype node = Black | White
prensani@13020
     8
wenzelm@42174
     9
type_synonym nodes = "node list"
wenzelm@42174
    10
type_synonym edge = "nat \<times> nat"
wenzelm@42174
    11
type_synonym edges = "edge list"
prensani@13020
    12
prensani@13020
    13
consts Roots :: "nat set"
prensani@13020
    14
haftmann@35416
    15
definition Proper_Roots :: "nodes \<Rightarrow> bool" where
prensani@13020
    16
  "Proper_Roots M \<equiv> Roots\<noteq>{} \<and> Roots \<subseteq> {i. i<length M}"
prensani@13020
    17
haftmann@35416
    18
definition Proper_Edges :: "(nodes \<times> edges) \<Rightarrow> bool" where
prensani@13020
    19
  "Proper_Edges \<equiv> (\<lambda>(M,E). \<forall>i<length E. fst(E!i)<length M \<and> snd(E!i)<length M)"
prensani@13020
    20
haftmann@35416
    21
definition BtoW :: "(edge \<times> nodes) \<Rightarrow> bool" where
prensani@13020
    22
  "BtoW \<equiv> (\<lambda>(e,M). (M!fst e)=Black \<and> (M!snd e)\<noteq>Black)"
prensani@13020
    23
haftmann@35416
    24
definition Blacks :: "nodes \<Rightarrow> nat set" where
prensani@13020
    25
  "Blacks M \<equiv> {i. i<length M \<and> M!i=Black}"
prensani@13020
    26
haftmann@35416
    27
definition Reach :: "edges \<Rightarrow> nat set" where
prensani@13020
    28
  "Reach E \<equiv> {x. (\<exists>path. 1<length path \<and> path!(length path - 1)\<in>Roots \<and> x=path!0
prensani@13020
    29
              \<and> (\<forall>i<length path - 1. (\<exists>j<length E. E!j=(path!(i+1), path!i))))
wenzelm@32960
    30
              \<or> x\<in>Roots}"
prensani@13020
    31
wenzelm@59189
    32
text\<open>Reach: the set of reachable nodes is the set of Roots together with the
prensani@13020
    33
nodes reachable from some Root by a path represented by a list of
prensani@13020
    34
  nodes (at least two since we traverse at least one edge), where two
wenzelm@59189
    35
consecutive nodes correspond to an edge in E.\<close>
prensani@13020
    36
wenzelm@59189
    37
subsection \<open>Proofs about Graphs\<close>
prensani@13020
    38
prensani@13020
    39
lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def
prensani@13020
    40
declare Graph_defs [simp]
prensani@13020
    41
wenzelm@59189
    42
subsubsection\<open>Graph 1\<close>
prensani@13020
    43
wenzelm@59189
    44
lemma Graph1_aux [rule_format]:
prensani@13020
    45
  "\<lbrakk> Roots\<subseteq>Blacks M; \<forall>i<length E. \<not>BtoW(E!i,M)\<rbrakk>
wenzelm@59189
    46
  \<Longrightarrow> 1< length path \<longrightarrow> (path!(length path - 1))\<in>Roots \<longrightarrow>
wenzelm@59189
    47
  (\<forall>i<length path - 1. (\<exists>j. j < length E \<and> E!j=(path!(Suc i), path!i)))
prensani@13020
    48
  \<longrightarrow> M!(path!0) = Black"
prensani@13020
    49
apply(induct_tac "path")
prensani@13020
    50
 apply force
prensani@13020
    51
apply clarify
prensani@13020
    52
apply simp
prensani@13020
    53
apply(case_tac "list")
prensani@13020
    54
 apply force
prensani@13020
    55
apply simp
blanchet@55417
    56
apply(rename_tac lista)
berghofe@13601
    57
apply(rotate_tac -2)
prensani@13020
    58
apply(erule_tac x = "0" in all_dupE)
prensani@13020
    59
apply simp
prensani@13020
    60
apply clarify
prensani@13020
    61
apply(erule allE , erule (1) notE impE)
prensani@13020
    62
apply simp
prensani@13020
    63
apply(erule mp)
prensani@13020
    64
apply(case_tac "lista")
prensani@13020
    65
 apply force
prensani@13020
    66
apply simp
prensani@13020
    67
apply(erule mp)
prensani@13020
    68
apply clarify
prensani@13020
    69
apply(erule_tac x = "Suc i" in allE)
prensani@13020
    70
apply force
prensani@13020
    71
done
prensani@13020
    72
wenzelm@59189
    73
lemma Graph1:
wenzelm@59189
    74
  "\<lbrakk>Roots\<subseteq>Blacks M; Proper_Edges(M, E); \<forall>i<length E. \<not>BtoW(E!i,M) \<rbrakk>
prensani@13020
    75
  \<Longrightarrow> Reach E\<subseteq>Blacks M"
prensani@13020
    76
apply (unfold Reach_def)
prensani@13020
    77
apply simp
prensani@13020
    78
apply clarify
prensani@13020
    79
apply(erule disjE)
prensani@13020
    80
 apply clarify
prensani@13020
    81
 apply(rule conjI)
prensani@13020
    82
  apply(subgoal_tac "0< length path - Suc 0")
prensani@13020
    83
   apply(erule allE , erule (1) notE impE)
prensani@13020
    84
   apply force
prensani@13020
    85
  apply simp
prensani@13020
    86
 apply(rule Graph1_aux)
prensani@13020
    87
apply auto
prensani@13020
    88
done
prensani@13020
    89
wenzelm@59189
    90
subsubsection\<open>Graph 2\<close>
prensani@13020
    91
wenzelm@59189
    92
lemma Ex_first_occurrence [rule_format]:
wenzelm@58860
    93
  "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))"
prensani@13020
    94
apply(rule nat_less_induct)
prensani@13020
    95
apply clarify
prensani@13020
    96
apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
prensani@13020
    97
apply auto
prensani@13020
    98
done
prensani@13020
    99
prensani@13020
   100
lemma Compl_lemma: "(n::nat)\<le>l \<Longrightarrow> (\<exists>m. m\<le>l \<and> n=l - m)"
prensani@13020
   101
apply(rule_tac x = "l - n" in exI)
prensani@13020
   102
apply arith
prensani@13020
   103
done
prensani@13020
   104
wenzelm@59189
   105
lemma Ex_last_occurrence:
prensani@13020
   106
  "\<lbrakk>P (n::nat); n\<le>l\<rbrakk> \<Longrightarrow> (\<exists>m. P (l - m) \<and> (\<forall>i. i<m \<longrightarrow> \<not>P (l - i)))"
prensani@13020
   107
apply(drule Compl_lemma)
prensani@13020
   108
apply clarify
prensani@13020
   109
apply(erule Ex_first_occurrence)
prensani@13020
   110
done
prensani@13020
   111
wenzelm@59189
   112
lemma Graph2:
prensani@13020
   113
  "\<lbrakk>T \<in> Reach E; R<length E\<rbrakk> \<Longrightarrow> T \<in> Reach (E[R:=(fst(E!R), T)])"
prensani@13020
   114
apply (unfold Reach_def)
prensani@13020
   115
apply clarify
prensani@13020
   116
apply simp
prensani@13020
   117
apply(case_tac "\<forall>z<length path. fst(E!R)\<noteq>path!z")
prensani@13020
   118
 apply(rule_tac x = "path" in exI)
prensani@13020
   119
 apply simp
prensani@13020
   120
 apply clarify
prensani@13020
   121
 apply(erule allE , erule (1) notE impE)
prensani@13020
   122
 apply clarify
prensani@13020
   123
 apply(rule_tac x = "j" in exI)
prensani@13020
   124
 apply(case_tac "j=R")
prensani@13020
   125
  apply(erule_tac x = "Suc i" in allE)
prensani@13020
   126
  apply simp
prensani@13020
   127
 apply (force simp add:nth_list_update)
prensani@13020
   128
apply simp
prensani@13020
   129
apply(erule exE)
prensani@13020
   130
apply(subgoal_tac "z \<le> length path - Suc 0")
prensani@13020
   131
 prefer 2 apply arith
prensani@13020
   132
apply(drule_tac P = "\<lambda>m. m<length path \<and> fst(E!R)=path!m" in Ex_last_occurrence)
prensani@13020
   133
 apply assumption
prensani@13020
   134
apply clarify
prensani@13020
   135
apply simp
prensani@13020
   136
apply(rule_tac x = "(path!0)#(drop (length path - Suc m) path)" in exI)
prensani@13020
   137
apply simp
prensani@13020
   138
apply(case_tac "length path - (length path - Suc m)")
prensani@13020
   139
 apply arith
prensani@13020
   140
apply simp
prensani@13020
   141
apply(subgoal_tac "(length path - Suc m) + nat \<le> length path")
prensani@13020
   142
 prefer 2 apply arith
prensani@13020
   143
apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0")
wenzelm@59189
   144
 prefer 2 apply arith
prensani@13020
   145
apply clarify
prensani@13020
   146
apply(case_tac "i")
prensani@13020
   147
 apply(force simp add: nth_list_update)
prensani@13020
   148
apply simp
prensani@13020
   149
apply(subgoal_tac "(length path - Suc m) + nata \<le> length path")
prensani@13020
   150
 prefer 2 apply arith
prensani@13020
   151
apply(subgoal_tac "(length path - Suc m) + (Suc nata) \<le> length path")
prensani@13020
   152
 prefer 2 apply arith
prensani@13020
   153
apply simp
prensani@13020
   154
apply(erule_tac x = "length path - Suc m + nata" in allE)
prensani@13020
   155
apply simp
prensani@13020
   156
apply clarify
prensani@13020
   157
apply(rule_tac x = "j" in exI)
prensani@13020
   158
apply(case_tac "R=j")
prensani@13020
   159
 prefer 2 apply force
prensani@13020
   160
apply simp
prensani@13020
   161
apply(drule_tac t = "path ! (length path - Suc m)" in sym)
prensani@13020
   162
apply simp
prensani@13020
   163
apply(case_tac " length path - Suc 0 < m")
prensani@13020
   164
 apply(subgoal_tac "(length path - Suc m)=0")
prensani@13020
   165
  prefer 2 apply arith
prensani@13020
   166
 apply(simp del: diff_is_0_eq)
prensani@13020
   167
 apply(subgoal_tac "Suc nata\<le>nat")
prensani@13020
   168
 prefer 2 apply arith
prensani@13020
   169
 apply(drule_tac n = "Suc nata" in Compl_lemma)
prensani@13020
   170
 apply clarify
haftmann@31082
   171
 using [[linarith_split_limit = 0]]
prensani@13020
   172
 apply force
haftmann@31082
   173
 using [[linarith_split_limit = 9]]
prensani@13020
   174
apply(drule leI)
prensani@13020
   175
apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
prensani@13020
   176
 apply(erule_tac x = "m - (Suc nata)" in allE)
prensani@13020
   177
 apply(case_tac "m")
prensani@13020
   178
  apply simp
prensani@13020
   179
 apply simp
berghofe@13601
   180
apply simp
prensani@13020
   181
done
prensani@13020
   182
webertj@20432
   183
wenzelm@59189
   184
subsubsection\<open>Graph 3\<close>
prensani@13020
   185
haftmann@54863
   186
declare min.absorb1 [simp] min.absorb2 [simp]
haftmann@32642
   187
wenzelm@59189
   188
lemma Graph3:
prensani@13020
   189
  "\<lbrakk> T\<in>Reach E; R<length E \<rbrakk> \<Longrightarrow> Reach(E[R:=(fst(E!R),T)]) \<subseteq> Reach E"
prensani@13020
   190
apply (unfold Reach_def)
prensani@13020
   191
apply clarify
prensani@13020
   192
apply simp
prensani@13020
   193
apply(case_tac "\<exists>i<length path - 1. (fst(E!R),T)=(path!(Suc i),path!i)")
wenzelm@62042
   194
\<comment>\<open>the changed edge is part of the path\<close>
prensani@13020
   195
 apply(erule exE)
prensani@13020
   196
 apply(drule_tac P = "\<lambda>i. i<length path - 1 \<and> (fst(E!R),T)=(path!Suc i,path!i)" in Ex_first_occurrence)
prensani@13020
   197
 apply clarify
prensani@13020
   198
 apply(erule disjE)
wenzelm@62042
   199
\<comment>\<open>T is NOT a root\<close>
prensani@13020
   200
  apply clarify
prensani@13020
   201
  apply(rule_tac x = "(take m path)@patha" in exI)
prensani@13020
   202
  apply(subgoal_tac "\<not>(length path\<le>m)")
prensani@13020
   203
   prefer 2 apply arith
nipkow@32442
   204
  apply(simp)
prensani@13020
   205
  apply(rule conjI)
prensani@13020
   206
   apply(subgoal_tac "\<not>(m + length patha - 1 < m)")
prensani@13020
   207
    prefer 2 apply arith
nipkow@32442
   208
   apply(simp add: nth_append)
prensani@13020
   209
  apply(rule conjI)
prensani@13020
   210
   apply(case_tac "m")
prensani@13020
   211
    apply force
prensani@13020
   212
   apply(case_tac "path")
prensani@13020
   213
    apply force
prensani@13020
   214
   apply force
prensani@13020
   215
  apply clarify
prensani@13020
   216
  apply(case_tac "Suc i\<le>m")
prensani@13020
   217
   apply(erule_tac x = "i" in allE)
prensani@13020
   218
   apply simp
prensani@13020
   219
   apply clarify
prensani@13020
   220
   apply(rule_tac x = "j" in exI)
prensani@13020
   221
   apply(case_tac "Suc i<m")
nipkow@22230
   222
    apply(simp add: nth_append)
prensani@13020
   223
    apply(case_tac "R=j")
prensani@13020
   224
     apply(simp add: nth_list_update)
prensani@13020
   225
     apply(case_tac "i=m")
prensani@13020
   226
      apply force
prensani@13020
   227
     apply(erule_tac x = "i" in allE)
prensani@13020
   228
     apply force
prensani@13020
   229
    apply(force simp add: nth_list_update)
nipkow@22230
   230
   apply(simp add: nth_append)
prensani@13020
   231
   apply(subgoal_tac "i=m - 1")
prensani@13020
   232
    prefer 2 apply arith
prensani@13020
   233
   apply(case_tac "R=j")
prensani@13020
   234
    apply(erule_tac x = "m - 1" in allE)
prensani@13020
   235
    apply(simp add: nth_list_update)
prensani@13020
   236
   apply(force simp add: nth_list_update)
nipkow@32442
   237
  apply(simp add: nth_append)
prensani@13020
   238
  apply(rotate_tac -4)
prensani@13020
   239
  apply(erule_tac x = "i - m" in allE)
prensani@13020
   240
  apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
prensani@13020
   241
    prefer 2 apply arith
prensani@13020
   242
   apply simp
wenzelm@62042
   243
\<comment>\<open>T is a root\<close>
prensani@13020
   244
 apply(case_tac "m=0")
prensani@13020
   245
  apply force
prensani@13020
   246
 apply(rule_tac x = "take (Suc m) path" in exI)
prensani@13020
   247
 apply(subgoal_tac "\<not>(length path\<le>Suc m)" )
prensani@13020
   248
  prefer 2 apply arith
nipkow@32442
   249
 apply clarsimp
prensani@13020
   250
 apply(erule_tac x = "i" in allE)
prensani@13020
   251
 apply simp
prensani@13020
   252
 apply clarify
prensani@13020
   253
 apply(case_tac "R=j")
prensani@13020
   254
  apply(force simp add: nth_list_update)
prensani@13020
   255
 apply(force simp add: nth_list_update)
wenzelm@62042
   256
\<comment>\<open>the changed edge is not part of the path\<close>
prensani@13020
   257
apply(rule_tac x = "path" in exI)
prensani@13020
   258
apply simp
prensani@13020
   259
apply clarify
prensani@13020
   260
apply(erule_tac x = "i" in allE)
prensani@13020
   261
apply clarify
prensani@13020
   262
apply(case_tac "R=j")
prensani@13020
   263
 apply(erule_tac x = "i" in allE)
prensani@13020
   264
 apply simp
prensani@13020
   265
apply(force simp add: nth_list_update)
prensani@13020
   266
done
prensani@13020
   267
wenzelm@59189
   268
subsubsection\<open>Graph 4\<close>
prensani@13020
   269
wenzelm@59189
   270
lemma Graph4:
wenzelm@59189
   271
  "\<lbrakk>T \<in> Reach E; Roots\<subseteq>Blacks M; I\<le>length E; T<length M; R<length E;
wenzelm@59189
   272
  \<forall>i<I. \<not>BtoW(E!i,M); R<I; M!fst(E!R)=Black; M!T\<noteq>Black\<rbrakk> \<Longrightarrow>
prensani@13020
   273
  (\<exists>r. I\<le>r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))"
prensani@13020
   274
apply (unfold Reach_def)
prensani@13020
   275
apply simp
prensani@13020
   276
apply(erule disjE)
prensani@13020
   277
 prefer 2 apply force
prensani@13020
   278
apply clarify
wenzelm@62042
   279
\<comment>\<open>there exist a black node in the path to T\<close>
prensani@13020
   280
apply(case_tac "\<exists>m<length path. M!(path!m)=Black")
prensani@13020
   281
 apply(erule exE)
prensani@13020
   282
 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence)
prensani@13020
   283
 apply clarify
prensani@13020
   284
 apply(case_tac "ma")
prensani@13020
   285
  apply force
prensani@13020
   286
 apply simp
prensani@13020
   287
 apply(case_tac "length path")
prensani@13020
   288
  apply force
prensani@13020
   289
 apply simp
wenzelm@59807
   290
 apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> P i" and x = "nat" for P in allE)
prensani@13020
   291
 apply simp
prensani@13020
   292
 apply clarify
wenzelm@59807
   293
 apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> P i" and x = "nat" for P in allE)
prensani@13020
   294
 apply simp
prensani@13020
   295
 apply(case_tac "j<I")
prensani@13020
   296
  apply(erule_tac x = "j" in allE)
prensani@13020
   297
  apply force
prensani@13020
   298
 apply(rule_tac x = "j" in exI)
prensani@13020
   299
 apply(force  simp add: nth_list_update)
prensani@13020
   300
apply simp
prensani@13020
   301
apply(rotate_tac -1)
prensani@13020
   302
apply(erule_tac x = "length path - 1" in allE)
prensani@13020
   303
apply(case_tac "length path")
prensani@13020
   304
 apply force
prensani@13020
   305
apply force
prensani@13020
   306
done
prensani@13020
   307
haftmann@54863
   308
declare min.absorb1 [simp del] min.absorb2 [simp del]
haftmann@32642
   309
wenzelm@59189
   310
subsubsection \<open>Graph 5\<close>
prensani@13020
   311
wenzelm@59189
   312
lemma Graph5:
wenzelm@59189
   313
  "\<lbrakk> T \<in> Reach E ; Roots \<subseteq> Blacks M; \<forall>i<R. \<not>BtoW(E!i,M); T<length M;
wenzelm@59189
   314
    R<length E; M!fst(E!R)=Black; M!snd(E!R)=Black; M!T \<noteq> Black\<rbrakk>
prensani@13020
   315
   \<Longrightarrow> (\<exists>r. R<r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))"
prensani@13020
   316
apply (unfold Reach_def)
prensani@13020
   317
apply simp
prensani@13020
   318
apply(erule disjE)
prensani@13020
   319
 prefer 2 apply force
prensani@13020
   320
apply clarify
wenzelm@62042
   321
\<comment>\<open>there exist a black node in the path to T\<close>
prensani@13020
   322
apply(case_tac "\<exists>m<length path. M!(path!m)=Black")
prensani@13020
   323
 apply(erule exE)
prensani@13020
   324
 apply(drule_tac P = "\<lambda>m. m<length path \<and> M!(path!m)=Black" in Ex_first_occurrence)
prensani@13020
   325
 apply clarify
prensani@13020
   326
 apply(case_tac "ma")
prensani@13020
   327
  apply force
prensani@13020
   328
 apply simp
prensani@13020
   329
 apply(case_tac "length path")
prensani@13020
   330
  apply force
prensani@13020
   331
 apply simp
wenzelm@59807
   332
 apply(erule_tac P = "\<lambda>i. i < nata \<longrightarrow> P i" and x = "nat" for P in allE)
prensani@13020
   333
 apply simp
prensani@13020
   334
 apply clarify
wenzelm@59807
   335
 apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> P i" and x = "nat" for P in allE)
prensani@13020
   336
 apply simp
prensani@13020
   337
 apply(case_tac "j\<le>R")
wenzelm@26316
   338
  apply(drule le_imp_less_or_eq [of _ R])
prensani@13020
   339
  apply(erule disjE)
prensani@13020
   340
   apply(erule allE , erule (1) notE impE)
prensani@13020
   341
   apply force
prensani@13020
   342
  apply force
prensani@13020
   343
 apply(rule_tac x = "j" in exI)
prensani@13020
   344
 apply(force  simp add: nth_list_update)
prensani@13020
   345
apply simp
prensani@13020
   346
apply(rotate_tac -1)
prensani@13020
   347
apply(erule_tac x = "length path - 1" in allE)
prensani@13020
   348
apply(case_tac "length path")
prensani@13020
   349
 apply force
prensani@13020
   350
apply force
prensani@13020
   351
done
prensani@13020
   352
wenzelm@59189
   353
subsubsection \<open>Other lemmas about graphs\<close>
prensani@13020
   354
wenzelm@59189
   355
lemma Graph6:
prensani@13020
   356
 "\<lbrakk>Proper_Edges(M,E); R<length E ; T<length M\<rbrakk> \<Longrightarrow> Proper_Edges(M,E[R:=(fst(E!R),T)])"
prensani@13020
   357
apply (unfold Proper_Edges_def)
prensani@13020
   358
 apply(force  simp add: nth_list_update)
prensani@13020
   359
done
prensani@13020
   360
wenzelm@59189
   361
lemma Graph7:
prensani@13020
   362
 "\<lbrakk>Proper_Edges(M,E)\<rbrakk> \<Longrightarrow> Proper_Edges(M[T:=a],E)"
prensani@13020
   363
apply (unfold Proper_Edges_def)
prensani@13020
   364
apply force
prensani@13020
   365
done
prensani@13020
   366
wenzelm@59189
   367
lemma Graph8:
prensani@13020
   368
 "\<lbrakk>Proper_Roots(M)\<rbrakk> \<Longrightarrow> Proper_Roots(M[T:=a])"
prensani@13020
   369
apply (unfold Proper_Roots_def)
prensani@13020
   370
apply force
prensani@13020
   371
done
prensani@13020
   372
wenzelm@59189
   373
text\<open>Some specific lemmata for the verification of garbage collection algorithms.\<close>
prensani@13020
   374
prensani@13020
   375
lemma Graph9: "j<length M \<Longrightarrow> Blacks M\<subseteq>Blacks (M[j := Black])"
prensani@13020
   376
apply (unfold Blacks_def)
prensani@13020
   377
 apply(force simp add: nth_list_update)
prensani@13020
   378
done
prensani@13020
   379
prensani@13020
   380
lemma Graph10 [rule_format (no_asm)]: "\<forall>i. M!i=a \<longrightarrow>M[i:=a]=M"
prensani@13020
   381
apply(induct_tac "M")
prensani@13020
   382
apply auto
prensani@13020
   383
apply(case_tac "i")
prensani@13020
   384
apply auto
prensani@13020
   385
done
prensani@13020
   386
wenzelm@59189
   387
lemma Graph11 [rule_format (no_asm)]:
prensani@13020
   388
  "\<lbrakk> M!j\<noteq>Black;j<length M\<rbrakk> \<Longrightarrow> Blacks M \<subset> Blacks (M[j := Black])"
prensani@13020
   389
apply (unfold Blacks_def)
prensani@13020
   390
apply(rule psubsetI)
prensani@13020
   391
 apply(force simp add: nth_list_update)
prensani@13020
   392
apply safe
prensani@13020
   393
apply(erule_tac c = "j" in equalityCE)
prensani@13020
   394
apply auto
prensani@13020
   395
done
prensani@13020
   396
prensani@13020
   397
lemma Graph12: "\<lbrakk>a\<subseteq>Blacks M;j<length M\<rbrakk> \<Longrightarrow> a\<subseteq>Blacks (M[j := Black])"
prensani@13020
   398
apply (unfold Blacks_def)
prensani@13020
   399
apply(force simp add: nth_list_update)
prensani@13020
   400
done
prensani@13020
   401
prensani@13020
   402
lemma Graph13: "\<lbrakk>a\<subset> Blacks M;j<length M\<rbrakk> \<Longrightarrow> a \<subset> Blacks (M[j := Black])"
prensani@13020
   403
apply (unfold Blacks_def)
prensani@13020
   404
apply(erule psubset_subset_trans)
prensani@13020
   405
apply(force simp add: nth_list_update)
prensani@13020
   406
done
prensani@13020
   407
prensani@13020
   408
declare Graph_defs [simp del]
prensani@13020
   409
prensani@13020
   410
end