Theory RG_Syntax_Extensions

(* Title:       	 Syntax Extension for Rely-Guarantee
   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 ‹Rely-Guarantee (RG) Syntax Extensions›

text ‹The core extensions to the built-in RG library:
improved syntax of RG sentences in the quintuple- and 
keyword-styles, with data-invariants.

Also: subgoal-generating methods for RG inference-rules that work
with the structured proof-language, Isar.›

theory RG_Syntax_Extensions

imports
  "HOL-Hoare_Parallel.RG_Syntax"
  "HOL-Eisbach.Eisbach"

begin

text ‹We begin with some basic notions that are used later on.›

text ‹Notation for forward function-composition:
defined in the built-in @{text ‹Fun.thy›} but disabled at the 
end of that theory.
%
This operator is useful for modelling atomic primitives such as Swap
and Fetch-And-Increment, and also useful when coupling concrete- and
auxiliary-variable instructions.›

notation fcomp (infixl "∘>" 60)

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

text ‹In applications, guarantee-relations often stipulates that Thread
@{text i} should ``preserve the rely-relations of all other threads''.
This pattern is supported by the following higher-order function, where 
@{text j} ranges through all the threads that are not @{text i}.›

abbreviation for_others :: "('index ⇒ 'state rel) ⇒ 'index ⇒ 'state rel" where
  "for_others R i ≡ ⋂ j ∈ -{i}. R j"

text ‹Relies and guarantees often state that certain variables remain 
unchanged. We support this pattern with the following syntactic sugars.›

abbreviation record_id :: "('record ⇒ 'field) ⇒ 'record rel"
  ("id'(_')" [75] 74) where
  "id(c) ≡ ⦃ ªc = ºc ⦄"

abbreviation record_ids :: "('record ⇒ 'field) set ⇒ 'record rel"
  ("ids'(_')" [75] 74) where
  "ids(cs) ≡ ⋂ c ∈ cs. id(c)"

abbreviation record_id_indexed ::
  "('record ⇒ 'index ⇒ 'field) ⇒ 'index ⇒ 'record rel"
  ("id'( _ @ _ ')") where
  "id(c @ self) ≡ ⦃ ºc self = ªc self ⦄"

abbreviation record_ids_indexed ::
  "('record ⇒ 'index ⇒ 'field) set ⇒ 'index ⇒ 'record rel"
  ("ids'( _ @ _ ')") where
  "ids(cs @ self) ≡ ⋂ c ∈ cs. id(c @ self)"

text ‹The following simple method performs an optional simplification-step, 
and then tries to apply one of the RG rules, before attempting to discharge 
each subgoal using @{text force}.
%
This method works well on simple RG sentences.›

method method_rg_try_each = 
  (clarsimp | simp)?,
  ( rule Basic | rule Seq | rule Cond | rule While 
  | rule Await | rule Conseq | rule Parallel);
   force+

(* The "clarsimp" was added due to "Example2_param",
   where one of the cases could not be handled by "simp". *)

(*============================================================================*)
subsection ‹Lifting of Invariants›

text ‹There are different ways to combine the invariant with the rely
or guarantee, as long as the invariant is preserved.
%
Here, a rely- or guarantee-relation @{term R} is combined with the 
invariant @{term I} into @{term ‹{(s,s'). (s ∈ I ⟶ s' ∈ I) ∧ R}›}.›

definition pred_to_rel :: "'a set ⇒ 'a rel" where
  "pred_to_rel P ≡ {(s,s') . s ∈ P ⟶ s' ∈ P}"

definition invar_and_guar :: "'a set ⇒ 'a rel ⇒ 'a rel" where
  "invar_and_guar I G ≡ G ∩ pred_to_rel I" 

lemmas simp_defs [simp] = pred_to_rel_def invar_and_guar_def

(*============================================================================*)
subsection ‹RG Sentences›

text ‹The quintuple-style of RG sentences.›
abbreviation rg_quint ::
  "'a set ⇒ 'a rel ⇒ 'a com ⇒ 'a rel ⇒ 'a set ⇒ bool"
  ("{_,_} _ {_,_}") where
  "{P, R} C {G, Q} ≡ ⊢ C sat [P, R, G, Q]"

text ‹Quintuples with invariants.›

abbreviation rg_quint_invar :: 
  "'a set ⇒ 'a rel ⇒ 'a com ⇒ 'a set ⇒ 'a rel ⇒ 'a set ⇒ bool" 
  ("{_,_} _ ⫽ _ {_,_}") where
  "{P, R} C ⫽ I {G, Q} ≡ ⊢ C sat [
    P ∩ I, 
    R ∩ pred_to_rel I, 
    invar_and_guar I G, 
    Q ∩ I]"

