theory week11A_demo imports "~~/src/HOL/Hoare_Parallel/OG_Syntax" begin text\ We look at 2 examples of Hoare_Parallel/OG_Examples. We don't focus on the proof here (just copied here) but on finding the assertions. \ text\ We use the parametric parallel composition COBEGIN SCHEME [0\i subsubsection \Set Elements of an Array to Zero\ record Example1 = a :: "nat \ nat" (* \a (typed \acute) is syntax for field access in the record *) lemma Example1: "\- \True\ COBEGIN SCHEME [0\iTrue\ \a:=\a (i:=0) \\a i=0\ COEND \\i < n. \a i = 0\" apply oghoare apply simp_all done subsubsection \Increment a Variable in Parallel\ text \First some lemmas about summation properties.\ text\SKIP THIS --------------------------\ 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..i=0..i=0..j") apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2) apply(rotate_tac -1) apply(erule ssubst) apply simp_all done text\UNTIL HERE --------------------------\ record Example2 = c :: "nat \ nat" x :: nat (* lemma Example_2: "0 \- \\x=0 \ COBEGIN SCHEME [0\iTODO\ \x:=\x+(Suc 0) \TODO\ COEND \\x=n\" *) text\Need auxilliary variable\ (* lemma Example_2: "0 \- \\x=0 \ (\i=0..c i)=0\ COBEGIN SCHEME [0\iTODO\ \ \x:=\x+(Suc 0),, \c:=\c (i:=(Suc 0)) \ \TODO\ COEND \\x=n\" *) 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 \\x=n\" apply oghoare apply (simp_all cong del: sum.strong_cong) apply (tactic \ALLGOALS (clarify_tac @{context})\) apply (simp_all cong del: sum.strong_cong) apply(erule (1) Example2_lemma2) apply(erule (1) Example2_lemma2) apply(erule (1) Example2_lemma2) apply(simp) done end