Theory RG_Examples_Reworked

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

section ‹Examples Reworked›

text ‹Reworking of the examples in the original library, using our new
framework's syntax and tactics.›

theory RG_Examples_Reworked
  imports RG_Annotated_Methods
begin

(*============================================================================*)
subsection ‹Set 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':
  "global_init: ⦃ N = length ´A ⦄
   global_rely: ⦃ ºA = ªA ⦄
   ∥ i < N @
   { ⦃ True ⦄,
     ⦃ length ºA = length ªA ∧ ºA ! i = ªA ! i ⦄ }
     ´A := ´A [i := f i] ⫽ ⦃ i < N ∧ N = length ´A ⦄
   { ⦃ 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] ⦄"
proof method_multi_parallel
  case post
  then show ?case
    apply clarsimp
    apply standard
     apply standard
     apply force
    by (clarsimp simp add: map_upt_eqI)
qed (fastforce+)

theorem Example1'':
  "valid_multipar: annotated 
  global_init: ⦃ length ´A = Nz ⦄ 
  global_rely: ⦃ ªA = ºA ⦄
   ∥ i < Nz @
   { ⦃ True ⦄,
     ⦃  length ªA = length ºA ∧ ªA ! i = ºA ! i⦄ }
     (´A := ´A [i := f i])- ⫽ ⦃ length ´A = Nz ⦄
   { ⦃ length ªA = length ºA ∧ (∀j. i ≠ j ⟶   ªA ! j = ºA ! j ) ⦄,
     ⦃ ´A ! i = f i ⦄ }
   global_guar: ⦃ length ºA = Nz ⟶ length ªA = length ºA⦄
   global_post: ⦃ take Nz ´A = map f [0 ..< Nz] ⦄"
  apply (decompose_and_discharge simps: atLeast_upt; simp_divide_blast)
  by (simp add: map_upt_eqI)

text ‹These examples demonstrate the syntax for using a range for process ids starting somewhere other than 0›
lemma Example1_parameterized:
  assumes "k < t"
  shows "valid_multipar: annotated
    global_init: ⦃t*n < length ´A⦄
    global_rely: ⦃t*n < length ºA ∧ length ºA=length ªA ∧ (∀i<n. ºA!(k*n+i)=ªA!(k*n+i))⦄
    ∥ k*n ≤ i < (Suc k) *n @
      {⦃t*n < length ´A⦄,
       ⦃t*n < length ºA ∧ length ºA=length ªA ∧ ºA!i = ªA!i⦄}
        (´A:=´A[i:=0])-
      {⦃t*n < length ºA ∧ length ºA=length ªA ∧ (∀j<length ºA . i≠j ⟶ ºA!j = ªA!j)⦄,
      ⦃´A!i=0⦄}   
    global_guar: ⦃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))⦄
    global_post: ⦃∀i<n. ´A!(k*n+i) = 0⦄"
  apply (decompose_and_discharge ; simp_divide_blast)
    apply (metis Groups.mult_ac(2) Suc_leI assms less_add_same_cancel1 less_le_not_le linear nat_0_less_mult_iff nat_mult_less_cancel1 nth_list_update_eq order_le_less_trans times_nat.simps(2) trans_less_add2)
   apply (metis add.commute add_less_imp_less_left le_iff_add)
  by (smt  Suc_leI assms dual_order.strict_trans1 less_or_eq_imp_le mult_Suc mult_le_mono1)

