# Theory RG_Examples

theory RG_Examples
imports RG_Syntax
```section ‹Examples›

theory RG_Examples
imports RG_Syntax
begin

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

subsection ‹Set Elements of an Array to Zero›

lemma le_less_trans2: "⟦(j::nat)<k; i≤ j⟧ ⟹ i<k"
by simp

lemma add_le_less_mono: "⟦ (a::nat) < c; b≤d ⟧ ⟹ a + b < c + d"
by simp

record Example1 =
A :: "nat list"

lemma Example1:
"⊢ 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<n. i ≠ 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)
done

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 ∧ (∀j<length ºA . i≠j ⟶ ºA!j = ªA!j)⦄,
⦃´A!i=0⦄)
COEND
SAT [⦃t*n < length ´A⦄,
⦃t*n < length ºA ∧ length ºA=length ªA ∧ (∀i<n. ºA!(k*n+i)=ªA!(k*n+i))⦄,
⦃t*n < length ºA ∧ length ºA=length ªA ∧
(∀i<length ºA . (i<k*n ⟶ ºA!i = ªA!i) ∧ ((Suc k)*n ≤ i⟶ ºA!i = ªA!i))⦄,
⦃∀i<n. ´A!(k*n+i) = 0⦄]"
apply(rule Parallel)
apply auto
apply(erule_tac x="k*n +i" in allE)
apply(subgoal_tac "k*n+i <length (A b)")
apply force
apply(erule le_less_trans2)
apply(case_tac t,simp+)
apply(rule Basic)
apply simp
apply clarify
apply (subgoal_tac "k*n+i< length (A x)")
apply simp
apply(erule le_less_trans2)
apply(case_tac t,simp+)
done

subsection ‹Increment a Variable in Parallel›

subsubsection ‹Two components›

record Example2 =
x  :: nat
c_0 :: nat
c_1 :: nat

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 =ª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 =ªc_0 + ªc_1)⦄,
⦃´x=´c_0 + ´c_1 ∧ ´c_1=1⦄)
COEND
SAT [⦃´x=0 ∧ ´c_0=0 ∧ ´c_1=0⦄,
⦃ºx=ªx ∧  ºc_0= ªc_0 ∧ ºc_1=ªc_1⦄,
⦃True⦄,
⦃´x=2⦄]"
apply(rule Parallel)
apply simp_all
apply clarify
apply(case_tac i)
apply simp
apply(rule conjI)
apply clarify
apply simp
apply clarify
apply simp
apply simp
apply(rule conjI)
apply clarify
apply simp
apply clarify
apply simp
apply(subgoal_tac "xa=0")
apply simp
apply arith
apply clarify
apply(case_tac xaa, simp, simp)
apply clarify
apply simp
apply(erule_tac x=0 in all_dupE)
apply(erule_tac x=1 in allE,simp)
apply clarify
apply(case_tac i,simp)
apply(rule Await)
apply simp_all
apply(clarify)
apply(rule Seq)
prefer 2
apply(rule Basic)
apply simp_all
apply(rule subset_refl)
apply(rule Basic)
apply simp_all
apply clarify
apply simp
apply(rule Await)
apply simp_all
apply(clarify)
apply(rule Seq)
prefer 2
apply(rule Basic)
apply simp_all
apply(rule subset_refl)
apply(auto intro!: Basic)
done

subsubsection ‹Parameterized›

lemma Example2_lemma2_aux: "j<n ⟹
(∑i=0..<n. (b i::nat)) =
(∑i=0..<j. b i) + b j + (∑i=0..<n-(Suc j) . b (Suc j + i))"
apply(induct n)
apply simp_all
apply(auto)
apply(subgoal_tac "n - j = Suc(n- Suc j)")
apply simp
apply arith
done

lemma Example2_lemma2_aux2:
"j≤ s ⟹ (∑i::nat=0..<j. (b (s:=t)) i) = (∑i=0..<j. b i)"
by (induct j) simp_all

lemma Example2_lemma2:
"⟦j<n; b j=0⟧ ⟹ Suc (∑i::nat=0..<n. b i)=(∑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 + (∑i=0..<n - Suc j. b (Suc j + i)))=(sum b {0..<j} + Suc (b j) + (∑i=0..<n - Suc j. b (Suc j + i)))")
apply(rotate_tac -1)
apply(erule ssubst)
apply(subgoal_tac "j≤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

lemma Example2_lemma2_Suc0: "⟦j<n; b j=0⟧ ⟹
Suc (∑i::nat=0..< n. b i)=(∑i=0..< n. (b (j:=Suc 0)) i)"

record Example2_parameterized =
C :: "nat ⇒ nat"
y  :: nat

lemma Example2_parameterized: "0<n ⟹
⊢ COBEGIN SCHEME  [0≤i<n]
(⟨ ´y:=´y+1;; ´C:=´C (i:=1) ⟩,
⦃´y=(∑i=0..<n. ´C i) ∧ ´C i=0⦄,
⦃ºC i = ªC i ∧
(ºy=(∑i=0..<n. ºC i) ⟶ ªy =(∑i=0..<n. ªC i))⦄,
⦃(∀j<n. i≠j ⟶ ºC j = ªC j) ∧
(ºy=(∑i=0..<n. ºC i) ⟶ ªy =(∑i=0..<n. ªC i))⦄,
⦃´y=(∑i=0..<n. ´C i) ∧ ´C i=1⦄)
COEND
SAT [⦃´y=0 ∧ (∑i=0..<n. ´C i)=0 ⦄, ⦃ºC=ªC ∧ ºy=ªy⦄, ⦃True⦄, ⦃´y=n⦄]"
apply(rule Parallel)
apply force
apply force
apply(force)
apply clarify
apply simp
apply simp
apply clarify
apply simp
apply(rule Await)
apply simp_all
apply clarify
apply(rule Seq)
prefer 2
apply(rule Basic)
apply(rule subset_refl)
apply simp+
apply(rule Basic)
apply simp
apply clarify
apply simp
apply simp_all
done

subsection ‹Find Least Element›

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" )
prefer 2 apply (simp (no_asm_use))
apply(subgoal_tac "j=j div n*n + j mod n")
prefer 2 apply (simp (no_asm_use))
apply simp
apply(subgoal_tac "a div n*n < j div n*n")
prefer 2 apply arith
apply(subgoal_tac "j div n*n < (a div n + 1)*n")
prefer 2 apply simp
apply (simp only:mult_less_cancel2)
apply arith
done

record Example3 =
X :: "nat ⇒ nat"
Y :: "nat ⇒ nat"

lemma Example3: "m mod n=0 ⟹
⊢ COBEGIN
SCHEME [0≤i<n]
(WHILE (∀j<n. ´X 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<m ⟶ P(B!(´Y i)) ∧ ´Y i≤ m+i)⦄,
⦃(∀j<n. i≠j ⟶ ªY j ≤ ºY j) ∧ ºX i = ªX i ∧
ºY i = ªY i⦄,
⦃(∀j<n. i≠j ⟶ º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<m ⟶ P(B!(´Y i)) ∧ ´Y i≤ m+i) ∧ (∃j<n. ´Y j ≤ ´X i) ⦄)
COEND
SAT [⦃ ∀i<n. ´X i=i ∧ ´Y i=m+i ⦄,⦃ºX=ªX ∧ ºY=ªY⦄,⦃True⦄,
⦃∀i<n. (´X i) mod n=i ∧ (∀j<´X i. j mod n=i ⟶ ¬P(B!j)) ∧
(´Y i<m ⟶ P(B!(´Y i)) ∧ ´Y i≤ m+i) ∧ (∃j<n. ´Y j ≤ ´X i)⦄]"
apply(rule Parallel)
― ‹5 subgoals left›
apply force+
apply clarify
apply simp
apply(rule While)
apply force
apply force
apply force
apply (erule dvdE)
apply(rule_tac pre'="⦃ ´X i mod n = i ∧ (∀j. j<´X i ⟶ j mod n = i ⟶ ¬P(B!j)) ∧ (´Y i < n * k ⟶ P (B!(´Y i))) ∧ ´X i<´Y i⦄" in Conseq)
apply force
apply(rule subset_refl)+
apply(rule Cond)
apply force
apply(rule Basic)
apply force
apply fastforce
apply force
apply force
apply(rule Basic)
apply simp
apply clarify
apply simp
apply (case_tac "X x (j mod n) ≤ j")
apply (drule le_imp_less_or_eq)
apply (erule disjE)
apply (drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
apply auto
done

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≤i<n]
(WHILE (∀j<n. ´X!i < ´Y!j)  DO
IF P(B!(´X!i)) THEN ´Y:=´Y[i:=´X!i] ELSE ´X:= ´X[i:=(´X!i)+ n] FI
OD,
⦃n<length ´X ∧ n<length ´Y ∧ (´X!i) mod n=i ∧ (∀j<´X!i. j mod n=i ⟶ ¬P(B!j)) ∧ (´Y!i<m ⟶ P(B!(´Y!i)) ∧ ´Y!i≤ m+i)⦄,
⦃(∀j<n. i≠j ⟶ ªY!j ≤ ºY!j) ∧ ºX!i = ªX!i ∧
ºY!i = ªY!i ∧ length ºX = length ªX ∧ length ºY = length ªY⦄,
⦃(∀j<n. i≠j ⟶ º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<m ⟶ P(B!(´Y!i)) ∧ ´Y!i≤ m+i) ∧ (∃j<n. ´Y!j ≤ ´X!i) ⦄) COEND)
SAT [⦃n<length ´X ∧ n<length ´Y ∧ (∀i<n. ´X!i=i ∧ ´Y!i=m+i) ⦄,
⦃ºX=ªX ∧ ºY=ªY⦄,
⦃True⦄,
⦃∀i<n. (´X!i) mod n=i ∧ (∀j<´X!i. j mod n=i ⟶ ¬P(B!j)) ∧
(´Y!i<m ⟶ P(B!(´Y!i)) ∧ ´Y!i≤ m+i) ∧ (∃j<n. ´Y!j ≤ ´X!i)⦄]"
apply (rule Parallel)
apply (auto cong del: strong_INF_cong strong_SUP_cong)
apply force
apply (rule While)
apply force
apply force
apply force
apply (erule dvdE)
apply(rule_tac pre'="⦃n<length ´X ∧ n<length ´Y ∧ ´X ! i mod n = i ∧ (∀j. j < ´X ! i ⟶ j mod n = i ⟶ ¬ P (B ! j)) ∧ (´Y ! i < n * k ⟶ P (B ! (´Y ! i))) ∧ ´X!i<´Y!i⦄" in Conseq)
apply force
apply(rule subset_refl)+
apply(rule Cond)
apply force
apply(rule Basic)
apply force
apply force
apply force
apply force
apply(rule Basic)
apply simp
apply clarify
apply simp
apply(rule allI)
apply(rule impI)+
apply(case_tac "X x ! i≤ j")
apply(drule le_imp_less_or_eq)
apply(erule disjE)
apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
apply auto
done

end
```