Theory Graph

chapter ‹Case Study: Single and Multi-Mutator Garbage Collection Algorithms›

section ‹Formalization of the Memory›

theory Graph imports Main begin

datatype node = Black | White

type_synonym nodes = "node list"
type_synonym edge = "nat × nat"
type_synonym edges = "edge list"

consts Roots :: "nat set"

definition Proper_Roots :: "nodes  bool" where
  "Proper_Roots M  Roots{}  Roots  {i. i<length M}"

definition Proper_Edges :: "(nodes × edges)  bool" where
  "Proper_Edges  (λ(M,E). i<length E. fst(E!i)<length M  snd(E!i)<length M)"

definition BtoW :: "(edge × nodes)  bool" where
  "BtoW  (λ(e,M). (M!fst e)=Black  (M!snd e)Black)"

definition Blacks :: "nodes  nat set" where
  "Blacks M  {i. i<length M  M!i=Black}"

definition Reach :: "edges  nat set" where
  "Reach E  {x. (path. 1<length path  path!(length path - 1)Roots  x=path!0
               (i<length path - 1. (j<length E. E!j=(path!(i+1), path!i))))
               xRoots}"

text‹Reach: the set of reachable nodes is the set of Roots together with the
nodes reachable from some Root by a path represented by a list of
  nodes (at least two since we traverse at least one edge), where two
consecutive nodes correspond to an edge in E.›

subsection ‹Proofs about Graphs›

lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def
declare Graph_defs [simp]

subsubsection‹Graph 1›

lemma Graph1_aux [rule_format]:
  " RootsBlacks M; i<length E. ¬BtoW(E!i,M)
   1< length path  (path!(length path - 1))Roots 
  (i<length path - 1. (j. j < length E  E!j=(path!(Suc i), path!i)))
   M!(path!0) = Black"
apply(induct_tac "path")
 apply force
apply clarify
apply simp
apply(case_tac "list")
 apply force
apply simp
apply(rename_tac lista)
apply(rotate_tac -2)
apply(erule_tac x = "0" in all_dupE)
apply simp
apply clarify
apply(erule allE , erule (1) notE impE)
apply simp
apply(erule mp)
apply(case_tac "lista")
 apply force
apply simp
apply(erule mp)
apply clarify
apply(erule_tac x = "Suc i" in allE)
apply force
done

lemma Graph1:
  "RootsBlacks M; Proper_Edges(M, E); i<length E. ¬BtoW(E!i,M) 
   Reach EBlacks M"
apply (unfold Reach_def)
apply simp
apply clarify
apply(erule disjE)
 apply clarify
 apply(rule conjI)
  apply(subgoal_tac "0< length path - Suc 0")
   apply(erule allE , erule (1) notE impE)
   apply force
  apply simp
 apply(rule Graph1_aux)
apply auto
done

subsubsection‹Graph 2›

lemma Ex_first_occurrence [rule_format]:
  "P (n::nat)  (m. P m  (i. i<m  ¬ P i))"
apply(rule nat_less_induct)
apply clarify
apply(case_tac "m. m<n  ¬ P m")
apply auto
done

lemma Compl_lemma: "(n::nat)l  (m. ml  n=l - m)"
apply(rule_tac x = "l - n" in exI)
apply arith
done

lemma Ex_last_occurrence:
  "P (n::nat); nl  (m. P (l - m)  (i. i<m  ¬P (l - i)))"
apply(drule Compl_lemma)
apply clarify
apply(erule Ex_first_occurrence)
done

lemma Graph2:
  "T  Reach E; R<length E  T  Reach (E[R:=(fst(E!R), T)])"
apply (unfold Reach_def)
apply clarify
apply simp
apply(case_tac "z<length path. fst(E!R)path!z")
 apply(rule_tac x = "path" in exI)
 apply simp
 apply clarify
 apply(erule allE , erule (1) notE impE)
 apply clarify
 apply(rule_tac x = "j" in exI)
 apply(case_tac "j=R")
  apply(erule_tac x = "Suc i" in allE)
  apply simp
 apply (force simp add:nth_list_update)
apply simp
apply(erule exE)
apply(subgoal_tac "z  length path - Suc 0")
 prefer 2 apply arith
apply(drule_tac P = "λm. m<length path  fst(E!R)=path!m" in Ex_last_occurrence)
 apply assumption
apply clarify
apply simp
apply(rule_tac x = "(path!0)#(drop (length path - Suc m) path)" in exI)
apply simp
apply(case_tac "length path - (length path - Suc m)")
 apply arith
