Theory Assume_Guarantee

(*<*)
theory Assume_Guarantee
imports
  "ConcurrentHOL.ConcurrentHOL"
begin

(*>*)
section‹ Assume/Guarantee rule sets\label{sec:ag} ›

text‹

The rules in \<^theory>‹ConcurrentHOL.Refinement› are deficient in various ways:
 ▪ redundant stability requirements
 ▪ interleaving of program decomposition with stability goals
 ▪ insufficiently instantiated

The following are some experimental rules aimed at practical assume/guarantee reasoning.

›


subsection‹ Implicit stabilisation\label{sec:ag-implicit_stabilisation} ›

text‹

We can define a relation ‹ceilr P› to be the largest (weakest assumption) for which ‹P› is stable.
This always yields a preorder (i.e., it is reflexive and transitive). Later we use this to inline
stability side conditions into assume/guarantee rules (\S\ref{sec:ag-iag}).

This relation is not very pleasant to work with: it is not monotonic
and does not have many useful algebraic properties. However it
suffices to defer the checking of assumes (see \S\ref{sec:ag-iag}).

This is a cognate of the ∗‹strongest guarantee› used by
\<^citet>‹‹Definition~8.31› in "deRoeverEtAl:2001"› in their completeness proof for the rely-guarantee
method.

›

definition ceilr :: "'a pred ⇒ 'a rel" where
  "ceilr P = ⨆{r. stable r P}"

lemma ceilr_alt_def:
  shows "ceilr P = {(s, s'). P s ⟶ P s'}"
by (auto simp: ceilr_def stable_def monotone_def le_bool_def order_eq_iff Sup_upper)

lemma ceilrE[elim]:
  assumes "(x, y) ∈ ceilr P"
  assumes "P x"
  shows "P y"
using assms by (simp add: ceilr_alt_def)

setup ‹Sign.mandatory_path "ceilr"›

named_theorems simps ‹simp rules for \<^const>‹ceilr››

lemma bot[ceilr.simps]:
  shows "ceilr ⊥ = UNIV"
by (simp_all add: ceilr_alt_def)

lemma top[ceilr.simps]:
  shows "ceilr ⊤ = UNIV"
by (simp_all add: ceilr_alt_def)

lemma const[ceilr.simps]:
  shows "ceilr ⟨c⟩ = UNIV"
    and "ceilr (P ❙∧ ⟨c⟩) = (if c then ceilr P else UNIV)"
    and "ceilr (⟨c⟩ ❙∧ P) = (if c then ceilr P else UNIV)"
    and "ceilr (P ❙∧ ⟨c⟩ ❙∧ P') = (if c then ceilr (P ❙∧ P') else UNIV)"
by (simp_all add: ceilr_alt_def)

lemma Id_le:
  shows "Id ⊆ ceilr P"
by (auto simp: ceilr_alt_def)

lemmas refl[iff] = ceilr.Id_le[folded refl_alt_def]

lemma trans[iff]:
  shows "trans (ceilr P)"
by (simp add: ceilr_alt_def trans_def)

lemma stable[stable.intro]:
  shows "stable (ceilr P) P"
by (simp add: ceilr_def stable.Union_conv)

lemma largest[stable.intro]:
  assumes "stable r P"
  shows "r ⊆ ceilr P"
by (simp add: ceilr_def assms Sup_upper)

lemma disj_subseteq: ―‹ Converse does not hold ›
  shows "ceilr (P ❙∨ Q) ⊆ ceilr P ∪ ceilr Q"
by (fastforce simp: ceilr_alt_def)

lemma Ex_subseteq: ―‹ Converse does not hold ›
  shows "ceilr (❙∃x. P x) ⊆ (⋃x. ceilr (P x))"
by (fastforce simp: ceilr_alt_def)

lemma conj_subseteq: ―‹ Converse does not hold ›
  shows "ceilr P ∩ ceilr Q ⊆ ceilr (P ❙∧ Q)"
by (fastforce simp: ceilr_alt_def)

lemma All_subseteq: ―‹ Converse does not hold ›
  shows "(⋂x. ceilr (P x)) ⊆ ceilr (❙∀x. P x)"
by (fastforce simp: ceilr_alt_def)

lemma const_implies[ceilr.simps]:
  shows "ceilr (⟨P⟩ ❙⟶ Q) = (if P then ceilr Q else UNIV)"
