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