--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Sat Dec 27 19:51:55 2014 +0100
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Sat Dec 27 20:32:06 2014 +0100
@@ -1,10 +1,10 @@
-section {* The Single Mutator Case *}
+section \<open>The Single Mutator Case\<close>
theory Gar_Coll imports Graph OG_Syntax begin
declare psubsetE [rule del]
-text {* Declaration of variables: *}
+text \<open>Declaration of variables:\<close>
record gar_coll_state =
M :: nodes
@@ -12,32 +12,32 @@
bc :: "nat set"
obc :: "nat set"
Ma :: nodes
- ind :: nat
+ ind :: nat
k :: nat
z :: bool
-subsection {* The Mutator *}
+subsection \<open>The Mutator\<close>
-text {* The mutator first redirects an arbitrary edge @{text "R"} from
+text \<open>The mutator first redirects an arbitrary edge @{text "R"} from
an arbitrary accessible node towards an arbitrary accessible node
-@{text "T"}. It then colors the new target @{text "T"} black.
+@{text "T"}. It then colors the new target @{text "T"} black.
-We declare the arbitrarily selected node and edge as constants:*}
+We declare the arbitrarily selected node and edge as constants:\<close>
consts R :: nat T :: nat
-text {* \noindent The following predicate states, given a list of
+text \<open>\noindent The following predicate states, given a list of
nodes @{text "m"} and a list of edges @{text "e"}, the conditions
under which the selected edge @{text "R"} and node @{text "T"} are
-valid: *}
+valid:\<close>
definition Mut_init :: "gar_coll_state \<Rightarrow> bool" where
"Mut_init \<equiv> \<guillemotleft> T \<in> Reach \<acute>E \<and> R < length \<acute>E \<and> T < length \<acute>M \<guillemotright>"
-text {* \noindent For the mutator we
+text \<open>\noindent For the mutator we
consider two modules, one for each action. An auxiliary variable
@{text "\<acute>z"} is set to false if the mutator has already redirected an
-edge but has not yet colored the new target. *}
+edge but has not yet colored the new target.\<close>
definition Redirect_Edge :: "gar_coll_state ann_com" where
"Redirect_Edge \<equiv> \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace> \<langle>\<acute>E:=\<acute>E[R:=(fst(\<acute>E!R), T)],, \<acute>z:= (\<not>\<acute>z)\<rangle>"
@@ -47,15 +47,15 @@
definition Mutator :: "gar_coll_state ann_com" where
"Mutator \<equiv>
- \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace>
- WHILE True INV \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace>
+ \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace>
+ WHILE True INV \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace>
DO Redirect_Edge ;; Color_Target OD"
-subsubsection {* Correctness of the mutator *}
+subsubsection \<open>Correctness of the mutator\<close>
lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def
-lemma Redirect_Edge:
+lemma Redirect_Edge:
"\<turnstile> Redirect_Edge pre(Color_Target)"
apply (unfold mutator_defs)
apply annhoare
@@ -70,7 +70,7 @@
apply(simp_all)
done
-lemma Mutator:
+lemma Mutator:
"\<turnstile> Mutator \<lbrace>False\<rbrace>"
apply(unfold Mutator_def)
apply annhoare
@@ -78,17 +78,17 @@
apply(simp add:mutator_defs)
done
-subsection {* The Collector *}
+subsection \<open>The Collector\<close>
-text {* \noindent A constant @{text "M_init"} is used to give @{text "\<acute>Ma"} a
+text \<open>\noindent A constant @{text "M_init"} is used to give @{text "\<acute>Ma"} a
suitable first value, defined as a list of nodes where only the @{text
-"Roots"} are black. *}
+"Roots"} are black.\<close>
consts M_init :: nodes
definition Proper_M_init :: "gar_coll_state \<Rightarrow> bool" where
"Proper_M_init \<equiv> \<guillemotleft> Blacks M_init=Roots \<and> length M_init=length \<acute>M \<guillemotright>"
-
+
definition Proper :: "gar_coll_state \<Rightarrow> bool" where
"Proper \<equiv> \<guillemotleft> Proper_Roots \<acute>M \<and> Proper_Edges(\<acute>M, \<acute>E) \<and> \<acute>Proper_M_init \<guillemotright>"
@@ -97,24 +97,24 @@
lemmas collector_defs = Proper_M_init_def Proper_def Safe_def
-subsubsection {* Blackening the roots *}
+subsubsection \<open>Blackening the roots\<close>
definition Blacken_Roots :: " gar_coll_state ann_com" where
- "Blacken_Roots \<equiv>
+ "Blacken_Roots \<equiv>
\<lbrace>\<acute>Proper\<rbrace>
\<acute>ind:=0;;
\<lbrace>\<acute>Proper \<and> \<acute>ind=0\<rbrace>
- WHILE \<acute>ind<length \<acute>M
+ WHILE \<acute>ind<length \<acute>M
INV \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
DO \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
- IF \<acute>ind\<in>Roots THEN
- \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots\<rbrace>
+ IF \<acute>ind\<in>Roots THEN
+ \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots\<rbrace>
\<acute>M:=\<acute>M[\<acute>ind:=Black] FI;;
\<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind+1. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
- \<acute>ind:=\<acute>ind+1
+ \<acute>ind:=\<acute>ind+1
OD"
-lemma Blacken_Roots:
+lemma Blacken_Roots:
"\<turnstile> Blacken_Roots \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace>"
apply (unfold Blacken_Roots_def)
apply annhoare
@@ -127,7 +127,7 @@
apply force
done
-subsubsection {* Propagating black *}
+subsubsection \<open>Propagating black\<close>
definition PBInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
"PBInv \<equiv> \<guillemotleft> \<lambda>ind. \<acute>obc < Blacks \<acute>M \<or> (\<forall>i <ind. \<not>BtoW (\<acute>E!i, \<acute>M) \<or>
@@ -137,25 +137,25 @@
"Propagate_Black_aux \<equiv>
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M\<rbrace>
\<acute>ind:=0;;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0\<rbrace>
- WHILE \<acute>ind<length \<acute>E
- INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0\<rbrace>
+ WHILE \<acute>ind<length \<acute>E
+ INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E\<rbrace>
- DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
- \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace>
- IF \<acute>M!(fst (\<acute>E!\<acute>ind)) = Black THEN
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace>
+ IF \<acute>M!(fst (\<acute>E!\<acute>ind)) = Black THEN
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black\<rbrace>
\<acute>M:=\<acute>M[snd(\<acute>E!\<acute>ind):=Black];;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> \<acute>PBInv (\<acute>ind + 1) \<and> \<acute>ind<length \<acute>E\<rbrace>
\<acute>ind:=\<acute>ind+1
FI
OD"
-lemma Propagate_Black_aux:
+lemma Propagate_Black_aux:
"\<turnstile> Propagate_Black_aux
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace>"
apply (unfold Propagate_Black_aux_def PBInv_def collector_defs)
apply annhoare
@@ -163,7 +163,7 @@
apply force
apply force
apply force
---{* 4 subgoals left *}
+--\<open>4 subgoals left\<close>
apply clarify
apply(simp add:Proper_Edges_def Proper_Roots_def Graph6 Graph7 Graph8 Graph12)
apply (erule disjE)
@@ -189,10 +189,10 @@
apply(erule subset_psubset_trans)
apply(erule Graph11)
apply fast
---{* 3 subgoals left *}
+--\<open>3 subgoals left\<close>
apply force
apply force
---{* last *}
+--\<open>last\<close>
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
@@ -206,11 +206,11 @@
apply arith
done
-subsubsection {* Refining propagating black *}
+subsubsection \<open>Refining propagating black\<close>
definition Auxk :: "gar_coll_state \<Rightarrow> bool" where
- "Auxk \<equiv> \<guillemotleft>\<acute>k<length \<acute>M \<and> (\<acute>M!\<acute>k\<noteq>Black \<or> \<not>BtoW(\<acute>E!\<acute>ind, \<acute>M) \<or>
- \<acute>obc<Blacks \<acute>M \<or> (\<not>\<acute>z \<and> \<acute>ind=R \<and> snd(\<acute>E!R)=T
+ "Auxk \<equiv> \<guillemotleft>\<acute>k<length \<acute>M \<and> (\<acute>M!\<acute>k\<noteq>Black \<or> \<not>BtoW(\<acute>E!\<acute>ind, \<acute>M) \<or>
+ \<acute>obc<Blacks \<acute>M \<or> (\<not>\<acute>z \<and> \<acute>ind=R \<and> snd(\<acute>E!R)=T
\<and> (\<exists>r. \<acute>ind<r \<and> r<length \<acute>E \<and> BtoW(\<acute>E!r, \<acute>M))))\<guillemotright>"
definition Propagate_Black :: " gar_coll_state ann_com" where
@@ -218,28 +218,28 @@
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M\<rbrace>
\<acute>ind:=0;;
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0\<rbrace>
- WHILE \<acute>ind<length \<acute>E
- INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ WHILE \<acute>ind<length \<acute>E
+ INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E\<rbrace>
- DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
- \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace>
- IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))=Black THEN
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace>
+ IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))=Black THEN
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black\<rbrace>
\<acute>k:=(snd(\<acute>E!\<acute>ind));;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
- \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black
\<and> \<acute>Auxk\<rbrace>
\<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],, \<acute>ind:=\<acute>ind+1\<rangle>
- ELSE \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
- \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace>
- \<langle>IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle>
+ ELSE \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace>
+ \<langle>IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle>
FI
OD"
-lemma Propagate_Black:
+lemma Propagate_Black:
"\<turnstile> Propagate_Black
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace>"
apply (unfold Propagate_Black_def PBInv_def Auxk_def collector_defs)
apply annhoare
@@ -247,10 +247,10 @@
apply force
apply force
apply force
---{* 5 subgoals left *}
+--\<open>5 subgoals left\<close>
apply clarify
apply(simp add:BtoW_def Proper_Edges_def)
---{* 4 subgoals left *}
+--\<open>4 subgoals left\<close>
apply clarify
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
apply (erule disjE)
@@ -287,7 +287,7 @@
apply(erule subset_psubset_trans)
apply(erule Graph11)
apply fast
---{* 2 subgoals left *}
+--\<open>2 subgoals left\<close>
apply clarify
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
apply (erule disjE)
@@ -304,61 +304,61 @@
apply arith
apply (simp add: BtoW_def)
apply (simp add: BtoW_def)
---{* last *}
+--\<open>last\<close>
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
apply (simp)
apply(drule Graph1)
apply simp
- apply clarify
+ apply clarify
apply(erule allE, erule impE, assumption)
apply force
apply force
apply arith
done
-subsubsection {* Counting black nodes *}
+subsubsection \<open>Counting black nodes\<close>
definition CountInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
"CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>"
definition Count :: " gar_coll_state ann_com" where
"Count \<equiv>
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
- \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
+ \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}\<rbrace>
\<acute>ind:=0;;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
- \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
- \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
+ \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}
\<and> \<acute>ind=0\<rbrace>
- WHILE \<acute>ind<length \<acute>M
- INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
- \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ WHILE \<acute>ind<length \<acute>M
+ INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
+ \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
\<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
- DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
- \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
- \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
- \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M\<rbrace>
- IF \<acute>M!\<acute>ind=Black
- THEN \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
- \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
+ \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
+ \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M\<rbrace>
+ IF \<acute>M!\<acute>ind=Black
+ THEN \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
+ \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
\<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace>
\<acute>bc:=insert \<acute>ind \<acute>bc
FI;;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
- \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
+ \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
\<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv (\<acute>ind+1)
\<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M\<rbrace>
\<acute>ind:=\<acute>ind+1
OD"
-lemma Count:
- "\<turnstile> Count
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
+lemma Count:
+ "\<turnstile> Count
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
\<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M
\<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace>"
apply(unfold Count_def)
@@ -377,14 +377,14 @@
apply force
done
-subsubsection {* Appending garbage nodes to the free list *}
+subsubsection \<open>Appending garbage nodes to the free list\<close>
axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
where
Append_to_free0: "length (Append_to_free (i, e)) = length e" and
- Append_to_free1: "Proper_Edges (m, e)
+ Append_to_free1: "Proper_Edges (m, e)
\<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and
- Append_to_free2: "i \<notin> Reach e
+ Append_to_free2: "i \<notin> Reach e
\<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
definition AppendInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
@@ -395,20 +395,20 @@
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe\<rbrace>
\<acute>ind:=0;;
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0\<rbrace>
- WHILE \<acute>ind<length \<acute>M
+ WHILE \<acute>ind<length \<acute>M
INV \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
DO \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M\<rbrace>
- IF \<acute>M!\<acute>ind=Black THEN
- \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace>
- \<acute>M:=\<acute>M[\<acute>ind:=White]
+ IF \<acute>M!\<acute>ind=Black THEN
+ \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace>
+ \<acute>M:=\<acute>M[\<acute>ind:=White]
ELSE \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E\<rbrace>
\<acute>E:=Append_to_free(\<acute>ind,\<acute>E)
FI;;
- \<lbrace>\<acute>Proper \<and> \<acute>AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M\<rbrace>
+ \<lbrace>\<acute>Proper \<and> \<acute>AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M\<rbrace>
\<acute>ind:=\<acute>ind+1
OD"
-lemma Append:
+lemma Append:
"\<turnstile> Append \<lbrace>\<acute>Proper\<rbrace>"
apply(unfold Append_def AppendInv_def)
apply annhoare
@@ -429,41 +429,41 @@
apply force
done
-subsubsection {* Correctness of the Collector *}
+subsubsection \<open>Correctness of the Collector\<close>
definition Collector :: " gar_coll_state ann_com" where
"Collector \<equiv>
-\<lbrace>\<acute>Proper\<rbrace>
- WHILE True INV \<lbrace>\<acute>Proper\<rbrace>
- DO
- Blacken_Roots;;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace>
- \<acute>obc:={};;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}\<rbrace>
- \<acute>bc:=Roots;;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots\<rbrace>
- \<acute>Ma:=M_init;;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>Ma=M_init\<rbrace>
- WHILE \<acute>obc\<noteq>\<acute>bc
- INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
- \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M
- \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace>
+\<lbrace>\<acute>Proper\<rbrace>
+ WHILE True INV \<lbrace>\<acute>Proper\<rbrace>
+ DO
+ Blacken_Roots;;
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace>
+ \<acute>obc:={};;
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}\<rbrace>
+ \<acute>bc:=Roots;;
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots\<rbrace>
+ \<acute>Ma:=M_init;;
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>Ma=M_init\<rbrace>
+ WHILE \<acute>obc\<noteq>\<acute>bc
+ INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
+ \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace>
DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M\<rbrace>
\<acute>obc:=\<acute>bc;;
- Propagate_Black;;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
- \<and> (\<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace>
+ Propagate_Black;;
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
+ \<and> (\<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace>
\<acute>Ma:=\<acute>M;;
- \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma
- \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M
+ \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma
+ \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M
\<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace>
\<acute>bc:={};;
- Count
- OD;;
- Append
+ Count
+ OD;;
+ Append
OD"
-lemma Collector:
+lemma Collector:
"\<turnstile> Collector \<lbrace>False\<rbrace>"
apply(unfold Collector_def)
apply annhoare
@@ -478,14 +478,14 @@
apply(force dest:subset_antisym)
done
-subsection {* Interference Freedom *}
+subsection \<open>Interference Freedom\<close>
-lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def
+lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def
Propagate_Black_def Count_def Append_def
lemmas Invariants = PBInv_def Auxk_def CountInv_def AppendInv_def
lemmas abbrev = collector_defs mutator_defs Invariants
-lemma interfree_Blacken_Roots_Redirect_Edge:
+lemma interfree_Blacken_Roots_Redirect_Edge:
"interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)"
apply (unfold modules)
apply interfree_aux
@@ -493,7 +493,7 @@
apply (simp_all add:Graph6 Graph12 abbrev)
done
-lemma interfree_Redirect_Edge_Blacken_Roots:
+lemma interfree_Redirect_Edge_Blacken_Roots:
"interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)"
apply (unfold modules)
apply interfree_aux
@@ -501,7 +501,7 @@
apply(simp add:abbrev)+
done
-lemma interfree_Blacken_Roots_Color_Target:
+lemma interfree_Blacken_Roots_Color_Target:
"interfree_aux (Some Blacken_Roots, {}, Some Color_Target)"
apply (unfold modules)
apply interfree_aux
@@ -509,7 +509,7 @@
apply(simp_all add:Graph7 Graph8 nth_list_update abbrev)
done
-lemma interfree_Color_Target_Blacken_Roots:
+lemma interfree_Color_Target_Blacken_Roots:
"interfree_aux (Some Color_Target, {}, Some Blacken_Roots)"
apply (unfold modules )
apply interfree_aux
@@ -517,18 +517,18 @@
apply(simp add:abbrev)+
done
-lemma interfree_Propagate_Black_Redirect_Edge:
+lemma interfree_Propagate_Black_Redirect_Edge:
"interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)"
apply (unfold modules )
apply interfree_aux
---{* 11 subgoals left *}
+--\<open>11 subgoals left\<close>
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
- apply(erule Graph4)
+ apply(erule Graph4)
apply(simp)+
apply (simp add:BtoW_def)
apply (simp add:BtoW_def)
@@ -536,11 +536,11 @@
apply (force simp add:BtoW_def)
apply(erule Graph4)
apply simp+
---{* 7 subgoals left *}
+--\<open>7 subgoals left\<close>
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
- apply(erule Graph4)
+ apply(erule Graph4)
apply(simp)+
apply (simp add:BtoW_def)
apply (simp add:BtoW_def)
@@ -548,12 +548,12 @@
apply (force simp add:BtoW_def)
apply(erule Graph4)
apply simp+
---{* 6 subgoals left *}
+--\<open>6 subgoals left\<close>
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
apply(rule conjI)
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
- apply(erule Graph4)
+ apply(erule Graph4)
apply(simp)+
apply (simp add:BtoW_def)
apply (simp add:BtoW_def)
@@ -561,15 +561,15 @@
apply (force simp add:BtoW_def)
apply(erule Graph4)
apply simp+
-apply(simp add:BtoW_def nth_list_update)
+apply(simp add:BtoW_def nth_list_update)
apply force
---{* 5 subgoals left *}
+--\<open>5 subgoals left\<close>
apply(clarify, simp add:abbrev Graph6 Graph12)
---{* 4 subgoals left *}
+--\<open>4 subgoals left\<close>
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(rule conjI)
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
- apply(erule Graph4)
+ apply(erule Graph4)
apply(simp)+
apply (simp add:BtoW_def)
apply (simp add:BtoW_def)
@@ -589,13 +589,13 @@
apply simp+
apply(force simp add:BtoW_def)
apply(force simp add:BtoW_def)
---{* 3 subgoals left *}
+--\<open>3 subgoals left\<close>
apply(clarify, simp add:abbrev Graph6 Graph12)
---{* 2 subgoals left *}
+--\<open>2 subgoals left\<close>
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
apply clarify
- apply(erule Graph4)
+ apply(erule Graph4)
apply(simp)+
apply (simp add:BtoW_def)
apply (simp add:BtoW_def)
@@ -605,84 +605,84 @@
apply simp+
done
-lemma interfree_Redirect_Edge_Propagate_Black:
+lemma interfree_Redirect_Edge_Propagate_Black:
"interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev)+
done
-lemma interfree_Propagate_Black_Color_Target:
+lemma interfree_Propagate_Black_Color_Target:
"interfree_aux (Some Propagate_Black, {}, Some Color_Target)"
apply (unfold modules )
apply interfree_aux
---{* 11 subgoals left *}
+--\<open>11 subgoals left\<close>
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)+
apply(erule conjE)+
-apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
+apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
- erule allE, erule impE, assumption, erule impE, assumption,
- simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
---{* 7 subgoals left *}
+ erule allE, erule impE, assumption, erule impE, assumption,
+ simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
+--\<open>7 subgoals left\<close>
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply(erule conjE)+
-apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
+apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
- erule allE, erule impE, assumption, erule impE, assumption,
- simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
---{* 6 subgoals left *}
+ erule allE, erule impE, assumption, erule impE, assumption,
+ simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
+--\<open>6 subgoals left\<close>
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply clarify
apply (rule conjI)
- apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
+ apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
- erule allE, erule impE, assumption, erule impE, assumption,
- simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
+ erule allE, erule impE, assumption, erule impE, assumption,
+ simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
apply(simp add:nth_list_update)
---{* 5 subgoals left *}
+--\<open>5 subgoals left\<close>
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
---{* 4 subgoals left *}
+--\<open>4 subgoals left\<close>
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply (rule conjI)
- apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
+ apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
- erule allE, erule impE, assumption, erule impE, assumption,
- simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
+ erule allE, erule impE, assumption, erule impE, assumption,
+ simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
apply(rule conjI)
apply(simp add:nth_list_update)
-apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10,
+apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10,
erule subset_psubset_trans, erule Graph11, force)
---{* 3 subgoals left *}
+--\<open>3 subgoals left\<close>
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
---{* 2 subgoals left *}
+--\<open>2 subgoals left\<close>
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
-apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
+apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
- erule allE, erule impE, assumption, erule impE, assumption,
- simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
---{* 3 subgoals left *}
+ erule allE, erule impE, assumption, erule impE, assumption,
+ simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
+--\<open>3 subgoals left\<close>
apply(simp add:abbrev)
done
-lemma interfree_Color_Target_Propagate_Black:
+lemma interfree_Color_Target_Propagate_Black:
"interfree_aux (Some Color_Target, {}, Some Propagate_Black)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev)+
done
-lemma interfree_Count_Redirect_Edge:
+lemma interfree_Count_Redirect_Edge:
"interfree_aux (Some Count, {}, Some Redirect_Edge)"
apply (unfold modules)
apply interfree_aux
---{* 9 subgoals left *}
+--\<open>9 subgoals left\<close>
apply(simp_all add:abbrev Graph6 Graph12)
---{* 6 subgoals left *}
+--\<open>6 subgoals left\<close>
apply(clarify, simp add:abbrev Graph6 Graph12,
erule disjE,erule disjI1,rule disjI2,rule subset_trans, erule Graph3,force,force)+
done
-lemma interfree_Redirect_Edge_Count:
+lemma interfree_Redirect_Edge_Count:
"interfree_aux (Some Redirect_Edge, {}, Some Count)"
apply (unfold modules )
apply interfree_aux
@@ -690,26 +690,26 @@
apply(simp add:abbrev)
done
-lemma interfree_Count_Color_Target:
+lemma interfree_Count_Color_Target:
"interfree_aux (Some Count, {}, Some Color_Target)"
apply (unfold modules )
apply interfree_aux
---{* 9 subgoals left *}
+--\<open>9 subgoals left\<close>
apply(simp_all add:abbrev Graph7 Graph8 Graph12)
---{* 6 subgoals left *}
+--\<open>6 subgoals left\<close>
apply(clarify,simp add:abbrev Graph7 Graph8 Graph12,
erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+
---{* 2 subgoals left *}
+--\<open>2 subgoals left\<close>
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply(rule conjI)
- apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
+ apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
apply(simp add:nth_list_update)
---{* 1 subgoal left *}
+--\<open>1 subgoal left\<close>
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12,
erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
done
-lemma interfree_Color_Target_Count:
+lemma interfree_Color_Target_Count:
"interfree_aux (Some Color_Target, {}, Some Count)"
apply (unfold modules )
apply interfree_aux
@@ -717,7 +717,7 @@
apply(simp add:abbrev)
done
-lemma interfree_Append_Redirect_Edge:
+lemma interfree_Append_Redirect_Edge:
"interfree_aux (Some Append, {}, Some Redirect_Edge)"
apply (unfold modules )
apply interfree_aux
@@ -725,7 +725,7 @@
apply(clarify, simp add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12, force dest:Graph3)+
done
-lemma interfree_Redirect_Edge_Append:
+lemma interfree_Redirect_Edge_Append:
"interfree_aux (Some Redirect_Edge, {}, Some Append)"
apply (unfold modules )
apply interfree_aux
@@ -734,7 +734,7 @@
apply(clarify, simp add:abbrev Append_to_free0)+
done
-lemma interfree_Append_Color_Target:
+lemma interfree_Append_Color_Target:
"interfree_aux (Some Append, {}, Some Color_Target)"
apply (unfold modules )
apply interfree_aux
@@ -742,7 +742,7 @@
apply(simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)
done
-lemma interfree_Color_Target_Append:
+lemma interfree_Color_Target_Append:
"interfree_aux (Some Color_Target, {}, Some Append)"
apply (unfold modules )
apply interfree_aux
@@ -751,17 +751,17 @@
apply(clarify,simp add:abbrev Append_to_free0)+
done
-lemmas collector_mutator_interfree =
- interfree_Blacken_Roots_Redirect_Edge interfree_Blacken_Roots_Color_Target
- interfree_Propagate_Black_Redirect_Edge interfree_Propagate_Black_Color_Target
- interfree_Count_Redirect_Edge interfree_Count_Color_Target
- interfree_Append_Redirect_Edge interfree_Append_Color_Target
- interfree_Redirect_Edge_Blacken_Roots interfree_Color_Target_Blacken_Roots
- interfree_Redirect_Edge_Propagate_Black interfree_Color_Target_Propagate_Black
- interfree_Redirect_Edge_Count interfree_Color_Target_Count
+lemmas collector_mutator_interfree =
+ interfree_Blacken_Roots_Redirect_Edge interfree_Blacken_Roots_Color_Target
+ interfree_Propagate_Black_Redirect_Edge interfree_Propagate_Black_Color_Target
+ interfree_Count_Redirect_Edge interfree_Count_Color_Target
+ interfree_Append_Redirect_Edge interfree_Append_Color_Target
+ interfree_Redirect_Edge_Blacken_Roots interfree_Color_Target_Blacken_Roots
+ interfree_Redirect_Edge_Propagate_Black interfree_Color_Target_Propagate_Black
+ interfree_Redirect_Edge_Count interfree_Color_Target_Count
interfree_Redirect_Edge_Append interfree_Color_Target_Append
-subsubsection {* Interference freedom Collector-Mutator *}
+subsubsection \<open>Interference freedom Collector-Mutator\<close>
lemma interfree_Collector_Mutator:
"interfree_aux (Some Collector, {}, Some Mutator)"
@@ -769,20 +769,20 @@
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
apply(unfold modules collector_defs Mut_init_def)
-apply(tactic {* TRYALL (interfree_aux_tac @{context}) *})
---{* 32 subgoals left *}
+apply(tactic \<open>TRYALL (interfree_aux_tac @{context})\<close>)
+--\<open>32 subgoals left\<close>
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
---{* 20 subgoals left *}
-apply(tactic{* TRYALL (clarify_tac @{context}) *})
+--\<open>20 subgoals left\<close>
+apply(tactic\<open>TRYALL (clarify_tac @{context})\<close>)
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
-apply(tactic {* TRYALL (etac disjE) *})
+apply(tactic \<open>TRYALL (etac disjE)\<close>)
apply simp_all
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
+apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}])\<close>)
+apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}])\<close>)
+apply(tactic \<open>TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}])\<close>)
done
-subsubsection {* Interference freedom Mutator-Collector *}
+subsubsection \<open>Interference freedom Mutator-Collector\<close>
lemma interfree_Mutator_Collector:
"interfree_aux (Some Mutator, {}, Some Collector)"
@@ -790,30 +790,30 @@
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
apply(unfold modules collector_defs Mut_init_def)
-apply(tactic {* TRYALL (interfree_aux_tac @{context}) *})
---{* 64 subgoals left *}
+apply(tactic \<open>TRYALL (interfree_aux_tac @{context})\<close>)
+--\<open>64 subgoals left\<close>
apply(simp_all add:nth_list_update Invariants Append_to_free0)+
-apply(tactic{* TRYALL (clarify_tac @{context}) *})
---{* 4 subgoals left *}
+apply(tactic\<open>TRYALL (clarify_tac @{context})\<close>)
+--\<open>4 subgoals left\<close>
apply force
apply(simp add:Append_to_free2)
apply force
apply(simp add:Append_to_free2)
done
-subsubsection {* The Garbage Collection algorithm *}
+subsubsection \<open>The Garbage Collection algorithm\<close>
-text {* In total there are 289 verification conditions. *}
+text \<open>In total there are 289 verification conditions.\<close>
-lemma Gar_Coll:
- "\<parallel>- \<lbrace>\<acute>Proper \<and> \<acute>Mut_init \<and> \<acute>z\<rbrace>
- COBEGIN
+lemma Gar_Coll:
+ "\<parallel>- \<lbrace>\<acute>Proper \<and> \<acute>Mut_init \<and> \<acute>z\<rbrace>
+ COBEGIN
Collector
\<lbrace>False\<rbrace>
- \<parallel>
+ \<parallel>
Mutator
- \<lbrace>False\<rbrace>
- COEND
+ \<lbrace>False\<rbrace>
+ COEND
\<lbrace>False\<rbrace>"
apply oghoare
apply(force simp add: Mutator_def Collector_def modules)