chapter \<open>Case Study: Single and Multi-Mutator Garbage Collection Algorithms\<close>
section \<open>Formalization of the Memory\<close>
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
definition Proper_Edges :: "(nodes \ edges) \ bool" where
"Proper_Edges \ (\(M,E). \i snd(E!i)
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 M!i=Black}"
definition Reach :: "edges \ nat set" where
"Reach E \ {x. (\path. 1 path!(length path - 1)\Roots \ x=path!0
\<and> (\<forall>i<length path - 1. (\<exists>j<length E. E!j=(path!(i+1), path!i))))
\<or> x\<in>Roots}"
text\<open>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.\<close>
subsection \<open>Proofs about Graphs\<close>
lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def
declare Graph_defs [simp]
subsubsection\<open>Graph 1\<close>
lemma Graph1_aux [rule_format]:
"\ Roots\Blacks M; \iBtoW(E!i,M)\
\<Longrightarrow> 1< length path \<longrightarrow> (path!(length path - 1))\<in>Roots \<longrightarrow>
(\<forall>i<length path - 1. (\<exists>j. j < length E \<and> E!j=(path!(Suc i), path!i)))
\<longrightarrow> 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:
"\Roots\Blacks M; Proper_Edges(M, E); \iBtoW(E!i,M) \
\<Longrightarrow> Reach E\<subseteq>Blacks 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\<open>Graph 2\<close>
lemma Ex_first_occurrence [rule_format]:
"P (n::nat) \ (\m. P m \ (\i. i \ P i))"
apply(rule nat_less_induct)
apply clarify
apply(case_tac "\m. m \ P m")
apply auto
done
lemma Compl_lemma: "(n::nat)\l \ (\m. m\l \ n=l - m)"
apply(rule_tac x = "l - n" in exI)
apply arith
done
lemma Ex_last_occurrence:
"\P (n::nat); n\l\ \ (\m. P (l - m) \ (\i. i \P (l - i)))"
apply(drule Compl_lemma)
apply clarify
apply(erule Ex_first_occurrence)
done
lemma Graph2:
"\T \ Reach E; R \ T \ Reach (E[R:=(fst(E!R), T)])"
apply (unfold Reach_def)
apply clarify
apply simp
apply(case_tac "\zpath!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 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 nata\nat")
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\<open>Graph 3\<close>
declare min.absorb1 [simp] min.absorb2 [simp]
lemma Graph3:
"\ T\Reach E; R \ Reach(E[R:=(fst(E!R),T)]) \ Reach E"
apply (unfold Reach_def)
apply clarify
apply simp
apply(case_tac "\i
\<comment> \<open>the changed edge is part of the path\<close>
apply(erule exE)
apply(drule_tac P = "\i. i (fst(E!R),T)=(path!Suc i,path!i)" in Ex_first_occurrence)
apply clarify
apply(erule disjE)
\<comment> \<open>T is NOT a root\<close>
apply clarify
apply(rule_tac x = "(take m path)@patha" in exI)
apply(subgoal_tac "\(length path\m)")
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 i\m")
apply(erule_tac x = "i" in allE)
apply simp
apply clarify
apply(rule_tac x = "j" in exI)
apply(case_tac "Suc i)
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
\<comment> \<open>T is a root\<close>
apply(case_tac "m=0")
apply force
apply(rule_tac x = "take (Suc m) path" in exI)
apply(subgoal_tac "\(length path\Suc 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)
\<comment> \<open>the changed edge is not part of the path\<close>
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\<open>Graph 4\<close>
lemma Graph4:
"\T \ Reach E; Roots\Blacks M; I\length E; T
\<forall>i<I. \<not>BtoW(E!i,M); R<I; M!fst(E!R)=Black; M!T\<noteq>Black\<rbrakk> \<Longrightarrow>
(\<exists>r. I\<le>r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))"
apply (unfold Reach_def)
apply simp
apply(erule disjE)
prefer 2 apply force
apply clarify
\<comment> \<open>there exist a black node in the path to T\<close>
apply(case_tac "\m
apply(erule exE)
apply(drule_tac P = "\m. m 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)
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 \<open>Graph 5\<close>
lemma Graph5:
"\ T \ Reach E ; Roots \ Blacks M; \iBtoW(E!i,M); T
R<length E; M!fst(E!R)=Black; M!snd(E!R)=Black; M!T \<noteq> Black\<rbrakk>
\<Longrightarrow> (\<exists>r. R<r \<and> r<length E \<and> BtoW(E[R:=(fst(E!R),T)]!r,M))"
apply (unfold Reach_def)
apply simp
apply(erule disjE)
prefer 2 apply force
apply clarify
\<comment> \<open>there exist a black node in the path to T\<close>
apply(case_tac "\m
apply(erule exE)
apply(drule_tac P = "\m. m 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\R")
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 \<open>Other lemmas about graphs\<close>
lemma Graph6:
"\Proper_Edges(M,E); R \ 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\<open>Some specific lemmata for the verification of garbage collection algorithms.\<close>
lemma Graph9: "j Blacks M\Blacks (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!j\Black;j \ 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: "\a\Blacks M;j \ a\Blacks (M[j := Black])"
apply (unfold Blacks_def)
apply(force simp add: nth_list_update)
done
lemma Graph13: "\a\ Blacks M;j \ 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
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
