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