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