apply simp
apply(subgoal_tac "(length path - Suc m) + nat  length path")
 prefer 2 apply arith
apply(subgoal_tac "length path - Suc m + nat = length path - Suc 0")
 prefer 2 apply arith
apply clarify
apply(case_tac "i")
 apply(force simp add: nth_list_update)
apply simp
apply(subgoal_tac "(length path - Suc m) + nata  length path")
 prefer 2 apply arith
apply(subgoal_tac "(length path - Suc m) + (Suc nata)  length path")
 prefer 2 apply arith
apply simp
apply(erule_tac x = "length path - Suc m + nata" in allE)
apply simp
apply clarify
apply(rule_tac x = "j" in exI)
apply(case_tac "R=j")
 prefer 2 apply force
apply simp
apply(drule_tac t = "path ! (length path - Suc m)" in sym)
apply simp
apply(case_tac " length path - Suc 0 < m")
 apply(subgoal_tac "(length path - Suc m)=0")
  prefer 2 apply arith
 apply(simp del: diff_is_0_eq)
 apply(subgoal_tac "Suc natanat")
 prefer 2 apply arith
 apply(drule_tac n = "Suc nata" in Compl_lemma)
 apply clarify
 subgoal using [[linarith_split_limit = 0]] by force
apply(drule leI)
apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
 apply(erule_tac x = "m - (Suc nata)" in allE)
 apply(case_tac "m")
  apply simp
 apply simp
apply simp
done


subsubsection‹Graph 3›

declare min.absorb1 [simp] min.absorb2 [simp]

lemma Graph3:
  " TReach E; R<length E   Reach(E[R:=(fst(E!R),T)])  Reach E"
apply (unfold Reach_def)
apply clarify
apply simp
apply(case_tac "i<length path - 1. (fst(E!R),T)=(path!(Suc i),path!i)")
― ‹the changed edge is part of the path›
 apply(erule exE)
 apply(drule_tac P = "λi. i<length path - 1  (fst(E!R),T)=(path!Suc i,path!i)" in Ex_first_occurrence)
 apply clarify
 apply(erule disjE)
― ‹T is NOT a root›
  apply clarify
  apply(rule_tac x = "(take m path)@patha" in exI)
  apply(subgoal_tac "¬(length pathm)")
   prefer 2 apply arith
  apply(simp)
  apply(rule conjI)
   apply(subgoal_tac "¬(m + length patha - 1 < m)")
    prefer 2 apply arith
   apply(simp add: nth_append)
  apply(rule conjI)
   apply(case_tac "m")
    apply force
   apply(case_tac "path")
    apply force
   apply force
  apply clarify
  apply(case_tac "Suc im")
   apply(erule_tac x = "i" in allE)
   apply simp
   apply clarify
   apply(rule_tac x = "j" in exI)
   apply(case_tac "Suc i<m")
    apply(simp add: nth_append)
    apply(case_tac "R=j")
     apply(simp add: nth_list_update)
     apply(case_tac "i=m")
      apply force
     apply(erule_tac x = "i" in allE)
     apply force
    apply(force simp add: nth_list_update)
   apply(simp add: nth_append)
   apply(subgoal_tac "i=m - 1")
    prefer 2 apply arith
   apply(case_tac "R=j")
    apply(erule_tac x = "m - 1" in allE)
    apply(simp add: nth_list_update)
   apply(force simp add: nth_list_update)
  apply(simp add: nth_append)
  apply(rotate_tac -4)
  apply(erule_tac x = "i - m" in allE)
  apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
    prefer 2 apply arith
   apply simp
― ‹T is a root›
 apply(case_tac "m=0")
  apply force
 apply(rule_tac x = "take (Suc m) path" in exI)
 apply(subgoal_tac "¬(length pathSuc m)" )
  prefer 2 apply arith
 apply clarsimp
 apply(erule_tac x = "i" in allE)
 apply simp
 apply clarify
 apply(case_tac "R=j")
  apply(force simp add: nth_list_update)
 apply(force simp add: nth_list_update)
― ‹the changed edge is not part of the path›
apply(rule_tac x = "path" in exI)
apply simp
apply clarify
apply(erule_tac x = "i" in allE)
apply clarify
apply(case_tac "R=j")
 apply(erule_tac x = "i" in allE)
 apply simp
apply(force simp add: nth_list_update)
done

subsubsection‹Graph 4›

lemma Graph4:
  "T  Reach E; RootsBlacks M; Ilength E; T<length M; R<length E;
  i<I. ¬BtoW(E!i,M); R<I; M!fst(E!R)=Black; M!TBlack 
  (r. Ir  r<length E  BtoW(E[R:=(fst(E!R),T)]!r,M))"
