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