by (simp add: ceilr.simps)

lemma Id_proj_on:
  shows "(⋂c. ceilr (⟨c⟩ ❙= f)) = Id⇘f⇙"
    and "(⋂c. ceilr (f ❙= ⟨c⟩)) = Id⇘f⇙"
by (fastforce simp: ceilr_alt_def)+

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "stable"›

lemma Inter_ceilr:
  shows "stable (⋂v. ceilr (Q v)) (Q v)"
by (rule antimonoD[where y="ceilr (Q v)", OF stable.antimono_rel, unfolded le_bool_def, rule_format, rotated])
   (auto simp: ceilr.stable)

setup ‹Sign.parent_path›

text‹

We can internalize the stability conditions; see \S\ref{sec:ag-iag} for further discussion.

›

setup ‹Sign.mandatory_path "ag.prog"›

lemma p2s_s2p_ag_ceilr:
  shows "prog.p2s (prog.s2p (⦃P⦄, ceilr P ∩ (⋂v. ceilr (Q v)) ⊢ G, ⦃Q⦄))
       = ⦃P⦄, ceilr P ∩ (⋂v. ceilr (Q v)) ⊢ G, ⦃Q⦄"
by (simp add: ag.prog.p2s_s2p_ag_stable ceilr.stable stable.Inter_ceilr stable.infI)

setup ‹Sign.parent_path›


subsubsection‹ Assume/guarantee rules using implicit stability\label{sec:ag-iag} ›

text‹

We use \<^const>‹ceilr› to incorporate stability side conditions directly into the assume/guarantee
rules. In other words, instead of working with arbitrary relations, we work with the largest
(most general) ∗‹assume› that makes the relevant predicates \<^const>‹stable›.

In practice this allows us to defer all stability obligations to the end of a proof, which may be
in any convenient context (typically a function). This approach could be considered a semantic
version of how \<^citet>‹"ZakowskiEtAl:2019"› split sequential and assume/guarantee reasoning.
See \<^citet>‹‹\S4› in "Vafeiadis:2008"› for a discussion on when to check stability.

We defer the ∗‹guarantee› proofs by incorporating them into preconditions. This also allows
control flow context to be accumulated.

These are backchaining (``weakest precondition'') rules: the guarantee and post condition
need to be instantiated and the rules instantiate assume and pre condition schematics.

Note that the rule for \<^const>‹prog.bind› duplicates stability goals.

See \S\ref{sec:ex_findP} for an example of using these rules.

›

setup ‹Sign.mandatory_path "iag"›

named_theorems intro ‹safe backchaining intro rules›