text ‹The keyword-style of RG sentences.›

abbreviation rg_keyword ::
  "'a rel ⇒ 'a rel ⇒ 'a set ⇒ 'a com ⇒ 'a set ⇒ bool"
  ("rely:_ guar:_ code: {_} _ {_}") where
  "rg_keyword R G P C Q ≡ ⊢ C sat [P, R, G, Q]"

text ‹Keyword-style RG sentences with invariants.›

abbreviation rg_keyword_invar ::
  "'a rel ⇒ 'a rel ⇒ 'a set ⇒ 'a set ⇒ 'a com ⇒ 'a set ⇒ bool"
  ("rely:_ guar:_ inv:_ code: {_} _ {_}") where
  "rg_keyword_invar R G I P C Q ≡ ⊢ C sat [
    P ∩ I, 
    R ∩ pred_to_rel I, 
    invar_and_guar I G, 
    Q ∩ I]"

(*============================================================================*)
subsection ‹RG Subgoal-Generating Methods›

text ‹As in Floyd-Hoare logic, in RG we can strengthen (make smaller) the 
precondition and weaken (make larger) the postcondition without affecting the
validity of an RG sentence.›

theorem strengthen_pre:
  assumes "P' ⊆ P"
      and "⊢ c sat [P,  R, G, Q]"
    shows "⊢ c sat [P', R, G, Q]"
  using assms Conseq by blast

theorem weaken_post:
  assumes "Q ⊆ Q'"
      and "⊢ c sat [P, R, G, Q ]"
    shows "⊢ c sat [P, R, G, Q']"
  using assms Conseq by blast

text ‹We then develop subgoal-generating methods for various instruction 
types and patterns, to be used in conjunction with the Isar proof-language.›

(*----------------------------------------------------------------------------*)
subsubsection ‹Basic›

text ‹A @{text Basic} instruction wraps a state-transformation function.›

theorem rg_basic_named[intro]:
  assumes "stable P R"
      and "stable Q R"
      and "∀s. s ∈ P ⟶ (s, s) ∈ G"
      and "∀s. s ∈ P ⟶ (s, f s) ∈ G"
      and "P ⊆ ⦃ ´f ∈ Q ⦄" 
    shows "{P, R} Basic f {G, Q}"
  using assms apply -
  by (rule Basic; fastforce)

method method_basic =
  rule rg_basic_named,
  goal_cases stable_pre stable_post guar_id establish_guar establish_post

text ‹The \emph{skip} command is a @{text Basic} instruction whose function is
the identity.›

theorem rg_skip_named: 
  assumes "stable P R"
      and "stable Q R"
      and "Id ⊆ G"
      and "P ⊆ Q"
    shows "{P, R} SKIP {G, Q}"
  using assms by force

method method_skip =
  rule rg_skip_named,
  goal_cases stab_pre stab_post guar_id est_post

text ‹An alternative version with an invariant subgoal.›

