Theory RG_Annotated_Commands

(*
Title:         Rely-Guarantee Annotated Commands
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 ‹Annotated Commands›

text ‹This theory defines \emph{annotated commands} on top of the build-in
RG library. It also defines the relevant syntax and subgoal-generating methods.›

theory RG_Annotated_Commands
imports RG_Syntax_Extensions
begin

datatype 'a anncom =
    NoAnno     "'a com"                            ("'(_')-")
  | BasicAnno  "'a ⇒ 'a"
  | WeakPre    "'a set"    "'a anncom"             ("{_} _"  52)
  | StrongPost "'a anncom" "'a set"                ("_ {_}"  53)
  | SeqAnno    "'a anncom" "'a set"    "'a anncom" ("_ .; {_} _" [60,0,61] 60)
  | CondAnno   "'a bexp"   "'a anncom" "'a anncom" 
  | WhileAnno  "'a bexp"   "'a set"    "'a anncom" 
  | AwaitAnno  "'a bexp"   "'a anncom" 

fun anncom_to_com :: "'a anncom ⇒ 'a com" where
    "anncom_to_com (NoAnno c)    = c"
  | "anncom_to_com (BasicAnno f) = Basic f"
  | "anncom_to_com (WeakPre b c)    = anncom_to_com c"
  | "anncom_to_com (StrongPost c b) = anncom_to_com c"
  | "anncom_to_com (SeqAnno c1 mid c2) = Seq     (anncom_to_com c1) (anncom_to_com c2)"
  | "anncom_to_com (CondAnno b c1 c2)  = Cond  b (anncom_to_com c1) (anncom_to_com c2)"
  | "anncom_to_com (WhileAnno b b' c)  = While b (anncom_to_com c)"
  | "anncom_to_com (AwaitAnno b c)     = Await b (anncom_to_com c)"

fun add_invar :: "'a set ⇒ 'a anncom ⇒ 'a anncom" where
    "add_invar I (NoAnno c)          = NoAnno c"
  | "add_invar I (BasicAnno f)       = BasicAnno f"
  | "add_invar I (WeakPre b c)       = WeakPre (b ∩ I) (add_invar I c)"
  | "add_invar I (StrongPost c b)    = StrongPost      (add_invar I c)  (b ∩ I)"
  | "add_invar I (SeqAnno c1 mid c2) = SeqAnno         (add_invar I c1) (mid ∩ I) (add_invar I c2)"
  | "add_invar I (CondAnno b c1 c2)  = CondAnno  b     (add_invar I c1) (add_invar I c2)"
  | "add_invar I (WhileAnno b b' c)  = WhileAnno b b'  (add_invar I c)"
  | "add_invar I (AwaitAnno b c)     = AwaitAnno b     (add_invar I c)"

(*============================================================================*)
subsection ‹Syntactic Sugars›

abbreviation "SKIPa ≡ NoAnno SKIP"

syntax (* anncom *)
  "_CondAnno" :: "'a bexp ⇒ 'a anncom ⇒ 'a anncom ⇒ 'a anncom"
    ("(0IFa _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)

  "_Cond2Anno" :: "'a bexp ⇒ 'a anncom ⇒ 'a anncom"
    ("IFa _ THEN _ FI"  67)

  "_WhileAnno" :: "'a bexp ⇒ 'a set ⇒ 'a anncom ⇒ 'a anncom"
    ("(0WHILEa _ /DO {stable'_guard: _ } _ /OD)"  [0, 0] 61)

  "_WhileAnno_simple_b" :: "'a bexp ⇒ 'a anncom ⇒ 'a anncom"
    ("(0WHILEa _ /DO  _ /OD)"  [0, 0] 61)

  "_Spinloop" :: "'a bexp ⇒ 'a anncom"
    ("(SPIN _)"   63)

  "_AwaitAnno" :: "'a bexp ⇒ 'a anncom ⇒ 'a anncom"
    ("(0AWAITa _ /THEN /_ /END)"  [0,0] 61)

 (* "_AtomAnno" :: "'a com ⇒ 'a anncom"
    ("(⟨_⟩a)" 61)*)

  "_WaitAnno" :: "'a bexp ⇒ 'a anncom"
    ("(0WAITa _ END)" 61)

  "_CondAnno_NoAnnotations" :: "'a bexp ⇒ 'a com ⇒ 'a com ⇒ 'a anncom"
    ("(0IF. _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)

translations (* anncom *)
  "IFa b THEN c1 ELSE c2 FI" ⇀ "CONST CondAnno ⦃b⦄ c1 c2"
  "IFa b THEN c FI" ⇌ "IFa b THEN c ELSE (CONST SKIPa) FI"
  "IF. b THEN c1 ELSE c2 FI" ⇀ "CONST CondAnno ⦃b⦄ (CONST NoAnno c1) (CONST NoAnno c2)"

  "WHILEa b DO {stable_guard: b'} c OD" ⇀ "CONST WhileAnno ⦃b⦄ b' c"
  "WHILEa b DO  c OD" ⇀ "CONST WhileAnno ⦃b⦄ ⦃b⦄ c"
  (*"SPIN b " ⇀ "CONST WhileAnno ⦃b⦄ CONST UNIV CONST SKIPa"*)

  "AWAITa b THEN c END" ⇌ "CONST AwaitAnno ⦃b⦄ c"
 (* "⟨c⟩a" ⇌ "AWAITa CONST True THEN c END"*)
  "WAITa b END" ⇌ "AWAITa b THEN SKIP END"

abbreviation "Cond_Skip_Right b c ≡  CondAnno b c  SKIPa"

abbreviation "Spinloop b ≡ WhileAnno b UNIV SKIPa"
translations (* anncom *)
  "SPIN b " ⇀ "CONST Spinloop ⦃b⦄ "

definition Forever:: "'a anncom ⇒ 'a anncom" ("FOREVER _" 55)
  where "FOREVER c ≡ WHILEa (CONST True) DO c OD "

syntax  "_When" :: "'a set ⇒ 'a anncom ⇒ 'a anncom"
    ("(WHEN _ /DO  _ /OD)"  [0, 0] 61)

translations  "WHEN b DO  c OD" ⇀ " FOREVER (IFa b THEN c FI)"

text ‹We remove the slash notation to avoid ambiguous syntax›
no_notation  inverse_divide    (infixl "'/" 70)

text "Syntax for when you just want to give a block of sequential code to be executed
atomically, with no annotations"
abbreviation Atomic :: "'a com ⇒ 'a anncom" ("⟨_⟩a")
  where "Atomic c ≡ AwaitAnno UNIV (NoAnno c)"

abbreviation left_Basic_seq_comp:: "'a com ⇒ 'a set ⇒ 'a anncom ⇒ 'a anncom" 
  ("_ ..; _ _" [61, 0, 61] 62) where
  "a ..;m c ≡ NoAnno a .;{m} c"

abbreviation left_Atomic_seq_comp:: "'a com ⇒ 'a set ⇒ 'a anncom ⇒ 'a anncom" 
  ("⟨_⟩ .; _ _" [0, 0, 62] 64) where
  "⟨a⟩ .;m c ≡ ⟨a⟩a .;{m} c"

abbreviation ExplicitPre:: "'a set ⇒ 'a anncom ⇒ 'a anncom" 
  ("_ '/ _" [62, 53] 53) where
  "p / c ≡ {p} c"

abbreviation ExplicitPost:: "'a anncom ⇒ 'a set ⇒ 'a anncom" 
  ("_ '/ _" [56, 64] 56) where
  "c / p ≡ c {p}"

lemma 
  "SKIPa = p / (c::'a anncom) .;{m} c / p"

  "SKIPa = p / c .;{m} (SPIN b) / p"
  "SKIPa = p / a ..; m (SPIN b) / p"
  "SKIPa = IFa pp THEN a ..; m c FI"
  "SKIPa = a ..; m IFa pp THEN a ..; m c / p FI"

  "SKIPa = ⟨x⟩ .; m (z)- / p"

  "SKIPa = p / ⟨x⟩ .; m a ..; m ⟨x⟩ .; m (z)- / p"
  "SKIPa = p / ⟨x⟩ .; ⦃q⦄ a ..; m ⟨x⟩ .; m (z)- / p"
  "SKIPa = a ..; ⦃q⦄ a ..; m ⟨x⟩ .; m (z)- "

  "⟨kk ;; kk⟩ .; ⦃jj ∧ dd⦄ SKIPa = SKIPa"
  oops (* Checking the syntax plays nicely together *)

(*============================================================================*)
subsection ‹Validity›

fun anncom_spec_valid ::
  "'a set ⇒ 'a rel ⇒ 'a rel ⇒ 'a set ⇒ 'a anncom ⇒ bool"
  where
  "anncom_spec_valid pre rely guar post (NoAnno c)
  = (⊢ c sat [pre, rely, guar, post])"

| "anncom_spec_valid pre rely guar post (BasicAnno f)
  =
       (stable pre rely
      ∧ stable post rely
      ∧ (∀s. s ∈ pre ⟶ (s, s) ∈ guar)
      ∧  (∀s. s ∈ pre ⟶ (s, f s) ∈ guar)
      ∧  pre ⊆ ⦃ ´f ∈ post ⦄)" 

| "anncom_spec_valid pre rely guar post (WeakPre p' ac)
  = ((pre ⊆ p') ∧
     (anncom_spec_valid p' rely guar post ac))"

| "anncom_spec_valid pre rely guar post (StrongPost ac q')
  = ((q' ⊆ post) ∧
     (anncom_spec_valid pre rely guar q' ac))"

| "anncom_spec_valid pre rely guar post (SeqAnno ac1 mid ac2)
  = ((anncom_spec_valid pre rely guar mid  ac1) ∧
     (anncom_spec_valid mid rely guar post ac2))"

| "anncom_spec_valid pre rely guar post (CondAnno b ac1 ac2)
  = ((stable pre rely) ∧
     (Id ⊆ guar) ∧
     (anncom_spec_valid (pre ∩  b) rely guar post ac1) ∧
     (anncom_spec_valid (pre ∩ -b) rely guar post ac2))"

| "anncom_spec_valid pre rely guar post (WhileAnno b b' ac)
  = ((stable pre rely) ∧
     (stable post rely) ∧
     (Id ⊆ guar) ∧
     (pre ∩ -b ⊆ post) ∧
     (pre ∩  b ⊆ b') ∧
     (anncom_spec_valid (pre ∩ b') rely guar pre ac))"

| "anncom_spec_valid pre rely guar post (AwaitAnno b ac)
  = ((stable pre rely) ∧
     (stable post rely) ∧
     (∀ s. anncom_spec_valid (pre ∩ b ∩ {s}) Id UNIV ({s'. (s, s') ∈ guar} ∩ post) ac))"

theorem anncom_spec_valid_sound:
  "anncom_spec_valid pre rely guar post ac ⟹ ⊢ anncom_to_com ac sat [pre, rely, guar, post]"
proof (induction ac arbitrary: pre rely guar post)
  case (NoAnno x)
  then show ?case by(cases x ; simp; auto)
next
 case (BasicAnno x)
  then show ?case
    by auto (* Use "simp" if having different definition in "anncom_spec_valid.BasicAnno" *)
next
  case (WeakPre pre' ac)
  then show ?case using Conseq by fastforce
next
  case (StrongPost ac x2)
  then show ?case using weaken_post by fastforce
next
  case (SeqAnno ac1 x2 ac2)
  then show ?case using Seq by fastforce
next
  case (CondAnno x1a ac1 ac2)
  then show ?case by (simp add: Cond subset_iff)
next
  case (WhileAnno x1a x2 ac)
  then show ?case
    apply simp using While
    by (smt (verit, best) Int_subset_iff RG_Hoare.stable_def in_mono inf_le1 pair_in_Id_conv strengthen_pre)
next
  case (AwaitAnno x1a ac)
  then show ?case apply simp 
    apply (rule Await)
    using AwaitAnno.prems anncom_spec_valid.simps(8) apply blast+
    apply auto[1]
    by (smt (verit, best) Conseq IdI case_prodE mem_Collect_eq subset_iff)
qed

theorem anncom_spec_valid_sound_format:
  assumes "anncom_spec_valid pre rely guar post ac"
and "anncom_to_com ac = c"
shows " ⊢ c sat [pre, rely, guar, post]"
  using anncom_spec_valid_sound assms(1) assms(2) by blast

theorem anncom_spec_valid_sound_NoAnno:
  assumes "anncom_spec_valid pre rely guar post (NoAnno c)"
shows " ⊢ c sat [pre, rely, guar, post]"
  using assms by auto

(*==================================================================*)
subsection ‹Annotated Quintuples›

text ‹An annotated quintuple includes an annotated command along with
its top-level pre/post-conditions and rely/guarantee-relations.›

datatype 'a annquin = AnnQuin "'a set" "'a rel" "'a anncom" "'a rel" "'a set"
  ("{_,_} _ {_,_}" ) 

text "Helper functions for extracting the fields from the syntax"

fun  preOf :: "'a annquin ⇒ 'a set"
  where "preOf (AnnQuin pre rely ac guar post) = pre"

fun relyOf :: "'a annquin ⇒ 'a rel"
  where "relyOf (AnnQuin pre rely ac guar post) = rely"

fun  cmdOf :: "'a annquin ⇒ 'a anncom"
  where "cmdOf (AnnQuin pre rely ac guar post) = ac"

fun guarOf :: "'a annquin ⇒ 'a rel"
  where "guarOf (AnnQuin pre rely ac guar post) = guar"

fun postOf :: "'a annquin ⇒ 'a set"
  where "postOf (AnnQuin pre rely ac guar post) = post"

text ‹Where an invariant permeates an annotated command, this can be 
abbreviated by drawing the invariant out to the top level, and
transformed into an annotated quintuple.›

text "Alternative abbreviation for a quintuple using explicit keywords"

abbreviation annquin_keyword ::
  "'a rel ⇒  'a rel ⇒ 'a set ⇒ 'a anncom  ⇒ 'a set ⇒ 'a annquin"
  ("rely:_ guar:_ annotated'_code: {_} _ {_}") where
  "annquin_keyword rely guar pre ac post ≡ AnnQuin pre rely ac guar post"

definition annquin_invar ::
  "'a set ⇒ 'a rel ⇒ 'a anncom ⇒ 'a set ⇒ 'a rel ⇒ 'a set ⇒ 'a annquin"
  ("{_ , _}/_⫽_/{_ , _}") where
  "annquin_invar pre rely ac I guar post
    ≡ AnnQuin (pre ∩ I) (lift_rely I rely) (add_invar I ac) (lift_guar I guar) (post ∩ I)"

lemma preOf_with_invariant[simp]:
  "preOf  {p, r} c ⫽ invar {g, q} = p ∩ invar"
  "relyOf {p, r} c ⫽ invar {g, q} = lift_rely invar r"
  "guarOf {p, r} c ⫽ invar {g, q} = lift_guar invar g"
  "postOf {p, r} c ⫽ invar {g, q} = q ∩ invar"
  by (auto simp add: annquin_invar_def)

text "Simple abbreviation for particular order of parameters"

abbreviation annquin_valid ::
  "'a annquin ⇒ bool" where
  "annquin_valid rgac ≡ case rgac of (AnnQuin pre rely ac guar post) ⇒
   anncom_spec_valid pre rely guar post ac"

lemma annquin_simp:
  "annquin_valid (AnnQuin p r c g q) = anncom_spec_valid p r g q c" (* {p,r} c {g,q} *)
  by simp

abbreviation annquin_keyword_invar ::
  "'a rel ⇒ 'a rel ⇒ 'a set ⇒ 'a set ⇒ 'a anncom ⇒ 'a set ⇒ 'a annquin"
  ("rely:_ guar:_ inv:_ annotated'_code: {_} _ {_}") where
  "annquin_keyword_invar rely guar I pre ac post
    ≡ {pre, rely} ac ⫽ I {guar, post}"

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

subsubsection ‹Binary Parallel›

text ‹Abbreviate all helpers that specialise quantification over n threads to two threads.›
lemmas binpar_from_gen_simps = simp_all_2 simp_gen_Un_2 simp_gen_Un_2_not0 simp_gen_Int_2

text "Encapsulate two processes working parallel, along with the global r/g/p/q"
datatype 'a binary_par_with_rg = ParCode
    "'a set "" 'a rel "" 'a annquin "" 'a annquin "" 'a rel "" 'a set "  ("{_,_} _ ∥a _ {_,_}")

text "Alternative syntax using keywords and bringing g/q up front"
abbreviation binary_par_with_rg_keywords:: "'a set ⇒ 'a rel ⇒ 'a rel ⇒ 'a set ⇒ 'a annquin ⇒ 'a annquin ⇒  'a binary_par_with_rg"
  ("global'_init: _ global'_rely: _ global'_guar: _ global'_post: _ _ ∥a _") where
  "global_init: i global_rely: R global_guar: G global_post: Q c1 ∥a c2 ≡ {i, R} c1 ∥a c2 {G, Q}"

text "Make explicit the proof obligations for two processes working in parallel, using the above data type"
fun valid_binary_parallel_composition:: "'a binary_par_with_rg ⇒ bool" ("validpar:_") where
  "validpar: {init, gr} ac1 ∥a ac2 {gg, final} = 
    ((annquin_valid ac1) ∧
     (annquin_valid ac2) ∧
      init ⊆ preOf ac1 ∩ preOf ac2 ∧
      gr ⊆ relyOf ac1 ∩ relyOf ac2 ∧
      guarOf ac1 ⊆ relyOf ac2 ∧ guarOf ac2 ⊆ relyOf ac1 ∧
      guarOf ac1 ∪ guarOf ac2 ⊆ gg ∧
      postOf ac1 ∩ postOf ac2 ⊆ final)"

text "Make explicit the proof obligations for two processes working in parallel, using the above data type"
lemma valid_binary_parallel_composition_expand:
  "validpar: {init, gr} (rely: r1 guar: g1 annotated_code: {p1}c1{q1}) ∥a (rely: r2 guar: g2 annotated_code: {p2}c2{q2}) {gg, final} = 
    (annquin_valid (rely: r1 guar: g1 annotated_code: {p1}c1{q1}) ∧
     annquin_valid (rely: r2 guar: g2 annotated_code: {p2}c2{q2}) ∧
      init ⊆ p1 ∩ p2 ∧
      gr ⊆ r1 ∩ r2 ∧
      g1 ⊆ r2 ∧ g2 ⊆ r1 ∧
      g1 ∪ g2 ⊆ gg ∧
      q1 ∩ q2 ⊆ final)"
  by auto

text "The following theorem shows that the conditions of ``expand satisfiability binpar'' above are sufficient for the relevant proof in original PN style"
theorem valid_binary_parallel:
 "validpar: {init,gr}
 (rely: r1 guar: g1 annotated_code: {p1} c1 {q1}) ∥a (rely: r2 guar: g2 annotated_code: {p2} c2 {q2}) 
           {gg,final}
 ⟹ ⊢ COBEGIN (anncom_to_com c1, p1, r1, g1, q1) ∥ (anncom_to_com c2, p2, r2, g2, q2) 
       COEND SAT [init, gr, gg, final]"
  apply auto[1]
  apply(rule Parallel)
      apply (simp add: binpar_from_gen_simps)
     using less_Suc_eq apply auto
  by (simp add: anncom_spec_valid_sound)+

text "..and again but for existence of such"
theorem valid_binary_parallel_exists:
 "validpar: {init,gr}
 (rely: r1 guar: g1 annotated_code: {p1} c1 {q1}) ∥a (rely: r2 guar: g2 annotated_code: {p2} c2 {q2}) 
            {gg,final}
 ⟹ {init, gr} anncom_to_com c1 ∥ anncom_to_com c2 {gg, final}"
  by (meson valid_binary_parallel)

theorem valid_binary_parallel_exists_annotated:
  assumes "validpar:
          {init,gr}
          (rely: r1 guar: g1 annotated_code: {p1} c1' {q1}) ∥a
          (rely: r2 guar: g2 annotated_code: {p2} c2' {q2}) 
          {gg,final}"
     and "anncom_to_com c1' = c1"
     and "anncom_to_com c2' = c2"
   shows "{init, gr} c1 ∥ c2 {gg, final}"
  using assms by (meson valid_binary_parallel)

theorem valid_binary_par:
  assumes
    "annquin_valid ac1" and
    "annquin_valid ac2" and
      "init ⊆ preOf ac1 ∩ preOf ac2" and
      "gr ⊆ relyOf ac1 ∩ relyOf ac2" and
      "guarOf ac1 ⊆ relyOf ac2 ∧ guarOf ac2 ⊆ relyOf ac1" and
      "guarOf ac1 ∪ guarOf ac2 ⊆ gg" and
      "postOf ac1 ∩ postOf ac2 ⊆ final" 
    shows
  "validpar: {init, gr} ac1 ∥a ac2 {gg, final}  "
  apply(simp only: valid_binary_parallel_composition.simps)
  using assms by auto


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

datatype 'a multi_par_with_rg = MultiParCode
  "'a  set" (* global init *)
  "'a  rel" (* global rely *)
   nat nat  (* indices *)
  "nat ⇒ 'a annquin" (* indexed program *)
  "'a  rel" (* global guar *)
  "'a  set" (* global post *)

syntax multi_parallel_anno ::
  "'a set ⇒ 'a rel ⇒ idt ⇒ nat ⇒
   ('a annquin) ⇒
   'a rel ⇒ 'a set ⇒ 'a multi_par_with_rg"
  ("annotated global'_init: _ global'_rely: _ ∥  _ < _ @ _ global'_guar: _ global'_post: _") 

syntax multi_parallel_anno_lo_hi ::
  "'a set ⇒ 'a rel ⇒ nat ⇒ idt ⇒ nat ⇒ 
   ('a annquin) ⇒
   'a rel ⇒ 'a set ⇒ 'a multi_par_with_rg"
  ("annotated global'_init: _ global'_rely: _ ∥  _ ≤ _ < _ @ _ global'_guar: _ global'_post: _") 

translations 
  "annotated global_init: Init global_rely: RR ∥ i < N @
    rgac global_guar: GG global_post: QQ"
  ⇀ "CONST MultiParCode Init RR 0 N (λi. rgac) GG QQ"

  "annotated global_init: Init global_rely: RR ∥ lo ≤ i < hi @
    rgac global_guar: GG global_post: QQ"
  ⇀ "CONST MultiParCode Init RR lo hi (λi. rgac) GG QQ"


abbreviation nat_range_set_neq_i:: "nat ⇒ nat ⇒ nat ⇒ nat set" ("{_..<_≠_}") where
  "nat_range_set_neq_i lo hi x ≡ {lo..<hi} - {x}"

text "Proof obligations for N processes working in parallel, using the above data type"
fun valid_multi_parallel_composition:: "'a multi_par_with_rg ⇒ bool" ("valid'_multipar:_") where
  "valid_multipar: MultiParCode init RR lo N iac gg final =
   ( (∀i∈{lo..<N}. annquin_valid (iac i)) ∧
      init ⊆ (⋂i∈{lo..<N}.  preOf (iac i)) ∧
      RR ⊆ (⋂i∈{lo..<N}. relyOf (iac i)) ∧
      (∀i∈{lo..<N}. guarOf (iac i) ⊆ (⋂j∈{lo..<N≠i}. relyOf (iac j))) ∧
      (⋃i∈{lo..<N}. guarOf (iac i)) ⊆ gg ∧
      (⋂i∈{lo..<N}. postOf (iac i)) ⊆ final )"

fun valid_multi_parallel_composition_offset:: "'a multi_par_with_rg ⇒ bool" ("valid'_multipar'_offset:_") where
  "valid_multipar_offset: MultiParCode init RR lo N iac gg final =
   ( (∀i<(N-lo). annquin_valid (iac (lo + i))) ∧
      init ⊆ (⋂i<(N-lo).  preOf (iac (lo + i))) ∧
      RR ⊆ (⋂i<(N-lo). relyOf (iac (lo + i))) ∧
      (∀i<(N-lo). guarOf (iac (lo + i)) ⊆ (⋂j∈{0..<(N-lo)≠i}. relyOf (iac (lo + j)))) ∧
      (⋃i<(N-lo). guarOf (iac (lo + i))) ⊆ gg ∧
      (⋂i<(N-lo). postOf (iac (lo + i))) ⊆ final )"

lemma Int_set_range_to_offset: "(⋂i∈{lo..<hi::nat}.  f i) = (⋂i<(hi-lo).  f (lo + i))"
  apply auto
  by (metis add.commute le_iff_add lessThan_iff less_diff_conv)

lemma Un_set_range_to_offset: "(⋃i∈{lo..<hi::nat}.  g (f i)) = (⋃i<(hi-lo).  g (f (lo + i)))"
  apply auto
  apply (metis add_diff_cancel_left' diff_less_mono le_Suc_ex lessThan_iff)
  by (metis add.commute atLeastLessThan_iff le_add1 less_diff_conv)

lemma Int_set_range_neq_to_offset: "i = lo + ii ⟹ (⋂j∈{lo..<hi≠i}.  f j) = (⋂j∈{0..<(hi-lo)≠ ii}.  f (lo + j))"
  apply (auto simp add: Ball_def Bex_def image_def)
  apply (metis add.commute add_left_imp_eq le_add1 less_diff_conv)
  by (metis Nat.add_diff_assoc add_diff_cancel_left' diff_less_mono)

lemma forall_range_to_offset: "(∀i∈{lo..<(hi::nat)}. P i) ⟷ (∀i∈{0..<(hi - lo)}. P (lo + i))"
  apply (auto simp add: Ball_def)
  by (metis Nat.add_diff_assoc add_diff_cancel_left' diff_less_mono)

lemma valid_multipar_offset_equiv: "valid_multipar: MultiParCode init RR lo hi iac gg final ⟷
  valid_multipar_offset: MultiParCode init RR lo hi iac  gg final"
  apply simp
  apply (intro conjI iffI impI ; elim conjE)
             apply (simp_all add: Int_set_range_to_offset Un_set_range_to_offset)
    apply(simp add: Ball_def)
  using Int_set_range_neq_to_offset
    apply (smt (verit, ccfv_SIG) Sup.SUP_cong add.commute le_add1 less_diff_conv)
   apply (smt (verit, best) add.commute atLeastLessThan_iff le_iff_add less_diff_conv)
  apply(simp only: forall_range_to_offset[of lo hi] Int_set_range_neq_to_offset)
  by (metis atLeastLessThan_iff)

text "Discharging a ``valid multipar'' wrapped around the syntax of a multiway composition (with proof annotations) 
proves the relevant top-level theorem in PN"

lemma valid_multipar: 
  assumes "valid_multipar: MultiParCode Init RR lo N rgac GG QQ"
  shows "⊢ COBEGIN SCHEME [lo ≤ i < N] (
         CONST anncom_to_com (cmdOf (rgac i)),
          preOf (rgac i),
          relyOf (rgac i),
          guarOf (rgac i) ,
          postOf (rgac i) 
        ) COEND
     SAT [Init, RR , GG, QQ]"
  apply (rule Parallel)
  using assms 
      apply (auto simp add: subset_iff)
     apply(simp_all add: Ball_def)
     apply (metis add.commute add_right_cancel le_add1 less_diff_conv)
    apply (metis add.commute atLeastLessThan_iff le_add1 less_diff_conv)
   apply (metis add.commute add_diff_inverse_nat less_diff_conv not_le)
  by (smt (verit) add.commute anncom_spec_valid_sound annquin_simp bot_nat_0.extremum cmdOf.simps guarOf.simps le_add_same_cancel1 less_diff_conv postOf.elims preOf.simps relyOf.simps)

lemma valid_multipar_with_internal_rg: 
  assumes "valid_multipar: MultiParCode Init RR lo N (λi. {p i, r i} ac i {g i, q i}) GG QQ"
and "∀i. anncom_to_com (ac i) = c i"
shows "⊢ COBEGIN SCHEME [lo ≤ i < N] (c i, p i, r i, g i, q i) COEND
     SAT [Init, RR , GG, QQ]"
  apply(rule Parallel)
  using assms apply (simp_all add: subset_iff)
  apply(auto simp add: Ball_def)[1]
  apply (metis add.commute add_left_imp_eq le_add1 less_diff_conv)
  apply (metis add.commute atLeastLessThan_iff le_add1 less_diff_conv)
  apply (metis add.commute atLeastLessThan_iff less_diff_conv nat_le_iff_add)
  by (metis add.commute anncom_spec_valid_sound atLeastLessThan_iff le_add1 less_diff_conv)

theorem valid_multipar_explicit:
  assumes 
    local_sat: "⋀i. lo ≤ i ∧ i < N ⟹ annquin_valid (iac i)" and
    pre:  "⋀i. lo ≤ i ∧ i < N ⟹ init ⊆  preOf (iac i)" and
    rely: "⋀i. lo ≤ i ∧ i < N ⟹ RR ⊆ relyOf (iac i)" and     
    guar_imp_rely: "⋀i j. lo ≤ i ∧ i<N ⟹ lo ≤ j ∧ j < N ⟹ i ≠ j ⟹ guarOf (iac i) ⊆ relyOf (iac j)" and 
    guar: "⋀i. lo ≤ i ∧ i < N ⟹ guarOf (iac i) ⊆ gg" and 
    post: "(⋂i∈{lo..<N}. postOf (iac i)) ⊆ final"
    shows "valid_multipar: MultiParCode init RR lo N iac gg final"
  using assms apply auto
  by blast+

theorem valid_multipar_offset_explicit:
  assumes 
    local_sat: "⋀i. lo ≤ i ∧ i < N ⟹ annquin_valid (iac i)" and
    pre:  "⋀i. lo ≤ i ∧ i < N ⟹ init ⊆  preOf (iac i)" and
    rely: "⋀i. lo ≤ i ∧ i < N ⟹ RR ⊆ relyOf (iac i)" and     
    guar_imp_rely: "⋀i j. lo ≤ i ∧ i<N ⟹ lo ≤ j ∧ j < N ⟹ i ≠ j ⟹ guarOf (iac i) ⊆ relyOf (iac j)" and 
    guar: "⋀i. lo ≤ i ∧ i < N ⟹ guarOf (iac i) ⊆ gg" and 
    post: "(⋂i∈{lo..<N}. postOf (iac i)) ⊆ final"
  shows "valid_multipar_offset: MultiParCode init RR lo N iac gg final"
  apply(simp flip: valid_multipar_offset_equiv )
  using assms apply auto
  apply (auto simp add: subset_iff Ball_def Bex_def image_def)
  apply (metis add.commute add_right_cancel le_add2 less_diff_conv)
  apply (metis add.commute le_add1 less_diff_conv)
  by (metis le_add_diff_inverse le_add_diff_inverse2 less_diff_conv)

lemma LT_offset: "(∀i. lo ≤ i ∧ i < (N::nat) ⟶ P i) ⟷ (∀i<N - lo. P (lo + i))"
  by (metis add.commute le_add1 le_add_diff_inverse2 less_diff_conv)

theorem valid_multipar_explicit2:
  assumes 
    local_sat: "⋀i. lo ≤ i ∧ i < N ⟹ annquin_valid {p i,r i} c i {g i ,q i}" and
    pre:  "⋀i. lo ≤ i ∧ i < N ⟹ init ⊆  p i" and
    rely: "⋀i. lo ≤ i ∧ i < N ⟹ RR ⊆ r i" and     
    guar_imp_rely: "⋀i j. lo ≤ i ∧ i<N ⟹ lo ≤ j ∧ j < N ⟹ i ≠ j ⟹ g i ⊆ r j" and 
    guar: "⋀i. lo ≤ i ∧ i < N ⟹ g i ⊆ gg" and 
    post: "(⋂i∈{lo..<N}. q i) ⊆ final"
    shows "valid_multipar: MultiParCode init RR lo N (λi. {p i,r i} c i {g i ,q i}) gg final"
  using assms LT_offset by (auto simp add: subset_iff)

text "With explicit invariant abbreviation"
theorem valid_multipar_explicit_with_invariant:
  assumes 
    local_sat: "⋀i. i < N ⟹ annquin_valid {p i,r i} c i ⫽ Inv {g i ,q i}" and
    pre:  "⋀i. i < N ⟹ init ⊆  p i ∩ Inv" and
    rely: "⋀i. i < N ⟹ RR ⊆ lift_rely Inv (r i)" and     
    guar_imp_rely: "⋀i j. i<N ⟹ j < N ⟹ i ≠ j ⟹ lift_guar Inv (g i) ⊆ r j" and 
    guar: "⋀i. i < N ⟹ lift_guar Inv (g i) ⊆ gg" and 
    post: "(⋂i<N. q i ∩ Inv) ⊆ final"
  shows "valid_multipar: MultiParCode init RR 0 N (λi. {p i,r i} c i ⫽ Inv {g i ,q i}) gg final"
  apply (rule valid_multipar_explicit)
  using assms
       apply (simp only: annquin_invar_def)
      apply (metis annquin_invar_def pre preOf.simps)
     apply (simp add: annquin_invar_def)
  using rely 
     apply simp
    apply (simp add: annquin_invar_def subset_iff)
  apply clarsimp
  using guar_imp_rely apply fastforce
   apply (simp add: annquin_invar_def)
  using guar annquin_invar_def
   apply auto[1]
  apply (simp add: annquin_invar_def)
  using post by fastforce

method method_annquin_multi_parallel =
  rule valid_multipar_explicit2,
  goal_cases local_sat pre rely guar_imp_rely guar post

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

abbreviation triple_par_with_rg ::
    "'a set ⇒ 'a rel ⇒ 'a annquin ⇒ 'a annquin ⇒ 'a annquin ⇒ 'a rel ⇒ 'a set ⇒ 'a multi_par_with_rg"  ("{_,_} _ ∥3 _ ∥3 _ {_,_}")
    where
      "{I, R} p1 ∥3 p2 ∥3 p3 {G,Q} ≡ 
        MultiParCode I R 0 3 (λi. case i of 0 ⇒ p1 | Suc 0 ⇒ p2 | Suc (Suc 0) ⇒ p3) G Q"

theorem valid_3way_parallel_composition:
  assumes 
    "annquin_valid {p1,r1} c1 {g1,q1}"
    "annquin_valid {p2,r2} c2 {g2,q2}"
    "annquin_valid {p3,r3} c3 {g3,q3}"
    "I ⊆ p1 ∩ p2 ∩ p3"
    "R ⊆ r1 ∩ r2 ∩ r3"
    "g1 ⊆ r2 ∩ r3"
    "g2 ⊆ r1 ∩ r3"
    "g3 ⊆ r1 ∩ r2"
    "g1 ∪ g2 ∪ g3 ⊆ G "
    "q1 ∩ q2 ∩ q3 ⊆ Q"
  shows   "valid_multipar: ({I, R} ({p1,r1} c1 {g1,q1}) ∥3 ({p2,r2}c2{g2,q2}) ∥3 ({p3,r3}c3{g3,q3}) {G,Q})"
  apply auto
  using assms
       apply (simp_all add: subset_iff)
  subgoal for i apply (cases i; simp)
    subgoal for nat by(cases nat; simp)
    done
      apply(auto  split: nat.split)
    apply (metis (no_types, lifting) guarOf.simps less_2_cases linorder_neqE_nat nat.case(2) not_less_eq numeral_3_eq_3 numerals(2) old.nat.simps(4) relyOf.simps)
   apply (metis Nitpick.case_nat_unfold add_diff_cancel_left' guarOf.simps less_2_cases less_Suc_eq numeral_2_eq_2 numeral_3_eq_3 plus_1_eq_Suc)
  apply(auto simp add: Ball_def)
  by (metis bot_nat_0.extremum_strict lessI less_Suc_numeral nat.case(2) not_less_iff_gr_or_eq numerals(2) old.nat.simps(4) postOf.simps pred_numeral_simps(3))

theorem  valid_3way_parallel_composition_with_invariant:
  assumes 
    "annquin_valid {p1,r1} c1 ⫽invar {g1,q1}" and
    "annquin_valid {p2,r2} c2 ⫽invar {g2,q2}" and
    "annquin_valid {p3,r3} c3 ⫽invar {g3,q3}" and
    "I ⊆ invar" and
    "I ⊆ p1" and "I ⊆ p2" and "I ⊆ p3" and
    "R ⊆ lift_rely invar r1" and "R ⊆ lift_rely invar r2" and "R ⊆ lift_rely invar r3" and 
    "lift_guar invar g1 ⊆ r2" and "lift_guar invar g1 ⊆ r3" and
    "lift_guar invar g2 ⊆ r1" and "lift_guar invar g2 ⊆ r3" and
    "lift_guar invar g3 ⊆ r1" and "lift_guar invar g3 ⊆ r2" and
    "Restr g1 invar ⊆ G" and "Restr g2 invar ⊆ G" and "Restr g3 invar ⊆ G" and
    "Id ⊆ G" and 
    "q1 ∩ q2 ∩ q3 ∩ invar ⊆ Q"
  shows   "valid_multipar: ({I, R} ({p1,r1} c1 ⫽ invar {g1,q1}) ∥3 ({p2,r2}c2 ⫽ invar{g2,q2}) ∥3 ({p3,r3}c3⫽ invar{g3,q3}) {G,Q})"
  apply(simp only: annquin_invar_def)
  apply(rule valid_3way_parallel_composition)
           apply (metis annquin_invar_def assms(1))
          apply (metis annquin_invar_def assms(2))
         apply (metis annquin_invar_def assms(3))
  using assms(4) assms(5) assms(6) assms(7)
        apply auto[1]
       apply (simp add: assms(10) assms(8) assms(9))
  using assms(10) assms(8) assms(9) apply force
  using assms(11) assms(12) apply auto[1]
  using assms(13) assms(14) apply auto[1]
  using assms(15) assms(16) apply auto[1]
  using assms(17) assms(18) assms(19) apply auto[1]

   apply (simp add: assms(17) assms(18) assms(19))
  using assms(20) apply blast
  using assms(21) by blast

end