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