theorem rg_basic_inv[intro]:
  assumes "stable (P ∩ I) (R ∩ pred_to_rel I)"
      and "stable (Q ∩ I) (R ∩ pred_to_rel I)"
      and "∀s. s ∈ P ∩ I ⟶ (s, s) ∈ G"
      and "∀s. s ∈ P ∩ I ⟶ f s ∈ I"
      and "∀s. s ∈ P ∩ I ⟶ f s ∈ Q"
      and "∀s. s ∈ P ∩ I ⟶ (s, f s) ∈ G"
    shows "⊢ (Basic f) sat [
      P ∩ I, 
      R ∩ pred_to_rel I, 
      invar_and_guar I G, 
      Q ∩ I]"
  using assms apply -
  by (method_basic; fastforce)

method method_basic_inv = rule rg_basic_inv,
  goal_cases stab_pre stab_post id_guar est_inv est_post est_guar

(*----------------------------------------------------------------------------*)
subsubsection ‹Looping constructs›

theorem rg_general_loop_named[intro]:
  assumes "stable P R"
      and "stable Q R"
      and "Id ⊆ G"
      and "P ∩ -b ⊆ Q"
      and "{P ∩ b, R} c {G, P}"
    shows "{P, R} While b c {G, Q}"
  using assms apply -
  by (rule While; fastforce)

method method_loop =
  rule rg_general_loop_named,
  goal_cases stable_pre stable_post id_guar loop_exit loop_body

text ‹A similar version but with the @{text loop_body} subgoal having a
weakend precondition.›

theorem rg_general_loop_no_guard[intro]:
  assumes "stable P R"
      and "stable Q R"
      and "Id ⊆ G"
      and "P ∩ -b ⊆ Q"
      and "{P, R} c {G, P}"
    shows "{P, R} While b c {G, Q}"
  apply(rule rg_general_loop_named)
  by (fastforce intro!: assms Int_lower1 intro: strengthen_pre)+

method method_loop_no_guard = 
  rule rg_general_loop_no_guard,
  goal_cases stab_pre stab_post guar_id loop_exit loop_body

text ‹A \emph{spinloop} is a loop with an empty body. Such a loop repeatedly
checks a property, and is a key construct in mutual exclusion algorithms.›

theorem rg_spinloop_named[intro]:
  assumes "stable P R"
      and "stable Q R"
      and "Id ⊆ G"
      and "P ∩ -b ⊆ Q"
    shows "{P, R} While b SKIP {G, Q}"
  using assms
  by (fastforce simp: rg_general_loop_no_guard rg_skip_named)


method method_spinloop = 
  rule rg_spinloop_named,
  goal_cases stable_pre stable_post guar_id est_post

theorem rg_infinite_loop:
  assumes "stable P R"
      and "Id ⊆ G"
      and "{P, R} C {G, P}"
    shows "{P, R} While UNIV C {G, Q}"
proof -
  have "{P, R} While UNIV C {G, {}}"
    using assms by (fastforce simp: rg_general_loop_no_guard)
  thus ?thesis
    using weaken_post by fastforce
qed

method method_infinite_loop =
  rule rg_infinite_loop,
  goal_cases stable_pre guar_id loop_body,
  clarsimp+

theorem rg_infinite_loop_syntax:
  assumes "stable P R"
      and "Id ⊆ G"
      and "{P, R} C {G, P}"
    shows "{P, R} WHILE True DO C OD {G, Q}"
  using assms by (fastforce simp: rg_infinite_loop)

method method_infinite_loop_syntax =
  rule rg_infinite_loop_syntax,
  goal_cases stable_pre guar_id loop_body

text ‹A \emph{repeat-loop} encodes the pattern where the loop body is executed 
before the first evaluation of the guard.›

theorem rg_repeat_loop[intro]:
  assumes "stable P R"
      and "stable Q R"
      and "Id ⊆ G"
      and "P ∩ b ⊆ Q"
      and loop_body: "{P, R} C {G, P}"
    shows "{P, R} C ;; While (-b) C {G, Q}"
  using assms apply -
  apply (rule Seq)
   apply (force intro: loop_body)
  by (method_loop_no_guard; fastforce)

