Theory RG_Examples_Reworked

(* Title:      	   Reworked RG Examples
   Author(s):     Robert Colvin, Scott Heiner, Peter Hoefner, Roger Su
   License:       BSD 2-Clause
   Maintainer(s): Roger Su <roger.c.su@proton.me>
                  Peter Hoefner <peter@hoefner-online.de>
*)

section ‹Examples Reworked›

text ‹The examples in the original library~\cite{RGinIsabelle}, 
expressed using our new syntax, and proved using our new tactics.›

theory RG_Examples_Reworked

imports RG_Annotated_Commands

begin
declare [[syntax_ambiguity_warning = false]]
(*============================================================================*)
subsection ‹Setting Elements of an Array to Zero›

record Example1 =
  A :: "nat list"

theorem Example1:
  "global_init: ⦃ n < length ´A ⦄
   global_rely: id(A)
    ∥ i < n @
     { ⦃ i < length ´A ⦄,
       ⦃ length ºA = length ªA ∧ ºA ! i = ªA ! i ⦄ }
   ´A := ´A[i := 0]
     { ⦃ length ºA = length ªA ∧ (∀j < n. i ≠ j ⟶ ºA ! j = ªA ! j) ⦄,
       ⦃ ´A ! i = 0 ⦄ }
   global_guar: ⦃ True ⦄
   global_post: ⦃ ∀i < n. ´A ! i = 0 ⦄"
  by method_rg_try_each

theorem Example1'':
  "annotated global_init: ⦃ length ´A = N ⦄ global_rely: ⦃ ªA = ºA ⦄
   ∥ i < N @
   { ⦃ True ⦄,
     ⦃  length ªA = length ºA ∧ ªA ! i = ºA ! i⦄ }
     (´A := ´A [i := f i])- ⫽ ⦃length ´A = N ⦄
   { ⦃ length ªA = length ºA ∧ (∀j. i ≠ j ⟶   ªA ! j = ºA ! j ) ⦄,
     ⦃ ´A ! i = f i ⦄ }
   global_guar: ⦃ length ªA = length ºA⦄
   global_post: ⦃ take N ´A = map f [0 ..< N] ⦄"
  apply rg_proof_expand
  by (fastforce split: if_splits simp: map_upt_eqI)

(*============================================================================*)
subsection ‹Incrementing a Variable in Parallel›

text ‹Two Components›

record Example2 =
  x   :: nat (* shared var *)
  c_0 :: nat (* aux var of Thread 0 *)
  c_1 :: nat (* aux var of Thread 1 *)

lemma ex2_leftside:  
  "{ ⦃ ´c_0 = 0 ⦄, id(c_0) }
     Basic ((´x ← ´x + 1) ∘> (´c_0 ← 1))
   ⫽ ⦃ ´x = ´c_0 + ´c_1 ⦄
   { id(c_1), ⦃ ´c_0 = 1 ⦄}"
  by method_rg_try_each

lemma ex2_rightside:  
  "{ ⦃ ´c_1 = 0 ⦄, id(c_1) }
     Basic ((´x ← ´x + 1) ∘> (´c_1 ← 1))
   ⫽ ⦃ ´x = ´c_0 + ´c_1 ⦄
   { id(c_0), ⦃ ´c_1 = 1 ⦄}"
  by method_rg_try_each

theorem Example2b:
  "{ ⦃ ´c_0 = 0 ∧ ´c_1 = 0 ⦄, ids({c_0, c_1}) }
   (Basic ((´x ← ´x + 1) ∘> (´c_0 ← 1))) ∥ (Basic ((´x ← ´x + 1) ∘> (´c_1 ← 1)))
   ⫽ ⦃ ´x = ´c_0 + ´c_1 ⦄
   { UNIV, ⦃ True ⦄ }"
  using ex2_leftside ex2_rightside (* needs to instantiate *)
  by (rule rg_binary_parallel_invar_conseq; blast)

text ‹Parameterised›

lemma sum_split:
  "(j::nat) < (n::nat)
  ⟹ sum a {0..<n} = sum a {0..<j} + a j + sum a {j+1..<n}"
  by (metis Suc_eq_plus1 bot_nat_0.extremum group_cancel.add1 le_eq_less_or_eq sum.atLeastLessThan_concat sum.atLeast_Suc_lessThan)

text ‹Intuition of the lemma above:
Consider the sum of a function @{term ‹b k›} with @{term k} ranging 
from 0 to @{term ‹n - 1›}.
Let @{term j} be an index in this range, and assume @{term ‹b j = 0›}.
Then, replacing @{term ‹b j›} with 1 in the sum, the result is the
same as adding 1 to the original sum.›

lemma Example2_lemma2_replace:
  assumes "(j::nat) < n"
      and "b' = b(j:=xx::nat)"
    shows "(∑ i = 0 ..< n. b' i) = (∑ i = 0 ..< n. b i) - b j + xx"
  apply (subst sum_split, rule assms(1))
  apply (subst sum_split, rule assms(1))
  using assms(2) by clarsimp