lemma init:
  assumes "c ≤ ⦃P⦄, A ⊢ G, ⦃Q⦄"
  assumes "⋀s. P' s ⟹ P s"
  assumes "A' ⊆ A" ―‹ these rules use \<^const>‹ceilr› which always yields a reflexive relation (@{thm [source] "ceilr.refl"} ›
  shows "c ≤ ⦃P'⦄, A' ⊢ G, ⦃Q⦄"
using assms(2,3) by (auto intro: ag.mono order.trans[OF assms(1)])

lemmas mono = ag.mono

lemmas gen_asm = ag.gen_asm

lemmas pre = ag.pre
lemmas pre_pre = ag.pre_pre
lemmas pre_post = ag.pre_post
lemmas pre_ag = ag.pre_ag
lemmas pre_a = ag.pre_a
lemmas pre_g = ag.pre_g

lemmas post_imp = ag.post_imp

lemmas conj_lift = ag.conj_lift
lemmas disj_lift = ag.disj_lift
lemmas all_lift = ag.all_lift

lemmas augment_a = ag.augment_a
lemmas augment_post = ag.augment_post
lemmas augment_post_imp = ag.augment_post_imp

lemmas stable_augment_base = ag.stable_augment_base
lemmas stable_augment = ag.stable_augment
lemmas stable_augment_post = ag.stable_augment_post
lemmas stable_augment_frame = ag.stable_augment_frame

lemma bind[iag.intro]:
  assumes "⋀v. prog.p2s (g v) ≤ ⦃Q' v⦄, A⇩₂ v ⊢ G, ⦃Q⦄"
  assumes "prog.p2s f ≤ ⦃P⦄, A⇩₁ ⊢ G, ⦃Q'⦄"
  shows "prog.p2s (f ⤜ g) ≤ ⦃P⦄, A⇩₁ ∩ (⋂v. A⇩₂ v) ⊢ G, ⦃Q⦄"
by (auto simp: prog.p2s.simps intro: assms ag.spec.bind ag.pre)

lemmas rev_bind = iag.bind[rotated]

lemma read[iag.intro]:
  shows "prog.p2s (prog.read F) ≤ ⦃λs. Q (F s) s⦄, ceilr (λs. Q (F s) s) ∩ (⋂s. ceilr (Q (F s))) ⊢ G, ⦃Q⦄"
by (rule ag.pre[OF ag.prog.action[where P="λs. Q (F s) s"
                                    and Q=Q
                                    and A="ceilr (λs. Q (F s) s) ∩ (⋂s. ceilr (Q (F s)))"
                                    and G=G]];
    fastforce intro: stable.intro stable.Inter_ceilr stable.infI)

lemma return[iag.intro]:
  shows "prog.p2s (prog.return v) ≤ ⦃Q v⦄, ceilr (Q v) ⊢ G, ⦃Q⦄"
unfolding prog.return_alt_def by (rule iag.init[OF iag.read]; fastforce)

lemma "write"[iag.intro]: ―‹ this is where ∗‹guarantee› obligations arise ›
  shows "prog.p2s (prog.write F)
      ≤ ⦃(λs. Q () (F s) ∧ (s, F s) ∈ G)⦄, ceilr (λs. Q () (F s) ∧ (s, F s) ∈ G) ∩ ceilr (Q ()) ⊢ G, ⦃Q⦄"
by (rule ag.prog.action; fastforce intro: stable.intro stable.Inter_ceilr stable.infI1 stable.infI2)

lemma parallel: ―‹ not in the ‹iag› format; instantiate the first two assumptions ›
  assumes "prog.p2s c⇩₁ ≤ ⦃P⇩₁⦄, A⇩₁ ⊢ G⇩₁, ⦃Q⇩₁⦄"
  assumes "prog.p2s c⇩₂ ≤ ⦃P⇩₂⦄, A⇩₂ ⊢ G⇩₂, ⦃Q⇩₂⦄"
  assumes "⋀s. ⟦Q⇩₁ () s; Q⇩₂ () s⟧ ⟹ Q () s"
  assumes "G⇩₂ ⊆ A⇩₁"
  assumes "G⇩₁ ⊆ A⇩₂"
  assumes "G⇩₁ ∪ G⇩₂ ⊆ G"
  shows "prog.p2s (prog.parallel c⇩₁ c⇩₂) ≤ ⦃P⇩₁ ❙∧ P⇩₂⦄, A⇩₁ ∩ A⇩₂ ⊢ G, ⦃Q⦄"
by (rule order.trans[OF ag.prog.parallel[OF iag.pre_a[OF assms(1)] iag.pre_a[OF assms(2)],
                                         where A="A⇩₁ ∩ A⇩₂", simplified, OF ‹G⇩₂ ⊆ A⇩₁› ‹G⇩₁ ⊆ A⇩₂›]];
    use assms(3,6) in ‹force intro: iag.mono›)

lemmas local = ag.prog.local ―‹ not in the ‹iag› format ›

lemma "if"[iag.intro]:
  assumes "b ⟹ prog.p2s c⇩₁ ≤ ⦃P⇩₁⦄, A⇩₁ ⊢ G, ⦃Q⦄"
  assumes "¬b ⟹ prog.p2s c⇩₂ ≤ ⦃P⇩₂⦄, A⇩₂ ⊢ G, ⦃Q⦄"
  shows "prog.p2s (if b then c⇩₁ else c⇩₂) ≤ ⦃if b then P⇩₁ else P⇩₂⦄, A⇩₁ ∩ A⇩₂ ⊢ G, ⦃Q⦄"
using assms by (fastforce intro: ag.pre_ag)

lemma case_option[iag.intro]:
  assumes "x = None ⟹ prog.p2s none ≤ ⦃P⇩_n⦄, A⇩_n ⊢ G, ⦃Q⦄"
  assumes "⋀v. x = Some v ⟹ prog.p2s (some v) ≤ ⦃P⇩_s v⦄, A⇩_s v ⊢ G, ⦃Q⦄"
  shows "prog.p2s (case_option none some x) ≤ ⦃case x of None ⇒ P⇩_n | Some v ⇒ P⇩_s v⦄, case_option A⇩_n A⇩_s x ⊢ G, ⦃Q⦄"
using assms by (fastforce intro: ag.pre_ag split: option.split)

lemma case_sum[iag.intro]:
  assumes "⋀v. x = Inl v ⟹ prog.p2s (left v) ≤ ⦃P⇩_l v⦄, A⇩_l v ⊢ G, ⦃Q⦄"
  assumes "⋀v. x = Inr v ⟹ prog.p2s (right v) ≤ ⦃P⇩_r v⦄, A⇩_r v ⊢ G, ⦃Q⦄"
  shows "prog.p2s (case_sum left right x) ≤ ⦃case_sum P⇩_l P⇩_r x⦄, case_sum A⇩_l A⇩_r x ⊢ G, ⦃Q⦄"
using assms by (fastforce intro: ag.pre_ag split: sum.split)

lemma case_list[iag.intro]:
  assumes "x = [] ⟹ prog.p2s nil ≤ ⦃P⇩_n⦄, A⇩_n ⊢ G, ⦃Q⦄"
  assumes "⋀v vs. x = v # vs ⟹ prog.p2s (cons v vs) ≤ ⦃P⇩_c v vs⦄, A⇩_c v vs ⊢ G, ⦃Q⦄"
  shows "prog.p2s (case_list nil cons x) ≤ ⦃case_list P⇩_n P⇩_c x⦄, case_list A⇩_n A⇩_c x ⊢ G, ⦃Q⦄"
using assms by (fastforce intro: ag.pre_ag split: list.split)

lemma while:
  fixes c :: "'k ⇒ ('s, 'k + 'v) prog"
  assumes c: "⋀k. prog.p2s (c k) ≤ ⦃P k⦄, A ⊢ G, ⦃case_sum I Q⦄"
  shows "prog.p2s (prog.while c k) ≤ ⦃⟨∀v s. I v s ⟶ P v s⟩ ❙∧ I k⦄, A ∩ (⋂v. ceilr (Q v)) ⊢ G, ⦃Q⦄"
by (rule iag.gen_asm)
   (rule ag.prog.while[OF ag.pre_a[OF c]]; blast intro: stable.Inter_ceilr stable.infI2)

lemmas whenM = iag.if[where c⇩₁=c and A⇩₁=A and P⇩₁=P, OF _ iag.return[where v="()"]] for A c P

setup ‹Sign.parent_path›


subsection‹ Refinement with relational assumes\label{sec:ag-rar} ›

text‹

Two sets of refinement rules:
 ▪ relational assumes
 ▪ relational assumes and ‹prog.sinvmap› (inverse state abstraction)

›

setup ‹Sign.mandatory_path "rar.prog"›

lemma bind:
  assumes "⋀v. prog.p2s (g v) ≤ ⦃Q' v⦄, ag.assm A ⊩ prog.p2s (g' v), ⦃Q⦄"
  assumes "prog.p2s f ≤ ⦃P⦄, ag.assm A ⊩ prog.p2s f', ⦃Q'⦄"
  shows "prog.p2s (f ⤜ g) ≤ ⦃P⦄, ag.assm A ⊩ prog.p2s (f' ⤜ g'), ⦃Q⦄"
by (rule refinement.prog.bind[OF refinement.pre_a[OF assms(1) refinement.spec.bind.res.rel_le[OF order.refl]]])
   (simp add: spec.term.all.rel assms(2))

lemmas rev_bind = rar.prog.bind[rotated]

lemma action:
  fixes F :: "('v × 's × 's) set"
  fixes F' :: "('v × 's × 's) set"
  assumes Q: "⋀v s s'. ⟦P s; (v, s, s') ∈ F⟧ ⟹ Q v s'"
  assumes F': "⋀v s s'. ⟦P s; (v, s, s') ∈ F⟧ ⟹ (v, s, s') ∈ F'"
  assumes sP: "stable A P"
  assumes sQ: "⋀v s s'. ⟦P s; (v, s, s') ∈ F⟧ ⟹ stable A (Q v)"
  shows "prog.p2s (prog.action F) ≤ ⦃P⦄, ag.assm A ⊩ prog.p2s (prog.action F'), ⦃Q⦄"