method method_repeat_loop =
  rule rg_repeat_loop,
  goal_cases stab_pre stab_post guar_id loop_exit loop_body

text ‹When reasoning about repeat-loops, we may need information from @{text P} 
to determine whether we reach the postcondition. In this case we can use the 
following form, which introduces a mid-state.›

theorem rg_repeat_loop_mid[intro]:
  assumes stab_pre:  "stable (P ∩ M) R"
      and stab_post: "stable Q R"
      and guar_id:   "Id ⊆ G"
      and loop_exit: "P ∩ M ∩ b ⊆ Q"
      and loop_body: "{P, R} C {G, P ∩ M}"
    shows "{P, R} C ;; While (-b) C {G, Q}"
 using assms apply -
  apply (rule Seq)
   apply (fast intro: loop_body)
  by (method_loop_no_guard; fast intro: loop_body strengthen_pre)

method method_repeat_loop_mid =
  rule rg_repeat_loop_mid,
  goal_cases stab_pre stab_post guar_id loop_exit loop_body

text ‹We define dedicated syntax for the repeat-loop pattern.›

definition Repeat :: "'a com ⇒ 'a bexp ⇒ 'a com" where
  "Repeat c b ≡ c ;; While (-b) c"

syntax "_Repeat" :: "'a com ⇒ 'a bexp ⇒ 'a com"  ("(0REPEAT _ /UNTIL _ /END)"  [0, 0] 61)
translations "REPEAT c UNTIL b END" ⇀ "CONST Repeat c ⦃b⦄"

theorem rg_repeat_loop_def[intro]:
  assumes stab_pre:  "stable P R"
      and stab_post: "stable Q R"
      and guar_id:   "Id ⊆ G"
      and loop_exit: "P ∩ b ⊆ Q"
      and loop_body: "{P, R} C {G, P}"
    shows "{P, R} Repeat C b {G, Q}"
  using assms 
  by (fastforce simp: Repeat_def rg_repeat_loop)

method method_repeat_loop_def =
  rule rg_repeat_loop_def,
  goal_cases stab_pre stab_post guar_id loop_exit loop_body

(*----------------------------------------------------------------------------*)
subsubsection ‹Conditionals›

text ‹We first cover conditional-statements with or without the else-branch.›

theorem rg_cond_named[intro]:
  assumes stab_pre:  "stable P R"
      and stab_post: "stable Q R"
      and guar_id:   "Id ⊆ G"
      and then_br:   "{P ∩  b, R} c1 {G, Q}"
      and else_br:   "{P ∩ -b, R} c2 {G, Q}"
    shows "{P, R} Cond b c1 c2 {G, Q}"
  using assms apply -
  by (rule Cond; fastforce)

theorem rg_cond2_named[intro]:
  assumes stab_pre:  "stable P R"
      and stab_post: "stable Q R"
      and guar_id:   "Id ⊆ G"
      and then_br:   "{P ∩  b, R} c1 {G, Q}"
      and else_br:   "P ∩ -b ⊆ Q"
    shows "{P, R} Cond b c1 SKIP {G, Q}"
  using assms apply -
  by (rule rg_cond_named; fastforce simp: rg_skip_named strengthen_pre)
 
method method_cond =
  (rule rg_cond2_named | rule rg_cond_named),
  goal_cases stab_pre stab_post guar_id then_br else_br

text ‹Variants without the stable-post subgoal.›

theorem rg_cond_no_post[intro]:
  assumes stable_pre: "stable P R"
      and guar_id: "Id ⊆ G"
      and then_br: "{P ∩ b, R} c1 {G, Q}"
      and else_br: "{P ∩ -b, R} c2 {G, Q}"
    shows "{P, R} Cond b c1 c2 {G, Q}"
  using assms by (fastforce simp: Cond subset_iff)

