# HG changeset patch # User wenzelm # Date 1419708726 -3600 # Node ID ad8e0a789af6ab8191675f706adbea3e1dd8b38e # Parent e99f706aeab9fccb936f931d3aba77fe8d7428fb update_cartouches; trimmed whitespace; diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/Gar_Coll.thy --- 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 \The Single Mutator Case\ theory Gar_Coll imports Graph OG_Syntax begin declare psubsetE [rule del] -text {* Declaration of variables: *} +text \Declaration of variables:\ 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 \The Mutator\ -text {* The mutator first redirects an arbitrary edge @{text "R"} from +text \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:\ consts R :: nat T :: nat -text {* \noindent The following predicate states, given a list of +text \\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:\ definition Mut_init :: "gar_coll_state \ bool" where "Mut_init \ \ T \ Reach \E \ R < length \E \ T < length \M \" -text {* \noindent For the mutator we +text \\noindent For the mutator we consider two modules, one for each action. An auxiliary variable @{text "\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.\ definition Redirect_Edge :: "gar_coll_state ann_com" where "Redirect_Edge \ \\Mut_init \ \z\ \\E:=\E[R:=(fst(\E!R), T)],, \z:= (\\z)\" @@ -47,15 +47,15 @@ definition Mutator :: "gar_coll_state ann_com" where "Mutator \ - \\Mut_init \ \z\ - WHILE True INV \\Mut_init \ \z\ + \\Mut_init \ \z\ + WHILE True INV \\Mut_init \ \z\ DO Redirect_Edge ;; Color_Target OD" -subsubsection {* Correctness of the mutator *} +subsubsection \Correctness of the mutator\ lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def -lemma Redirect_Edge: +lemma Redirect_Edge: "\ Redirect_Edge pre(Color_Target)" apply (unfold mutator_defs) apply annhoare @@ -70,7 +70,7 @@ apply(simp_all) done -lemma Mutator: +lemma Mutator: "\ Mutator \False\" apply(unfold Mutator_def) apply annhoare @@ -78,17 +78,17 @@ apply(simp add:mutator_defs) done -subsection {* The Collector *} +subsection \The Collector\ -text {* \noindent A constant @{text "M_init"} is used to give @{text "\Ma"} a +text \\noindent A constant @{text "M_init"} is used to give @{text "\Ma"} a suitable first value, defined as a list of nodes where only the @{text -"Roots"} are black. *} +"Roots"} are black.\ consts M_init :: nodes definition Proper_M_init :: "gar_coll_state \ bool" where "Proper_M_init \ \ Blacks M_init=Roots \ length M_init=length \M \" - + definition Proper :: "gar_coll_state \ bool" where "Proper \ \ Proper_Roots \M \ Proper_Edges(\M, \E) \ \Proper_M_init \" @@ -97,24 +97,24 @@ lemmas collector_defs = Proper_M_init_def Proper_def Safe_def -subsubsection {* Blackening the roots *} +subsubsection \Blackening the roots\ definition Blacken_Roots :: " gar_coll_state ann_com" where - "Blacken_Roots \ + "Blacken_Roots \ \\Proper\ \ind:=0;; \\Proper \ \ind=0\ - WHILE \indM + WHILE \indM INV \\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \ind\length \M\ DO \\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \indM\ - IF \ind\Roots THEN - \\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \indM \ \ind\Roots\ + IF \ind\Roots THEN + \\Proper \ (\i<\ind. i \ Roots \ \M!i=Black) \ \indM \ \ind\Roots\ \M:=\M[\ind:=Black] FI;; \\Proper \ (\i<\ind+1. i \ Roots \ \M!i=Black) \ \indM\ - \ind:=\ind+1 + \ind:=\ind+1 OD" -lemma Blacken_Roots: +lemma Blacken_Roots: "\ Blacken_Roots \\Proper \ Roots\Blacks \M\" apply (unfold Blacken_Roots_def) apply annhoare @@ -127,7 +127,7 @@ apply force done -subsubsection {* Propagating black *} +subsubsection \Propagating black\ definition PBInv :: "gar_coll_state \ nat \ bool" where "PBInv \ \ \ind. \obc < Blacks \M \ (\i BtoW (\E!i, \M) \ @@ -137,25 +137,25 @@ "Propagate_Black_aux \ \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M\ \ind:=0;; - \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \ind=0\ - WHILE \indE - INV \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \ind=0\ + WHILE \indE + INV \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \PBInv \ind \ \ind\length \E\ - DO \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \indE\ - IF \M!(fst (\E!\ind)) = Black THEN - \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + DO \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \indE\ + IF \M!(fst (\E!\ind)) = Black THEN + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \PBInv \ind \ \indE \ \M!fst(\E!\ind)=Black\ \M:=\M[snd(\E!\ind):=Black];; - \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \PBInv (\ind + 1) \ \indE\ \ind:=\ind+1 FI OD" -lemma Propagate_Black_aux: +lemma Propagate_Black_aux: "\ Propagate_Black_aux - \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ ( \obc < Blacks \M \ \Safe)\" 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 *} +--\4 subgoals left\ 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 *} +--\3 subgoals left\ apply force apply force ---{* last *} +--\last\ apply clarify apply simp apply(subgoal_tac "ind x = length (E x)") @@ -206,11 +206,11 @@ apply arith done -subsubsection {* Refining propagating black *} +subsubsection \Refining propagating black\ definition Auxk :: "gar_coll_state \ bool" where - "Auxk \ \\kM \ (\M!\k\Black \ \BtoW(\E!\ind, \M) \ - \obcM \ (\\z \ \ind=R \ snd(\E!R)=T + "Auxk \ \\kM \ (\M!\k\Black \ \BtoW(\E!\ind, \M) \ + \obcM \ (\\z \ \ind=R \ snd(\E!R)=T \ (\r. \ind rE \ BtoW(\E!r, \M))))\" definition Propagate_Black :: " gar_coll_state ann_com" where @@ -218,28 +218,28 @@ \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M\ \ind:=0;; \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \ind=0\ - WHILE \indE - INV \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + WHILE \indE + INV \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \PBInv \ind \ \ind\length \E\ - DO \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \indE\ - IF (\M!(fst (\E!\ind)))=Black THEN - \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + DO \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \indE\ + IF (\M!(fst (\E!\ind)))=Black THEN + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ \PBInv \ind \ \indE \ (\M!fst(\E!\ind))=Black\ \k:=(snd(\E!\ind));; - \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \indE \ (\M!fst(\E!\ind))=Black + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \indE \ (\M!fst(\E!\ind))=Black \ \Auxk\ \\M:=\M[\k:=Black],, \ind:=\ind+1\ - ELSE \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ \PBInv \ind \ \indE\ - \IF (\M!(fst (\E!\ind)))\Black THEN \ind:=\ind+1 FI\ + ELSE \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ \PBInv \ind \ \indE\ + \IF (\M!(fst (\E!\ind)))\Black THEN \ind:=\ind+1 FI\ FI OD" -lemma Propagate_Black: +lemma Propagate_Black: "\ Propagate_Black - \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ ( \obc < Blacks \M \ \Safe)\" 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 *} +--\5 subgoals left\ apply clarify apply(simp add:BtoW_def Proper_Edges_def) ---{* 4 subgoals left *} +--\4 subgoals left\ 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 *} +--\2 subgoals left\ 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 *} +--\last\ 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 \Counting black nodes\ definition CountInv :: "gar_coll_state \ nat \ bool" where "CountInv \ \ \ind. {i. i \Ma!i=Black}\\bc \" definition Count :: " gar_coll_state ann_com" where "Count \ - \\Proper \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \\Proper \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe) \ \bc={}\ \ind:=0;; - \\Proper \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe) \ \bc={} + \\Proper \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe) \ \bc={} \ \ind=0\ - WHILE \indM - INV \\Proper \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + WHILE \indM + INV \\Proper \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \CountInv \ind \ ( \obc < Blacks \Ma \ \Safe) \ \ind\length \M\ - DO \\Proper \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ \CountInv \ind - \ ( \obc < Blacks \Ma \ \Safe) \ \indM\ - IF \M!\ind=Black - THEN \\Proper \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + DO \\Proper \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ \CountInv \ind + \ ( \obc < Blacks \Ma \ \Safe) \ \indM\ + IF \M!\ind=Black + THEN \\Proper \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \CountInv \ind \ ( \obc < Blacks \Ma \ \Safe) \ \indM \ \M!\ind=Black\ \bc:=insert \ind \bc FI;; - \\Proper \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \\Proper \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ \CountInv (\ind+1) \ ( \obc < Blacks \Ma \ \Safe) \ \indM\ \ind:=\ind+1 OD" -lemma Count: - "\ Count - \\Proper \ Roots\Blacks \M +lemma Count: + "\ Count + \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma \ Blacks \Ma\\bc \ \bc\Blacks \M \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe)\" apply(unfold Count_def) @@ -377,14 +377,14 @@ apply force done -subsubsection {* Appending garbage nodes to the free list *} +subsubsection \Appending garbage nodes to the free list\ axiomatization Append_to_free :: "nat \ edges \ 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) \ Proper_Edges (m, Append_to_free(i, e))" and - Append_to_free2: "i \ Reach e + Append_to_free2: "i \ Reach e \ n \ Reach (Append_to_free(i, e)) = ( n = i \ n \ Reach e)" definition AppendInv :: "gar_coll_state \ nat \ bool" where @@ -395,20 +395,20 @@ \\Proper \ Roots\Blacks \M \ \Safe\ \ind:=0;; \\Proper \ Roots\Blacks \M \ \Safe \ \ind=0\ - WHILE \indM + WHILE \indM INV \\Proper \ \AppendInv \ind \ \ind\length \M\ DO \\Proper \ \AppendInv \ind \ \indM\ - IF \M!\ind=Black THEN - \\Proper \ \AppendInv \ind \ \indM \ \M!\ind=Black\ - \M:=\M[\ind:=White] + IF \M!\ind=Black THEN + \\Proper \ \AppendInv \ind \ \indM \ \M!\ind=Black\ + \M:=\M[\ind:=White] ELSE \\Proper \ \AppendInv \ind \ \indM \ \ind\Reach \E\ \E:=Append_to_free(\ind,\E) FI;; - \\Proper \ \AppendInv (\ind+1) \ \indM\ + \\Proper \ \AppendInv (\ind+1) \ \indM\ \ind:=\ind+1 OD" -lemma Append: +lemma Append: "\ Append \\Proper\" apply(unfold Append_def AppendInv_def) apply annhoare @@ -429,41 +429,41 @@ apply force done -subsubsection {* Correctness of the Collector *} +subsubsection \Correctness of the Collector\ definition Collector :: " gar_coll_state ann_com" where "Collector \ -\\Proper\ - WHILE True INV \\Proper\ - DO - Blacken_Roots;; - \\Proper \ Roots\Blacks \M\ - \obc:={};; - \\Proper \ Roots\Blacks \M \ \obc={}\ - \bc:=Roots;; - \\Proper \ Roots\Blacks \M \ \obc={} \ \bc=Roots\ - \Ma:=M_init;; - \\Proper \ Roots\Blacks \M \ \obc={} \ \bc=Roots \ \Ma=M_init\ - WHILE \obc\\bc - INV \\Proper \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\\bc \ \bc\Blacks \M - \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe)\ +\\Proper\ + WHILE True INV \\Proper\ + DO + Blacken_Roots;; + \\Proper \ Roots\Blacks \M\ + \obc:={};; + \\Proper \ Roots\Blacks \M \ \obc={}\ + \bc:=Roots;; + \\Proper \ Roots\Blacks \M \ \obc={} \ \bc=Roots\ + \Ma:=M_init;; + \\Proper \ Roots\Blacks \M \ \obc={} \ \bc=Roots \ \Ma=M_init\ + WHILE \obc\\bc + INV \\Proper \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\\bc \ \bc\Blacks \M + \ length \Ma=length \M \ (\obc < Blacks \Ma \ \Safe)\ DO \\Proper \ Roots\Blacks \M \ \bc\Blacks \M\ \obc:=\bc;; - Propagate_Black;; - \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ (\obc < Blacks \M \ \Safe)\ + Propagate_Black;; + \\Proper \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ (\obc < Blacks \M \ \Safe)\ \Ma:=\M;; - \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma - \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M + \\Proper \ Roots\Blacks \M \ \obc\Blacks \Ma + \ Blacks \Ma\Blacks \M \ \bc\Blacks \M \ length \Ma=length \M \ ( \obc < Blacks \Ma \ \Safe)\ \bc:={};; - Count - OD;; - Append + Count + OD;; + Append OD" -lemma Collector: +lemma Collector: "\ Collector \False\" apply(unfold Collector_def) apply annhoare @@ -478,14 +478,14 @@ apply(force dest:subset_antisym) done -subsection {* Interference Freedom *} +subsection \Interference Freedom\ -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 *} +--\11 subgoals left\ 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 *} +--\7 subgoals left\ 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 *} +--\6 subgoals left\ 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 *} +--\5 subgoals left\ apply(clarify, simp add:abbrev Graph6 Graph12) ---{* 4 subgoals left *} +--\4 subgoals left\ 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 *} +--\3 subgoals left\ apply(clarify, simp add:abbrev Graph6 Graph12) ---{* 2 subgoals left *} +--\2 subgoals left\ 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 *} +--\11 subgoals left\ 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) +--\7 subgoals left\ 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) +--\6 subgoals left\ 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 *} +--\5 subgoals left\ apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) ---{* 4 subgoals left *} +--\4 subgoals left\ 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 *} +--\3 subgoals left\ apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) ---{* 2 subgoals left *} +--\2 subgoals left\ 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) +--\3 subgoals left\ 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 *} +--\9 subgoals left\ apply(simp_all add:abbrev Graph6 Graph12) ---{* 6 subgoals left *} +--\6 subgoals left\ 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 *} +--\9 subgoals left\ apply(simp_all add:abbrev Graph7 Graph8 Graph12) ---{* 6 subgoals left *} +--\6 subgoals left\ apply(clarify,simp add:abbrev Graph7 Graph8 Graph12, erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+ ---{* 2 subgoals left *} +--\2 subgoals left\ 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 *} +--\1 subgoal left\ 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 \Interference freedom Collector-Mutator\ 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 \TRYALL (interfree_aux_tac @{context})\) +--\32 subgoals left\ apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) ---{* 20 subgoals left *} -apply(tactic{* TRYALL (clarify_tac @{context}) *}) +--\20 subgoals left\ +apply(tactic\TRYALL (clarify_tac @{context})\) apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) -apply(tactic {* TRYALL (etac disjE) *}) +apply(tactic \TRYALL (etac disjE)\) 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 \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}])\) done -subsubsection {* Interference freedom Mutator-Collector *} +subsubsection \Interference freedom Mutator-Collector\ 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 \TRYALL (interfree_aux_tac @{context})\) +--\64 subgoals left\ apply(simp_all add:nth_list_update Invariants Append_to_free0)+ -apply(tactic{* TRYALL (clarify_tac @{context}) *}) ---{* 4 subgoals left *} +apply(tactic\TRYALL (clarify_tac @{context})\) +--\4 subgoals left\ apply force apply(simp add:Append_to_free2) apply force apply(simp add:Append_to_free2) done -subsubsection {* The Garbage Collection algorithm *} +subsubsection \The Garbage Collection algorithm\ -text {* In total there are 289 verification conditions. *} +text \In total there are 289 verification conditions.\ -lemma Gar_Coll: - "\- \\Proper \ \Mut_init \ \z\ - COBEGIN +lemma Gar_Coll: + "\- \\Proper \ \Mut_init \ \z\ + COBEGIN Collector \False\ - \ + \ Mutator - \False\ - COEND + \False\ + COEND \False\" apply oghoare apply(force simp add: Mutator_def Collector_def modules) diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/Graph.thy --- a/src/HOL/Hoare_Parallel/Graph.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/Graph.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,6 +1,6 @@ -chapter {* Case Study: Single and Multi-Mutator Garbage Collection Algorithms *} +chapter \Case Study: Single and Multi-Mutator Garbage Collection Algorithms\ -section {* Formalization of the Memory *} +section \Formalization of the Memory\ theory Graph imports Main begin @@ -29,22 +29,22 @@ \ (\ij x\Roots}" -text{* Reach: the set of reachable nodes is the set of Roots together with the +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. *} +consecutive nodes correspond to an edge in E.\ -subsection {* Proofs about Graphs *} +subsection \Proofs about Graphs\ lemmas Graph_defs= Blacks_def Proper_Roots_def Proper_Edges_def BtoW_def declare Graph_defs [simp] -subsubsection{* Graph 1 *} +subsubsection\Graph 1\ -lemma Graph1_aux [rule_format]: +lemma Graph1_aux [rule_format]: "\ Roots\Blacks M; \iBtoW(E!i,M)\ - \ 1< length path \ (path!(length path - 1))\Roots \ - (\ij. j < length E \ E!j=(path!(Suc i), path!i))) + \ 1< length path \ (path!(length path - 1))\Roots \ + (\ij. j < length E \ E!j=(path!(Suc i), path!i))) \ M!(path!0) = Black" apply(induct_tac "path") apply force @@ -70,8 +70,8 @@ apply force done -lemma Graph1: - "\Roots\Blacks M; Proper_Edges(M, E); \iBtoW(E!i,M) \ +lemma Graph1: + "\Roots\Blacks M; Proper_Edges(M, E); \iBtoW(E!i,M) \ \ Reach E\Blacks M" apply (unfold Reach_def) apply simp @@ -87,9 +87,9 @@ apply auto done -subsubsection{* Graph 2 *} +subsubsection\Graph 2\ -lemma Ex_first_occurrence [rule_format]: +lemma Ex_first_occurrence [rule_format]: "P (n::nat) \ (\m. P m \ (\i. i \ P i))" apply(rule nat_less_induct) apply clarify @@ -102,14 +102,14 @@ apply arith done -lemma Ex_last_occurrence: +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: +lemma Graph2: "\T \ Reach E; R \ T \ Reach (E[R:=(fst(E!R), T)])" apply (unfold Reach_def) apply clarify @@ -141,7 +141,7 @@ 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 + prefer 2 apply arith apply clarify apply(case_tac "i") apply(force simp add: nth_list_update) @@ -181,22 +181,22 @@ done -subsubsection{* Graph 3 *} +subsubsection\Graph 3\ declare min.absorb1 [simp] min.absorb2 [simp] -lemma Graph3: +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 "\ithe changed edge is part of the path\ 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) ---{* T is NOT a root *} +--\T is NOT a root\ apply clarify apply(rule_tac x = "(take m path)@patha" in exI) apply(subgoal_tac "\(length path\m)") @@ -240,7 +240,7 @@ apply(subgoal_tac "Suc (i - m)=(Suc i - m)" ) prefer 2 apply arith apply simp ---{* T is a root *} +--\T is a root\ apply(case_tac "m=0") apply force apply(rule_tac x = "take (Suc m) path" in exI) @@ -253,7 +253,7 @@ 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 *} +--\the changed edge is not part of the path\ apply(rule_tac x = "path" in exI) apply simp apply clarify @@ -265,18 +265,18 @@ apply(force simp add: nth_list_update) done -subsubsection{* Graph 4 *} +subsubsection\Graph 4\ -lemma Graph4: - "\T \ Reach E; Roots\Blacks M; I\length E; TiBtoW(E!i,M); RBlack\ \ +lemma Graph4: + "\T \ Reach E; Roots\Blacks M; I\length E; TiBtoW(E!i,M); RBlack\ \ (\r. I\r \ r 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 *} +--\there exist a black node in the path to T\ apply(case_tac "\mGraph 5\ -lemma Graph5: - "\ T \ Reach E ; Roots \ Blacks M; \iBtoW(E!i,M); T Black\ +lemma Graph5: + "\ T \ Reach E ; Roots \ Blacks M; \iBtoW(E!i,M); T Black\ \ (\r. R r 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*} +--\there exist a black node in the path to T\ apply(case_tac "\mOther lemmas about graphs\ -lemma Graph6: +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: +lemma Graph7: "\Proper_Edges(M,E)\ \ Proper_Edges(M[T:=a],E)" apply (unfold Proper_Edges_def) apply force done -lemma Graph8: +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. *} +text\Some specific lemmata for the verification of garbage collection algorithms.\ lemma Graph9: "j Blacks M\Blacks (M[j := Black])" apply (unfold Blacks_def) @@ -384,7 +384,7 @@ apply auto done -lemma Graph11 [rule_format (no_asm)]: +lemma Graph11 [rule_format (no_asm)]: "\ M!j\Black;j \ Blacks M \ Blacks (M[j := Black])" apply (unfold Blacks_def) apply(rule psubsetI) diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,15 +1,15 @@ -section {* The Multi-Mutator Case *} +section \The Multi-Mutator Case\ theory Mul_Gar_Coll imports Graph OG_Syntax begin -text {* The full theory takes aprox. 18 minutes. *} +text \The full theory takes aprox. 18 minutes.\ record mut = Z :: bool R :: nat T :: nat -text {* Declaration of variables: *} +text \Declaration of variables:\ record mul_gar_coll_state = M :: nodes @@ -17,45 +17,45 @@ bc :: "nat set" obc :: "nat set" Ma :: nodes - ind :: nat + ind :: nat k :: nat q :: nat l :: nat Muts :: "mut list" -subsection {* The Mutators *} +subsection \The Mutators\ definition Mul_mut_init :: "mul_gar_coll_state \ nat \ bool" where - "Mul_mut_init \ \ \n. n=length \Muts \ (\iMuts!i)E + "Mul_mut_init \ \ \n. n=length \Muts \ (\iMuts!i)E \ T (\Muts!i)M) \" definition Mul_Redirect_Edge :: "nat \ nat \ mul_gar_coll_state ann_com" where "Mul_Redirect_Edge j n \ \\Mul_mut_init n \ Z (\Muts!j)\ - \IF T(\Muts!j) \ Reach \E THEN - \E:= \E[R (\Muts!j):= (fst (\E!R(\Muts!j)), T (\Muts!j))] FI,, + \IF T(\Muts!j) \ Reach \E THEN + \E:= \E[R (\Muts!j):= (fst (\E!R(\Muts!j)), T (\Muts!j))] FI,, \Muts:= \Muts[j:= (\Muts!j) \Z:=False\]\" definition Mul_Color_Target :: "nat \ nat \ mul_gar_coll_state ann_com" where "Mul_Color_Target j n \ - \\Mul_mut_init n \ \ Z (\Muts!j)\ + \\Mul_mut_init n \ \ Z (\Muts!j)\ \\M:=\M[T (\Muts!j):=Black],, \Muts:=\Muts[j:= (\Muts!j) \Z:=True\]\" definition Mul_Mutator :: "nat \ nat \ mul_gar_coll_state ann_com" where "Mul_Mutator j n \ - \\Mul_mut_init n \ Z (\Muts!j)\ - WHILE True - INV \\Mul_mut_init n \ Z (\Muts!j)\ - DO Mul_Redirect_Edge j n ;; - Mul_Color_Target j n + \\Mul_mut_init n \ Z (\Muts!j)\ + WHILE True + INV \\Mul_mut_init n \ Z (\Muts!j)\ + DO Mul_Redirect_Edge j n ;; + Mul_Color_Target j n OD" -lemmas mul_mutator_defs = Mul_mut_init_def Mul_Redirect_Edge_def Mul_Color_Target_def +lemmas mul_mutator_defs = Mul_mut_init_def Mul_Redirect_Edge_def Mul_Color_Target_def -subsubsection {* Correctness of the proof outline of one mutator *} +subsubsection \Correctness of the proof outline of one mutator\ -lemma Mul_Redirect_Edge: "0\j \ j - \ Mul_Redirect_Edge j n +lemma Mul_Redirect_Edge: "0\j \ j + \ Mul_Redirect_Edge j n pre(Mul_Color_Target j n)" apply (unfold mul_mutator_defs) apply annhoare @@ -64,8 +64,8 @@ apply(simp add:nth_list_update) done -lemma Mul_Color_Target: "0\j \ j - \ Mul_Color_Target j n +lemma Mul_Color_Target: "0\j \ j + \ Mul_Color_Target j n \\Mul_mut_init n \ Z (\Muts!j)\" apply (unfold mul_mutator_defs) apply annhoare @@ -74,7 +74,7 @@ apply(simp add:nth_list_update) done -lemma Mul_Mutator: "0\j \ j +lemma Mul_Mutator: "0\j \ j \ Mul_Mutator j n \False\" apply(unfold Mul_Mutator_def) apply annhoare @@ -82,10 +82,10 @@ apply(simp add:mul_mutator_defs Mul_Redirect_Edge_def) done -subsubsection {* Interference freedom between mutators *} +subsubsection \Interference freedom between mutators\ -lemma Mul_interfree_Redirect_Edge_Redirect_Edge: - "\0\i; ij; jj\ \ +lemma Mul_interfree_Redirect_Edge_Redirect_Edge: + "\0\i; ij; jj\ \ interfree_aux (Some (Mul_Redirect_Edge i n),{}, Some(Mul_Redirect_Edge j n))" apply (unfold mul_mutator_defs) apply interfree_aux @@ -93,8 +93,8 @@ apply(simp_all add: nth_list_update) done -lemma Mul_interfree_Redirect_Edge_Color_Target: - "\0\i; ij; jj\ \ +lemma Mul_interfree_Redirect_Edge_Color_Target: + "\0\i; ij; jj\ \ interfree_aux (Some(Mul_Redirect_Edge i n),{},Some(Mul_Color_Target j n))" apply (unfold mul_mutator_defs) apply interfree_aux @@ -102,8 +102,8 @@ apply(simp_all add: nth_list_update) done -lemma Mul_interfree_Color_Target_Redirect_Edge: - "\0\i; ij; jj\ \ +lemma Mul_interfree_Color_Target_Redirect_Edge: + "\0\i; ij; jj\ \ interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Redirect_Edge j n))" apply (unfold mul_mutator_defs) apply interfree_aux @@ -111,8 +111,8 @@ apply(simp_all add:nth_list_update) done -lemma Mul_interfree_Color_Target_Color_Target: - " \0\i; ij; jj\ \ +lemma Mul_interfree_Color_Target_Color_Target: + " \0\i; ij; jj\ \ interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Color_Target j n))" apply (unfold mul_mutator_defs) apply interfree_aux @@ -120,22 +120,22 @@ apply(simp_all add: nth_list_update) done -lemmas mul_mutator_interfree = +lemmas mul_mutator_interfree = Mul_interfree_Redirect_Edge_Redirect_Edge Mul_interfree_Redirect_Edge_Color_Target Mul_interfree_Color_Target_Redirect_Edge Mul_interfree_Color_Target_Color_Target -lemma Mul_interfree_Mutator_Mutator: "\i < n; j < n; i \ j\ \ +lemma Mul_interfree_Mutator_Mutator: "\i < n; j < n; i \ j\ \ interfree_aux (Some (Mul_Mutator i n), {}, Some (Mul_Mutator j n))" apply(unfold Mul_Mutator_def) apply(interfree_aux) apply(simp_all add:mul_mutator_interfree) apply(simp_all add: mul_mutator_defs) -apply(tactic {* TRYALL (interfree_aux_tac @{context}) *}) -apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) +apply(tactic \TRYALL (interfree_aux_tac @{context})\) +apply(tactic \ALLGOALS (clarify_tac @{context})\) apply (simp_all add:nth_list_update) done -subsubsection {* Modular Parameterized Mutators *} +subsubsection \Modular Parameterized Mutators\ lemma Mul_Parameterized_Mutators: "0 \- \\Mul_mut_init n \ (\iMuts!i))\ @@ -152,7 +152,7 @@ apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update) done -subsection {* The Collector *} +subsection \The Collector\ definition Queue :: "mul_gar_coll_state \ nat" where "Queue \ \ length (filter (\i. \ Z i \ \M!(T i) \ Black) \Muts) \" @@ -170,25 +170,25 @@ lemmas mul_collector_defs = Proper_M_init_def Mul_Proper_def Safe_def -subsubsection {* Blackening Roots *} +subsubsection \Blackening Roots\ definition Mul_Blacken_Roots :: "nat \ mul_gar_coll_state ann_com" where "Mul_Blacken_Roots n \ \\Mul_Proper n\ \ind:=0;; \\Mul_Proper n \ \ind=0\ - WHILE \indM + WHILE \indM INV \\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \ind\length \M\ DO \\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \indM\ - IF \ind\Roots THEN - \\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \indM \ \ind\Roots\ + IF \ind\Roots THEN + \\Mul_Proper n \ (\i<\ind. i\Roots \ \M!i=Black) \ \indM \ \ind\Roots\ \M:=\M[\ind:=Black] FI;; \\Mul_Proper n \ (\i<\ind+1. i\Roots \ \M!i=Black) \ \indM\ - \ind:=\ind+1 + \ind:=\ind+1 OD" -lemma Mul_Blacken_Roots: - "\ Mul_Blacken_Roots n +lemma Mul_Blacken_Roots: + "\ Mul_Blacken_Roots n \\Mul_Proper n \ Roots \ Blacks \M\" apply (unfold Mul_Blacken_Roots_def) apply annhoare @@ -201,10 +201,10 @@ apply force done -subsubsection {* Propagating Black *} +subsubsection \Propagating Black\ definition Mul_PBInv :: "mul_gar_coll_state \ bool" where - "Mul_PBInv \ \\Safe \ \obc\Blacks \M \ \l<\Queue + "Mul_PBInv \ \\Safe \ \obc\Blacks \M \ \l<\Queue \ (\i<\ind. \BtoW(\E!i,\M)) \ \l\\Queue\" definition Mul_Auxk :: "mul_gar_coll_state \ bool" where @@ -212,49 +212,49 @@ definition Mul_Propagate_Black :: "nat \ mul_gar_coll_state ann_com" where "Mul_Propagate_Black n \ - \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M - \ (\Safe \ \l\\Queue \ \obc\Blacks \M)\ + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M + \ (\Safe \ \l\\Queue \ \obc\Blacks \M)\ \ind:=0;; - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \M \ Blacks \M\Blacks \M \ \bc\Blacks \M - \ (\Safe \ \l\\Queue \ \obc\Blacks \M) \ \ind=0\ - WHILE \indE - INV \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \M \ \bc\Blacks \M + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \M \ Blacks \M\Blacks \M \ \bc\Blacks \M + \ (\Safe \ \l\\Queue \ \obc\Blacks \M) \ \ind=0\ + WHILE \indE + INV \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \M \ \bc\Blacks \M \ \Mul_PBInv \ \ind\length \E\ - DO \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \M \ \bc\Blacks \M + DO \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \M \ \bc\Blacks \M \ \Mul_PBInv \ \indE\ - IF \M!(fst (\E!\ind))=Black THEN - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \M \ \bc\Blacks \M + IF \M!(fst (\E!\ind))=Black THEN + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \M \ \bc\Blacks \M \ \Mul_PBInv \ (\M!fst(\E!\ind))=Black \ \indE\ \k:=snd(\E!\ind);; - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \M \ \bc\Blacks \M - \ (\Safe \ \obc\Blacks \M \ \l<\Queue \ (\i<\ind. \BtoW(\E!i,\M)) - \ \l\\Queue \ \Mul_Auxk ) \ \kM \ \M!fst(\E!\ind)=Black + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \M \ \bc\Blacks \M + \ (\Safe \ \obc\Blacks \M \ \l<\Queue \ (\i<\ind. \BtoW(\E!i,\M)) + \ \l\\Queue \ \Mul_Auxk ) \ \kM \ \M!fst(\E!\ind)=Black \ \indE\ \\M:=\M[\k:=Black],,\ind:=\ind+1\ - ELSE \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \M \ \bc\Blacks \M + ELSE \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \M \ \bc\Blacks \M \ \Mul_PBInv \ \indE\ \IF \M!(fst (\E!\ind))\Black THEN \ind:=\ind+1 FI\ FI OD" -lemma Mul_Propagate_Black: - "\ Mul_Propagate_Black n - \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M +lemma Mul_Propagate_Black: + "\ Mul_Propagate_Black n + \\Mul_Proper n \ Roots\Blacks \M \ \obc\Blacks \M \ \bc\Blacks \M \ (\Safe \ \obc\Blacks \M \ \l<\Queue \ (\l\\Queue \ \obc\Blacks \M))\" apply(unfold Mul_Propagate_Black_def) apply annhoare apply(simp_all add:Mul_PBInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def) ---{* 8 subgoals left *} +--\8 subgoals left\ apply force apply force apply force apply(force simp add:BtoW_def Graph_defs) ---{* 4 subgoals left *} +--\4 subgoals left\ apply clarify apply(simp add: mul_collector_defs Graph12 Graph6 Graph7 Graph8) apply(disjE_tac) @@ -269,7 +269,7 @@ apply(force) apply(force) apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force) ---{* 2 subgoals left *} +--\2 subgoals left\ apply clarify apply(conjI_tac) apply(disjE_tac) @@ -278,7 +278,7 @@ apply(erule less_SucE) apply force apply (simp add:BtoW_def) ---{* 1 subgoal left *} +--\1 subgoal left\ apply clarify apply simp apply(disjE_tac) @@ -287,66 +287,66 @@ apply simp_all done -subsubsection {* Counting Black Nodes *} +subsubsection \Counting Black Nodes\ definition Mul_CountInv :: "mul_gar_coll_state \ nat \ bool" where "Mul_CountInv \ \ \ind. {i. i \Ma!i=Black}\\bc \" definition Mul_Count :: "nat \ mul_gar_coll_state ann_com" where - "Mul_Count n \ - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M - \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M) ) + "Mul_Count n \ + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M + \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M) ) \ \q \bc={}\ \ind:=0;; - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M - \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M) ) + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M + \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M) ) \ \q \bc={} \ \ind=0\ - WHILE \indM - INV \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ \Mul_CountInv \ind + WHILE \indM + INV \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ \Mul_CountInv \ind \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) \ \q \ind\length \M\ - DO \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ \Mul_CountInv \ind + DO \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ \Mul_CountInv \ind \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \indM\ - IF \M!\ind=Black - THEN \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ \Mul_CountInv \ind + \ \q \indM\ + IF \M!\ind=Black + THEN \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ \Mul_CountInv \ind \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) \ \q \indM \ \M!\ind=Black\ \bc:=insert \ind \bc FI;; - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ \Mul_CountInv (\ind+1) + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ \Mul_CountInv (\ind+1) \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) \ \q \indM\ \ind:=\ind+1 OD" - -lemma Mul_Count: - "\ Mul_Count n - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ Blacks \Ma\\bc - \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) + +lemma Mul_Count: + "\ Mul_Count n + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ Blacks \Ma\\bc + \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) \ \q" apply (unfold Mul_Count_def) apply annhoare apply(simp_all add:Mul_CountInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def) ---{* 7 subgoals left *} +--\7 subgoals left\ apply force apply force apply force ---{* 4 subgoals left *} +--\4 subgoals left\ apply clarify apply(conjI_tac) apply(disjE_tac) @@ -357,7 +357,7 @@ back apply force apply force ---{* 3 subgoals left *} +--\3 subgoals left\ apply clarify apply(conjI_tac) apply(disjE_tac) @@ -369,15 +369,15 @@ apply simp apply(rotate_tac -1) apply (force simp add:Blacks_def) ---{* 2 subgoals left *} +--\2 subgoals left\ apply force ---{* 1 subgoal left *} +--\1 subgoal left\ apply clarify apply(drule_tac x = "ind x" in le_imp_less_or_eq) apply (simp_all add:Blacks_def) done -subsubsection {* Appending garbage nodes to the free list *} +subsubsection \Appending garbage nodes to the free list\ axiomatization Append_to_free :: "nat \ edges \ edges" where @@ -391,30 +391,30 @@ "Mul_AppendInv \ \ \ind. (\i. ind\i \ iM \ i\Reach \E \ \M!i=Black)\" definition Mul_Append :: "nat \ mul_gar_coll_state ann_com" where - "Mul_Append n \ + "Mul_Append n \ \\Mul_Proper n \ Roots\Blacks \M \ \Safe\ \ind:=0;; \\Mul_Proper n \ Roots\Blacks \M \ \Safe \ \ind=0\ - WHILE \indM + WHILE \indM INV \\Mul_Proper n \ \Mul_AppendInv \ind \ \ind\length \M\ DO \\Mul_Proper n \ \Mul_AppendInv \ind \ \indM\ - IF \M!\ind=Black THEN - \\Mul_Proper n \ \Mul_AppendInv \ind \ \indM \ \M!\ind=Black\ - \M:=\M[\ind:=White] - ELSE - \\Mul_Proper n \ \Mul_AppendInv \ind \ \indM \ \ind\Reach \E\ + IF \M!\ind=Black THEN + \\Mul_Proper n \ \Mul_AppendInv \ind \ \indM \ \M!\ind=Black\ + \M:=\M[\ind:=White] + ELSE + \\Mul_Proper n \ \Mul_AppendInv \ind \ \indM \ \ind\Reach \E\ \E:=Append_to_free(\ind,\E) FI;; - \\Mul_Proper n \ \Mul_AppendInv (\ind+1) \ \indM\ + \\Mul_Proper n \ \Mul_AppendInv (\ind+1) \ \indM\ \ind:=\ind+1 OD" -lemma Mul_Append: - "\ Mul_Append n +lemma Mul_Append: + "\ Mul_Append n \\Mul_Proper n\" apply(unfold Mul_Append_def) apply annhoare -apply(simp_all add: mul_collector_defs Mul_AppendInv_def +apply(simp_all add: mul_collector_defs Mul_AppendInv_def Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) apply(force simp add:Blacks_def) apply(force simp add:Blacks_def) @@ -426,71 +426,71 @@ apply force done -subsubsection {* Collector *} +subsubsection \Collector\ definition Mul_Collector :: "nat \ mul_gar_coll_state ann_com" where "Mul_Collector n \ -\\Mul_Proper n\ -WHILE True INV \\Mul_Proper n\ -DO -Mul_Blacken_Roots n ;; -\\Mul_Proper n \ Roots\Blacks \M\ - \obc:={};; -\\Mul_Proper n \ Roots\Blacks \M \ \obc={}\ - \bc:=Roots;; -\\Mul_Proper n \ Roots\Blacks \M \ \obc={} \ \bc=Roots\ - \l:=0;; -\\Mul_Proper n \ Roots\Blacks \M \ \obc={} \ \bc=Roots \ \l=0\ - WHILE \l\Mul_Proper n \ Roots\Blacks \M \ \bc\Blacks \M \ - (\Safe \ (\l\\Queue \ \bc\Blacks \M) \ \l - DO \\Mul_Proper n \ Roots\Blacks \M \ \bc\Blacks \M +\\Mul_Proper n\ +WHILE True INV \\Mul_Proper n\ +DO +Mul_Blacken_Roots n ;; +\\Mul_Proper n \ Roots\Blacks \M\ + \obc:={};; +\\Mul_Proper n \ Roots\Blacks \M \ \obc={}\ + \bc:=Roots;; +\\Mul_Proper n \ Roots\Blacks \M \ \obc={} \ \bc=Roots\ + \l:=0;; +\\Mul_Proper n \ Roots\Blacks \M \ \obc={} \ \bc=Roots \ \l=0\ + WHILE \l\Mul_Proper n \ Roots\Blacks \M \ \bc\Blacks \M \ + (\Safe \ (\l\\Queue \ \bc\Blacks \M) \ \l + DO \\Mul_Proper n \ Roots\Blacks \M \ \bc\Blacks \M \ (\Safe \ \l\\Queue \ \bc\Blacks \M)\ \obc:=\bc;; - Mul_Propagate_Black n;; - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \M \ \bc\Blacks \M - \ (\Safe \ \obc\Blacks \M \ \l<\Queue - \ (\l\\Queue \ \obc\Blacks \M))\ + Mul_Propagate_Black n;; + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \M \ \bc\Blacks \M + \ (\Safe \ \obc\Blacks \M \ \l<\Queue + \ (\l\\Queue \ \obc\Blacks \M))\ \bc:={};; - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \M \ \bc\Blacks \M - \ (\Safe \ \obc\Blacks \M \ \l<\Queue - \ (\l\\Queue \ \obc\Blacks \M)) \ \bc={}\ + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \M \ \bc\Blacks \M + \ (\Safe \ \obc\Blacks \M \ \l<\Queue + \ (\l\\Queue \ \obc\Blacks \M)) \ \bc={}\ \ \Ma:=\M,, \q:=\Queue \;; - Mul_Count n;; - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ Blacks \Ma\\bc - \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q + Mul_Count n;; + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ Blacks \Ma\\bc + \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) + \ \q IF \obc=\bc THEN - \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ Blacks \Ma\\bc - \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \obc=\bc\ - \l:=\l+1 - ELSE \\Mul_Proper n \ Roots\Blacks \M - \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M - \ length \Ma=length \M \ Blacks \Ma\\bc - \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) - \ \q \obc\\bc\ - \l:=0 FI - OD;; - Mul_Append n + \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ Blacks \Ma\\bc + \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) + \ \q \obc=\bc\ + \l:=\l+1 + ELSE \\Mul_Proper n \ Roots\Blacks \M + \ \obc\Blacks \Ma \ Blacks \Ma\Blacks \M \ \bc\Blacks \M + \ length \Ma=length \M \ Blacks \Ma\\bc + \ (\Safe \ \obc\Blacks \Ma \ \l<\q \ (\q\\Queue \ \obc\Blacks \M)) + \ \q \obc\\bc\ + \l:=0 FI + OD;; + Mul_Append n OD" -lemmas mul_modules = Mul_Redirect_Edge_def Mul_Color_Target_def - Mul_Blacken_Roots_def Mul_Propagate_Black_def +lemmas mul_modules = Mul_Redirect_Edge_def Mul_Color_Target_def + Mul_Blacken_Roots_def Mul_Propagate_Black_def Mul_Count_def Mul_Append_def lemma Mul_Collector: - "\ Mul_Collector n + "\ Mul_Collector n \False\" apply(unfold Mul_Collector_def) apply annhoare -apply(simp_all only:pre.simps Mul_Blacken_Roots +apply(simp_all only:pre.simps Mul_Blacken_Roots Mul_Propagate_Black Mul_Count Mul_Append) apply(simp_all add:mul_modules) apply(simp_all add:mul_collector_defs Queue_def) @@ -505,10 +505,10 @@ apply force done -subsection {* Interference Freedom *} +subsection \Interference Freedom\ -lemma le_length_filter_update[rule_format]: - "\i. (\P (list!i) \ P j) \ ii. (\P (list!i) \ P j) \ i length(filter P list) \ length(filter P (list[i:=j]))" apply(induct_tac "list") apply(simp) @@ -518,8 +518,8 @@ apply(simp) done -lemma less_length_filter_update [rule_format]: - "\i. P j \ \(P (list!i)) \ ii. P j \ \(P (list!i)) \ i length(filter P list) < length(filter P (list[i:=j]))" apply(induct_tac "list") apply(simp) @@ -529,7 +529,7 @@ apply(simp) done -lemma Mul_interfree_Blacken_Roots_Redirect_Edge: "\0\j; j \ +lemma Mul_interfree_Blacken_Roots_Redirect_Edge: "\0\j; j \ interfree_aux (Some(Mul_Blacken_Roots n),{},Some(Mul_Redirect_Edge j n))" apply (unfold mul_modules) apply interfree_aux @@ -537,7 +537,7 @@ apply(simp_all add:Graph6 Graph9 Graph12 nth_list_update mul_mutator_defs mul_collector_defs) done -lemma Mul_interfree_Redirect_Edge_Blacken_Roots: "\0\j; j\ +lemma Mul_interfree_Redirect_Edge_Blacken_Roots: "\0\j; j\ interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Blacken_Roots n))" apply (unfold mul_modules) apply interfree_aux @@ -545,7 +545,7 @@ apply(simp_all add:mul_mutator_defs nth_list_update) done -lemma Mul_interfree_Blacken_Roots_Color_Target: "\0\j; j\ +lemma Mul_interfree_Blacken_Roots_Color_Target: "\0\j; j\ interfree_aux (Some(Mul_Blacken_Roots n),{},Some (Mul_Color_Target j n ))" apply (unfold mul_modules) apply interfree_aux @@ -553,7 +553,7 @@ apply(simp_all add:mul_mutator_defs mul_collector_defs nth_list_update Graph7 Graph8 Graph9 Graph12) done -lemma Mul_interfree_Color_Target_Blacken_Roots: "\0\j; j\ +lemma Mul_interfree_Color_Target_Blacken_Roots: "\0\j; j\ interfree_aux (Some(Mul_Color_Target j n ),{},Some (Mul_Blacken_Roots n ))" apply (unfold mul_modules) apply interfree_aux @@ -561,12 +561,12 @@ apply(simp_all add:mul_mutator_defs nth_list_update) done -lemma Mul_interfree_Propagate_Black_Redirect_Edge: "\0\j; j\ +lemma Mul_interfree_Propagate_Black_Redirect_Edge: "\0\j; j\ interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Redirect_Edge j n ))" apply (unfold mul_modules) apply interfree_aux apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_PBInv_def nth_list_update Graph6) ---{* 7 subgoals left *} +--\7 subgoals left\ apply clarify apply(disjE_tac) apply(simp_all add:Graph6) @@ -574,7 +574,7 @@ apply(rule conjI) apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) ---{* 6 subgoals left *} +--\6 subgoals left\ apply clarify apply(disjE_tac) apply(simp_all add:Graph6) @@ -582,7 +582,7 @@ apply(rule conjI) apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) ---{* 5 subgoals left *} +--\5 subgoals left\ apply clarify apply(disjE_tac) apply(simp_all add:Graph6) @@ -606,7 +606,7 @@ apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update) apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans) apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update) ---{* 4 subgoals left *} +--\4 subgoals left\ apply clarify apply(disjE_tac) apply(simp_all add:Graph6) @@ -630,7 +630,7 @@ apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update) apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans) apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update) ---{* 3 subgoals left *} +--\3 subgoals left\ apply clarify apply(disjE_tac) apply(simp_all add:Graph6) @@ -686,7 +686,7 @@ apply (force simp add: nth_list_update) apply(rule impI, (rule disjI2)+, erule le_trans) apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update) ---{* 2 subgoals left *} +--\2 subgoals left\ apply clarify apply(rule conjI) apply(disjE_tac) @@ -741,7 +741,7 @@ apply(case_tac "R (Muts x ! j)= ind x") apply(simp add:nth_list_update) apply(simp add:nth_list_update) -apply(disjE_tac) +apply(disjE_tac) apply simp_all apply(conjI_tac) apply(rule impI) @@ -756,7 +756,7 @@ apply(rule disjI1, erule less_le_trans) apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply force ---{* 1 subgoal left *} +--\1 subgoal left\ apply clarify apply(disjE_tac) apply(simp_all add:Graph6) @@ -782,7 +782,7 @@ apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update) done -lemma Mul_interfree_Redirect_Edge_Propagate_Black: "\0\j; j\ +lemma Mul_interfree_Redirect_Edge_Propagate_Black: "\0\j; j\ interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Propagate_Black n))" apply (unfold mul_modules) apply interfree_aux @@ -790,12 +790,12 @@ apply(simp_all add:mul_mutator_defs nth_list_update) done -lemma Mul_interfree_Propagate_Black_Color_Target: "\0\j; j\ +lemma Mul_interfree_Propagate_Black_Color_Target: "\0\j; j\ interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Color_Target j n ))" apply (unfold mul_modules) apply interfree_aux apply(simp_all add: mul_collector_defs mul_mutator_defs) ---{* 7 subgoals left *} +--\7 subgoals left\ apply clarify apply (simp add:Graph7 Graph8 Graph12) apply(disjE_tac) @@ -803,9 +803,9 @@ apply(case_tac "M x!(T (Muts x!j))=Black") apply(rule disjI2,rule disjI1, erule le_trans) apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10) - apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) + apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9) ---{* 6 subgoals left *} +--\6 subgoals left\ apply clarify apply (simp add:Graph7 Graph8 Graph12) apply(disjE_tac) @@ -813,13 +813,13 @@ apply(case_tac "M x!(T (Muts x!j))=Black") apply(rule disjI2,rule disjI1, erule le_trans) apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10) - apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) + apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9) ---{* 5 subgoals left *} +--\5 subgoals left\ apply clarify apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12) apply(disjE_tac) - apply(simp add:Graph7 Graph8 Graph12) + apply(simp add:Graph7 Graph8 Graph12) apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9) apply(case_tac "M x!(T (Muts x!j))=Black") apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans) @@ -832,8 +832,8 @@ apply(simp add:Graph10) apply(erule le_trans) apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10) -apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) ---{* 4 subgoals left *} +apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) +--\4 subgoals left\ apply clarify apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12) apply(disjE_tac) @@ -850,8 +850,8 @@ apply(simp add:Graph10) apply(erule le_trans) apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10) -apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) ---{* 3 subgoals left *} +apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) +--\3 subgoals left\ apply clarify apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12) apply(case_tac "M x!(T (Muts x!j))=Black") @@ -864,10 +864,10 @@ apply((rule disjI2)+,erule le_trans) apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10) apply(rule conjI) - apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) + apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) apply (force simp add:nth_list_update) ---{* 2 subgoals left *} -apply clarify +--\2 subgoals left\ +apply clarify apply(simp add:Mul_Auxk_def Graph7 Graph8 Graph12) apply(case_tac "M x!(T (Muts x!j))=Black") apply(simp add:Graph10) @@ -881,13 +881,13 @@ apply((rule impI)+) apply simp apply(erule disjE) - apply(rule disjI1, erule less_le_trans) + apply(rule disjI1, erule less_le_trans) apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10) apply force apply(rule conjI) - apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) + apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) apply (force simp add:nth_list_update) ---{* 1 subgoal left *} +--\1 subgoal left\ apply clarify apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12) apply(case_tac "M x!(T (Muts x!j))=Black") @@ -899,10 +899,10 @@ apply(erule conjE) apply((rule disjI2)+,erule le_trans) apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10) -apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) +apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) done -lemma Mul_interfree_Color_Target_Propagate_Black: "\0\j; j\ +lemma Mul_interfree_Color_Target_Propagate_Black: "\0\j; j\ interfree_aux (Some(Mul_Color_Target j n),{},Some(Mul_Propagate_Black n ))" apply (unfold mul_modules) apply interfree_aux @@ -910,11 +910,11 @@ apply(simp_all add:mul_mutator_defs nth_list_update) done -lemma Mul_interfree_Count_Redirect_Edge: "\0\j; j\ +lemma Mul_interfree_Count_Redirect_Edge: "\0\j; j\ interfree_aux (Some(Mul_Count n ),{},Some(Mul_Redirect_Edge j n))" apply (unfold mul_modules) apply interfree_aux ---{* 9 subgoals left *} +--\9 subgoals left\ apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def Graph6) apply clarify apply disjE_tac @@ -928,9 +928,9 @@ apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(simp add:Graph6) ---{* 8 subgoals left *} +--\8 subgoals left\ apply(simp add:mul_mutator_defs nth_list_update) ---{* 7 subgoals left *} +--\7 subgoals left\ apply(simp add:mul_mutator_defs mul_collector_defs) apply clarify apply disjE_tac @@ -944,7 +944,7 @@ apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(simp add:Graph6) ---{* 6 subgoals left *} +--\6 subgoals left\ apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def) apply clarify apply disjE_tac @@ -958,7 +958,7 @@ apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(simp add:Graph6) ---{* 5 subgoals left *} +--\5 subgoals left\ apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def) apply clarify apply disjE_tac @@ -972,7 +972,7 @@ apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(simp add:Graph6) ---{* 4 subgoals left *} +--\4 subgoals left\ apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def) apply clarify apply disjE_tac @@ -986,9 +986,9 @@ apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(simp add:Graph6) ---{* 3 subgoals left *} +--\3 subgoals left\ apply(simp add:mul_mutator_defs nth_list_update) ---{* 2 subgoals left *} +--\2 subgoals left\ apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def) apply clarify apply disjE_tac @@ -1002,11 +1002,11 @@ apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(simp add:Graph6) ---{* 1 subgoal left *} +--\1 subgoal left\ apply(simp add:mul_mutator_defs nth_list_update) done -lemma Mul_interfree_Redirect_Edge_Count: "\0\j; j\ +lemma Mul_interfree_Redirect_Edge_Count: "\0\j; j\ interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Count n ))" apply (unfold mul_modules) apply interfree_aux @@ -1014,12 +1014,12 @@ apply(simp_all add:mul_mutator_defs nth_list_update) done -lemma Mul_interfree_Count_Color_Target: "\0\j; j\ +lemma Mul_interfree_Count_Color_Target: "\0\j; j\ interfree_aux (Some(Mul_Count n ),{},Some(Mul_Color_Target j n))" apply (unfold mul_modules) apply interfree_aux apply(simp_all add:mul_collector_defs mul_mutator_defs Mul_CountInv_def) ---{* 6 subgoals left *} +--\6 subgoals left\ apply clarify apply disjE_tac apply (simp add: Graph7 Graph8 Graph12) @@ -1033,7 +1033,7 @@ apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11) apply (simp add: Graph7 Graph8 Graph12) apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9) ---{* 5 subgoals left *} +--\5 subgoals left\ apply clarify apply disjE_tac apply (simp add: Graph7 Graph8 Graph12) @@ -1047,7 +1047,7 @@ apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11) apply (simp add: Graph7 Graph8 Graph12) apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9) ---{* 4 subgoals left *} +--\4 subgoals left\ apply clarify apply disjE_tac apply (simp add: Graph7 Graph8 Graph12) @@ -1061,7 +1061,7 @@ apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11) apply (simp add: Graph7 Graph8 Graph12) apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9) ---{* 3 subgoals left *} +--\3 subgoals left\ apply clarify apply disjE_tac apply (simp add: Graph7 Graph8 Graph12) @@ -1075,7 +1075,7 @@ apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11) apply (simp add: Graph7 Graph8 Graph12) apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9) ---{* 2 subgoals left *} +--\2 subgoals left\ apply clarify apply disjE_tac apply (simp add: Graph7 Graph8 Graph12 nth_list_update) @@ -1093,7 +1093,7 @@ apply(rule conjI) apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9) apply (simp add: nth_list_update) ---{* 1 subgoal left *} +--\1 subgoal left\ apply clarify apply disjE_tac apply (simp add: Graph7 Graph8 Graph12) @@ -1109,7 +1109,7 @@ apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9) done -lemma Mul_interfree_Color_Target_Count: "\0\j; j\ +lemma Mul_interfree_Color_Target_Count: "\0\j; j\ interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Count n ))" apply (unfold mul_modules) apply interfree_aux @@ -1117,137 +1117,137 @@ apply(simp_all add:mul_mutator_defs nth_list_update) done -lemma Mul_interfree_Append_Redirect_Edge: "\0\j; j\ +lemma Mul_interfree_Append_Redirect_Edge: "\0\j; j\ interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))" apply (unfold mul_modules) apply interfree_aux -apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) +apply(tactic \ALLGOALS (clarify_tac @{context})\) apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def) apply(erule_tac x=j in allE, force dest:Graph3)+ done -lemma Mul_interfree_Redirect_Edge_Append: "\0\j; j\ +lemma Mul_interfree_Redirect_Edge_Append: "\0\j; j\ interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))" apply (unfold mul_modules) apply interfree_aux -apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) +apply(tactic \ALLGOALS (clarify_tac @{context})\) apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def mul_mutator_defs nth_list_update) done -lemma Mul_interfree_Append_Color_Target: "\0\j; j\ +lemma Mul_interfree_Append_Color_Target: "\0\j; j\ interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))" apply (unfold mul_modules) apply interfree_aux -apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) -apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1 +apply(tactic \ALLGOALS (clarify_tac @{context})\) +apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update) done -lemma Mul_interfree_Color_Target_Append: "\0\j; j\ +lemma Mul_interfree_Color_Target_Append: "\0\j; j\ interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))" apply (unfold mul_modules) apply interfree_aux -apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) +apply(tactic \ALLGOALS (clarify_tac @{context})\) apply(simp_all add: mul_mutator_defs nth_list_update) apply(simp add:Mul_AppendInv_def Append_to_free0) done -subsubsection {* Interference freedom Collector-Mutator *} +subsubsection \Interference freedom Collector-Mutator\ -lemmas mul_collector_mutator_interfree = - Mul_interfree_Blacken_Roots_Redirect_Edge Mul_interfree_Blacken_Roots_Color_Target - Mul_interfree_Propagate_Black_Redirect_Edge Mul_interfree_Propagate_Black_Color_Target - Mul_interfree_Count_Redirect_Edge Mul_interfree_Count_Color_Target - Mul_interfree_Append_Redirect_Edge Mul_interfree_Append_Color_Target - Mul_interfree_Redirect_Edge_Blacken_Roots Mul_interfree_Color_Target_Blacken_Roots - Mul_interfree_Redirect_Edge_Propagate_Black Mul_interfree_Color_Target_Propagate_Black - Mul_interfree_Redirect_Edge_Count Mul_interfree_Color_Target_Count +lemmas mul_collector_mutator_interfree = + Mul_interfree_Blacken_Roots_Redirect_Edge Mul_interfree_Blacken_Roots_Color_Target + Mul_interfree_Propagate_Black_Redirect_Edge Mul_interfree_Propagate_Black_Color_Target + Mul_interfree_Count_Redirect_Edge Mul_interfree_Count_Color_Target + Mul_interfree_Append_Redirect_Edge Mul_interfree_Append_Color_Target + Mul_interfree_Redirect_Edge_Blacken_Roots Mul_interfree_Color_Target_Blacken_Roots + Mul_interfree_Redirect_Edge_Propagate_Black Mul_interfree_Color_Target_Propagate_Black + Mul_interfree_Redirect_Edge_Count Mul_interfree_Color_Target_Count Mul_interfree_Redirect_Edge_Append Mul_interfree_Color_Target_Append -lemma Mul_interfree_Collector_Mutator: "j +lemma Mul_interfree_Collector_Mutator: "j interfree_aux (Some (Mul_Collector n), {}, Some (Mul_Mutator j n))" apply(unfold Mul_Collector_def Mul_Mutator_def) apply interfree_aux apply(simp_all add:mul_collector_mutator_interfree) apply(unfold mul_modules mul_collector_defs mul_mutator_defs) -apply(tactic {* TRYALL (interfree_aux_tac @{context}) *}) ---{* 42 subgoals left *} +apply(tactic \TRYALL (interfree_aux_tac @{context})\) +--\42 subgoals left\ apply (clarify,simp add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)+ ---{* 24 subgoals left *} +--\24 subgoals left\ apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) ---{* 14 subgoals left *} -apply(tactic {* TRYALL (clarify_tac @{context}) *}) +--\14 subgoals left\ +apply(tactic \TRYALL (clarify_tac @{context})\) apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) -apply(tactic {* TRYALL (rtac conjI) *}) -apply(tactic {* TRYALL (rtac impI) *}) -apply(tactic {* TRYALL (etac disjE) *}) -apply(tactic {* TRYALL (etac conjE) *}) -apply(tactic {* TRYALL (etac disjE) *}) -apply(tactic {* TRYALL (etac disjE) *}) ---{* 72 subgoals left *} +apply(tactic \TRYALL (rtac conjI)\) +apply(tactic \TRYALL (rtac impI)\) +apply(tactic \TRYALL (etac disjE)\) +apply(tactic \TRYALL (etac conjE)\) +apply(tactic \TRYALL (etac disjE)\) +apply(tactic \TRYALL (etac disjE)\) +--\72 subgoals left\ apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) ---{* 35 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}]) *}) ---{* 28 subgoals left *} -apply(tactic {* TRYALL (etac conjE) *}) -apply(tactic {* TRYALL (etac disjE) *}) ---{* 34 subgoals left *} +--\35 subgoals left\ +apply(tactic \TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}])\) +--\28 subgoals left\ +apply(tactic \TRYALL (etac conjE)\) +apply(tactic \TRYALL (etac disjE)\) +--\34 subgoals left\ apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(case_tac [!] "M x!(T (Muts x ! j))=Black") apply(simp_all add:Graph10) ---{* 47 subgoals left *} -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *}) ---{* 41 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, +--\47 subgoals left\ +apply(tactic \TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}])\) +--\41 subgoals left\ +apply(tactic \TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{context} addsimps - [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *}) ---{* 35 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *}) ---{* 31 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *}) ---{* 29 subgoals left *} -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *}) ---{* 25 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, + [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])])\) +--\35 subgoals left\ +apply(tactic \TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}])\) +--\31 subgoals left\ +apply(tactic \TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}])\) +--\29 subgoals left\ +apply(tactic \TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}])\) +--\25 subgoals left\ +apply(tactic \TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{context} addsimps - [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *}) ---{* 10 subgoals left *} + [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])])\) +--\10 subgoals left\ apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+ done -subsubsection {* Interference freedom Mutator-Collector *} +subsubsection \Interference freedom Mutator-Collector\ -lemma Mul_interfree_Mutator_Collector: " j < n \ +lemma Mul_interfree_Mutator_Collector: " j < n \ interfree_aux (Some (Mul_Mutator j n), {}, Some (Mul_Collector n))" apply(unfold Mul_Collector_def Mul_Mutator_def) apply interfree_aux apply(simp_all add:mul_collector_mutator_interfree) apply(unfold mul_modules mul_collector_defs mul_mutator_defs) -apply(tactic {* TRYALL (interfree_aux_tac @{context}) *}) ---{* 76 subgoals left *} +apply(tactic \TRYALL (interfree_aux_tac @{context})\) +--\76 subgoals left\ apply (clarsimp simp add: nth_list_update)+ ---{* 56 subgoals left *} +--\56 subgoals left\ apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+ done -subsubsection {* The Multi-Mutator Garbage Collection Algorithm *} +subsubsection \The Multi-Mutator Garbage Collection Algorithm\ -text {* The total number of verification conditions is 328 *} +text \The total number of verification conditions is 328\ -lemma Mul_Gar_Coll: - "\- \\Mul_Proper n \ \Mul_mut_init n \ (\iMuts!i))\ - COBEGIN +lemma Mul_Gar_Coll: + "\- \\Mul_Proper n \ \Mul_mut_init n \ (\iMuts!i))\ + COBEGIN Mul_Collector n \False\ - \ + \ SCHEME [0\ j< n] Mul_Mutator j n - \False\ - COEND + \False\ + COEND \False\" apply oghoare ---{* Strengthening the precondition *} +--\Strengthening the precondition\ apply(rule Int_greatest) apply (case_tac n) apply(force simp add: Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append) @@ -1257,15 +1257,15 @@ apply(case_tac i) apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append) apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt) ---{* Collector *} +--\Collector\ apply(rule Mul_Collector) ---{* Mutator *} +--\Mutator\ apply(erule Mul_Mutator) ---{* Interference freedom *} +--\Interference freedom\ apply(simp add:Mul_interfree_Collector_Mutator) apply(simp add:Mul_interfree_Mutator_Collector) apply(simp add:Mul_interfree_Mutator_Mutator) ---{* Weakening of the postcondition *} +--\Weakening of the postcondition\ apply(case_tac n) apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append) apply(simp add:Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append) diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/OG_Com.thy --- a/src/HOL/Hoare_Parallel/OG_Com.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Com.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,34 +1,34 @@ -chapter {* The Owicki-Gries Method *} +chapter \The Owicki-Gries Method\ -section {* Abstract Syntax *} +section \Abstract Syntax\ theory OG_Com imports Main begin -text {* Type abbreviations for boolean expressions and assertions: *} +text \Type abbreviations for boolean expressions and assertions:\ type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" -text {* The syntax of commands is defined by two mutually recursive +text \The syntax of commands is defined by two mutually recursive datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a -com"} for non-annotated commands. *} +com"} for non-annotated commands.\ -datatype 'a ann_com = - AnnBasic "('a assn)" "('a \ 'a)" - | AnnSeq "('a ann_com)" "('a ann_com)" - | AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)" - | AnnCond2 "('a assn)" "('a bexp)" "('a ann_com)" - | AnnWhile "('a assn)" "('a bexp)" "('a assn)" "('a ann_com)" - | AnnAwait "('a assn)" "('a bexp)" "('a com)" -and 'a com = +datatype 'a ann_com = + AnnBasic "('a assn)" "('a \ 'a)" + | AnnSeq "('a ann_com)" "('a ann_com)" + | AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)" + | AnnCond2 "('a assn)" "('a bexp)" "('a ann_com)" + | AnnWhile "('a assn)" "('a bexp)" "('a assn)" "('a ann_com)" + | AnnAwait "('a assn)" "('a bexp)" "('a com)" +and 'a com = Parallel "('a ann_com option \ 'a assn) list" - | Basic "('a \ 'a)" - | Seq "('a com)" "('a com)" - | Cond "('a bexp)" "('a com)" "('a com)" + | Basic "('a \ 'a)" + | Seq "('a com)" "('a com)" + | Cond "('a bexp)" "('a com)" "('a com)" | While "('a bexp)" "('a assn)" "('a com)" -text {* The function @{text pre} extracts the precondition of an -annotated command: *} +text \The function @{text pre} extracts the precondition of an +annotated command:\ primrec pre ::"'a ann_com \ 'a assn" where "pre (AnnBasic r f) = r" @@ -38,7 +38,7 @@ | "pre (AnnWhile r b i c) = r" | "pre (AnnAwait r b c) = r" -text {* Well-formedness predicate for atomic programs: *} +text \Well-formedness predicate for atomic programs:\ primrec atom_com :: "'a com \ bool" where "atom_com (Parallel Ts) = False" @@ -46,5 +46,5 @@ | "atom_com (Seq c1 c2) = (atom_com c1 \ atom_com c2)" | "atom_com (Cond b c1 c2) = (atom_com c1 \ atom_com c2)" | "atom_com (While b i c) = atom_com c" - + end \ No newline at end of file diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/OG_Examples.thy --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,206 +1,206 @@ -section {* Examples *} +section \Examples\ theory OG_Examples imports OG_Syntax begin -subsection {* Mutual Exclusion *} +subsection \Mutual Exclusion\ -subsubsection {* Peterson's Algorithm I*} +subsubsection \Peterson's Algorithm I\ -text {* Eike Best. "Semantics of Sequential and Parallel Programs", page 217. *} +text \Eike Best. "Semantics of Sequential and Parallel Programs", page 217.\ record Petersons_mutex_1 = pr1 :: nat pr2 :: nat in1 :: bool - in2 :: bool + in2 :: bool hold :: nat -lemma Petersons_mutex_1: - "\- \\pr1=0 \ \\in1 \ \pr2=0 \ \\in2 \ - COBEGIN \\pr1=0 \ \\in1\ - WHILE True INV \\pr1=0 \ \\in1\ - DO - \\pr1=0 \ \\in1\ \ \in1:=True,,\pr1:=1 \;; - \\pr1=1 \ \in1\ \ \hold:=1,,\pr1:=2 \;; - \\pr1=2 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)\ - AWAIT (\\in2 \ \(\hold=1)) THEN \pr1:=3 END;; - \\pr1=3 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)\ - \\in1:=False,,\pr1:=0\ - OD \\pr1=0 \ \\in1\ - \ - \\pr2=0 \ \\in2\ - WHILE True INV \\pr2=0 \ \\in2\ - DO - \\pr2=0 \ \\in2\ \ \in2:=True,,\pr2:=1 \;; - \\pr2=1 \ \in2\ \ \hold:=2,,\pr2:=2 \;; - \\pr2=2 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))\ - AWAIT (\\in1 \ \(\hold=2)) THEN \pr2:=3 END;; - \\pr2=3 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))\ - \\in2:=False,,\pr2:=0\ - OD \\pr2=0 \ \\in2\ - COEND +lemma Petersons_mutex_1: + "\- \\pr1=0 \ \\in1 \ \pr2=0 \ \\in2 \ + COBEGIN \\pr1=0 \ \\in1\ + WHILE True INV \\pr1=0 \ \\in1\ + DO + \\pr1=0 \ \\in1\ \ \in1:=True,,\pr1:=1 \;; + \\pr1=1 \ \in1\ \ \hold:=1,,\pr1:=2 \;; + \\pr1=2 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)\ + AWAIT (\\in2 \ \(\hold=1)) THEN \pr1:=3 END;; + \\pr1=3 \ \in1 \ (\hold=1 \ \hold=2 \ \pr2=2)\ + \\in1:=False,,\pr1:=0\ + OD \\pr1=0 \ \\in1\ + \ + \\pr2=0 \ \\in2\ + WHILE True INV \\pr2=0 \ \\in2\ + DO + \\pr2=0 \ \\in2\ \ \in2:=True,,\pr2:=1 \;; + \\pr2=1 \ \in2\ \ \hold:=2,,\pr2:=2 \;; + \\pr2=2 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))\ + AWAIT (\\in1 \ \(\hold=2)) THEN \pr2:=3 END;; + \\pr2=3 \ \in2 \ (\hold=2 \ (\hold=1 \ \pr1=2))\ + \\in2:=False,,\pr2:=0\ + OD \\pr2=0 \ \\in2\ + COEND \\pr1=0 \ \\in1 \ \pr2=0 \ \\in2\" apply oghoare ---{* 104 verification conditions. *} +--\104 verification conditions.\ apply auto done -subsubsection {*Peterson's Algorithm II: A Busy Wait Solution *} - -text {* Apt and Olderog. "Verification of sequential and concurrent Programs", page 282. *} +subsubsection \Peterson's Algorithm II: A Busy Wait Solution\ + +text \Apt and Olderog. "Verification of sequential and concurrent Programs", page 282.\ record Busy_wait_mutex = flag1 :: bool flag2 :: bool turn :: nat - after1 :: bool + after1 :: bool after2 :: bool -lemma Busy_wait_mutex: - "\- \True\ - \flag1:=False,, \flag2:=False,, - COBEGIN \\\flag1\ - WHILE True - INV \\\flag1\ - DO \\\flag1\ \ \flag1:=True,,\after1:=False \;; - \\flag1 \ \\after1\ \ \turn:=1,,\after1:=True \;; - \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ - WHILE \(\flag2 \ \turn=2) - INV \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ - DO \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ SKIP OD;; +lemma Busy_wait_mutex: + "\- \True\ + \flag1:=False,, \flag2:=False,, + COBEGIN \\\flag1\ + WHILE True + INV \\\flag1\ + DO \\\flag1\ \ \flag1:=True,,\after1:=False \;; + \\flag1 \ \\after1\ \ \turn:=1,,\after1:=True \;; + \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ + WHILE \(\flag2 \ \turn=2) + INV \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ + DO \\flag1 \ \after1 \ (\turn=1 \ \turn=2)\ SKIP OD;; \\flag1 \ \after1 \ (\flag2 \ \after2 \ \turn=2)\ - \flag1:=False - OD - \False\ - \ - \\\flag2\ - WHILE True - INV \\\flag2\ - DO \\\flag2\ \ \flag2:=True,,\after2:=False \;; - \\flag2 \ \\after2\ \ \turn:=2,,\after2:=True \;; - \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ - WHILE \(\flag1 \ \turn=1) - INV \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ - DO \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ SKIP OD;; - \\flag2 \ \after2 \ (\flag1 \ \after1 \ \turn=1)\ - \flag2:=False - OD - \False\ - COEND + \flag1:=False + OD + \False\ + \ + \\\flag2\ + WHILE True + INV \\\flag2\ + DO \\\flag2\ \ \flag2:=True,,\after2:=False \;; + \\flag2 \ \\after2\ \ \turn:=2,,\after2:=True \;; + \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ + WHILE \(\flag1 \ \turn=1) + INV \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ + DO \\flag2 \ \after2 \ (\turn=1 \ \turn=2)\ SKIP OD;; + \\flag2 \ \after2 \ (\flag1 \ \after1 \ \turn=1)\ + \flag2:=False + OD + \False\ + COEND \False\" apply oghoare ---{* 122 vc *} +--\122 vc\ apply auto done -subsubsection {* Peterson's Algorithm III: A Solution using Semaphores *} +subsubsection \Peterson's Algorithm III: A Solution using Semaphores\ record Semaphores_mutex = out :: bool who :: nat -lemma Semaphores_mutex: - "\- \i\j\ - \out:=True ,, - COBEGIN \i\j\ - WHILE True INV \i\j\ - DO \i\j\ AWAIT \out THEN \out:=False,, \who:=i END;; - \\\out \ \who=i \ i\j\ \out:=True OD - \False\ - \ - \i\j\ - WHILE True INV \i\j\ - DO \i\j\ AWAIT \out THEN \out:=False,,\who:=j END;; - \\\out \ \who=j \ i\j\ \out:=True OD - \False\ - COEND +lemma Semaphores_mutex: + "\- \i\j\ + \out:=True ,, + COBEGIN \i\j\ + WHILE True INV \i\j\ + DO \i\j\ AWAIT \out THEN \out:=False,, \who:=i END;; + \\\out \ \who=i \ i\j\ \out:=True OD + \False\ + \ + \i\j\ + WHILE True INV \i\j\ + DO \i\j\ AWAIT \out THEN \out:=False,,\who:=j END;; + \\\out \ \who=j \ i\j\ \out:=True OD + \False\ + COEND \False\" apply oghoare ---{* 38 vc *} +--\38 vc\ apply auto done -subsubsection {* Peterson's Algorithm III: Parameterized version: *} +subsubsection \Peterson's Algorithm III: Parameterized version:\ -lemma Semaphores_parameterized_mutex: - "0 \- \True\ - \out:=True ,, +lemma Semaphores_parameterized_mutex: + "0 \- \True\ + \out:=True ,, COBEGIN SCHEME [0\ i< n] - \True\ - WHILE True INV \True\ - DO \True\ AWAIT \out THEN \out:=False,, \who:=i END;; + \True\ + WHILE True INV \True\ + DO \True\ AWAIT \out THEN \out:=False,, \who:=i END;; \\\out \ \who=i\ \out:=True OD - \False\ + \False\ COEND - \False\" + \False\" apply oghoare ---{* 20 vc *} +--\20 vc\ apply auto done -subsubsection{* The Ticket Algorithm *} +subsubsection\The Ticket Algorithm\ record Ticket_mutex = num :: nat nextv :: nat turn :: "nat list" - index :: nat + index :: nat -lemma Ticket_mutex: - "\ 0n=length \turn \ 0<\nextv \ (\k l. k l k\l +lemma Ticket_mutex: + "\ 0n=length \turn \ 0<\nextv \ (\k l. k l k\l \ \turn!k < \num \ (\turn!k =0 \ \turn!k\\turn!l))\ \ - \ \- \n=length \turn\ + \ \- \n=length \turn\ \index:= 0,, - WHILE \index < n INV \n=length \turn \ (\i<\index. \turn!i=0)\ + WHILE \index < n INV \n=length \turn \ (\i<\index. \turn!i=0)\ DO \turn:= \turn[\index:=0],, \index:=\index +1 OD,, - \num:=1 ,, \nextv:=1 ,, + \num:=1 ,, \nextv:=1 ,, COBEGIN SCHEME [0\ i< n] - \\I\ - WHILE True INV \\I\ - DO \\I\ \ \turn :=\turn[i:=\num],, \num:=\num+1 \;; + \\I\ + WHILE True INV \\I\ + DO \\I\ \ \turn :=\turn[i:=\num],, \num:=\num+1 \;; \\I\ WAIT \turn!i=\nextv END;; \\I \ \turn!i=\nextv\ \nextv:=\nextv+1 OD - \False\ + \False\ COEND - \False\" + \False\" apply oghoare ---{* 35 vc *} +--\35 vc\ apply simp_all ---{* 21 vc *} -apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) ---{* 11 vc *} +--\21 vc\ +apply(tactic \ALLGOALS (clarify_tac @{context})\) +--\11 vc\ apply simp_all -apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) ---{* 10 subgoals left *} +apply(tactic \ALLGOALS (clarify_tac @{context})\) +--\10 subgoals left\ apply(erule less_SucE) apply simp apply simp ---{* 9 subgoals left *} +--\9 subgoals left\ apply(case_tac "i=k") apply force apply simp apply(case_tac "i=l") apply force apply force ---{* 8 subgoals left *} +--\8 subgoals left\ prefer 8 apply force apply force ---{* 6 subgoals left *} +--\6 subgoals left\ prefer 6 apply(erule_tac x=i in allE) apply fastforce ---{* 5 subgoals left *} +--\5 subgoals left\ prefer 5 apply(case_tac [!] "j=k") ---{* 10 subgoals left *} +--\10 subgoals left\ apply simp_all apply(erule_tac x=k in allE) apply force ---{* 9 subgoals left *} +--\9 subgoals left\ apply(case_tac "j=l") apply simp apply(erule_tac x=k in allE) @@ -211,7 +211,7 @@ apply(erule_tac x=k in allE) apply(erule_tac x=l in allE) apply force ---{* 8 subgoals left *} +--\8 subgoals left\ apply force apply(case_tac "j=l") apply simp @@ -220,21 +220,21 @@ apply force apply force apply force ---{* 5 subgoals left *} +--\5 subgoals left\ apply(erule_tac x=k in allE) apply(erule_tac x=l in allE) apply(case_tac "j=l") apply force apply force apply force ---{* 3 subgoals left *} +--\3 subgoals left\ apply(erule_tac x=k in allE) apply(erule_tac x=l in allE) apply(case_tac "j=l") apply force apply force apply force ---{* 1 subgoals left *} +--\1 subgoals left\ apply(erule_tac x=k in allE) apply(erule_tac x=l in allE) apply(case_tac "j=l") @@ -242,11 +242,11 @@ apply force done -subsection{* Parallel Zero Search *} +subsection\Parallel Zero Search\ -text {* Synchronized Zero Search. Zero-6 *} +text \Synchronized Zero Search. Zero-6\ -text {*Apt and Olderog. "Verification of sequential and concurrent Programs" page 294: *} +text \Apt and Olderog. "Verification of sequential and concurrent Programs" page 294:\ record Zero_search = turn :: nat @@ -254,87 +254,87 @@ x :: nat y :: nat -lemma Zero_search: - "\I1= \ a\\x \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) - \ (\\found \ a<\ x \ f(\x)\0) \ ; - I2= \\y\a+1 \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) - \ (\\found \ \y\a \ f(\y)\0) \ \ \ - \- \\ u. f(u)=0\ - \turn:=1,, \found:= False,, - \x:=a,, \y:=a+1 ,, - COBEGIN \\I1\ - WHILE \\found - INV \\I1\ - DO \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ - WAIT \turn=1 END;; - \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ - \turn:=2;; - \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ - \ \x:=\x+1,, - IF f(\x)=0 THEN \found:=True ELSE SKIP FI\ - OD;; - \\I1 \ \found\ - \turn:=2 - \\I1 \ \found\ - \ - \\I2\ - WHILE \\found - INV \\I2\ - DO \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ - WAIT \turn=2 END;; - \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ - \turn:=1;; - \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ - \ \y:=(\y - 1),, - IF f(\y)=0 THEN \found:=True ELSE SKIP FI\ - OD;; - \\I2 \ \found\ - \turn:=1 - \\I2 \ \found\ - COEND +lemma Zero_search: + "\I1= \ a\\x \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) + \ (\\found \ a<\ x \ f(\x)\0) \ ; + I2= \\y\a+1 \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) + \ (\\found \ \y\a \ f(\y)\0) \ \ \ + \- \\ u. f(u)=0\ + \turn:=1,, \found:= False,, + \x:=a,, \y:=a+1 ,, + COBEGIN \\I1\ + WHILE \\found + INV \\I1\ + DO \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ + WAIT \turn=1 END;; + \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ + \turn:=2;; + \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ + \ \x:=\x+1,, + IF f(\x)=0 THEN \found:=True ELSE SKIP FI\ + OD;; + \\I1 \ \found\ + \turn:=2 + \\I1 \ \found\ + \ + \\I2\ + WHILE \\found + INV \\I2\ + DO \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ + WAIT \turn=2 END;; + \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ + \turn:=1;; + \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ + \ \y:=(\y - 1),, + IF f(\y)=0 THEN \found:=True ELSE SKIP FI\ + OD;; + \\I2 \ \found\ + \turn:=1 + \\I2 \ \found\ + COEND \f(\x)=0 \ f(\y)=0\" apply oghoare ---{* 98 verification conditions *} -apply auto ---{* auto takes about 3 minutes !! *} +--\98 verification conditions\ +apply auto +--\auto takes about 3 minutes !!\ done -text {* Easier Version: without AWAIT. Apt and Olderog. page 256: *} +text \Easier Version: without AWAIT. Apt and Olderog. page 256:\ -lemma Zero_Search_2: -"\I1=\ a\\x \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) - \ (\\found \ a<\x \ f(\x)\0)\; - I2= \\y\a+1 \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) - \ (\\found \ \y\a \ f(\y)\0)\\ \ - \- \\u. f(u)=0\ - \found:= False,, - \x:=a,, \y:=a+1,, - COBEGIN \\I1\ - WHILE \\found - INV \\I1\ - DO \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ - \ \x:=\x+1,,IF f(\x)=0 THEN \found:=True ELSE SKIP FI\ - OD - \\I1 \ \found\ - \ - \\I2\ - WHILE \\found - INV \\I2\ - DO \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ - \ \y:=(\y - 1),,IF f(\y)=0 THEN \found:=True ELSE SKIP FI\ - OD - \\I2 \ \found\ - COEND +lemma Zero_Search_2: +"\I1=\ a\\x \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) + \ (\\found \ a<\x \ f(\x)\0)\; + I2= \\y\a+1 \ (\found \ (a<\x \ f(\x)=0) \ (\y\a \ f(\y)=0)) + \ (\\found \ \y\a \ f(\y)\0)\\ \ + \- \\u. f(u)=0\ + \found:= False,, + \x:=a,, \y:=a+1,, + COBEGIN \\I1\ + WHILE \\found + INV \\I1\ + DO \a\\x \ (\found \ \y\a \ f(\y)=0) \ (a<\x \ f(\x)\0)\ + \ \x:=\x+1,,IF f(\x)=0 THEN \found:=True ELSE SKIP FI\ + OD + \\I1 \ \found\ + \ + \\I2\ + WHILE \\found + INV \\I2\ + DO \\y\a+1 \ (\found \ a<\x \ f(\x)=0) \ (\y\a \ f(\y)\0)\ + \ \y:=(\y - 1),,IF f(\y)=0 THEN \found:=True ELSE SKIP FI\ + OD + \\I2 \ \found\ + COEND \f(\x)=0 \ f(\y)=0\" apply oghoare ---{* 20 vc *} +--\20 vc\ apply auto ---{* auto takes aprox. 2 minutes. *} +--\auto takes aprox. 2 minutes.\ done -subsection {* Producer/Consumer *} +subsection \Producer/Consumer\ -subsubsection {* Previous lemmas *} +subsubsection \Previous lemmas\ lemma nat_lemma2: "\ b = m*(n::nat) + t; a = s*n + u; t=u; b-a < n \ \ m \ s" proof - @@ -368,7 +368,7 @@ done -subsubsection {* Producer/Consumer Algorithm *} +subsubsection \Producer/Consumer Algorithm\ record Producer_consumer = ins :: nat @@ -380,104 +380,104 @@ buffer :: "nat list" b :: "nat list" -text {* The whole proof takes aprox. 4 minutes. *} +text \The whole proof takes aprox. 4 minutes.\ -lemma Producer_consumer: - "\INIT= \0 0buffer \ length \b=length a\ ; - I= \(\k<\ins. \outs\k \ (a ! k) = \buffer ! (k mod (length \buffer))) \ - \outs\\ins \ \ins-\outs\length \buffer\ ; - I1= \\I \ \li\length a\ ; - p1= \\I1 \ \li=\ins\ ; +lemma Producer_consumer: + "\INIT= \0 0buffer \ length \b=length a\ ; + I= \(\k<\ins. \outs\k \ (a ! k) = \buffer ! (k mod (length \buffer))) \ + \outs\\ins \ \ins-\outs\length \buffer\ ; + I1= \\I \ \li\length a\ ; + p1= \\I1 \ \li=\ins\ ; I2 = \\I \ (\k<\lj. (a ! k)=(\b ! k)) \ \lj\length a\ ; - p2 = \\I2 \ \lj=\outs\ \ \ - \- \\INIT\ + p2 = \\I2 \ \lj=\outs\ \ \ + \- \\INIT\ \ins:=0,, \outs:=0,, \li:=0,, \lj:=0,, - COBEGIN \\p1 \ \INIT\ - WHILE \li \p1 \ \INIT\ - DO \\p1 \ \INIT \ \li - \vx:= (a ! \li);; - \\p1 \ \INIT \ \li \vx=(a ! \li)\ - WAIT \ins-\outs < length \buffer END;; - \\p1 \ \INIT \ \li \vx=(a ! \li) - \ \ins-\outs < length \buffer\ - \buffer:=(list_update \buffer (\ins mod (length \buffer)) \vx);; - \\p1 \ \INIT \ \li (a ! \li)=(\buffer ! (\ins mod (length \buffer))) - \ \ins-\outs buffer\ - \ins:=\ins+1;; - \\I1 \ \INIT \ (\li+1)=\ins \ \li - \li:=\li+1 - OD - \\p1 \ \INIT \ \li=length a\ - \ - \\p2 \ \INIT\ - WHILE \lj < length a - INV \\p2 \ \INIT\ - DO \\p2 \ \lj \INIT\ - WAIT \outs<\ins END;; - \\p2 \ \lj \outs<\ins \ \INIT\ - \vy:=(\buffer ! (\outs mod (length \buffer)));; - \\p2 \ \lj \outs<\ins \ \vy=(a ! \lj) \ \INIT\ - \outs:=\outs+1;; - \\I2 \ (\lj+1)=\outs \ \lj \vy=(a ! \lj) \ \INIT\ - \b:=(list_update \b \lj \vy);; - \\I2 \ (\lj+1)=\outs \ \lj (a ! \lj)=(\b ! \lj) \ \INIT\ - \lj:=\lj+1 - OD - \\p2 \ \lj=length a \ \INIT\ - COEND + COBEGIN \\p1 \ \INIT\ + WHILE \li \p1 \ \INIT\ + DO \\p1 \ \INIT \ \li + \vx:= (a ! \li);; + \\p1 \ \INIT \ \li \vx=(a ! \li)\ + WAIT \ins-\outs < length \buffer END;; + \\p1 \ \INIT \ \li \vx=(a ! \li) + \ \ins-\outs < length \buffer\ + \buffer:=(list_update \buffer (\ins mod (length \buffer)) \vx);; + \\p1 \ \INIT \ \li (a ! \li)=(\buffer ! (\ins mod (length \buffer))) + \ \ins-\outs buffer\ + \ins:=\ins+1;; + \\I1 \ \INIT \ (\li+1)=\ins \ \li + \li:=\li+1 + OD + \\p1 \ \INIT \ \li=length a\ + \ + \\p2 \ \INIT\ + WHILE \lj < length a + INV \\p2 \ \INIT\ + DO \\p2 \ \lj \INIT\ + WAIT \outs<\ins END;; + \\p2 \ \lj \outs<\ins \ \INIT\ + \vy:=(\buffer ! (\outs mod (length \buffer)));; + \\p2 \ \lj \outs<\ins \ \vy=(a ! \lj) \ \INIT\ + \outs:=\outs+1;; + \\I2 \ (\lj+1)=\outs \ \lj \vy=(a ! \lj) \ \INIT\ + \b:=(list_update \b \lj \vy);; + \\I2 \ (\lj+1)=\outs \ \lj (a ! \lj)=(\b ! \lj) \ \INIT\ + \lj:=\lj+1 + OD + \\p2 \ \lj=length a \ \INIT\ + COEND \ \kb ! k)\" apply oghoare ---{* 138 vc *} -apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) ---{* 112 subgoals left *} +--\138 vc\ +apply(tactic \ALLGOALS (clarify_tac @{context})\) +--\112 subgoals left\ apply(simp_all (no_asm)) ---{* 97 subgoals left *} -apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *}) ---{* 930 subgoals left *} -apply(tactic {* ALLGOALS (clarify_tac @{context}) *}) ---{* 99 subgoals left *} +--\97 subgoals left\ +apply(tactic \ALLGOALS (conjI_Tac (K all_tac))\) +--\930 subgoals left\ +apply(tactic \ALLGOALS (clarify_tac @{context})\) +--\99 subgoals left\ apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym]) ---{* 20 subgoals left *} +--\20 subgoals left\ apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma) ---{* 9 subgoals left *} +--\9 subgoals left\ apply (force simp add:less_Suc_eq) apply(hypsubst_thin, drule sym) apply (force simp add:less_Suc_eq)+ done -subsection {* Parameterized Examples *} +subsection \Parameterized Examples\ -subsubsection {* Set Elements of an Array to Zero *} +subsubsection \Set Elements of an Array to Zero\ record Example1 = a :: "nat \ nat" -lemma Example1: +lemma Example1: "\- \True\ - COBEGIN SCHEME [0\iTrue\ \a:=\a (i:=0) \\a i=0\ COEND + COBEGIN SCHEME [0\iTrue\ \a:=\a (i:=0) \\a i=0\ COEND \\i < n. \a i = 0\" apply oghoare apply simp_all done -text {* Same example with lists as auxiliary variables. *} +text \Same example with lists as auxiliary variables.\ record Example1_list = A :: "nat list" -lemma Example1_list: - "\- \n < length \A\ - COBEGIN - SCHEME [0\in < length \A\ \A:=\A[i:=0] \\A!i=0\ - COEND +lemma Example1_list: + "\- \n < length \A\ + COBEGIN + SCHEME [0\in < length \A\ \A:=\A[i:=0] \\A!i=0\ + COEND \\i < n. \A!i = 0\" apply oghoare apply force+ done -subsubsection {* Increment a Variable in Parallel *} +subsubsection \Increment a Variable in Parallel\ -text {* First some lemmas about summation properties. *} +text \First some lemmas about summation properties.\ (* lemma Example2_lemma1: "!!b. j (\i::nat b j = 0 " apply(induct n) @@ -485,7 +485,7 @@ apply(force simp add: less_Suc_eq) done *) -lemma Example2_lemma2_aux: "!!b. j +lemma Example2_lemma2_aux: "!!b. j (\i=0..i=0..i=0.. s \ (\i::nat=0..i=0..j \ Suc (\i::nat=0..i=0.. nat" +record Example2 = + c :: "nat \ nat" x :: nat -lemma Example_2: "0 - \- \\x=0 \ (\i=0..c i)=0\ - COBEGIN - SCHEME [0\i\x=(\i=0..c i) \ \c i=0\ +lemma Example_2: "0 + \- \\x=0 \ (\i=0..c i)=0\ + COBEGIN + SCHEME [0\i\x=(\i=0..c i) \ \c i=0\ \ \x:=\x+(Suc 0),, \c:=\c (i:=(Suc 0)) \ \\x=(\i=0..c i) \ \c i=(Suc 0)\ - COEND + COEND \\x=n\" apply oghoare apply (simp_all cong del: setsum.strong_cong) -apply (tactic {* ALLGOALS (clarify_tac @{context}) *}) +apply (tactic \ALLGOALS (clarify_tac @{context})\) apply (simp_all cong del: setsum.strong_cong) apply(erule (1) Example2_lemma2) apply(erule (1) Example2_lemma2) diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/OG_Hoare.thy --- a/src/HOL/Hoare_Parallel/OG_Hoare.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Hoare.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,4 +1,4 @@ -section {* The Proof System *} +section \The Proof System\ theory OG_Hoare imports OG_Tran begin @@ -8,14 +8,14 @@ | "assertions (AnnCond1 r b c1 c2) = {r} \ assertions c1 \ assertions c2" | "assertions (AnnCond2 r b c) = {r} \ assertions c" | "assertions (AnnWhile r b i c) = {r, i} \ assertions c" -| "assertions (AnnAwait r b c) = {r}" +| "assertions (AnnAwait r b c) = {r}" primrec atomics :: "'a ann_com \ ('a assn \ 'a com) set" where "atomics (AnnBasic r f) = {(r, Basic f)}" | "atomics (AnnSeq c1 c2) = atomics c1 \ atomics c2" | "atomics (AnnCond1 r b c1 c2) = atomics c1 \ atomics c2" | "atomics (AnnCond2 r b c) = atomics c" -| "atomics (AnnWhile r b i c) = atomics c" +| "atomics (AnnWhile r b i c) = atomics c" | "atomics (AnnAwait r b c) = {(r \ b, c)}" primrec com :: "'a ann_triple_op \ 'a ann_com_op" where @@ -25,12 +25,12 @@ "post (c, q) = q" definition interfree_aux :: "('a ann_com_op \ 'a assn \ 'a ann_com_op) \ bool" where - "interfree_aux \ \(co, q, co'). co'= None \ + "interfree_aux \ \(co, q, co'). co'= None \ (\(r,a) \ atomics (the co'). \= (q \ r) a q \ (co = None \ (\p \ assertions (the co). \= (p \ r) a p)))" -definition interfree :: "(('a ann_triple_op) list) \ bool" where - "interfree Ts \ \i j. i < length Ts \ j < length Ts \ i \ j \ +definition interfree :: "(('a ann_triple_op) list) \ bool" where + "interfree Ts \ \i j. i < length Ts \ j < length Ts \ i \ j \ interfree_aux (com (Ts!i), post (Ts!i), com (Ts!j)) " inductive @@ -40,26 +40,26 @@ AnnBasic: "r \ {s. f s \ q} \ \ (AnnBasic r f) q" | AnnSeq: "\ \ c0 pre c1; \ c1 q \ \ \ (AnnSeq c0 c1) q" - -| AnnCond1: "\ r \ b \ pre c1; \ c1 q; r \ -b \ pre c2; \ c2 q\ + +| AnnCond1: "\ r \ b \ pre c1; \ c1 q; r \ -b \ pre c2; \ c2 q\ \ \ (AnnCond1 r b c1 c2) q" | AnnCond2: "\ r \ b \ pre c; \ c q; r \ -b \ q \ \ \ (AnnCond2 r b c) q" - -| AnnWhile: "\ r \ i; i \ b \ pre c; \ c i; i \ -b \ q \ + +| AnnWhile: "\ r \ i; i \ b \ pre c; \ c i; i \ -b \ q \ \ \ (AnnWhile r b i c) q" - + | AnnAwait: "\ atom_com c; \- (r \ b) c q \ \ \ (AnnAwait r b c) q" - + | AnnConseq: "\\ c q; q \ q' \ \ \ c q'" | Parallel: "\ \ic q. Ts!i = (Some c, q) \ \ c q; interfree Ts \ - \ \- (\i\{i. i \- (\i\{i. ii\{i. i- {s. f s \q} (Basic f) q" - + | Seq: "\ \- p c1 r; \- r c2 q \ \ \- p (Seq c1 c2) q " | Cond: "\ \- (p \ b) c1 q; \- (p \ -b) c2 q \ \ \- p (Cond b c1 c2) q" @@ -68,7 +68,7 @@ | Conseq: "\ p' \ p; \- p c q ; q \ q' \ \ \- p' c q'" -section {* Soundness *} +section \Soundness\ (* In the version Isabelle-10-Sep-1999: HOL: The THEN and ELSE parts of conditional expressions (if P then x else y) are no longer simplified. (This allows the simplifier to unfold recursive @@ -95,9 +95,9 @@ lemmas While = oghoare_ann_hoare.While lemmas Conseq = oghoare_ann_hoare.Conseq -subsection {* Soundness of the System for Atomic Programs *} +subsection \Soundness of the System for Atomic Programs\ -lemma Basic_ntran [rule_format]: +lemma Basic_ntran [rule_format]: "(Basic f, s) -Pn\ (Parallel Ts, t) \ All_None Ts \ t = f s" apply(induct "n") apply(simp (no_asm)) @@ -109,33 +109,33 @@ apply(simp (no_asm) add: L3_5v_lemma3) apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty) apply(rule conjI) - apply (blast dest: L3_5i) + apply (blast dest: L3_5i) apply(simp add: SEM_def sem_def id_def) -apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow) +apply (blast dest: Basic_ntran rtrancl_imp_UN_relpow) done -lemma atom_hoare_sound [rule_format]: +lemma atom_hoare_sound [rule_format]: " \- p c q \ atom_com(c) \ \= p c q" apply (unfold com_validity_def) apply(rule oghoare_induct) apply simp_all ---{*Basic*} +--\Basic\ apply(simp add: SEM_def sem_def) apply(fast dest: rtrancl_imp_UN_relpow Basic_ntran) ---{* Seq *} +--\Seq\ apply(rule impI) apply(rule subset_trans) prefer 2 apply simp apply(simp add: L3_5ii L3_5i) ---{* Cond *} +--\Cond\ apply(simp add: L3_5iv) ---{* While *} - apply (force simp add: L3_5v dest: SEM_fwhile) ---{* Conseq *} +--\While\ + apply (force simp add: L3_5v dest: SEM_fwhile) +--\Conseq\ apply(force simp add: SEM_def sem_def) done - -subsection {* Soundness of the System for Component Programs *} + +subsection \Soundness of the System for Component Programs\ inductive_cases ann_transition_cases: "(None,s) -1\ (c', s')" @@ -146,17 +146,17 @@ "(Some (AnnWhile r b I c), s) -1\ (c', s')" "(Some (AnnAwait r b c),s) -1\ (c', s')" -text {* Strong Soundness for Component Programs:*} +text \Strong Soundness for Component Programs:\ lemma ann_hoare_case_analysis [rule_format]: "\ C q' \ - ((\r f. C = AnnBasic r f \ (\q. r \ {s. f s \ q} \ q \ q')) \ - (\c0 c1. C = AnnSeq c0 c1 \ (\q. q \ q' \ \ c0 pre c1 \ \ c1 q)) \ - (\r b c1 c2. C = AnnCond1 r b c1 c2 \ (\q. q \ q' \ - r \ b \ pre c1 \ \ c1 q \ r \ -b \ pre c2 \ \ c2 q)) \ - (\r b c. C = AnnCond2 r b c \ - (\q. q \ q' \ r \ b \ pre c \ \ c q \ r \ -b \ q)) \ - (\r i b c. C = AnnWhile r b i c \ - (\q. q \ q' \ r \ i \ i \ b \ pre c \ \ c i \ i \ -b \ q)) \ + ((\r f. C = AnnBasic r f \ (\q. r \ {s. f s \ q} \ q \ q')) \ + (\c0 c1. C = AnnSeq c0 c1 \ (\q. q \ q' \ \ c0 pre c1 \ \ c1 q)) \ + (\r b c1 c2. C = AnnCond1 r b c1 c2 \ (\q. q \ q' \ + r \ b \ pre c1 \ \ c1 q \ r \ -b \ pre c2 \ \ c2 q)) \ + (\r b c. C = AnnCond2 r b c \ + (\q. q \ q' \ r \ b \ pre c \ \ c q \ r \ -b \ q)) \ + (\r i b c. C = AnnWhile r b i c \ + (\q. q \ q' \ r \ i \ i \ b \ pre c \ \ c i \ i \ -b \ q)) \ (\r b c. C = AnnAwait r b c \ (\q. q \ q' \ \- (r \ b) c q)))" apply(rule ann_hoare_induct) apply simp_all @@ -169,16 +169,16 @@ apply force done -lemma Strong_Soundness_aux_aux [rule_format]: - "(co, s) -1\ (co', t) \ (\c. co = Some c \ s\ pre c \ +lemma Strong_Soundness_aux_aux [rule_format]: + "(co, s) -1\ (co', t) \ (\c. co = Some c \ s\ pre c \ (\q. \ c q \ (if co' = None then t\q else t \ pre(the co') \ \ (the co') q )))" apply(rule ann_transition_transition.induct [THEN conjunct1]) -apply simp_all ---{* Basic *} +apply simp_all +--\Basic\ apply clarify apply(frule ann_hoare_case_analysis) apply force ---{* Seq *} +--\Seq\ apply clarify apply(frule ann_hoare_case_analysis,simp) apply(fast intro: AnnConseq) @@ -189,21 +189,21 @@ apply force apply(rule AnnSeq,simp) apply(fast intro: AnnConseq) ---{* Cond1 *} +--\Cond1\ apply clarify apply(frule ann_hoare_case_analysis,simp) apply(fast intro: AnnConseq) apply clarify apply(frule ann_hoare_case_analysis,simp) apply(fast intro: AnnConseq) ---{* Cond2 *} +--\Cond2\ apply clarify apply(frule ann_hoare_case_analysis,simp) apply(fast intro: AnnConseq) apply clarify apply(frule ann_hoare_case_analysis,simp) apply(fast intro: AnnConseq) ---{* While *} +--\While\ apply clarify apply(frule ann_hoare_case_analysis,simp) apply force @@ -214,17 +214,17 @@ apply simp apply(rule AnnWhile) apply simp_all ---{* Await *} +--\Await\ apply(frule ann_hoare_case_analysis,simp) apply clarify apply(drule atom_hoare_sound) - apply simp + apply simp apply(simp add: com_validity_def SEM_def sem_def) apply(simp add: Help All_None_def) apply force done -lemma Strong_Soundness_aux: "\ (Some c, s) -*\ (co, t); s \ pre c; \ c q \ +lemma Strong_Soundness_aux: "\ (Some c, s) -*\ (co, t); s \ pre c; \ c q \ \ if co = None then t \ q else t \ pre (the co) \ \ (the co) q" apply(erule rtrancl_induct2) apply simp @@ -235,7 +235,7 @@ apply simp_all done -lemma Strong_Soundness: "\ (Some c, s)-*\(co, t); s \ pre c; \ c q \ +lemma Strong_Soundness: "\ (Some c, s)-*\(co, t); s \ pre c; \ c q \ \ if co = None then t\q else t \ pre (the co)" apply(force dest:Strong_Soundness_aux) done @@ -247,9 +247,9 @@ apply simp_all done -subsection {* Soundness of the System for Parallel Programs *} +subsection \Soundness of the System for Parallel Programs\ -lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1\ (R', t) \ +lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1\ (R', t) \ (\Rs. R' = (Parallel Rs) \ (length Rs) = (length Ts) \ (\i. i post(Rs ! i) = post(Ts ! i)))" apply(erule transition_cases) @@ -259,8 +259,8 @@ apply simp+ done -lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*\ (R',t) \ - (\Rs. R' = (Parallel Rs) \ (length Rs) = (length Ts) \ +lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*\ (R',t) \ + (\Rs. R' = (Parallel Rs) \ (length Rs) = (length Ts) \ (\i. i post(Ts ! i) = post(Rs ! i)))" apply(erule rtrancl_induct2) apply(simp_all) @@ -275,7 +275,7 @@ apply auto done -lemma interfree_aux1 [rule_format]: +lemma interfree_aux1 [rule_format]: "(c,s) -1\ (r,t) \ (interfree_aux(c1, q1, c) \ interfree_aux(c1, q1, r))" apply (rule ann_transition_transition.induct [THEN conjunct1]) apply(safe) @@ -285,13 +285,13 @@ apply force+ done -lemma interfree_aux2 [rule_format]: +lemma interfree_aux2 [rule_format]: "(c,s) -1\ (r,t) \ (interfree_aux(c, q, a) \ interfree_aux(r, q, a) )" apply (rule ann_transition_transition.induct [THEN conjunct1]) apply(force simp add:interfree_aux_def)+ done -lemma interfree_lemma: "\ (Some c, s) -1\ (r, t);interfree Ts ; i (Some c, s) -1\ (r, t);interfree Ts ; i \ interfree (Ts[i:= (r, q)])" apply(simp add: interfree_def) apply clarify @@ -302,10 +302,10 @@ apply(force elim: interfree_aux2 simp add:nth_list_update) done -text {* Strong Soundness Theorem for Parallel Programs:*} +text \Strong Soundness Theorem for Parallel Programs:\ -lemma Parallel_Strong_Soundness_Seq_aux: - "\interfree Ts; i +lemma Parallel_Strong_Soundness_Seq_aux: + "\interfree Ts; i \ interfree (Ts[i:=(Some c0, pre c1)])" apply(simp add: interfree_def) apply clarify @@ -317,14 +317,14 @@ apply simp done -lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]: - "\ \i post(Ts!i) - else b \ pre(the(com(Ts!i))) \ \ the(com(Ts!i)) post(Ts!i)); - com(Ts ! i) = Some(AnnSeq c0 c1); i \ - (\ia post(Ts[i:=(Some c0, pre c1)]! ia) - else b \ pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) \ - \ the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia))) +lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]: + "\ \i post(Ts!i) + else b \ pre(the(com(Ts!i))) \ \ the(com(Ts!i)) post(Ts!i)); + com(Ts ! i) = Some(AnnSeq c0 c1); i \ + (\ia post(Ts[i:=(Some c0, pre c1)]! ia) + else b \ pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) \ + \ the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia))) \ interfree (Ts[i:= (Some c0, pre c1)])" apply(rule conjI) apply safe @@ -335,20 +335,20 @@ apply(fast elim: Parallel_Strong_Soundness_Seq_aux) done -lemma Parallel_Strong_Soundness_aux_aux [rule_format]: - "(Some c, b) -1\ (co, t) \ - (\Ts. i com(Ts ! i) = Some c \ - (\ipost(Ts!i) - else b\pre(the(com(Ts!i))) \ \ the(com(Ts!i)) post(Ts!i))) \ - interfree Ts \ - (\j. j i\j \ (if com(Ts!j) = None then t\post(Ts!j) +lemma Parallel_Strong_Soundness_aux_aux [rule_format]: + "(Some c, b) -1\ (co, t) \ + (\Ts. i com(Ts ! i) = Some c \ + (\ipost(Ts!i) + else b\pre(the(com(Ts!i))) \ \ the(com(Ts!i)) post(Ts!i))) \ + interfree Ts \ + (\j. j i\j \ (if com(Ts!j) = None then t\post(Ts!j) else t\pre(the(com(Ts!j))) \ \ the(com(Ts!j)) post(Ts!j))) )" apply(rule ann_transition_transition.induct [THEN conjunct1]) apply safe prefer 11 apply(rule TrueI) apply simp_all ---{* Basic *} +--\Basic\ apply(erule_tac x = "i" in all_dupE, erule (1) notE impE) apply(erule_tac x = "j" in allE , erule (1) notE impE) apply(simp add: interfree_def) @@ -362,15 +362,15 @@ apply clarify apply simp apply(erule_tac x="pre y" in ballE) - apply(force intro: converse_rtrancl_into_rtrancl + apply(force intro: converse_rtrancl_into_rtrancl simp add: com_validity_def SEM_def sem_def All_None_def) apply(simp add:assertions_lemma) ---{* Seqs *} +--\Seqs\ apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE) apply(drule Parallel_Strong_Soundness_Seq,simp+) apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE) apply(drule Parallel_Strong_Soundness_Seq,simp+) ---{* Await *} +--\Await\ apply(rule_tac x = "i" in allE , assumption , erule (1) notE impE) apply(erule_tac x = "j" in allE , erule (1) notE impE) apply(simp add: interfree_def) @@ -378,28 +378,28 @@ apply(erule_tac x = "i" in allE,simp) apply(drule_tac t = "i" in not_sym) apply(case_tac "com(Ts ! j)=None") - apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def + apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def com_validity_def SEM_def sem_def All_None_def Help) apply(simp add:interfree_aux_def) apply clarify apply simp apply(erule_tac x="pre y" in ballE) - apply(force intro: converse_rtrancl_into_rtrancl + apply(force intro: converse_rtrancl_into_rtrancl simp add: com_validity_def SEM_def sem_def All_None_def Help) apply(simp add:assertions_lemma) done -lemma Parallel_Strong_Soundness_aux [rule_format]: +lemma Parallel_Strong_Soundness_aux [rule_format]: "\(Ts',s) -P*\ (Rs',t); Ts' = (Parallel Ts); interfree Ts; - \i. i (\c q. (Ts ! i) = (Some c, q) \ s\(pre c) \ \ c q ) \ \ - \Rs. Rs' = (Parallel Rs) \ (\j. j - (if com(Rs ! j) = None then t\post(Ts ! j) + \i. i (\c q. (Ts ! i) = (Some c, q) \ s\(pre c) \ \ c q ) \ \ + \Rs. Rs' = (Parallel Rs) \ (\j. j + (if com(Rs ! j) = None then t\post(Ts ! j) else t\pre(the(com(Rs ! j))) \ \ the(com(Rs ! j)) post(Ts ! j))) \ interfree Rs" apply(erule rtrancl_induct2) apply clarify ---{* Base *} +--\Base\ apply force ---{* Induction step *} +--\Induction step\ apply clarify apply(drule Parallel_length_post_PStar) apply clarify @@ -419,9 +419,9 @@ apply simp_all done -lemma Parallel_Strong_Soundness: - "\(Parallel Ts, s) -P*\ (Parallel Rs, t); interfree Ts; ji. i (\c q. Ts ! i = (Some c, q) \ s\pre c \ \ c q) \ \ +lemma Parallel_Strong_Soundness: + "\(Parallel Ts, s) -P*\ (Parallel Rs, t); interfree Ts; ji. i (\c q. Ts ! i = (Some c, q) \ s\pre c \ \ c q) \ \ if com(Rs ! j) = None then t\post(Ts ! j) else t\pre (the(com(Rs ! j)))" apply(drule Parallel_Strong_Soundness_aux) apply simp+ @@ -431,7 +431,7 @@ apply (unfold com_validity_def) apply(rule oghoare_induct) apply(rule TrueI)+ ---{* Parallel *} +--\Parallel\ apply(simp add: SEM_def sem_def) apply(clarify, rename_tac x y i Ts') apply(frule Parallel_length_post_PStar) @@ -445,19 +445,19 @@ apply(drule_tac s = "length Rs" in sym) apply(erule allE, erule impE, assumption) apply(force dest: nth_mem simp add: All_None_def) ---{* Basic *} +--\Basic\ apply(simp add: SEM_def sem_def) apply(force dest: rtrancl_imp_UN_relpow Basic_ntran) ---{* Seq *} +--\Seq\ apply(rule subset_trans) prefer 2 apply assumption apply(simp add: L3_5ii L3_5i) ---{* Cond *} +--\Cond\ apply(simp add: L3_5iv) ---{* While *} +--\While\ apply(simp add: L3_5v) - apply (blast dest: SEM_fwhile) ---{* Conseq *} + apply (blast dest: SEM_fwhile) +--\Conseq\ apply(auto simp add: SEM_def sem_def) done diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/OG_Syntax.thy --- a/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy Sat Dec 27 20:32:06 2014 +0100 @@ -2,8 +2,8 @@ imports OG_Tactics Quote_Antiquote begin -text{* Syntax for commands and for assertions and boolean expressions in - commands @{text com} and annotated commands @{text ann_com}. *} +text\Syntax for commands and for assertions and boolean expressions in + commands @{text com} and annotated commands @{text ann_com}.\ abbreviation Skip :: "'a com" ("SKIP" 63) where "SKIP \ Basic id" @@ -28,14 +28,14 @@ ("_ //IF _ /THEN _ /ELSE _ /FI" [90,0,0,0] 61) "_AnnCond2" :: "'a assn \ 'a bexp \ 'a ann_com \ 'a ann_com" ("_ //IF _ /THEN _ /FI" [90,0,0] 61) - "_AnnWhile" :: "'a assn \ 'a bexp \ 'a assn \ 'a ann_com \ 'a ann_com" + "_AnnWhile" :: "'a assn \ 'a bexp \ 'a assn \ 'a ann_com \ 'a ann_com" ("_ //WHILE _ /INV _ //DO _//OD" [90,0,0,0] 61) "_AnnAwait" :: "'a assn \ 'a bexp \ 'a com \ 'a ann_com" ("_ //AWAIT _ /THEN /_ /END" [90,0,0] 61) "_AnnAtom" :: "'a assn \ 'a com \ 'a ann_com" ("_//\_\" [90,0] 61) "_AnnWait" :: "'a assn \ 'a bexp \ 'a ann_com" ("_//WAIT _ END" [90,0] 61) - "_Cond" :: "'a bexp \ 'a com \ 'a com \ 'a com" + "_Cond" :: "'a bexp \ 'a com \ 'a com \ 'a com" ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61) "_Cond2" :: "'a bexp \ 'a com \ 'a com" ("IF _ THEN _ FI" [0,0] 56) "_While_inv" :: "'a bexp \ 'a assn \ 'a com \ 'a com" @@ -55,7 +55,7 @@ "r AWAIT b THEN c END" \ "CONST AnnAwait r \b\ c" "r \c\" \ "r AWAIT CONST True THEN c END" "r WAIT b END" \ "r AWAIT b THEN SKIP END" - + nonterminal prgs syntax @@ -63,7 +63,7 @@ "_prg" :: "['a, 'a] \ prgs" ("_//_" [60, 90] 57) "_prgs" :: "['a, 'a, prgs] \ prgs" ("_//_//\//_" [60,90,57] 57) - "_prg_scheme" :: "['a, 'a, 'a, 'a, 'a] \ prgs" + "_prg_scheme" :: "['a, 'a, 'a, 'a, 'a] \ prgs" ("SCHEME [_ \ _ < _] _// _" [0,0,0,60, 90] 57) translations @@ -73,7 +73,7 @@ "_prg_scheme j i k c q" \ "CONST map (\i. (CONST Some c, q)) [j.. let fun quote_tr' f (t :: ts) = Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) @@ -123,6 +123,6 @@ (@{const_syntax AnnCond1}, K (annbexp_tr' @{syntax_const "_AnnCond1"})), (@{const_syntax AnnCond2}, K (annbexp_tr' @{syntax_const "_AnnCond2"}))] end; -*} +\ end \ No newline at end of file diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/OG_Tactics.thy --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,4 +1,4 @@ -section {* Generation of Verification Conditions *} +section \Generation of Verification Conditions\ theory OG_Tactics imports OG_Hoare @@ -7,15 +7,15 @@ lemmas ann_hoare_intros=AnnBasic AnnSeq AnnCond1 AnnCond2 AnnWhile AnnAwait AnnConseq lemmas oghoare_intros=Parallel Basic Seq Cond While Conseq -lemma ParallelConseqRule: - "\ p \ (\i\{i. i- (\i\{i. ii\{i. ii\{i. i q \ +lemma ParallelConseqRule: + "\ p \ (\i\{i. i- (\i\{i. ii\{i. ii\{i. i q \ \ \- p (Parallel Ts) q" apply (rule Conseq) -prefer 2 +prefer 2 apply fast apply assumption+ done @@ -39,8 +39,8 @@ apply fast+ done -lemma CondRule: - "\ p \ {s. (s\b \ s\w) \ (s\b \ s\w')}; \- w c1 q; \- w' c2 q \ +lemma CondRule: + "\ p \ {s. (s\b \ s\w) \ (s\b \ s\w')}; \- w c1 q; \- w' c2 q \ \ \- p (Cond b c1 c2) q" apply(rule Cond) apply(rule Conseq) @@ -49,17 +49,17 @@ apply force+ done -lemma WhileRule: "\ p \ i; \- (i \ b) c i ; (i \ (-b)) \ q \ +lemma WhileRule: "\ p \ i; \- (i \ b) c i ; (i \ (-b)) \ q \ \ \- p (While b i c) q" apply(rule Conseq) prefer 2 apply(rule While) apply assumption+ done -text {* Three new proof rules for special instances of the @{text +text \Three new proof rules for special instances of the @{text AnnBasic} and the @{text AnnAwait} commands when the transformation performed on the state is the identity, and for an @{text AnnAwait} -command where the boolean condition is @{text "{s. True}"}: *} +command where the boolean condition is @{text "{s. True}"}:\ lemma AnnatomRule: "\ atom_com(c); \- r c q \ \ \ (AnnAwait r {s. True} c) q" @@ -81,93 +81,93 @@ apply simp done -text {* Lemmata to avoid using the definition of @{text +text \Lemmata to avoid using the definition of @{text map_ann_hoare}, @{text interfree_aux}, @{text interfree_swap} and -@{text interfree} by splitting it into different cases: *} +@{text interfree} by splitting it into different cases:\ lemma interfree_aux_rule1: "interfree_aux(co, q, None)" by(simp add:interfree_aux_def) -lemma interfree_aux_rule2: +lemma interfree_aux_rule2: "\(R,r)\(atomics a). \- (q \ R) r q \ interfree_aux(None, q, Some a)" apply(simp add:interfree_aux_def) apply(force elim:oghoare_sound) done -lemma interfree_aux_rule3: +lemma interfree_aux_rule3: "(\(R, r)\(atomics a). \- (q \ R) r q \ (\p\(assertions c). \- (p \ R) r p)) \ interfree_aux(Some c, q, Some a)" apply(simp add:interfree_aux_def) apply(force elim:oghoare_sound) done -lemma AnnBasic_assertions: - "\interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\ \ +lemma AnnBasic_assertions: + "\interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\ \ interfree_aux(Some (AnnBasic r f), q, Some a)" apply(simp add: interfree_aux_def) by force -lemma AnnSeq_assertions: - "\ interfree_aux(Some c1, q, Some a); interfree_aux(Some c2, q, Some a)\\ +lemma AnnSeq_assertions: + "\ interfree_aux(Some c1, q, Some a); interfree_aux(Some c2, q, Some a)\\ interfree_aux(Some (AnnSeq c1 c2), q, Some a)" apply(simp add: interfree_aux_def) by force -lemma AnnCond1_assertions: - "\ interfree_aux(None, r, Some a); interfree_aux(Some c1, q, Some a); - interfree_aux(Some c2, q, Some a)\\ +lemma AnnCond1_assertions: + "\ interfree_aux(None, r, Some a); interfree_aux(Some c1, q, Some a); + interfree_aux(Some c2, q, Some a)\\ interfree_aux(Some(AnnCond1 r b c1 c2), q, Some a)" apply(simp add: interfree_aux_def) by force -lemma AnnCond2_assertions: - "\ interfree_aux(None, r, Some a); interfree_aux(Some c, q, Some a)\\ +lemma AnnCond2_assertions: + "\ interfree_aux(None, r, Some a); interfree_aux(Some c, q, Some a)\\ interfree_aux(Some (AnnCond2 r b c), q, Some a)" apply(simp add: interfree_aux_def) by force -lemma AnnWhile_assertions: - "\ interfree_aux(None, r, Some a); interfree_aux(None, i, Some a); - interfree_aux(Some c, q, Some a)\\ +lemma AnnWhile_assertions: + "\ interfree_aux(None, r, Some a); interfree_aux(None, i, Some a); + interfree_aux(Some c, q, Some a)\\ interfree_aux(Some (AnnWhile r b i c), q, Some a)" apply(simp add: interfree_aux_def) by force - -lemma AnnAwait_assertions: - "\ interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\\ + +lemma AnnAwait_assertions: + "\ interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\\ interfree_aux(Some (AnnAwait r b c), q, Some a)" apply(simp add: interfree_aux_def) by force - -lemma AnnBasic_atomics: + +lemma AnnBasic_atomics: "\- (q \ r) (Basic f) q \ interfree_aux(None, q, Some (AnnBasic r f))" by(simp add: interfree_aux_def oghoare_sound) -lemma AnnSeq_atomics: - "\ interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\\ +lemma AnnSeq_atomics: + "\ interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\\ interfree_aux(Any, q, Some (AnnSeq a1 a2))" apply(simp add: interfree_aux_def) by force lemma AnnCond1_atomics: - "\ interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\\ + "\ interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\\ interfree_aux(Any, q, Some (AnnCond1 r b a1 a2))" apply(simp add: interfree_aux_def) by force -lemma AnnCond2_atomics: +lemma AnnCond2_atomics: "interfree_aux (Any, q, Some a)\ interfree_aux(Any, q, Some (AnnCond2 r b a))" by(simp add: interfree_aux_def) -lemma AnnWhile_atomics: "interfree_aux (Any, q, Some a) +lemma AnnWhile_atomics: "interfree_aux (Any, q, Some a) \ interfree_aux(Any, q, Some (AnnWhile r b i a))" by(simp add: interfree_aux_def) -lemma Annatom_atomics: +lemma Annatom_atomics: "\- (q \ r) a q \ interfree_aux (None, q, Some (AnnAwait r {x. True} a))" -by(simp add: interfree_aux_def oghoare_sound) +by(simp add: interfree_aux_def oghoare_sound) -lemma AnnAwait_atomics: +lemma AnnAwait_atomics: "\- (q \ (r \ b)) a q \ interfree_aux (None, q, Some (AnnAwait r b a))" by(simp add: interfree_aux_def oghoare_sound) @@ -178,21 +178,21 @@ lemma interfree_swap_Empty: "interfree_swap (x, [])" by(simp add:interfree_swap_def) -lemma interfree_swap_List: - "\ interfree_aux (com x, post x, com y); - interfree_aux (com y, post y ,com x); interfree_swap (x, xs) \ +lemma interfree_swap_List: + "\ interfree_aux (com x, post x, com y); + interfree_aux (com y, post y ,com x); interfree_swap (x, xs) \ \ interfree_swap (x, y#xs)" by(simp add:interfree_swap_def) -lemma interfree_swap_Map: "\k. i\k \ k interfree_aux (com x, post x, c k) - \ interfree_aux (c k, Q k, com x) +lemma interfree_swap_Map: "\k. i\k \ k interfree_aux (com x, post x, c k) + \ interfree_aux (c k, Q k, com x) \ interfree_swap (x, map (\k. (c k, Q k)) [i.. interfree_swap(x, xs); interfree xs \ \ interfree (x#xs)" apply(simp add:interfree_def interfree_swap_def) apply clarify @@ -202,8 +202,8 @@ apply(case_tac j,simp+) done -lemma interfree_Map: - "(\i j. a\i \ i a\j \ j i\j \ interfree_aux (c i, Q i, c j)) +lemma interfree_Map: + "(\i j. a\i \ i a\j \ j i\j \ interfree_aux (c i, Q i, c j)) \ interfree (map (\k. (c k, Q k)) [a..k. i\k \ k \ (c k) (Q k) \ [\] map (\k. (Some (c k), Q k)) [i.. [\] Ts ; interfree Ts \ - \ \- (\i\{i. i \- (\i\{i. ii\{i. i \k (c k) (Q k); + "\ \k (c k) (Q k); \k l. k l k\l \ interfree_aux (Some(c k), Q k, Some(c l)) \ \ \- (\i\{i. iii\{i. iThe following are some useful lemmas and simplification tactics to control which theorems are used to simplify at each moment, so that the original input does not suffer any unexpected -transformation. *} +transformation.\ lemma Compl_Collect: "-(Collect b) = {x. \(b x)}" by fast @@ -273,7 +273,7 @@ Collect_mem_eq ball_simps option.simps primrecdef_list lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append -ML {* +ML \ fun before_interfree_simp_tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm com.simps}, @{thm post.simps}]) @@ -284,50 +284,50 @@ fun ParallelConseq ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms ParallelConseq_list} @ @{thms my_simp_list}) -*} +\ -text {* The following tactic applies @{text tac} to each conjunct in a +text \The following tactic applies @{text tac} to each conjunct in a subgoal of the form @{text "A \ a1 \ a2 \ .. \ an"} returning -@{text n} subgoals, one for each conjunct: *} +@{text n} subgoals, one for each conjunct:\ -ML {* +ML \ fun conjI_Tac tac i st = st |> ( (EVERY [rtac conjI i, conjI_Tac tac (i+1), tac i]) ORELSE (tac i) ) -*} +\ -subsubsection {* Tactic for the generation of the verification conditions *} +subsubsection \Tactic for the generation of the verification conditions\ -text {* The tactic basically uses two subtactics: +text \The tactic basically uses two subtactics: \begin{description} -\item[HoareRuleTac] is called at the level of parallel programs, it - uses the ParallelTac to solve parallel composition of programs. - This verification has two parts, namely, (1) all component programs are +\item[HoareRuleTac] is called at the level of parallel programs, it + uses the ParallelTac to solve parallel composition of programs. + This verification has two parts, namely, (1) all component programs are correct and (2) they are interference free. @{text HoareRuleTac} is also called at the level of atomic regions, i.e. @{text "\ \"} and @{text "AWAIT b THEN _ END"}, and at each interference freedom test. -\item[AnnHoareRuleTac] is for component programs which - are annotated programs and so, there are not unknown assertions +\item[AnnHoareRuleTac] is for component programs which + are annotated programs and so, there are not unknown assertions (no need to use the parameter precond, see NOTE). NOTE: precond(::bool) informs if the subgoal has the form @{text "\- ?p c q"}, - in this case we have precond=False and the generated verification - condition would have the form @{text "?p \ \"} which can be solved by + in this case we have precond=False and the generated verification + condition would have the form @{text "?p \ \"} which can be solved by @{text "rtac subset_refl"}, if True we proceed to simplify it using the simplification tactics above. \end{description} -*} +\ -ML {* +ML \ fun WlpTac ctxt i = (rtac (@{thm SeqRule}) i) THEN (HoareRuleTac ctxt false (i+1)) -and HoareRuleTac ctxt precond i st = st |> +and HoareRuleTac ctxt precond i st = st |> ( (WlpTac ctxt i THEN HoareRuleTac ctxt precond i) ORELSE (FIRST[rtac (@{thm SkipRule}) i, @@ -335,7 +335,7 @@ EVERY[rtac (@{thm ParallelConseqRule}) i, ParallelConseq ctxt (i+2), ParallelTac ctxt (i+1), - ParallelConseq ctxt i], + ParallelConseq ctxt i], EVERY[rtac (@{thm CondRule}) i, HoareRuleTac ctxt false (i+2), HoareRuleTac ctxt false (i+1)], @@ -345,7 +345,7 @@ THEN (if precond then (K all_tac i) else (rtac (@{thm subset_refl}) i)))) and AnnWlpTac ctxt i = (rtac (@{thm AnnSeq}) i) THEN (AnnHoareRuleTac ctxt (i+1)) -and AnnHoareRuleTac ctxt i st = st |> +and AnnHoareRuleTac ctxt i st = st |> ( (AnnWlpTac ctxt i THEN AnnHoareRuleTac ctxt i ) ORELSE (FIRST[(rtac (@{thm AnnskipRule}) i), @@ -387,7 +387,7 @@ rtac (@{thm allI}) i,rtac (@{thm impI}) i, conjI_Tac (interfree_aux_Tac ctxt) i]]) -and interfree_Tac ctxt i st = st |> +and interfree_Tac ctxt i st = st |> (FIRST[rtac (@{thm interfree_Empty}) i, EVERY[rtac (@{thm interfree_List}) i, interfree_Tac ctxt (i+1), @@ -396,7 +396,7 @@ rtac (@{thm allI}) i,rtac (@{thm allI}) i,rtac (@{thm impI}) i, interfree_aux_Tac ctxt i ]]) -and interfree_aux_Tac ctxt i = (before_interfree_simp_tac ctxt i ) THEN +and interfree_aux_Tac ctxt i = (before_interfree_simp_tac ctxt i ) THEN (FIRST[rtac (@{thm interfree_aux_rule1}) i, dest_assertions_Tac ctxt i]) @@ -441,59 +441,59 @@ EVERY[rtac (@{thm AnnAwait_atomics}) i, HoareRuleTac ctxt true i], K all_tac i]) -*} +\ -text {* The final tactic is given the name @{text oghoare}: *} +text \The final tactic is given the name @{text oghoare}:\ -ML {* +ML \ fun oghoare_tac ctxt = SUBGOAL (fn (_, i) => HoareRuleTac ctxt true i) -*} +\ -text {* Notice that the tactic for parallel programs @{text +text \Notice that the tactic for parallel programs @{text "oghoare_tac"} is initially invoked with the value @{text true} for the parameter @{text precond}. Parts of the tactic can be also individually used to generate the verification conditions for annotated sequential programs and to -generate verification conditions out of interference freedom tests: *} +generate verification conditions out of interference freedom tests:\ -ML {* +ML \ fun annhoare_tac ctxt = SUBGOAL (fn (_, i) => AnnHoareRuleTac ctxt i) fun interfree_aux_tac ctxt = SUBGOAL (fn (_, i) => interfree_aux_Tac ctxt i) -*} +\ -text {* The so defined ML tactics are then ``exported'' to be used in -Isabelle proofs. *} +text \The so defined ML tactics are then ``exported'' to be used in +Isabelle proofs.\ -method_setup oghoare = {* - Scan.succeed (SIMPLE_METHOD' o oghoare_tac) *} +method_setup oghoare = \ + Scan.succeed (SIMPLE_METHOD' o oghoare_tac)\ "verification condition generator for the oghoare logic" -method_setup annhoare = {* - Scan.succeed (SIMPLE_METHOD' o annhoare_tac) *} +method_setup annhoare = \ + Scan.succeed (SIMPLE_METHOD' o annhoare_tac)\ "verification condition generator for the ann_hoare logic" -method_setup interfree_aux = {* - Scan.succeed (SIMPLE_METHOD' o interfree_aux_tac) *} +method_setup interfree_aux = \ + Scan.succeed (SIMPLE_METHOD' o interfree_aux_tac)\ "verification condition generator for interference freedom tests" -text {* Tactics useful for dealing with the generated verification conditions: *} +text \Tactics useful for dealing with the generated verification conditions:\ -method_setup conjI_tac = {* - Scan.succeed (K (SIMPLE_METHOD' (conjI_Tac (K all_tac)))) *} +method_setup conjI_tac = \ + Scan.succeed (K (SIMPLE_METHOD' (conjI_Tac (K all_tac))))\ "verification condition generator for interference freedom tests" -ML {* +ML \ fun disjE_Tac tac i st = st |> ( (EVERY [etac disjE i, disjE_Tac tac (i+1), tac i]) ORELSE (tac i) ) -*} +\ -method_setup disjE_tac = {* - Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac)))) *} +method_setup disjE_tac = \ + Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac))))\ "verification condition generator for interference freedom tests" end diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/OG_Tran.thy --- a/src/HOL/Hoare_Parallel/OG_Tran.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/OG_Tran.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,10 +1,10 @@ -section {* Operational Semantics *} +section \Operational Semantics\ theory OG_Tran imports OG_Com begin type_synonym 'a ann_com_op = "('a ann_com) option" type_synonym 'a ann_triple_op = "('a ann_com_op \ 'a assn)" - + primrec com :: "'a ann_triple_op \ 'a ann_com_op" where "com (c, q) = c" @@ -14,10 +14,10 @@ definition All_None :: "'a ann_triple_op list \ bool" where "All_None Ts \ \(c, q) \ set Ts. c = None" -subsection {* The Transition Relation *} +subsection \The Transition Relation\ inductive_set - ann_transition :: "(('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a)) set" + ann_transition :: "(('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a)) set" and transition :: "(('a com \ 'a) \ ('a com \ 'a)) set" and ann_transition' :: "('a ann_com_op \ 'a) \ ('a ann_com_op \ 'a) \ bool" ("_ -1\ _"[81,81] 100) @@ -32,9 +32,9 @@ | AnnBasic: "(Some (AnnBasic r f), s) -1\ (None, f s)" -| AnnSeq1: "(Some c0, s) -1\ (None, t) \ +| AnnSeq1: "(Some c0, s) -1\ (None, t) \ (Some (AnnSeq c0 c1), s) -1\ (Some c1, t)" -| AnnSeq2: "(Some c0, s) -1\ (Some c2, t) \ +| AnnSeq2: "(Some c0, s) -1\ (Some c2, t) \ (Some (AnnSeq c0 c1), s) -1\ (Some (AnnSeq c2 c1), t)" | AnnCond1T: "s \ b \ (Some (AnnCond1 r b c1 c2), s) -1\ (Some c1, s)" @@ -44,11 +44,11 @@ | AnnCond2F: "s \ b \ (Some (AnnCond2 r b c), s) -1\ (None, s)" | AnnWhileF: "s \ b \ (Some (AnnWhile r b i c), s) -1\ (None, s)" -| AnnWhileT: "s \ b \ (Some (AnnWhile r b i c), s) -1\ +| AnnWhileT: "s \ b \ (Some (AnnWhile r b i c), s) -1\ (Some (AnnSeq c (AnnWhile i b i c)), s)" | AnnAwait: "\ s \ b; atom_com c; (c, s) -P*\ (Parallel [], t) \ \ - (Some (AnnAwait r b c), s) -1\ (None, t)" + (Some (AnnAwait r b c), s) -1\ (None, t)" | Parallel: "\ i (r, t) \ \ (Parallel Ts, s) -P1\ (Parallel (Ts [i:=(r, q)]), t)" @@ -66,10 +66,10 @@ monos "rtrancl_mono" -text {* The corresponding abbreviations are: *} +text \The corresponding abbreviations are:\ abbreviation - ann_transition_n :: "('a ann_com_op \ 'a) \ nat \ ('a ann_com_op \ 'a) + ann_transition_n :: "('a ann_com_op \ 'a) \ nat \ ('a ann_com_op \ 'a) \ bool" ("_ -_\ _"[81,81] 100) where "con_0 -n\ con_1 \ (con_0, con_1) \ ann_transition ^^ n" @@ -79,11 +79,11 @@ "con_0 -*\ con_1 \ (con_0, con_1) \ ann_transition\<^sup>*" abbreviation - transition_n :: "('a com \ 'a) \ nat \ ('a com \ 'a) \ bool" + transition_n :: "('a com \ 'a) \ nat \ ('a com \ 'a) \ bool" ("_ -P_\ _"[81,81,81] 100) where "con_0 -Pn\ con_1 \ (con_0, con_1) \ transition ^^ n" -subsection {* Definition of Semantics *} +subsection \Definition of Semantics\ definition ann_sem :: "'a ann_com \ 'a \ 'a set" where "ann_sem c \ \s. {t. (Some c, s) -*\ (None, t)}" @@ -104,17 +104,17 @@ "fwhile b c 0 = \" | "fwhile b c (Suc n) = Cond b (Seq c (fwhile b c n)) (Basic id)" -subsubsection {* Proofs *} +subsubsection \Proofs\ declare ann_transition_transition.intros [intro] -inductive_cases transition_cases: - "(Parallel T,s) -P1\ t" +inductive_cases transition_cases: + "(Parallel T,s) -P1\ t" "(Basic f, s) -P1\ t" - "(Seq c1 c2, s) -P1\ t" + "(Seq c1 c2, s) -P1\ t" "(Cond b c1 c2, s) -P1\ t" "(While b i c, s) -P1\ t" -lemma Parallel_empty_lemma [rule_format (no_asm)]: +lemma Parallel_empty_lemma [rule_format (no_asm)]: "(Parallel [],s) -Pn\ (Parallel Ts,t) \ Ts=[] \ n=0 \ s=t" apply(induct n) apply(simp (no_asm)) @@ -123,7 +123,7 @@ apply(force elim:transition_cases) done -lemma Parallel_AllNone_lemma [rule_format (no_asm)]: +lemma Parallel_AllNone_lemma [rule_format (no_asm)]: "All_None Ss \ (Parallel Ss,s) -Pn\ (Parallel Ts,t) \ Ts=Ss \ n=0 \ s=t" apply(induct "n") apply(simp (no_asm)) @@ -148,25 +148,25 @@ apply(simp add:All_None_def) done -text {* Set of lemmas from Apt and Olderog "Verification of sequential -and concurrent programs", page 63. *} +text \Set of lemmas from Apt and Olderog "Verification of sequential +and concurrent programs", page 63.\ -lemma L3_5i: "X\Y \ SEM c X \ SEM c Y" +lemma L3_5i: "X\Y \ SEM c X \ SEM c Y" apply (unfold SEM_def) apply force done -lemma L3_5ii_lemma1: - "\ (c1, s1) -P*\ (Parallel Ts, s2); All_None Ts; - (c2, s2) -P*\ (Parallel Ss, s3); All_None Ss \ +lemma L3_5ii_lemma1: + "\ (c1, s1) -P*\ (Parallel Ts, s2); All_None Ts; + (c2, s2) -P*\ (Parallel Ss, s3); All_None Ss \ \ (Seq c1 c2, s1) -P*\ (Parallel Ss, s3)" apply(erule converse_rtrancl_induct2) apply(force intro:converse_rtrancl_into_rtrancl)+ done -lemma L3_5ii_lemma2 [rule_format (no_asm)]: - "\c1 c2 s t. (Seq c1 c2, s) -Pn\ (Parallel Ts, t) \ - (All_None Ts) \ (\y m Rs. (c1,s) -P*\ (Parallel Rs, y) \ +lemma L3_5ii_lemma2 [rule_format (no_asm)]: + "\c1 c2 s t. (Seq c1 c2, s) -Pn\ (Parallel Ts, t) \ + (All_None Ts) \ (\y m Rs. (c1,s) -P*\ (Parallel Rs, y) \ (All_None Rs) \ (c2, y) -Pm\ (Parallel Ts, t) \ m \ n)" apply(induct "n") apply(force) @@ -176,9 +176,9 @@ apply (fast intro!: le_SucI elim!: relpow_imp_rtrancl converse_rtrancl_into_rtrancl) done -lemma L3_5ii_lemma3: - "\(Seq c1 c2,s) -P*\ (Parallel Ts,t); All_None Ts\ \ - (\y Rs. (c1,s) -P*\ (Parallel Rs,y) \ All_None Rs +lemma L3_5ii_lemma3: + "\(Seq c1 c2,s) -P*\ (Parallel Ts,t); All_None Ts\ \ + (\y Rs. (c1,s) -P*\ (Parallel Rs,y) \ All_None Rs \ (c2,y) -P*\ (Parallel Ts,t))" apply(drule rtrancl_imp_UN_relpow) apply(fast dest: L3_5ii_lemma2 relpow_imp_rtrancl) @@ -206,7 +206,7 @@ done -lemma L3_5v_lemma1[rule_format]: +lemma L3_5v_lemma1[rule_format]: "(S,s) -Pn\ (T,t) \ S=\ \ (\(\Rs. T=(Parallel Rs) \ All_None Rs))" apply (unfold UNIV_def) apply(rule nat_less_induct) @@ -238,8 +238,8 @@ apply(fast dest: L3_5v_lemma2) done -lemma L3_5v_lemma4 [rule_format]: - "\s. (While b i c, s) -Pn\ (Parallel Ts, t) \ All_None Ts \ +lemma L3_5v_lemma4 [rule_format]: + "\s. (While b i c, s) -Pn\ (Parallel Ts, t) \ All_None Ts \ (\k. (fwhile b c k, s) -P*\ (Parallel Ts, t))" apply(rule nat_less_induct) apply safe @@ -262,8 +262,8 @@ apply(fast elim: L3_5ii_lemma1) done -lemma L3_5v_lemma5 [rule_format]: - "\s. (fwhile b c k, s) -P*\ (Parallel Ts, t) \ All_None Ts \ +lemma L3_5v_lemma5 [rule_format]: + "\s. (fwhile b c k, s) -P*\ (Parallel Ts, t) \ All_None Ts \ (While b i c, s) -P*\ (Parallel Ts,t)" apply(induct "k") apply(force dest: L3_5v_lemma2) @@ -292,7 +292,7 @@ apply(fast intro: L3_5v_lemma5) done -section {* Validity of Correctness Formulas *} +section \Validity of Correctness Formulas\ definition com_validity :: "'a assn \ 'a com \ 'a assn \ bool" ("(3\= _// _//_)" [90,55,90] 50) where "\= p c q \ SEM c p \ q" diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/Quote_Antiquote.thy --- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,4 +1,4 @@ -section {* Concrete Syntax *} +section \Concrete Syntax\ theory Quote_Antiquote imports Main begin @@ -10,11 +10,11 @@ translations "\b\" \ "CONST Collect \b\" -parse_translation {* +parse_translation \ let fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t | quote_tr ts = raise TERM ("quote_tr", ts); in [(@{syntax_const "_quote"}, K quote_tr)] end -*} +\ end \ No newline at end of file diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/RG_Com.thy --- a/src/HOL/Hoare_Parallel/RG_Com.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Com.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,21 +1,21 @@ -chapter {* The Rely-Guarantee Method *} +chapter \The Rely-Guarantee Method\ -section {* Abstract Syntax *} +section \Abstract Syntax\ theory RG_Com imports Main begin -text {* Semantics of assertions and boolean expressions (bexp) as sets +text \Semantics of assertions and boolean expressions (bexp) as sets of states. Syntax of commands @{text com} and parallel commands -@{text par_com}. *} +@{text par_com}.\ type_synonym 'a bexp = "'a set" -datatype 'a com = +datatype 'a com = Basic "'a \'a" | Seq "'a com" "'a com" - | Cond "'a bexp" "'a com" "'a com" - | While "'a bexp" "'a com" - | Await "'a bexp" "'a com" + | Cond "'a bexp" "'a com" "'a com" + | While "'a bexp" "'a com" + | Await "'a bexp" "'a com" type_synonym 'a par_com = "'a com option list" diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/RG_Examples.thy --- a/src/HOL/Hoare_Parallel/RG_Examples.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,12 +1,12 @@ -section {* Examples *} +section \Examples\ theory RG_Examples imports RG_Syntax begin -lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def +lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def -subsection {* Set Elements of an Array to Zero *} +subsection \Set Elements of an Array to Zero\ lemma le_less_trans2: "\(j::nat) j\ \ i COBEGIN SCHEME [0 \ i < n] - (\A := \A [i := 0], - \ n < length \A \, - \ length \A = length \A \ \A ! i = \A ! i \, - \ length \A = length \A \ (\j j \ \A ! j = \A ! j) \, - \ \A ! i = 0 \) + (\A := \A [i := 0], + \ n < length \A \, + \ length \A = length \A \ \A ! i = \A ! i \, + \ length \A = length \A \ (\j j \ \A ! j = \A ! j) \, + \ \A ! i = 0 \) COEND SAT [\ n < length \A \, \ \A = \A \, \ True \, \ \i < n. \A ! i = 0 \]" apply(rule Parallel) -apply (auto intro!: Basic) +apply (auto intro!: Basic) done -lemma Example1_parameterized: +lemma Example1_parameterized: "k < t \ - \ COBEGIN - SCHEME [k*n\i<(Suc k)*n] (\A:=\A[i:=0], - \t*n < length \A\, - \t*n < length \A \ length \A=length \A \ \A!i = \A!i\, - \t*n < length \A \ length \A=length \A \ (\jA . i\j \ \A!j = \A!j)\, - \\A!i=0\) - COEND - SAT [\t*n < length \A\, - \t*n < length \A \ length \A=length \A \ (\iA!(k*n+i)=\A!(k*n+i))\, - \t*n < length \A \ length \A=length \A \ - (\iA . (i \A!i = \A!i) \ ((Suc k)*n \ i\ \A!i = \A!i))\, + \ COBEGIN + SCHEME [k*n\i<(Suc k)*n] (\A:=\A[i:=0], + \t*n < length \A\, + \t*n < length \A \ length \A=length \A \ \A!i = \A!i\, + \t*n < length \A \ length \A=length \A \ (\jA . i\j \ \A!j = \A!j)\, + \\A!i=0\) + COEND + SAT [\t*n < length \A\, + \t*n < length \A \ length \A=length \A \ (\iA!(k*n+i)=\A!(k*n+i))\, + \t*n < length \A \ length \A=length \A \ + (\iA . (i \A!i = \A!i) \ ((Suc k)*n \ i\ \A!i = \A!i))\, \\iA!(k*n+i) = 0\]" apply(rule Parallel) apply auto apply(erule_tac x="k*n +i" in allE) apply(subgoal_tac "k*n+i Increment a Variable in Parallel\ -subsubsection {* Two components *} +subsubsection \Two components\ record Example2 = x :: nat c_0 :: nat c_1 :: nat -lemma Example2: +lemma Example2: "\ COBEGIN - (\ \x:=\x+1;; \c_0:=\c_0 + 1 \, - \\x=\c_0 + \c_1 \ \c_0=0\, - \\c_0 = \c_0 \ - (\x=\c_0 + \c_1 - \ \x = \c_0 + \c_1)\, - \\c_1 = \c_1 \ - (\x=\c_0 + \c_1 + (\ \x:=\x+1;; \c_0:=\c_0 + 1 \, + \\x=\c_0 + \c_1 \ \c_0=0\, + \\c_0 = \c_0 \ + (\x=\c_0 + \c_1 + \ \x = \c_0 + \c_1)\, + \\c_1 = \c_1 \ + (\x=\c_0 + \c_1 \ \x =\c_0 + \c_1)\, \\x=\c_0 + \c_1 \ \c_0=1 \) \ - (\ \x:=\x+1;; \c_1:=\c_1+1 \, - \\x=\c_0 + \c_1 \ \c_1=0 \, - \\c_1 = \c_1 \ - (\x=\c_0 + \c_1 - \ \x = \c_0 + \c_1)\, - \\c_0 = \c_0 \ - (\x=\c_0 + \c_1 + (\ \x:=\x+1;; \c_1:=\c_1+1 \, + \\x=\c_0 + \c_1 \ \c_1=0 \, + \\c_1 = \c_1 \ + (\x=\c_0 + \c_1 + \ \x = \c_0 + \c_1)\, + \\c_0 = \c_0 \ + (\x=\c_0 + \c_1 \ \x =\c_0 + \c_1)\, \\x=\c_0 + \c_1 \ \c_1=1\) COEND - SAT [\\x=0 \ \c_0=0 \ \c_1=0\, + SAT [\\x=0 \ \c_0=0 \ \c_1=0\, \\x=\x \ \c_0= \c_0 \ \c_1=\c_1\, \True\, \\x=2\]" @@ -151,9 +151,9 @@ apply(auto intro!: Basic) done -subsubsection {* Parameterized *} +subsubsection \Parameterized\ -lemma Example2_lemma2_aux: "j +lemma Example2_lemma2_aux: "j (\i=0..i=0..i=0.. s \ (\i::nat=0..i=0..j \ Suc (\i::nat=0..i=0..i::nat=0..< n. b i)=(\i=0..< n. (b (j:=Suc 0)) i)" by(simp add:Example2_lemma2) -record Example2_parameterized = +record Example2_parameterized = C :: "nat \ nat" y :: nat -lemma Example2_parameterized: "0 +lemma Example2_parameterized: "0 \ COBEGIN SCHEME [0\i \y:=\y+1;; \C:=\C (i:=1) \, - \\y=(\i=0..C i) \ \C i=0\, - \\C i = \C i \ - (\y=(\i=0..C i) \ \y =(\i=0..C i))\, - \(\jj \ \C j = \C j) \ + (\ \y:=\y+1;; \C:=\C (i:=1) \, + \\y=(\i=0..C i) \ \C i=0\, + \\C i = \C i \ + (\y=(\i=0..C i) \ \y =(\i=0..C i))\, + \(\jj \ \C j = \C j) \ (\y=(\i=0..C i) \ \y =(\i=0..C i))\, - \\y=(\i=0..C i) \ \C i=1\) + \\y=(\i=0..C i) \ \C i=1\) COEND SAT [\\y=0 \ (\i=0..C i)=0 \, \\C=\C \ \y=\y\, \True\, \\y=n\]" apply(rule Parallel) @@ -229,9 +229,9 @@ apply simp_all done -subsection {* Find Least Element *} +subsection \Find Least Element\ -text {* A previous lemma: *} +text \A previous lemma:\ lemma mod_aux :"\i < (n::nat); a mod n = i; j < a + n; j mod n = i; a < j\ \ False" apply(subgoal_tac "a=a div n*n + a mod n" ) @@ -251,25 +251,25 @@ X :: "nat \ nat" Y :: "nat \ nat" -lemma Example3: "m mod n=0 \ - \ COBEGIN +lemma Example3: "m mod n=0 \ + \ COBEGIN SCHEME [0\ijX i < \Y j) DO - IF P(B!(\X i)) THEN \Y:=\Y (i:=\X i) - ELSE \X:= \X (i:=(\X i)+ n) FI + (WHILE (\jX i < \Y j) DO + IF P(B!(\X i)) THEN \Y:=\Y (i:=\X i) + ELSE \X:= \X (i:=(\X i)+ n) FI OD, \(\X i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ (\Y i P(B!(\Y i)) \ \Y i\ m+i)\, - \(\jj \ \Y j \ \Y j) \ \X i = \X i \ + \(\jj \ \Y j \ \Y j) \ \X i = \X i \ \Y i = \Y i\, - \(\jj \ \X j = \X j \ \Y j = \Y j) \ + \(\jj \ \X j = \X j \ \Y j = \Y j) \ \Y i \ \Y i\, - \(\X i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ (\Y i P(B!(\Y i)) \ \Y i\ m+i) \ (\jY j \ \X i) \) + \(\X i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ (\Y i P(B!(\Y i)) \ \Y i\ m+i) \ (\jY j \ \X i) \) COEND SAT [\ \iX i=i \ \Y i=m+i \,\\X=\X \ \Y=\Y\,\True\, - \\iX i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ + \\iX i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ (\Y i P(B!(\Y i)) \ \Y i\ m+i) \ (\jY j \ \X i)\]" apply(rule Parallel) ---{*5 subgoals left *} +--\5 subgoals left\ apply force+ apply clarify apply simp @@ -298,29 +298,29 @@ apply auto done -text {* Same but with a list as auxiliary variable: *} +text \Same but with a list as auxiliary variable:\ record Example3_list = X :: "nat list" Y :: "nat list" lemma Example3_list: "m mod n=0 \ \ (COBEGIN SCHEME [0\ijX!i < \Y!j) DO - IF P(B!(\X!i)) THEN \Y:=\Y[i:=\X!i] ELSE \X:= \X[i:=(\X!i)+ n] FI + (WHILE (\jX!i < \Y!j) DO + IF P(B!(\X!i)) THEN \Y:=\Y[i:=\X!i] ELSE \X:= \X[i:=(\X!i)+ n] FI OD, \nX \ nY \ (\X!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i)\, - \(\jj \ \Y!j \ \Y!j) \ \X!i = \X!i \ + \(\jj \ \Y!j \ \Y!j) \ \X!i = \X!i \ \Y!i = \Y!i \ length \X = length \X \ length \Y = length \Y\, - \(\jj \ \X!j = \X!j \ \Y!j = \Y!j) \ + \(\jj \ \X!j = \X!j \ \Y!j = \Y!j) \ \Y!i \ \Y!i \ length \X = length \X \ length \Y = length \Y\, \(\X!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i) \ (\jY!j \ \X!i) \) COEND) SAT [\nX \ nY \ (\iX!i=i \ \Y!i=m+i) \, \\X=\X \ \Y=\Y\, \True\, - \\iX!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ + \\iX!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i) \ (\jY!j \ \X!i)\]" apply (rule Parallel) -apply (auto cong del: strong_INF_cong strong_SUP_cong) +apply (auto cong del: strong_INF_cong strong_SUP_cong) apply force apply (rule While) apply force diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/RG_Hoare.thy --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,23 +1,23 @@ -section {* The Proof System *} +section \The Proof System\ theory RG_Hoare imports RG_Tran begin -subsection {* Proof System for Component Programs *} +subsection \Proof System for Component Programs\ declare Un_subset_iff [simp del] sup.bounded_iff [simp del] -definition stable :: "'a set \ ('a \ 'a) set \ bool" where - "stable \ \f g. (\x y. x \ f \ (x, y) \ g \ y \ f)" +definition stable :: "'a set \ ('a \ 'a) set \ bool" where + "stable \ \f g. (\x y. x \ f \ (x, y) \ g \ y \ f)" inductive - rghoare :: "['a com, 'a set, ('a \ 'a) set, ('a \ 'a) set, 'a set] \ bool" + rghoare :: "['a com, 'a set, ('a \ 'a) set, ('a \ 'a) set, 'a set] \ bool" ("\ _ sat [_, _, _, _]" [60,0,0,0,0] 45) where - Basic: "\ pre \ {s. f s \ post}; {(s,t). s \ pre \ (t=f s \ t=s)} \ guar; - stable pre rely; stable post rely \ + Basic: "\ pre \ {s. f s \ post}; {(s,t). s \ pre \ (t=f s \ t=s)} \ guar; + stable pre rely; stable post rely \ \ \ Basic f sat [pre, rely, guar, post]" -| Seq: "\ \ P sat [pre, rely, guar, mid]; \ Q sat [mid, rely, guar, post] \ +| Seq: "\ \ P sat [pre, rely, guar, mid]; \ Q sat [mid, rely, guar, post] \ \ \ Seq P Q sat [pre, rely, guar, post]" | Cond: "\ stable pre rely; \ P1 sat [pre \ b, rely, guar, post]; @@ -28,11 +28,11 @@ \ P sat [pre \ b, rely, guar, pre]; \s. (s,s)\guar \ \ \ While b P sat [pre, rely, guar, post]" -| Await: "\ stable pre rely; stable post rely; - \V. \ P sat [pre \ b \ {V}, {(s, t). s = t}, +| Await: "\ stable pre rely; stable post rely; + \V. \ P sat [pre \ b \ {V}, {(s, t). s = t}, UNIV, {s. (V, s) \ guar} \ post] \ \ \ Await b P sat [pre, rely, guar, post]" - + | Conseq: "\ pre \ pre'; rely \ rely'; guar' \ guar; post' \ post; \ P sat [pre', rely', guar', post'] \ \ \ P sat [pre, rely, guar, post]" @@ -52,7 +52,7 @@ definition Com :: "'a rgformula \ 'a com" where "Com x \ fst x" -subsection {* Proof System for Parallel Programs *} +subsection \Proof System for Parallel Programs\ type_synonym 'a par_rgformula = "('a rgformula) list \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set" @@ -61,20 +61,20 @@ par_rghoare :: "('a rgformula) list \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set \ bool" ("\ _ SAT [_, _, _, _]" [60,0,0,0,0] 45) where - Parallel: + Parallel: "\ \i (\j\{j. j j\i}. Guar(xs!j)) \ Rely(xs!i); (\j\{j. j guar; - pre \ (\i\{i. i (\i\{i. ii\{i. i post; \i Com(xs!i) sat [Pre(xs!i),Rely(xs!i),Guar(xs!i),Post(xs!i)] \ \ \ xs SAT [pre, rely, guar, post]" -section {* Soundness*} +section \Soundness\ -subsubsection {* Some previous lemmas *} +subsubsection \Some previous lemmas\ -lemma tl_of_assum_in_assum: - "(P, s) # (P, t) # xs \ assum (pre, rely) \ stable pre rely +lemma tl_of_assum_in_assum: + "(P, s) # (P, t) # xs \ assum (pre, rely) \ stable pre rely \ (P, t) # xs \ assum (pre, rely)" apply(simp add:assum_def) apply clarify @@ -88,51 +88,51 @@ apply simp done -lemma etran_in_comm: +lemma etran_in_comm: "(P, t) # xs \ comm(guar, post) \ (P, s) # (P, t) # xs \ comm(guar, post)" apply(simp add:comm_def) apply clarify apply(case_tac i,simp+) done -lemma ctran_in_comm: - "\(s, s) \ guar; (Q, s) # xs \ comm(guar, post)\ +lemma ctran_in_comm: + "\(s, s) \ guar; (Q, s) # xs \ comm(guar, post)\ \ (P, s) # (Q, s) # xs \ comm(guar, post)" apply(simp add:comm_def) apply clarify apply(case_tac i,simp+) done -lemma takecptn_is_cptn [rule_format, elim!]: +lemma takecptn_is_cptn [rule_format, elim!]: "\j. c \ cptn \ take (Suc j) c \ cptn" apply(induct "c") apply(force elim: cptn.cases) apply clarify -apply(case_tac j) +apply(case_tac j) apply simp apply(rule CptnOne) apply simp apply(force intro:cptn.intros elim:cptn.cases) done -lemma dropcptn_is_cptn [rule_format,elim!]: +lemma dropcptn_is_cptn [rule_format,elim!]: "\j cptn \ drop j c \ cptn" apply(induct "c") apply(force elim: cptn.cases) apply clarify -apply(case_tac j,simp+) +apply(case_tac j,simp+) apply(erule cptn.cases) apply simp apply force apply force done -lemma takepar_cptn_is_par_cptn [rule_format,elim]: +lemma takepar_cptn_is_par_cptn [rule_format,elim]: "\j. c \ par_cptn \ take (Suc j) c \ par_cptn" apply(induct "c") apply(force elim: cptn.cases) apply clarify -apply(case_tac j,simp) +apply(case_tac j,simp) apply(rule ParCptnOne) apply(force intro:par_cptn.intros elim:par_cptn.cases) done @@ -142,7 +142,7 @@ apply(induct "c") apply(force elim: par_cptn.cases) apply clarify -apply(case_tac j,simp+) +apply(case_tac j,simp+) apply(erule par_cptn.cases) apply simp apply force @@ -150,11 +150,11 @@ done lemma tl_of_cptn_is_cptn: "\x # xs \ cptn; xs \ []\ \ xs \ cptn" -apply(subgoal_tac "1 < length (x # xs)") +apply(subgoal_tac "1 < length (x # xs)") apply(drule dropcptn_is_cptn,simp+) done -lemma not_ctran_None [rule_format]: +lemma not_ctran_None [rule_format]: "\s. (None, s)#xs \ cptn \ (\i xs!i)" apply(induct xs,simp+) apply clarify @@ -170,9 +170,9 @@ apply(force elim:cptn.cases) done -lemma etran_or_ctran [rule_format]: - "\m i. x\cptn \ m \ length x - \ (\i. Suc i < m \ \ x!i -c\ x!Suc i) \ Suc i < m +lemma etran_or_ctran [rule_format]: + "\m i. x\cptn \ m \ length x + \ (\i. Suc i < m \ \ x!i -c\ x!Suc i) \ Suc i < m \ x!i -e\ x!Suc i" apply(induct x,simp) apply clarify @@ -189,7 +189,7 @@ apply(erule_tac x="0" and P="\j. ?H j \ (?J j) \ ctran" in allE,simp) done -lemma etran_or_ctran2 [rule_format]: +lemma etran_or_ctran2 [rule_format]: "\i. Suc i x\cptn \ (x!i -c\ x!Suc i \ \ x!i -e\ x!Suc i) \ (x!i -e\ x!Suc i \ \ x!i -c\ x!Suc i)" apply(induct x) @@ -202,15 +202,15 @@ apply simp done -lemma etran_or_ctran2_disjI1: +lemma etran_or_ctran2_disjI1: "\ x\cptn; Suc i x!Suc i\ \ \ x!i -e\ x!Suc i" by(drule etran_or_ctran2,simp_all) -lemma etran_or_ctran2_disjI2: +lemma etran_or_ctran2_disjI2: "\ x\cptn; Suc i x!Suc i\ \ \ x!i -c\ x!Suc i" by(drule etran_or_ctran2,simp_all) -lemma not_ctran_None2 [rule_format]: +lemma not_ctran_None2 [rule_format]: "\ (None, s) # xs \cptn; i \ \ ((None, s) # xs) ! i -c\ xs ! i" apply(frule not_ctran_None,simp) apply(case_tac i,simp) @@ -226,11 +226,11 @@ apply(case_tac "\m. m \ P m") apply auto done - -lemma stability [rule_format]: + +lemma stability [rule_format]: "\j k. x \ cptn \ stable p rely \ j\k \ k snd(x!j)\p \ - (\i. (Suc i) - (x!i -e\ x!(Suc i)) \ (snd(x!i), snd(x!(Suc i))) \ rely) \ + (\i. (Suc i) + (x!i -e\ x!(Suc i)) \ (snd(x!i), snd(x!(Suc i))) \ rely) \ (\i. j\i \ i x!i -e\ x!Suc i) \ snd(x!k)\p \ fst(x!j)=fst(x!k)" apply(induct x) apply clarify @@ -239,7 +239,7 @@ apply(erule cptn.cases,simp) apply simp apply(case_tac k,simp,simp) - apply(case_tac j,simp) + apply(case_tac j,simp) apply(erule_tac x=0 in allE) apply(erule_tac x="nat" and P="\j. (0\j) \ (?J j)" in allE,simp) apply(subgoal_tac "t\p") @@ -252,7 +252,7 @@ apply(simp(no_asm_use) only:stable_def) apply(erule_tac x=s in allE) apply(erule_tac x=t in allE) - apply simp + apply simp apply(erule mp) apply(erule mp) apply(rule Env) @@ -277,13 +277,13 @@ apply(erule_tac x="Suc i" and P="\j. (?H j) \ (?J j) \ (?T j)\rely" in allE,simp) done -subsection {* Soundness of the System for Component Programs *} +subsection \Soundness of the System for Component Programs\ -subsubsection {* Soundness of the Basic rule *} +subsubsection \Soundness of the Basic rule\ -lemma unique_ctran_Basic [rule_format]: - "\s i. x \ cptn \ x ! 0 = (Some (Basic f), s) \ - Suc i x!i -c\ x!Suc i \ +lemma unique_ctran_Basic [rule_format]: + "\s i. x \ cptn \ x ! 0 = (Some (Basic f), s) \ + Suc i x!i -c\ x!Suc i \ (\j. Suc j i\j \ x!j -e\ x!Suc j)" apply(induct x,simp) apply simp @@ -306,8 +306,8 @@ apply(erule etranE,simp) done -lemma exists_ctran_Basic_None [rule_format]: - "\s i. x \ cptn \ x ! 0 = (Some (Basic f), s) +lemma exists_ctran_Basic_None [rule_format]: + "\s i. x \ cptn \ x ! 0 = (Some (Basic f), s) \ i fst(x!i)=None \ (\j x!Suc j)" apply(induct x,simp) apply simp @@ -322,8 +322,8 @@ apply(rule_tac x=0 in exI,simp) done -lemma Basic_sound: - " \pre \ {s. f s \ post}; {(s, t). s \ pre \ t = f s} \ guar; +lemma Basic_sound: + " \pre \ {s. f s \ post}; {(s, t). s \ pre \ t = f s} \ guar; stable pre rely; stable post rely\ \ \ Basic f sat [pre, rely, guar, post]" apply(unfold com_validity_def) @@ -374,11 +374,11 @@ apply(simp add:last_length)+ done -subsubsection{* Soundness of the Await rule *} +subsubsection\Soundness of the Await rule\ -lemma unique_ctran_Await [rule_format]: - "\s i. x \ cptn \ x ! 0 = (Some (Await b c), s) \ - Suc i x!i -c\ x!Suc i \ +lemma unique_ctran_Await [rule_format]: + "\s i. x \ cptn \ x ! 0 = (Some (Await b c), s) \ + Suc i x!i -c\ x!Suc i \ (\j. Suc j i\j \ x!j -e\ x!Suc j)" apply(induct x,simp+) apply clarify @@ -399,8 +399,8 @@ apply(erule etranE,simp) done -lemma exists_ctran_Await_None [rule_format]: - "\s i. x \ cptn \ x ! 0 = (Some (Await b c), s) +lemma exists_ctran_Await_None [rule_format]: + "\s i. x \ cptn \ x ! 0 = (Some (Await b c), s) \ i fst(x!i)=None \ (\j x!Suc j)" apply(induct x,simp+) apply clarify @@ -414,7 +414,7 @@ apply(rule_tac x=0 in exI,simp) done -lemma Star_imp_cptn: +lemma Star_imp_cptn: "(P, s) -c*\ (R, t) \ \l \ cp P s. (last l)=(R, t) \ (\i. Suc i l!i -c\ l!Suc i)" apply (erule converse_rtrancl_induct2) @@ -438,12 +438,12 @@ apply(erule CptnComp) apply clarify done - -lemma Await_sound: + +lemma Await_sound: "\stable pre rely; stable post rely; - \V. \ P sat [pre \ b \ {s. s = V}, {(s, t). s = t}, + \V. \ P sat [pre \ b \ {s. s = V}, {(s, t). s = t}, UNIV, {s. (V, s) \ guar} \ post] \ - \ P sat [pre \ b \ {s. s = V}, {(s, t). s = t}, + \ P sat [pre \ b \ {s. s = V}, {(s, t). s = t}, UNIV, {s. (V, s) \ guar} \ post] \ \ \ Await b P sat [pre, rely, guar, post]" apply(unfold com_validity_def) @@ -458,9 +458,9 @@ apply(subgoal_tac "x\ cp (Some(Await b P)) s") apply(erule_tac i=i in unique_ctran_Await,force,simp_all) apply(simp add:cp_def) ---{* here starts the different part. *} +--\here starts the different part.\ apply(erule ctran.cases,simp_all) - apply(drule Star_imp_cptn) + apply(drule Star_imp_cptn) apply clarify apply(erule_tac x=sa in allE) apply clarify @@ -491,7 +491,7 @@ apply(case_tac "x!Suc j",simp) apply(rule ctran.cases,simp) apply(simp_all) -apply(drule Star_imp_cptn) +apply(drule Star_imp_cptn) apply clarify apply(erule_tac x=sa in allE) apply clarify @@ -512,10 +512,10 @@ apply(simp add:last_length)+ done -subsubsection{* Soundness of the Conditional rule *} +subsubsection\Soundness of the Conditional rule\ -lemma Cond_sound: - "\ stable pre rely; \ P1 sat [pre \ b, rely, guar, post]; +lemma Cond_sound: + "\ stable pre rely; \ P1 sat [pre \ b, rely, guar, post]; \ P2 sat [pre \ - b, rely, guar, post]; \s. (s,s)\guar\ \ \ (Cond b P1 P2) sat [pre, rely, guar, post]" apply(unfold com_validity_def) @@ -578,7 +578,7 @@ apply arith done -subsubsection{* Soundness of the Sequential rule *} +subsubsection\Soundness of the Sequential rule\ inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\ t" @@ -591,9 +591,9 @@ apply simp done -lemma Seq_sound1 [rule_format]: - "x\ cptn_mod \ \s P. x !0=(Some (Seq P Q), s) \ - (\iSome Q) \ +lemma Seq_sound1 [rule_format]: + "x\ cptn_mod \ \s P. x !0=(Some (Seq P Q), s) \ + (\iSome Q) \ (\xs\ cp (Some P) s. x=map (lift Q) xs)" apply(erule cptn_mod.induct) apply(unfold cp_def) @@ -619,11 +619,11 @@ apply simp done -lemma Seq_sound2 [rule_format]: - "x \ cptn \ \s P i. x!0=(Some (Seq P Q), s) \ i cptn \ \s P i. x!0=(Some (Seq P Q), s) \ i fst(x!i)=Some Q \ (\j(Some Q)) \ - (\xs ys. xs \ cp (Some P) s \ length xs=Suc i + (\xs ys. xs \ cp (Some P) s \ length xs=Suc i \ ys \ cp (Some Q) (snd(xs !i)) \ x=(map (lift Q) xs)@tl ys)" apply(erule cptn.induct) apply(unfold cp_def) @@ -668,7 +668,7 @@ apply(rule tl_zero,simp+) apply force apply(rule conjI,simp add:lift_def) -apply(subgoal_tac "lift Q (Some P2, ta) =(Some (Seq P2 Q), ta)") +apply(subgoal_tac "lift Q (Some P2, ta) =(Some (Seq P2 Q), ta)") apply(simp add:Cons_lift del:list.map) apply(rule nth_tl_if) apply force @@ -697,7 +697,7 @@ apply simp done -lemma Seq_sound: +lemma Seq_sound: "\\ P sat [pre, rely, guar, mid]; \ Q sat [mid, rely, guar, post]\ \ \ Seq P Q sat [pre, rely, guar, post]" apply(unfold com_validity_def) @@ -740,7 +740,7 @@ apply (simp del:list.map) apply(simp only:last_lift_not_None) apply simp ---{* @{text "\i@{text "\i apply(erule exE) apply(drule_tac n=i and P="\i. i < length x \ fst (x ! i) = Some Q" in Ex_first_occurrence) apply clarify @@ -756,7 +756,7 @@ apply(simp add:cp_def assum_def nth_append) apply clarify apply(erule_tac x=i in allE) - back + back apply(simp add:snd_lift) apply(erule mp) apply(force elim:etranE intro:Env simp add:lift_def) @@ -780,7 +780,7 @@ apply(erule mp) apply(case_tac "xs!m") apply(force elim:etran.cases intro:Env simp add:lift_def) - apply simp + apply simp apply simp apply clarify apply(rule conjI,clarify) @@ -788,12 +788,12 @@ apply(simp add:snd_lift) apply(erule allE, erule impE, assumption, erule mp) apply(case_tac "(xs ! i)") - apply(case_tac "(xs ! Suc i)") - apply(case_tac "fst(xs ! i)",force simp add:lift_def) + apply(case_tac "(xs ! Suc i)") + apply(case_tac "fst(xs ! i)",force simp add:lift_def) apply(case_tac "fst(xs ! Suc i)") apply (force simp add:lift_def) apply (force simp add:lift_def) - apply(erule_tac x="i-m" in allE) + apply(erule_tac x="i-m" in allE) back back apply(subgoal_tac "Suc (i - m) < length ys",simp) @@ -812,7 +812,7 @@ apply(case_tac "xs!m",case_tac "fst(xs!m)",simp add:lift_def snd_lift) apply(case_tac ys,simp+) apply(simp add:lift_def) - apply simp + apply simp apply force apply clarify apply(rule tl_zero) @@ -834,7 +834,7 @@ apply(case_tac ys,simp+) done -subsubsection{* Soundness of the While rule *} +subsubsection\Soundness of the While rule\ lemma last_append[rule_format]: "\xs. ys\[] \ ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))" @@ -844,10 +844,10 @@ apply (simp add:nth_append) done -lemma assum_after_body: - "\ \ P sat [pre \ b, rely, guar, pre]; +lemma assum_after_body: + "\ \ P sat [pre \ b, rely, guar, pre]; (Some P, s) # xs \ cptn_mod; fst (last ((Some P, s) # xs)) = None; s \ b; - (Some (While b P), s) # (Some (Seq P (While b P)), s) # + (Some (While b P), s) # (Some (Seq P (While b P)), s) # map (lift (While b P)) xs @ ys \ assum (pre, rely)\ \ (Some (While b P), snd (last ((Some P, s) # xs))) # ys \ assum (pre, rely)" apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod) @@ -875,20 +875,20 @@ apply(simp add:Cons_lift_append nth_append snd_lift) done -lemma While_sound_aux [rule_format]: +lemma While_sound_aux [rule_format]: "\ pre \ - b \ post; \ P sat [pre \ b, rely, guar, pre]; \s. (s, s) \ guar; - stable pre rely; stable post rely; x \ cptn_mod \ + stable pre rely; stable post rely; x \ cptn_mod \ \ \s xs. x=(Some(While b P),s)#xs \ x\assum(pre, rely) \ x \ comm (guar, post)" apply(erule cptn_mod.induct) apply safe apply (simp_all del:last.simps) ---{* 5 subgoals left *} +--\5 subgoals left\ apply(simp add:comm_def) ---{* 4 subgoals left *} +--\4 subgoals left\ apply(rule etran_in_comm) apply(erule mp) apply(erule tl_of_assum_in_assum,simp) ---{* While-None *} +--\While-None\ apply(ind_cases "((Some (While b P), s), None, t) \ ctran" for s t) apply(simp add:comm_def) apply(simp add:cptn_iff_cptn_mod [THEN sym]) @@ -908,12 +908,12 @@ apply(force simp add:assum_def subsetD) apply(simp add:assum_def) apply clarify - apply(erule_tac x="i" in allE,simp) - apply(erule_tac x="Suc i" in allE,simp) + apply(erule_tac x="i" in allE,simp) + apply(erule_tac x="Suc i" in allE,simp) apply simp apply clarify apply (simp add:last_length) ---{* WhileOne *} +--\WhileOne\ apply(thin_tac "P = While b P \ ?Q") apply(rule ctran_in_comm,simp) apply(simp add:Cons_lift del:list.map) @@ -949,23 +949,23 @@ apply(case_tac "fst(xs!i)") apply force apply force ---{* last=None *} +--\last=None\ apply clarify apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\[]") apply(drule last_conv_nth) apply (simp del:list.map) apply(simp only:last_lift_not_None) apply simp ---{* WhileMore *} +--\WhileMore\ apply(thin_tac "P = While b P \ ?Q") apply(rule ctran_in_comm,simp del:last.simps) ---{* metiendo la hipotesis antes de dividir la conclusion. *} +--\metiendo la hipotesis antes de dividir la conclusion.\ apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \ assum (pre, rely)") apply (simp del:last.simps) prefer 2 apply(erule assum_after_body) apply (simp del:last.simps)+ ---{* lo de antes. *} +--\lo de antes.\ apply(simp add:comm_def del:list.map last.simps) apply(rule conjI) apply clarify @@ -1001,8 +1001,8 @@ apply(case_tac "fst(xs!i)") apply force apply force ---{* @{text "i \ length xs"} *} -apply(subgoal_tac "i-length xs @{text "i \ length xs"}\ +apply(subgoal_tac "i-length xs length xs"} *} +--\@{text "i>length xs"}\ apply(case_tac "i-length xs") apply arith apply(simp add:nth_append del:list.map last.simps) @@ -1021,7 +1021,7 @@ prefer 2 apply arith apply simp ---{* last=None *} +--\last=None\ apply clarify apply(case_tac ys) apply(simp add:Cons_lift del:list.map last.simps) @@ -1042,7 +1042,7 @@ apply simp done -lemma While_sound: +lemma While_sound: "\stable pre rely; pre \ - b \ post; stable post rely; \ P sat [pre \ b, rely, guar, pre]; \s. (s,s)\guar\ \ \ While b P sat [pre, rely, guar, post]" @@ -1063,10 +1063,10 @@ apply(case_tac x,simp+) done -subsubsection{* Soundness of the Rule of Consequence *} +subsubsection\Soundness of the Rule of Consequence\ -lemma Conseq_sound: - "\pre \ pre'; rely \ rely'; guar' \ guar; post' \ post; +lemma Conseq_sound: + "\pre \ pre'; rely \ rely'; guar' \ guar; post' \ post; \ P sat [pre', rely', guar', post']\ \ \ P sat [pre, rely, guar, post]" apply(simp add:com_validity_def assum_def comm_def) @@ -1077,9 +1077,9 @@ apply force done -subsubsection {* Soundness of the system for sequential component programs *} +subsubsection \Soundness of the system for sequential component programs\ -theorem rgsound: +theorem rgsound: "\ P sat [pre, rely, guar, post] \ \ P sat [pre, rely, guar, post]" apply(erule rghoare.induct) apply(force elim:Basic_sound) @@ -1088,42 +1088,42 @@ apply(force elim:While_sound) apply(force elim:Await_sound) apply(erule Conseq_sound,simp+) -done +done -subsection {* Soundness of the System for Parallel Programs *} +subsection \Soundness of the System for Parallel Programs\ definition ParallelCom :: "('a rgformula) list \ 'a par_com" where - "ParallelCom Ps \ map (Some \ fst) Ps" + "ParallelCom Ps \ map (Some \ fst) Ps" -lemma two: - "\ \i (\j\{j. j < length xs \ j \ i}. Guar (xs ! j)) +lemma two: + "\ \i (\j\{j. j < length xs \ j \ i}. Guar (xs ! j)) \ Rely (xs ! i); pre \ (\i\{i. i < length xs}. Pre (xs ! i)); - \ii Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)]; length xs=length clist; x \ par_cp (ParallelCom xs) s; x\par_assum(pre, rely); \icp (Some(Com(xs!i))) s; x \ clist \ - \ \j i. i Suc j (clist!i!j) -c\ (clist!i!Suc j) + \ \j i. i Suc j (clist!i!j) -c\ (clist!i!Suc j) \ (snd(clist!i!j), snd(clist!i!Suc j)) \ Guar(xs!i)" apply(unfold par_cp_def) -apply (rule ccontr) ---{* By contradiction: *} +apply (rule ccontr) +--\By contradiction:\ apply simp apply(erule exE) ---{* the first c-tran that does not satisfy the guarantee-condition is from @{text "\_i"} at step @{text "m"}. *} +--\the first c-tran that does not satisfy the guarantee-condition is from @{text "\_i"} at step @{text "m"}.\ apply(drule_tac n=j and P="\j. \i. ?H i j" in Ex_first_occurrence) apply(erule exE) apply clarify ---{* @{text "\_i \ A(pre, rely_1)"} *} +--\@{text "\_i \ A(pre, rely_1)"}\ apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \ assum(Pre(xs!i), Rely(xs!i))") ---{* but this contradicts @{text "\ \_i sat [pre_i,rely_i,guar_i,post_i]"} *} +--\but this contradicts @{text "\ \_i sat [pre_i,rely_i,guar_i,post_i]"}\ apply(erule_tac x=i and P="\i. ?H i \ \ (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption) apply(simp add:com_validity_def) apply(erule_tac x=s in allE) apply(simp add:cp_def comm_def) apply(drule_tac c="take (Suc (Suc m)) (clist ! i)" in subsetD) apply simp - apply (blast intro: takecptn_is_cptn) + apply (blast intro: takecptn_is_cptn) apply simp apply clarify apply(erule_tac x=m and P="\j. ?I j \ ?J j \ ?H j" in allE) @@ -1142,9 +1142,9 @@ apply(simp add:conjoin_def compat_label_def) apply clarify apply(erule_tac x=ia and P="\j. ?H j \ (?P j) \ ?Q j" in allE,simp) ---{* each etran in @{text "\_1[0\m]"} corresponds to *} +--\each etran in @{text "\_1[0\m]"} corresponds to\ apply(erule disjE) ---{* a c-tran in some @{text "\_{ib}"} *} +--\a c-tran in some @{text "\_{ib}"}\ apply clarify apply(case_tac "i=ib",simp) apply(erule etranE,simp) @@ -1160,21 +1160,21 @@ apply(simp add:same_state_def) apply(erule_tac x=i and P="\j. (?T j) \ (\i. (?H j i) \ (snd (?d j i))=(snd (?e j i)))" in all_dupE) apply(erule_tac x=ib and P="\j. (?T j) \ (\i. (?H j i) \ (snd (?d j i))=(snd (?e j i)))" in allE,simp) ---{* or an e-tran in @{text "\"}, -therefore it satisfies @{text "rely \ guar_{ib}"} *} +--\or an e-tran in @{text "\"}, +therefore it satisfies @{text "rely \ guar_{ib}"}\ apply (force simp add:par_assum_def same_state_def) done -lemma three [rule_format]: - "\ xs\[]; \i (\j\{j. j < length xs \ j \ i}. Guar (xs ! j)) +lemma three [rule_format]: + "\ xs\[]; \i (\j\{j. j < length xs \ j \ i}. Guar (xs ! j)) \ Rely (xs ! i); pre \ (\i\{i. i < length xs}. Pre (xs ! i)); - \ii Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)]; length xs=length clist; x \ par_cp (ParallelCom xs) s; x \ par_assum(pre, rely); \icp (Some(Com(xs!i))) s; x \ clist \ - \ \j i. i Suc j (clist!i!j) -e\ (clist!i!Suc j) + \ \j i. i Suc j (clist!i!j) -e\ (clist!i!Suc j) \ (snd(clist!i!j), snd(clist!i!Suc j)) \ rely \ (\j\{j. j < length xs \ j \ i}. Guar (xs ! j))" apply(drule two) apply simp_all @@ -1196,14 +1196,14 @@ apply(erule_tac x=ia and P="\j. (?T j) \ (\i. (?H j i) \ (snd (?d j i))=(snd (?e j i)))" in allE,simp) done -lemma four: - "\xs\[]; \i < length xs. rely \ (\j\{j. j < length xs \ j \ i}. Guar (xs ! j)) +lemma four: + "\xs\[]; \i < length xs. rely \ (\j\{j. j < length xs \ j \ i}. Guar (xs ! j)) \ Rely (xs ! i); - (\j\{j. j < length xs}. Guar (xs ! j)) \ guar; + (\j\{j. j < length xs}. Guar (xs ! j)) \ guar; pre \ (\i\{i. i < length xs}. Pre (xs ! i)); \i < length xs. \ Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)]; - x \ par_cp (ParallelCom xs) s; x \ par_assum (pre, rely); Suc i < length x; + x \ par_cp (ParallelCom xs) s; x \ par_assum (pre, rely); Suc i < length x; x ! i -pc\ x ! Suc i\ \ (snd (x ! i), snd (x ! Suc i)) \ guar" apply(simp add: ParallelCom_def) @@ -1247,14 +1247,14 @@ apply(force elim:par_cptn.cases) done -lemma five: +lemma five: "\xs\[]; \i (\j\{j. j < length xs \ j \ i}. Guar (xs ! j)) \ Rely (xs ! i); - pre \ (\i\{i. i < length xs}. Pre (xs ! i)); + pre \ (\i\{i. i < length xs}. Pre (xs ! i)); (\i\{i. i < length xs}. Post (xs ! i)) \ post; \i < length xs. \ Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)]; - x \ par_cp (ParallelCom xs) s; x \ par_assum (pre, rely); + x \ par_cp (ParallelCom xs) s; x \ par_assum (pre, rely); All_None (fst (last x)) \ \ snd (last x) \ post" apply(simp add: ParallelCom_def) apply(subgoal_tac "(map (Some \ fst) xs)\[]") @@ -1316,8 +1316,8 @@ apply(simp add:conjoin_def same_length_def) done -lemma ParallelEmpty [rule_format]: - "\i s. x \ par_cp (ParallelCom []) s \ +lemma ParallelEmpty [rule_format]: + "\i s. x \ par_cp (ParallelCom []) s \ Suc i < length x \ (x ! i, x ! Suc i) \ par_ctran" apply(induct_tac x) apply(simp add:par_cp_def ParallelCom_def) @@ -1335,8 +1335,8 @@ apply simp done -theorem par_rgsound: - "\ c SAT [pre, rely, guar, post] \ +theorem par_rgsound: + "\ c SAT [pre, rely, guar, post] \ \ (ParallelCom c) SAT [pre, rely, guar, post]" apply(erule par_rghoare.induct) apply(case_tac xs,simp) @@ -1368,7 +1368,7 @@ apply(assumption+) apply clarify apply (erule allE, erule impE, assumption,erule rgsound) - apply(assumption+) + apply(assumption+) done end diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/RG_Syntax.thy --- a/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Syntax.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,4 +1,4 @@ -section {* Concrete Syntax *} +section \Concrete Syntax\ theory RG_Syntax imports RG_Hoare Quote_Antiquote @@ -45,17 +45,17 @@ translations "_prg_scheme j i k c" \ "(CONST map (\i. c) [j..Translations for variables before and after a transition:\ -syntax +syntax "_before" :: "id \ 'a" ("\_") "_after" :: "id \ 'a" ("\_") - + translations "\x" \ "x \CONST fst" "\x" \ "x \CONST snd" -print_translation {* +print_translation \ let fun quote_tr' f (t :: ts) = Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) @@ -77,6 +77,6 @@ (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})), (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While"}))] end -*} +\ end \ No newline at end of file diff -r e99f706aeab9 -r ad8e0a789af6 src/HOL/Hoare_Parallel/RG_Tran.thy --- a/src/HOL/Hoare_Parallel/RG_Tran.thy Sat Dec 27 19:51:55 2014 +0100 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy Sat Dec 27 20:32:06 2014 +0100 @@ -1,12 +1,12 @@ -section {* Operational Semantics *} +section \Operational Semantics\ theory RG_Tran imports RG_Com begin -subsection {* Semantics of Component Programs *} +subsection \Semantics of Component Programs\ -subsubsection {* Environment transitions *} +subsubsection \Environment transitions\ type_synonym 'a conf = "(('a com) option) \ 'a" @@ -20,7 +20,7 @@ lemma etranE: "c -e\ c' \ (\P s t. c = (P, s) \ c' = (P, t) \ Q) \ Q" by (induct c, induct c', erule etran.cases, blast) -subsubsection {* Component transitions *} +subsubsection \Component transitions\ inductive_set ctran :: "('a conf \ 'a conf) set" @@ -46,7 +46,7 @@ monos "rtrancl_mono" -subsection {* Semantics of Parallel Programs *} +subsection \Semantics of Parallel Programs\ type_synonym 'a par_conf = "('a par_com) \ 'a" @@ -69,9 +69,9 @@ (Ps ! i, s) -c\ (r, t) \ P) \ P" by (induct c, induct c', erule par_ctran.cases, blast) -subsection {* Computations *} +subsection \Computations\ -subsubsection {* Sequential computations *} +subsubsection \Sequential computations\ type_synonym 'a confs = "'a conf list" @@ -84,7 +84,7 @@ definition cp :: "('a com) option \ 'a \ ('a confs) set" where "cp P s \ {l. l!0=(P,s) \ l \ cptn}" -subsubsection {* Parallel computations *} +subsubsection \Parallel computations\ type_synonym 'a par_confs = "'a par_conf list" @@ -97,7 +97,7 @@ definition par_cp :: "'a par_com \ 'a \ ('a par_confs) set" where "par_cp P s \ {l. l!0=(P,s) \ l \ par_cptn}" -subsection{* Modular Definition of Computation *} +subsection\Modular Definition of Computation\ definition lift :: "'a com \ 'a conf \ 'a conf" where "lift Q \ \(P, s). (if P=None then (Some Q,s) else (Some(Seq (the P) Q), s))" @@ -125,7 +125,7 @@ (Some(While b P), snd(last ((Some P, s)#xs)))#ys \ cptn_mod\ \ (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs \ cptn_mod" -subsection {* Equivalence of Both Definitions.*} +subsection \Equivalence of Both Definitions.\ lemma last_length: "((a#xs)!(length xs))=last (a#xs)" by (induct xs) auto @@ -178,20 +178,20 @@ \ (Some a, s) # (Q, t) # xs \ cptn_mod" apply(induct a) apply simp_all ---{* basic *} +--\basic\ apply clarify apply(erule ctran.cases,simp_all) apply(rule CptnModNone,rule Basic,simp) apply clarify apply(erule ctran.cases,simp_all) ---{* Seq1 *} +--\Seq1\ apply(rule_tac xs="[(None,ta)]" in CptnModSeq2) apply(erule CptnModNone) apply(rule CptnModOne) apply simp apply simp apply(simp add:lift_def) ---{* Seq2 *} +--\Seq2\ apply(erule_tac x=sa in allE) apply(erule_tac x="Some P2" in allE) apply(erule allE,erule impE, assumption) @@ -208,12 +208,12 @@ apply (simp add:last_length) apply (simp add:last_length) apply(simp add:lift_def) ---{* Cond *} +--\Cond\ apply clarify apply(erule ctran.cases,simp_all) apply(force elim: CptnModCondT) apply(force elim: CptnModCondF) ---{* While *} +--\While\ apply clarify apply(erule ctran.cases,simp_all) apply(rule CptnModNone,erule WhileF,simp) @@ -223,7 +223,7 @@ apply(force elim:CptnModWhile1) apply clarify apply(force simp add:last_length elim:CptnModWhile2) ---{* await *} +--\await\ apply clarify apply(erule ctran.cases,simp_all) apply(rule CptnModNone,erule Await,simp+) @@ -295,7 +295,7 @@ apply(erule CondT,simp) apply(rule CptnComp) apply(erule CondF,simp) ---{* Seq1 *} +--\Seq1\ apply(erule cptn.cases,simp_all) apply(rule CptnOne) apply clarify @@ -315,7 +315,7 @@ apply(rule Seq2,simp) apply(drule_tac P=P1 in lift_is_cptn) apply(simp add:lift_def) ---{* Seq2 *} +--\Seq2\ apply(rule cptn_append_is_cptn) apply(drule_tac P=P1 in lift_is_cptn) apply(simp add:lift_def) @@ -325,12 +325,12 @@ apply(rule last_fst_esp) apply (simp add:last_length) apply(simp add:Cons_lift lift_def split_def last_conv_nth) ---{* While1 *} +--\While1\ apply(rule CptnComp) apply(rule WhileT,simp) apply(drule_tac P="While b P" in lift_is_cptn) apply(simp add:lift_def) ---{* While2 *} +--\While2\ apply(rule CptnComp) apply(rule WhileT,simp) apply(rule cptn_append_is_cptn) @@ -349,9 +349,9 @@ apply(erule cptn_if_cptn_mod) done -section {* Validity of Correctness Formulas*} +section \Validity of Correctness Formulas\ -subsection {* Validity for Component Programs. *} +subsection \Validity for Component Programs.\ type_synonym 'a rgformula = "'a com \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set" @@ -370,7 +370,7 @@ "\ P sat [pre, rely, guar, post] \ \s. cp (Some P) s \ assum(pre, rely) \ comm(guar, post)" -subsection {* Validity for Parallel Programs. *} +subsection \Validity for Parallel Programs.\ definition All_None :: "(('a com) option) list \ bool" where "All_None xs \ \c\set xs. c=None" @@ -389,9 +389,9 @@ "\ Ps SAT [pre, rely, guar, post] \ \s. par_cp Ps s \ par_assum(pre, rely) \ par_comm(guar, post)" -subsection {* Compositionality of the Semantics *} +subsection \Compositionality of the Semantics\ -subsubsection {* Definition of the conjoin operator *} +subsubsection \Definition of the conjoin operator\ definition same_length :: "'a par_confs \ ('a confs) list \ bool" where "same_length c clist \ (\i ('a confs) list \ bool" ("_ \ _" [65,65] 64) where "c \ clist \ (same_length c clist) \ (same_state c clist) \ (same_program c clist) \ (compat_label c clist)" -subsubsection {* Some previous lemmas *} +subsubsection \Some previous lemmas\ lemma list_eq_if [rule_format]: "\ys. xs=ys \ (length xs = length ys) \ (\i Suc j ys\[] \ P (tl(ys)!j)" by (induct ys) simp_all -subsection {* The Semantics is Compositional *} +subsection \The Semantics is Compositional\ lemma aux_if [rule_format]: "\xs s clist. (length clist = length xs \ (\i cptn) @@ -496,7 +496,7 @@ apply clarify apply(erule_tac x="0" and P="\j. ?H j \ (?P j \ ?Q j)" in all_dupE,simp) apply(erule disjE) ---{* first step is a Component step *} +--\first step is a Component step\ apply clarify apply simp apply(subgoal_tac "a=(xs[i:=(fst(clist!i!0))])") @@ -516,7 +516,7 @@ apply(erule etranE,simp) apply(rule ParCptnComp) apply(erule ParComp,simp) ---{* applying the induction hypothesis *} +--\applying the induction hypothesis\ apply(erule_tac x="xs[i := fst (clist ! i ! 0)]" in allE) apply(erule_tac x="snd (clist ! i ! 0)" in allE) apply(erule mp) @@ -630,7 +630,7 @@ apply(erule_tac x=ia and P="\j. ?H j \ (length (?s j) = ?t)" in allE,force) apply force apply(erule_tac x=ia and P="\j. ?H j \ (length (?s j) = ?t)" in allE,force) ---{* first step is an environmental step *} +--\first step is an environmental step\ apply clarify apply(erule par_etran.cases) apply simp