by (rule refinement.prog.action)
   (use assms in ‹simp_all add: spec.steps.rel stable_def monotone_def›)

lemma return:
  assumes sQ: "stable A (Q v)"
  shows "prog.p2s (prog.return v) ≤ ⦃Q v⦄, ag.assm A ⊩ prog.p2s (prog.return v), ⦃Q⦄"
using assms by (simp add: refinement.prog.return spec.steps.rel stable_def monotone_def)

lemma parallel_refinement:
  assumes c⇩₁: "prog.p2s c⇩₁ ≤ ⦃P⇩₁⦄, ag.assm (A ∪ G⇩₂) ⊩ prog.p2s (c⇩₁' ⊓ prog.rel G⇩₁), ⦃Q⇩₁⦄"
  assumes c⇩₂: "prog.p2s c⇩₂ ≤ ⦃P⇩₂⦄, ag.assm (A ∪ G⇩₁) ⊩ prog.p2s (c⇩₂' ⊓ prog.rel G⇩₂), ⦃Q⇩₂⦄"
  shows "prog.p2s (c⇩₁ ∥ c⇩₂) ≤ ⦃P⇩₁ ❙∧ P⇩₂⦄, ag.assm A ⊩ prog.p2s (c⇩₁' ⊓ prog.rel G⇩₁ ∥ c⇩₂' ⊓ prog.rel G⇩₂), ⦃λv. Q⇩₁ v ❙∧ Q⇩₂ v⦄"