theorem rg_cond_no_guard_no_post[intro]:
  assumes stable_pre: "stable P R"
      and guar_id: "Id ⊆ G"
      and then_br: "{P, R} c1 {G, Q}"
      and else_br: "{P, R} c2 {G, Q}"
    shows "{P, R} Cond b c1 c2 {G, Q}"
  using assms apply -
  by (rule Cond; fastforce intro: strengthen_pre)

method method_cond_no_post =
  (rule rg_cond_no_post | rule rg_cond_no_guard_no_post),
  goal_cases stab_pre guar_id then_br else_br

(*============================================================================*)
subsection ‹Parallel Compositions›

text ‹We now turn to the parallel composition, and cover several variants,
from the \emph{binary} parallel composition of two commands, to the
\emph{multi-parallel} composition of an indexed list of commands.
For each variant, we define the syntax and devise the subgoal-generating methods.›

(*----------------------------------------------------------------------------*)
subsubsection ‹Binary Parallel›

text ‹The syntax of binary parallel composition, without and with invariant.›

abbreviation binary_parallel :: 
  "'a set ⇒ 'a rel ⇒ 'a com ⇒ 'a com ⇒ 'a rel ⇒ 'a set ⇒ bool" 
 ("{_, _}  _ ∥ _  {_, _}") where
  "{P, R} C1 ∥ C2 {G, Q} ≡
    ∃ P1 P2 R1 R2 G1 G2 Q1 Q2. 
      ⊢ COBEGIN 
          (C1, P1, R1, G1, Q1) 
          ∥ 
          (C2, P2, R2, G2, Q2) 
      COEND SAT [P, R, G, Q]"

abbreviation binary_parallel_invar :: 
  "'a set ⇒ 'a rel ⇒ 'a com ⇒ 'a com ⇒ 'a set ⇒ 'a rel ⇒ 'a set ⇒ bool" 
 ("{_, _}  _ ∥  _ ⫽ _ {_, _}") where
  "{P, R} C1 ∥ C2 ⫽ I {G, Q} ≡
    ∃ P1 P2 R1 R2 G1 G2 Q1 Q2. 
      ⊢ COBEGIN 
          (C1, P1, R1, G1, Q1) 
          ∥ 
          (C2, P2, R2, G2, Q2) 
      COEND SAT [P ∩ I, R ∩ pred_to_rel I, invar_and_guar I G, Q ∩ I]"

(*----------------------------------------------------------------------------*)
text ‹Some helper lemmas for later.›

lemma simp_all_2:
  "(∀ i < Suc (Suc 0). P i) ⟷ P 0 ∧ P 1"
  by (fastforce simp: less_Suc_eq)

lemma simp_gen_Un_2:
  "(⋃ x ∈ ⦃´(<) (Suc (Suc 0)) ⦄. S x) = S 0 ∪ S 1"
  by (fastforce simp: less_Suc_eq)

lemma simp_gen_Un_2_not0:
  "(⋃ x ∈ ⦃´(<) (Suc (Suc 0)) ∧ ´(≠) (Suc 0) ⦄. S x) = S 0"
  by (fastforce simp: less_Suc_eq)

lemma simp_gen_Int_2:
  "(⋂ x ∈ ⦃´(<) (Suc (Suc 0)) ⦄. S x) = S 0 ∩ S 1"
  by (fastforce simp: less_Suc_eq)

theorem rg_binary_parallel:
  assumes "{P1, R1} (C1::'a com) {G1, Q1}"
      and "{P2, R2} (C2::'a com) {G2, Q2}"
      and "G1 ⊆ R2"
      and "G2 ⊆ R1"
      and "P ⊆ P1 ∩ P2"
      and "R ⊆ R1 ∩ R2"
      and "G1 ∪ G2 ⊆ G"
      and "Q1 ∩ Q2 ⊆ Q" 
    shows "⊢ COBEGIN 
      (C1, P1, R1, G1, Q1) 
       ∥ 
      (C2, P2, R2, G2, Q2) 
      COEND SAT [P, R, G, Q]"
  using assms apply -
  apply (rule Parallel)
  by (simp_all add: simp_all_2 simp_gen_Un_2 simp_gen_Int_2 simp_gen_Un_2_not0)

