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
```