apply (rule refinement.prog.parallel[OF refinement.pre_a[OF c⇩₁] refinement.pre_a[OF c⇩₂]])
 apply (rule order.trans[OF refinement.spec.env_hyp.mono[OF order.refl] ag.spec.Parallel_assm[where a=True and as=UNIV and G="λa. if a then G⇩₁ else G⇩₂", simplified]];
        simp add: ac_simps prog.p2s.simps; fail)
apply (rule order.trans[OF refinement.spec.env_hyp.mono[OF order.refl] ag.spec.Parallel_assm[where a=False and as=UNIV and G="λa. if a then G⇩₁ else G⇩₂", simplified]];
       simp add: ac_simps prog.p2s.simps; fail)
done

lemma parallel:
  assumes "prog.p2s c⇩₁ ≤ ⦃P⇩₁⦄, ag.assm (A ∪ G⇩₂) ⊩ prog.p2s c⇩₁', ⦃Q⇩₁⦄"
  assumes "prog.p2s c⇩₁ ≤ ⦃P⇩₁⦄, A ∪ G⇩₂ ⊢ G⇩₁, ⦃⊤⦄"
  assumes "prog.p2s c⇩₂ ≤ ⦃P⇩₂⦄, ag.assm (A ∪ G⇩₁) ⊩ prog.p2s c⇩₂', ⦃Q⇩₂⦄"
  assumes "prog.p2s c⇩₂ ≤ ⦃P⇩₂⦄, A ∪ G⇩₁ ⊢ G⇩₂, ⦃⊤⦄"
  shows "prog.p2s (c⇩₁ ∥ c⇩₂) ≤ ⦃P⇩₁ ❙∧ P⇩₂⦄, ag.assm A ⊩ prog.p2s (c⇩₁' ∥ c⇩₂'), ⦃λv. Q⇩₁ v ❙∧ Q⇩₂ v⦄"
by (rule order.trans[OF rar.prog.parallel_refinement
                        refinement.mono[OF order.refl order.refl prog.p2s.mono[OF prog.parallel.mono[OF inf.cobounded1 inf.cobounded1]] order.refl]])
   (force simp: prog.p2s.simps refinement.infR_conv[where Q⇩₂=⊤, simplified]
         simp flip: ag.refinement
             intro: assms)+