theorem rg_binary_parallel_exists: 
  assumes "{P1, R1} (C1::'a com) {G1, Q1}"
      and "{P2, R2} (C2::'a com) {G2, Q2}"
      and "G1 ⊆ R2"
      and "G2 ⊆ R1"
      and "P ⊆ P1 ∩ P2"
      and "R ⊆ R1 ∩ R2"
      and "G1 ∪ G2 ⊆ G"
      and "Q1 ∩ Q2 ⊆ Q" 
    shows "{P, R} C1 ∥ C2 {G, Q}"
  by (metis assms rg_binary_parallel)

theorem rg_binary_parallel_invar_conseq: 
  assumes C1: "{P1, R1} (C1::'a com) ⫽ I {G1, Q1}"
      and C2: "{P2, R2} (C2::'a com) ⫽ I {G2, Q2}"
      and "G1 ⊆ R2"
      and "G2 ⊆ R1"
      and "P ⊆ P1 ∩ P2"
      and "R ⊆ R1 ∩ R2"
      and "Q1 ∩ Q2 ⊆ Q"
      and "G1 ∪ G2 ⊆ G"
    shows "{P, R} C1 ∥ C2 ⫽ I {G, Q}"
  using assms apply -
  apply (rule rg_binary_parallel_exists)
  by force+

(*============================================================================*)
subsubsection ‹Multi-Parallel›

text ‹The syntax of multi-parallel, without and with invariants.›

syntax multi_parallel ::
  "'a set ⇒ 'a rel ⇒ idt ⇒ nat ⇒
   (nat ⇒ 'a set) ⇒ (nat ⇒ 'a rel) ⇒
   (nat ⇒ 'a com) ⇒
   (nat ⇒ 'a rel) ⇒ (nat ⇒ 'a set) ⇒
   'a rel ⇒ 'a set ⇒ bool"
  ("global'_init: _ global'_rely: _ ∥  _ < _ @ {_,_} _ {_,_} global'_guar: _ global'_post: _") 

translations 
  "global_init: Init global_rely: RR ∥ i < N @
   {P,R} c {G,Q} global_guar: GG global_post: QQ"
  ⇀ "⊢ COBEGIN SCHEME [0 ≤ i < N] (c, P, R, G, Q) COEND
     SAT [Init, RR , GG, QQ]"

syntax multi_parallel_inv ::
  "'a set ⇒ 'a rel ⇒ idt ⇒ nat ⇒
   (nat ⇒ 'a set) ⇒ (nat ⇒ 'a rel) ⇒
   (nat ⇒ 'a com) ⇒ (nat ⇒ 'a set) ⇒
   (nat ⇒ 'a rel) ⇒ (nat ⇒ 'a set) ⇒
   'a rel ⇒ 'a set ⇒ bool"
  ("global'_init: _ global'_rely: _ ∥  _ < _ @ {_,_} _ ⫽ _ {_,_} global'_guar: _ global'_post: _") 

translations 
  "global_init: Init global_rely: RR ∥ i < N @
   {P, R} c ⫽ I {G, Q} global_guar: GG global_post: QQ"
  ⇀ "⊢ COBEGIN SCHEME [0 ≤ i < N] (c,
          P ∩ I,
          R ∩ CONST pred_to_rel I,
          CONST invar_and_guar I G,
          Q ∩ I
        ) COEND
     SAT [Init, RR , GG, QQ]"

(*----------------------------------------------------------------------------*)
text ‹The subgoal-generating method for multi-parallel.›

