Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Hoare_Parallel/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 12 kB

Quelle Graph.thy Sprache: Isabelle

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

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.