lemma Example1_parameterized_with_invariant:
  assumes "k < t"
  shows "valid_multipar: annotated
  global_init: ⦃t*n < length ´A⦄
  global_rely: ⦃length ºA=length ªA ∧ (∀i<n. ºA!(k*n+i)=ªA!(k*n+i))⦄
  ∥ k*n ≤ i < (Suc k) *n @
    {UNIV,
    ⦃length ºA=length ªA ∧ ºA!i = ªA!i⦄}
      (´A:=´A[i:=0])- ⫽ ⦃t*n < length ´A⦄
    {⦃length ºA=length ªA ∧ (∀j<length ºA . i≠j ⟶ ºA!j = ªA!j)⦄,
    ⦃´A!i=0⦄}
   
  global_guar: ⦃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))⦄
  global_post: ⦃∀i<n. ´A!(k*n+i) = 0⦄"
  apply (decompose_and_discharge ; simp_divide_blast)
    apply (metis Groups.mult_ac(2) Suc_leI assms less_add_same_cancel1 less_le_not_le linear nat_0_less_mult_iff nat_mult_less_cancel1 nth_list_update_eq order_le_less_trans times_nat.simps(2) trans_less_add2)
   apply (metis add.commute add_less_imp_less_left le_iff_add)
  by (smt (verit) Suc_leI assms less_or_eq_imp_le mult.commute mult_Suc_right nat_mult_le_cancel_disj order_le_less_trans) 

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

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

theorem Example2b:
  "validpar: 
  {⦃ ´c_0 = 0 ∧ ´c_1 = 0 ∧ ´x = 0⦄, ids({c_0, c_1, x})}
    {⦃ ´c_0 = 0 ⦄, id(c_0)  }
      ⟨´x := ´x + 1 ;; ´c_0 := 1⟩a ⫽ ⦃ ´x = ´c_0 + ´c_1 ⦄
   { id(c_1), ⦃ ´c_0 = 1 ⦄} 
  ∥a
    {⦃ ´c_1 = 0 ⦄, id(c_1)}
      ⟨´x := ´x + 1 ;; ´c_1 := 1⟩a ⫽ ⦃ ´x = ´c_0 + ´c_1 ⦄
   { id(c_0), ⦃ ´c_1 = 1 ⦄}
  { UNIV, ⦃ ´x = 2 ⦄ }"
  by (decompose_and_discharge intros: valid_binary_par; simp_divide_blast)

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

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)

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"
  using assms sum_split[of j n b] sum_split[of j n b'] by auto

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)"
  by (metis assms Example2_lemma2_replace Suc_eq_plus1 diff_zero)

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 show ?case using assms by auto
qed (fastforce+)

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

theorem Example2_param_with_expansion:
  assumes "0 < n" shows "valid_multipar: annotated
  global_init: ⦃ ´y = 0 ∧ sum ´C {0 ..< n} = 0 ⦄
  global_rely: id(C) ∩ id(y)
    ∥ i < n @
  { ⦃ ´C i = 0 ⦄, id(C @ i) }
    ⟨´y := ´y + 1 ;; ´C[i] := 1⟩a ⫽ ⦃ ´y = sum ´C {0 ..< n} ⦄
  { ⦃ ∀ j < n. i ≠ j ⟶ ºC j = ªC j ⦄, ⦃ ´C i = 1 ⦄ }
  global_guar: UNIV
  global_post: ⦃ ´y = n ⦄"
  by (decompose_and_discharge ; simp_divide_blast useful: assms)

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

text ‹Titled "Find Least Element" in the original.›

text "This helper lemma is 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

text ‹This is the "findP" problem. Assuming that n divides m,
we divide the search for a P-element, by partitioning the indices into the
congruence classes modulo n, and letting Thread i search through the indices
that are "i mod n". 

m: the size of the array (arraySize)
n: the number of threads (numThreads)

P: the predicate
B: the array

X: "X i" is the next index to be checked by Thread i
Y: "Y i" is either
   the out-of-bound default "m + i" if Thread i hasn't found a P-element,
   or the index of the first P-element found by Thread i.

Assume: n divides m.
›

record Example3 = (* see above for comments *)
  X :: "nat ⇒ nat"
  Y :: "nat ⇒ nat"

lemma Example3:
  (* assumes "m mod n=0" *) (* Assumption not needed *)
  shows "valid_multipar: 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⦄} 
      IF. 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 (decompose_and_discharge )
      apply (metis order_trans)
    using linorder_not_le apply blast
   apply (metis linorder_neqE_nat mod_aux)
  by force


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