theorem rg_multi_parallel_subgoals:
  assumes assm_guar_rely: "∀ i j. i ≠ j ⟶ i < N ⟶ j < N ⟶ G j ⊆ R i"
      and assm_pre:  "∀ i < N. P' ⊆ P i"
      and assm_rely: "∀ i < N. R' ⊆ R i"
      and assm_guar: "∀ i < N. G i ⊆ G'"
      and assm_post: "(⋂ i ∈ { i. i < N }. Q i) ⊆ Q'"
      and assm_local: "∀ i<N. ⊢ C i sat [P i, R i, G i, Q i]"
    shows "⊢ COBEGIN SCHEME [0 ≤ i < (N::nat)]
           (C i, P i, R i, G i, Q i)
           COEND SAT [P', R', G', Q']"
proof (rule Parallel, goal_cases)
  case 1 show ?case using assm_rely assm_guar_rely by (simp add: SUP_le_iff)
  case 2 show ?case using assm_guar  by force
  case 3 show ?case using assm_pre   by force
  case 4 show ?case using assm_post  by force
  case 5 show ?case using assm_local by force
qed

method method_multi_parallel = rule rg_multi_parallel_subgoals,
  goal_cases guar_rely pre rely guar post body

theorem rg_multi_parallel_nobound_subgoals:
  assumes assm_guar_rely: "∀ i j. i ≠ j ⟶ G j ⊆ R i"
      and assm_pre:  "∀ i. P' ⊆ P i"
      and assm_rely: "∀ i. R' ⊆ R i"
      and assm_guar: "∀ i. G i ⊆ G'"
      and assm_post: "(⋂ i ∈ { i. i < N }. Q i) ⊆ Q'"
      and assm_local: "∀ i. ⊢ C i sat [P i, R i, G i, Q i]"
    shows "⊢ COBEGIN SCHEME [0 ≤ i < (N::nat)]
           (C i, P i, R i, G i, Q i)
           COEND SAT [P', R', G', Q']"
  using assms apply -
  apply (rule Parallel)
  by (simp_all add: SUP_le_iff INT_greatest)

method method_multi_parallel_nobound =
  rule rg_multi_parallel_nobound_subgoals,
  goal_cases guar_rely pre rely guar post body

(*============================================================================*)
subsection ‹Syntax of Record-Updates›

text ‹This section contains syntactic sugars for updating a field of a record.
As we use records to model the states of a program, these record-update
operations correspond to the variable-assignments.

The type @{typ idt} denotes a field of a record. The first syntactic sugar
expresses a Basic command (of type @{typ[cartouche=true] ‹'a com›}) that
updates a record-field @{term x} that is a function; often @{term x} models
an array. After the update, the new value of @{term[cartouche=true] ‹x i›}
becomes @{term a}.›

syntax "_record_array_assign" ::
  "idt ⇒ 'index ⇒ 'expr ⇒ 'state com" ("(´_[_] :=/ _)" [70, 65, 64] 61)
translations "´x[i] := a"
  ⇀ "CONST Basic «´(_update_name x (λ_. ´x(i:= a)))»"

text ‹The next two syntactic sugars express a state-transformation
function (rather than a command) that updates record-fields.
The first one simply updates an entire variable @{term x},
while the second updates an array @{term[cartouche=true] ‹x i›}.›

syntax "_record_update_field" ::
  "idt ⇒ 'expr ⇒ ('a ⇒ 'a)" ("´_ ←/ _" [70] 61)
translations "´x ← a"
  ⇌ "«´(_update_name x (λ_. a))»"

syntax "_record_update_array" ::
  "idt ⇒ 'expr ⇒ 'expr ⇒ ('a ⇒ 'a)" ("´_[_] ←/ _" [70, 71] 61)
translations "´x[i] ← a"
  ⇀ "«´(_update_name x (λ_. ´x(i:= a)))»"

text ‹Syntactic sugars for incrementing variables.›

syntax "_inc_fn" :: "idt ⇒ 'c ⇒ 'c"  ("(´_.++)" 61)
translations "´x.++ " ⇀ 
  " «´(_update_name x (λ_. ´x + 1))»"

syntax "_inc" :: "idt ⇒ 'c com"  ("(´_++)" 61)
translations "´x++ " ⇀ 
  "CONST Basic (´x.++)"

end