theory week11A_demo2
  imports "~~/src/HOL/Hoare_Parallel/RG_Syntax"
begin

text\<open> 
We look at an example of Hoare_Parallel/RG_Examples.
We don't focus on the proof but on finding the assertions.
\<close>

lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def

subsection \<open>Set Elements of an Array to Zero\<close>

record Example1 =
  A :: "nat list"

(* Try to find 
*)

lemma Example1:
 "\<turnstile> COBEGIN
      SCHEME [0 \<le> i < n]
     (\<acute>A := \<acute>A [i := 0],
     \<lbrace> TODOPrecond \<rbrace>,
     \<lbrace> TODORely \<rbrace>,
     \<lbrace> TODOGuarantee \<rbrace>,
     \<lbrace> TODOPostcond \<rbrace>)
    COEND
 SAT [\<lbrace> n < length \<acute>A \<rbrace>, \<lbrace> \<ordmasculine>A = \<ordfeminine>A \<rbrace>, \<lbrace> True \<rbrace>, \<lbrace> \<forall>i < n. \<acute>A ! i = 0 \<rbrace>]"
  apply(rule Parallel)
  apply (auto intro!: Basic)
  oops





lemma Example1:
 "\<turnstile> COBEGIN
      SCHEME [0 \<le> i < n]
     (\<acute>A := \<acute>A [i := 0],
     \<lbrace> n < length \<acute>A \<rbrace>,
     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> \<ordmasculine>A ! i = \<ordfeminine>A ! i \<rbrace>,
     \<lbrace> length \<ordmasculine>A = length \<ordfeminine>A \<and> (\<forall>j<n. i \<noteq> j \<longrightarrow> \<ordmasculine>A ! j = \<ordfeminine>A ! j) \<rbrace>,
     \<lbrace> \<acute>A ! i = 0 \<rbrace>)
    COEND
 SAT [\<lbrace> n < length \<acute>A \<rbrace>, \<lbrace> \<ordmasculine>A = \<ordfeminine>A \<rbrace>, \<lbrace> True \<rbrace>, \<lbrace> \<forall>i < n. \<acute>A ! i = 0 \<rbrace>]"
apply(rule Parallel)
apply (auto intro!: Basic)
done

    
end