apply (unfold Reach_def)
apply simp
apply(erule disjE)
 prefer 2 apply force
apply clarify
― ‹there exist a black node in the path to T›
apply(case_tac "m<length path. M!(path!m)=Black")
 apply(erule exE)
 apply(drule_tac P = "λm. m<length path  M!(path!m)=Black" in Ex_first_occurrence)
 apply clarify
 apply(case_tac "ma")
  apply force
 apply simp
 apply(case_tac "length path")
  apply force
 apply simp
 apply(erule_tac P = "λi. i < nata  P i" and x = "nat" for P in allE)
 apply simp
 apply clarify
 apply(erule_tac P = "λi. i < Suc nat  P i" and x = "nat" for P in allE)
 apply simp
 apply(case_tac "j<I")
  apply(erule_tac x = "j" in allE)
  apply force
 apply(rule_tac x = "j" in exI)
 apply(force  simp add: nth_list_update)
apply simp
apply(rotate_tac -1)
apply(erule_tac x = "length path - 1" in allE)
apply(case_tac "length path")
 apply force
apply force
done

declare min.absorb1 [simp del] min.absorb2 [simp del]

subsubsection ‹Graph 5›

lemma Graph5:
  " T  Reach E ; Roots  Blacks M; i<R. ¬BtoW(E!i,M); T<length M;
    R<length E; M!fst(E!R)=Black; M!snd(E!R)=Black; M!T  Black
    (r. R<r  r<length E  BtoW(E[R:=(fst(E!R),T)]!r,M))"
apply (unfold Reach_def)
apply simp
apply(erule disjE)
 prefer 2 apply force
apply clarify
― ‹there exist a black node in the path to T›
apply(case_tac "m<length path. M!(path!m)=Black")
 apply(erule exE)
 apply(drule_tac P = "λm. m<length path  M!(path!m)=Black" in Ex_first_occurrence)
 apply clarify
 apply(case_tac "ma")
  apply force
 apply simp
 apply(case_tac "length path")
  apply force
 apply simp
 apply(erule_tac P = "λi. i < nata  P i" and x = "nat" for P in allE)
 apply simp
 apply clarify
 apply(erule_tac P = "λi. i < Suc nat  P i" and x = "nat" for P in allE)
 apply simp
 apply(case_tac "jR")
  apply(drule le_imp_less_or_eq [of _ R])
  apply(erule disjE)
   apply(erule allE , erule (1) notE impE)
   apply force
  apply force
 apply(rule_tac x = "j" in exI)
 apply(force  simp add: nth_list_update)
apply simp
apply(rotate_tac -1)
apply(erule_tac x = "length path - 1" in allE)
apply(case_tac "length path")
 apply force
apply force
done

subsubsection ‹Other lemmas about graphs›

lemma Graph6:
 "Proper_Edges(M,E); R<length E ; T<length M  Proper_Edges(M,E[R:=(fst(E!R),T)])"
apply (unfold Proper_Edges_def)
 apply(force  simp add: nth_list_update)
done

lemma Graph7:
 "Proper_Edges(M,E)  Proper_Edges(M[T:=a],E)"
apply (unfold Proper_Edges_def)
apply force
done

lemma Graph8:
 "Proper_Roots(M)  Proper_Roots(M[T:=a])"
apply (unfold Proper_Roots_def)
apply force
done

text‹Some specific lemmata for the verification of garbage collection algorithms.›

lemma Graph9: "j<length M  Blacks MBlacks (M[j := Black])"
apply (unfold Blacks_def)
 apply(force simp add: nth_list_update)
done

lemma Graph10 [rule_format (no_asm)]: "i. M!i=a M[i:=a]=M"
apply(induct_tac "M")
apply auto
apply(case_tac "i")
apply auto
done

lemma Graph11 [rule_format (no_asm)]:
  " M!jBlack;j<length M  Blacks M  Blacks (M[j := Black])"
apply (unfold Blacks_def)
apply(rule psubsetI)
 apply(force simp add: nth_list_update)
apply safe
apply(erule_tac c = "j" in equalityCE)
apply auto
done

lemma Graph12: "aBlacks M;j<length M  aBlacks (M[j := Black])"
apply (unfold Blacks_def)
apply(force simp add: nth_list_update)
done

lemma Graph13: "a Blacks M;j<length M  a  Blacks (M[j := Black])"
apply (unfold Blacks_def)
apply(erule psubset_subset_trans)
apply(force simp add: nth_list_update)
done

declare Graph_defs [simp del]

end