lemma while:
  fixes c :: "'k ⇒ ('s, 'k + 'v) prog"
  fixes c' :: "'k ⇒ ('s, 'k + 'v) prog"
  assumes c: "⋀k. prog.p2s (c k) ≤ ⦃P k⦄, ag.assm A ⊩ prog.p2s (c' k), ⦃case_sum I Q⦄"
  assumes IP: "⋀s v. I v s ⟹ P v s"
  assumes sQ: "⋀v. stable A (Q v)"
  shows "prog.p2s (prog.while c k) ≤ ⦃I k⦄, ag.assm A ⊩ prog.p2s (prog.while c' k), ⦃Q⦄"
proof -
  have "∀k. prog.p2s (prog.while c k) ≤ ⦃P k⦄, ag.assm A ⊩ prog.p2s (prog.while c' k), ⦃Q⦄"
  proof(induct rule: prog.while.fixp_induct[where P="λR. ∀k. prog.p2s (R c k) ≤ ⦃P k⦄, ag.assm A ⊩ prog.p2s (prog.while c' k), ⦃Q⦄", case_names adm bot step])
    case (step R) from sQ show ?case
      apply (subst prog.while.simps)
      apply (intro allI rar.prog.rev_bind[OF c]
                   refinement.pre_pre[OF refinement.prog.case_sum[OF step[rule_format]
                                                                     rar.prog.return[OF sQ]]])
      apply (simp add: IP split: sum.splits)
      done
  qed simp_all
  then show ?thesis
    by (meson IP refinement.pre_pre)
qed

lemma app:
  fixes xs :: "'a list"
  fixes f :: "'a ⇒ ('s, unit) prog"
  fixes P :: "'a list ⇒ 's pred"
  assumes "⋀x ys zs. xs = ys @ x # zs ⟹ prog.p2s (f x) ≤ ⦃P ys⦄, ag.assm A ⊩ prog.p2s (f' x), ⦃λ_. P (ys @ [x])⦄"
  assumes "⋀ys. prefix ys xs ⟹ stable A (P ys)"
  shows "prog.p2s (prog.app f xs) ≤ ⦃P []⦄, ag.assm A ⊩ prog.p2s (prog.app f' xs), ⦃λ_. P xs⦄"
using assms
by (induct xs rule: rev_induct;
    force intro: rar.prog.return
           simp: prog.app.append prog.app.simps spec.steps.rel prog.bind.return rar.prog.rev_bind)

lemmas "if" = refinement.prog.if[where A="ag.assm A" for A]
lemmas case_option = refinement.prog.case_option[where A="ag.assm A" for A]

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "rair.prog"›

abbreviation (input) "absfn sf c ≡ prog.p2s (prog.sinvmap sf c)"

lemma bind:
  assumes "⋀v. prog.p2s (g v) ≤ ⦃Q' v⦄, ag.assm A ⊩ rair.prog.absfn sf (g' v), ⦃Q⦄"
  assumes "prog.p2s f ≤ ⦃P⦄, ag.assm A ⊩ rair.prog.absfn sf f', ⦃Q'⦄"
  shows "prog.p2s (f ⤜ g) ≤ ⦃P⦄, ag.assm A ⊩ rair.prog.absfn sf (f' ⤜ g'), ⦃Q⦄"
by (simp add: prog.invmap.bind rar.prog.bind[OF assms])

lemmas rev_bind = rair.prog.bind[rotated]

lemma action:
  fixes F :: "('v × 's × 's) set"
  fixes F' :: "('v × 't × 't) set"
  fixes sf :: "'s ⇒ 't"
  assumes Q: "⋀v s s'. ⟦P s; (v, s, s') ∈ F⟧ ⟹ Q v s'"
  assumes F': "⋀v s s'. ⟦P s; (v, s, s') ∈ F⟧ ⟹ (v, sf s, sf s') ∈ F'"
  assumes sP: "stable A P"
  assumes sQ: "⋀v s s'. ⟦P s; (v, s, s') ∈ F⟧ ⟹ stable A (Q v)"
  shows "prog.p2s (prog.action F) ≤ ⦃P⦄, ag.assm A ⊩ rair.prog.absfn sf (prog.action F'), ⦃Q⦄"
by (strengthen ord_to_strengthen(2)[OF prog.action.invmap_le])
   (simp add: rar.prog.action assms)

lemma return:
  assumes sQ: "stable A (Q v)"
  shows "prog.p2s (prog.return v) ≤ ⦃Q v⦄, ag.assm A ⊩ rair.prog.absfn sf (prog.return v), ⦃Q⦄"
using assms by (simp add: refinement.prog.invmap_return spec.steps.rel stable_def monotone_def)

