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 (simp add:add.commute)
  apply(simp add: add_le_mono)
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+)
   apply (simp add:add.commute)
   apply(rule add_le_mono, auto)
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 "x=0")
    apply simp
   apply arith
  apply clarify
  apply(case_tac xa, 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(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:
  "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)"
by(simp add:Example2_lemma2)

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 add:Example2_lemma2_Suc0 cong:if_cong)
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: image_cong_simp)
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