theory week11A_demo
  imports "~~/src/HOL/Hoare_Parallel/OG_Syntax"
begin

  
text\<open> 
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.
\<close>
  
text\<open> 
We use the parametric parallel composition 

COBEGIN SCHEME [0\<le>i<n] c COEND

corresponding to n programs in parallel,
each running the code c (which can refer to i).
\<close>
  
  
subsubsection \<open>Set Elements of an Array to Zero\<close>
 
  
record Example1 =
  a :: "nat \<Rightarrow> nat"

(* \<acute>a (typed \acute) is syntax for field access in the record  *)

lemma Example1:
 "\<parallel>- \<lbrace>True\<rbrace>
   COBEGIN SCHEME [0\<le>i<n] \<lbrace>True\<rbrace> \<acute>a:=\<acute>a (i:=0) \<lbrace>\<acute>a i=0\<rbrace> COEND
  \<lbrace>\<forall>i < n. \<acute>a i = 0\<rbrace>"
apply oghoare
apply simp_all
  done
    
    
    
    
    
subsubsection \<open>Increment a Variable in Parallel\<close>

text \<open>First some lemmas about summation properties.\<close>
  
text\<open>SKIP THIS --------------------------\<close>

lemma Example2_lemma2_aux: "!!b. j<n \<Longrightarrow>
 (\<Sum>i=0..<n. (b i::nat)) =
 (\<Sum>i=0..<j. b i) + b j + (\<Sum>i=0..<n-(Suc j) . b (Suc j + i))"
apply(induct n)
 apply simp_all
apply(simp add:less_Suc_eq)
 apply(auto)
apply(subgoal_tac "n - j = Suc(n- Suc j)")
  apply simp
apply arith
done

lemma Example2_lemma2_aux2:
  "!!b. j\<le> s \<Longrightarrow> (\<Sum>i::nat=0..<j. (b (s:=t)) i) = (\<Sum>i=0..<j. b i)"
apply(induct j)
 apply simp_all
done

lemma Example2_lemma2:
 "!!b. \<lbrakk>j<n; b j=0\<rbrakk> \<Longrightarrow> Suc (\<Sum>i::nat=0..<n. b i)=(\<Sum>i=0..<n. (b (j := Suc 0)) i)"
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
apply(erule_tac  t="sum (b(j := (Suc 0))) {0..<n}" in ssubst)
apply(frule_tac b=b in Example2_lemma2_aux)
apply(erule_tac  t="sum b {0..<n}" in ssubst)
apply(subgoal_tac "Suc (sum b {0..<j} + b j + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))=(sum b {0..<j} + Suc (b j) + (\<Sum>i=0..<n - Suc j. b (Suc j + i)))")
apply(rotate_tac -1)
apply(erule ssubst)
apply(subgoal_tac "j\<le>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\<open>UNTIL HERE --------------------------\<close>

  
record Example2 =
 c :: "nat \<Rightarrow> nat"
 x :: nat

 (*
lemma Example_2: "0<n \<Longrightarrow>
 \<parallel>- \<lbrace>\<acute>x=0 \<rbrace>
 COBEGIN
   SCHEME [0\<le>i<n]
  \<lbrace>TODO\<rbrace>
   \<acute>x:=\<acute>x+(Suc 0)
  \<lbrace>TODO\<rbrace>
 COEND
 \<lbrace>\<acute>x=n\<rbrace>"
  
  *)
  
  
  
  
  
  
  
text\<open>Need auxilliary variable\<close>
  
  (*
lemma Example_2: "0<n \<Longrightarrow>
 \<parallel>- \<lbrace>\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0\<rbrace>
 COBEGIN
   SCHEME [0\<le>i<n]
  \<lbrace>TODO\<rbrace>
   \<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
  \<lbrace>TODO\<rbrace>
 COEND
 \<lbrace>\<acute>x=n\<rbrace>"
  
  
  *)
    
  
  
  
  
  
  
  
  
  
lemma Example_2: "0<n \<Longrightarrow>
 \<parallel>- \<lbrace>\<acute>x=0 \<and> (\<Sum>i=0..<n. \<acute>c i)=0\<rbrace>
 COBEGIN
   SCHEME [0\<le>i<n]
  \<lbrace>\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=0\<rbrace>
   \<langle> \<acute>x:=\<acute>x+(Suc 0),, \<acute>c:=\<acute>c (i:=(Suc 0)) \<rangle>
  \<lbrace>\<acute>x=(\<Sum>i=0..<n. \<acute>c i) \<and> \<acute>c i=(Suc 0)\<rbrace>
 COEND
 \<lbrace>\<acute>x=n\<rbrace>"
apply oghoare 
apply (simp_all cong del: sum.strong_cong)
apply (tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
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