lemma Example2_lemma2_Suc0[simp]:
  assumes "(j::nat) < n"
      and "b j = 0"
      and "b' = b(j:=1)"
    shows "Suc (∑ i::nat = 0 ..< n. b i) = (∑ i = 0 ..< n. b' i)"
  using assms  Example2_lemma2_replace 
  by fastforce

record Example2_param =
  y ::  nat         (* shared var *)
  C :: "nat ⇒ nat" (* aux var for each thread *)

lemma Example2_local:
  "i < n ⟹
  { ⦃ ´C i = 0 ⦄,
     id(C @ i) }

    Basic ((´y ← ´y + 1) ∘> (´C ← ´C(i:=1)))
    ⫽ ⦃ ´y = (∑ k::nat = 0 ..< n. ´C k) ⦄

   { ⦃ ∀ j < n. i ≠ j ⟶ ºC j = ªC j ⦄,
     ⦃ ´C i = 1 ⦄ }"
  by method_rg_try_each

theorem Example2_param:
  assumes "0 < n" shows
  "global_init: ⦃ ´y = 0 ∧ sum ´C {0 ..< n} = 0 ⦄
   global_rely: id(C) ∩ id(y)
    ∥ i < n @
   { ⦃ ´C i = 0 ⦄,
     id(C @ i) }
     Basic ((´y ← ´y + 1) ∘> (´C ← ´C(i:=1)))
     ⫽ ⦃ ´y = sum ´C {0 ..< n} ⦄
   { ⦃ ∀ j < n. i ≠ j ⟶ ºC j = ªC j ⦄,
     ⦃ ´C i = 1 ⦄ }
   global_guar: ⦃ True ⦄
   global_post: ⦃ ´y = n ⦄"
proof method_multi_parallel
  case post
  then show ?case
    using assms by (clarsimp, fastforce)
next
  case body
  then show ?case
    by method_rg_try_each
qed (fastforce+)

text ‹As above, but using an explicit annotation and a different method.›

theorem Example2_param_with_expansion:
  assumes "0 < n" shows "annotated
  global_init: ⦃ ´y = 0 ∧ sum ´C {0 ..< n} = 0 ⦄
  global_rely: id(C) ∩ id(y)
    ∥ i < n @
  { ⦃ ´C i = 0 ⦄,
    id(C @ i) }
    (Basic ((´y ← ´y + 1) ∘> (´C ← ´C(i:=1))))-
    ⫽ ⦃ ´y = sum ´C {0 ..< n} ⦄
  { ⦃ ∀ j < n. i ≠ j ⟶ ºC j = ªC j ⦄,
    ⦃ ´C i = 1 ⦄ }
  global_guar: ⦃ True ⦄
  global_post: ⦃ ´y = n ⦄"
  apply rg_proof_expand
  using assms by (fastforce split: if_splits)

(*============================================================================*)
subsection ‹FindP›

text ‹Titled ``Find Least Element'' in the original~\cite{RGinIsabelle},
the "findP" problem assumes that @{text n} divides @{text m},
and runs @{text n} threads in parallel 
to search through a length-@{text m} array @{text B} 
for an element that satisfies a predicate @{text P}. 
The indices of the array @{text B} are partitioned 
into the congruence-classes modulo @{text n},
where Thread @{text i} searches through the indices
that are congruent to @{text i} mod @{text n}.

In the program, @{term ‹X i›} is the next index to be checked by 
Thread @{text i}. Meanwhile, @{term ‹Y i›} is either
the out-of-bound default @{term ‹m + i›} if Thread @{text i} has not 
found a @{text P}-element,
or the index of the first @{text P}-element found by Thread @{text i}.›

text ‹The first helper lemma: an equivalent version of @{text mod_aux}
found in the original.›

lemma mod_aux :
  "a mod (n::nat) = i ⟹  a < j ∧ j < a + n ⟹ j mod n ≠ i"
  using mod_eq_dvd_iff_nat nat_dvd_not_less by force

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

lemma Example3:
  assumes "m mod n=0" shows "annotated
  global_init: ⦃∀i < n. ´X i = i ∧ ´Y i = m + i ⦄
  global_rely: ⦃ ºX = ªX ∧ ºY = ªY⦄
    ∥ 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. i≠j ⟶ ªY j ≤ ºY j) ∧ ºX i = ªX i ∧ ºY i = ªY i⦄ } 

    WHILEa (∀ j < n. ´X i < ´Y j) DO
      {stable_guard: ⦃´X i < ´Y i⦄} 
      IFa P(B!(´X i)) THEN 
        (´Y[i] := ´X i)- 
      ELSE 
        (´X[i] := ´X i + n)-
      FI 
    OD

  { ⦃(∀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) ⦄ }

  global_guar: ⦃True⦄
  global_post: ⦃ ∀ 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 rg_proof_expand (* takes a bit long *)
           apply fastforce+
    apply (metis linorder_neqE_nat mod_aux)
   apply (metis antisym_conv3 mod_aux)
  by (metis leD mod_less_eq_dividend)

text ‹Below is the original version of the theorem, and is immediately
derivable from the above. We include some formatting changes (such as
line breaks) for better readability.›

lemma Example3_original: "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)⦄]"
  by (rule valid_multipar_with_internal_rg[OF Example3]; simp)

end