lemma parallel:
  fixes sf :: "'s ⇒ 't"
  assumes "prog.p2s c⇩₁ ≤ ⦃P⇩₁⦄, ag.assm (A ∪ G⇩₂) ⊩ rair.prog.absfn sf c⇩₁', ⦃Q⇩₁⦄"
  assumes "prog.p2s c⇩₁ ≤ ⦃P⇩₁⦄, A ∪ G⇩₂ ⊢ G⇩₁, ⦃⊤⦄"
  assumes "prog.p2s c⇩₂ ≤ ⦃P⇩₂⦄, ag.assm (A ∪ G⇩₁) ⊩ rair.prog.absfn sf c⇩₂', ⦃Q⇩₂⦄"
  assumes "prog.p2s c⇩₂ ≤ ⦃P⇩₂⦄, A ∪ G⇩₁ ⊢ G⇩₂, ⦃⊤⦄"
  shows "prog.p2s (c⇩₁ ∥ c⇩₂) ≤ ⦃P⇩₁ ❙∧ P⇩₂⦄, ag.assm A ⊩ rair.prog.absfn sf (c⇩₁' ∥ c⇩₂'), ⦃λv. Q⇩₁ v ❙∧ Q⇩₂ v⦄"
unfolding prog.invmap.parallel by (rule rar.prog.parallel[OF assms])

lemma while:
  fixes c :: "'k ⇒ ('s, 'k + 'v) prog"
  fixes c' :: "'k ⇒ ('t, 'k + 'v) prog"
  fixes sf :: "'s ⇒ 't"
  assumes c: "⋀k. prog.p2s (c k) ≤ ⦃P k⦄, ag.assm A ⊩ rair.prog.absfn sf (c' k), ⦃case_sum I Q⦄"
  assumes IP: "⋀s v. I v s ⟹ P v s"
  assumes sQ: "⋀v. stable A (Q v)"
  shows "prog.p2s (prog.while c k) ≤ ⦃I k⦄, ag.assm A ⊩ rair.prog.absfn sf (prog.while c' k), ⦃Q⦄"
by (strengthen ord_to_strengthen(2)[OF prog.while.invmap_le])
   (simp add: assms map_sum.id rar.prog.while[OF c])

lemma app:
  fixes xs :: "'a list"
  fixes f :: "'a ⇒ ('s, unit) prog"
  fixes P :: "'a list ⇒ 's pred"
  assumes "⋀x ys zs. xs = ys @ x # zs ⟹ prog.p2s (f x) ≤ ⦃P ys⦄, ag.assm A ⊩ rair.prog.absfn sf (f' x), ⦃λ_. P (ys @ [x])⦄"
  assumes "⋀ys. prefix ys xs ⟹ stable A (P ys)"
  shows "prog.p2s (prog.app f xs) ≤ ⦃P []⦄, ag.assm A ⊩ rair.prog.absfn sf (prog.app f' xs), ⦃λ_. P xs⦄"
by (strengthen ord_to_strengthen(2)[OF prog.sinvmap.app_le])
   (simp add: rar.prog.app assms)

lemma "if":
  assumes "i ⟹ prog.p2s t ≤ ⦃P⦄, ag.assm A ⊩ rair.prog.absfn sf t', ⦃Q⦄"
  assumes "¬i ⟹ prog.p2s e ≤ ⦃P'⦄, ag.assm A ⊩ rair.prog.absfn sf e', ⦃Q⦄"
  shows "prog.p2s (if i then t else e) ≤ ⦃if i then P else P'⦄, ag.assm A ⊩ rair.prog.absfn sf (if i then t' else e'), ⦃Q⦄"
using assms by fastforce

lemma case_option:
  assumes "opt = None ⟹ prog.p2s none ≤ ⦃P⇩_n⦄, ag.assm A ⊩ rair.prog.absfn sf none', ⦃Q⦄"
  assumes "⋀v. opt = Some v ⟹ prog.p2s (some v) ≤ ⦃P⇩_s v⦄, ag.assm A ⊩ rair.prog.absfn sf (some' v), ⦃Q⦄"
  shows "prog.p2s (case_option none some opt) ≤ ⦃case opt of None ⇒ P⇩_n | Some v ⇒ P⇩_s v⦄, ag.assm A ⊩ rair.prog.absfn sf (case_option none' some' opt), ⦃Q⦄"
using assms by (simp add: option.case_eq_if)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›
(*<*)

end
(*>*)