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