Theory Next_Imp

(*<*)
theory Next_Imp
imports
  Safety_Logic
begin

(*>*)
section‹ ``Next step'' implication ala Abadi and Merz (and Lamport)\label{sec:abadi_merz} ›

text‹

As was apparently well-known in the mid-1990s (see, e.g.,
\<^citet>‹‹\S4› in "XuCauCollette:1994"› and
the references therein), Heyting implication is inadequate for a
general refinement story. (We show it is strong enough for a
relational assume/guarantee program logic; see
\S\ref{sec:abadi_plotkin}, \S\ref{sec:refinement-ag} and
\S\ref{sec:abadi_plotkin-parallel}. In our setting it fails to
generalize (at least) because the composition theorem for Heyting
implication (\S\ref{sec:abadi_plotkin}) is not termination sensitive.)

We therefore follow \<^citet>‹"AbadiLamport:1995"› by developing a stronger implication
‹P ❙⟶⇩+ Q› with the intuitive semantics that the consequent ‹Q› holds for at least one
step beyond the antecedent ‹P›. This is some kind of step indexing.

Here we sketch the relevant parts of \<^citet>‹"AbadiMerz:1995"
and "AbadiMerz:1996"›, the latter of which has a fuller story,
including a formal account of the logical core of TLA and the
(implicit) observation that infinitary parallel composition poses no
problem for safety properties (see the comments under Theorem~5.2 and \S5.5).
\<^citet>‹"AbadiLamport:1995" and "XuCauCollette:1994" and
"CauCollette:1996"› provide further background;
\<^citet>‹‹Appendix~B› in
"JonssonTsay:1996"› provide a more syntactic account.

Observations:
 ▪ The hypothesis ‹P› is always a safety property here
 ▪ TLA does not label transitions or have termination markers
 ▪ Abadi/Cau/Collette/Lamport/Merz/Xu/... avoid naming this operator

Further references:
 ▪ \<^citet>‹"Maier:2001"›

›

definition "next_imp" :: "'a::preorder set ⇒ 'a set ⇒ 'a set" where ―‹ \<^citet>‹‹\S2› in "AbadiMerz:1995"› ›
  "next_imp P Q = {σ. ∀σ'≤σ. (∀σ''<σ'. σ'' ∈ P) ⟶ σ' ∈ Q}"

setup ‹Sign.mandatory_path "next_imp"›

lemma downwards_closed:
  assumes "P ∈ downwards.closed"
  shows "next_imp P Q ∈ downwards.closed"
unfolding next_imp_def by (blast elim: downwards.clE intro: order_trans)

lemma mono:
  assumes "x' ≤ x"
  assumes "y ≤ y'"
  shows "next_imp x y ≤ next_imp x' y'"
unfolding next_imp_def using assms by fast

lemma strengthen[strg]:
  assumes "st_ord (¬ F) X X'"
  assumes "st_ord F Y Y'"
  shows "st_ord F (next_imp X Y) (next_imp X' Y')"
using assms by (cases F) (auto simp: next_imp.mono)

lemma minimal:
  assumes "trace.T s xs v ∈ next_imp P Q"
  shows "trace.T s [] None ∈ Q"
using assms by (simp add: next_imp_def trace.less trace.less_eq_None)

lemma alt_def: ―‹ This definition coincides with \<^citet>‹"CauCollette:1996"›, \<^citet>‹‹\S3.5.3› in "AbadiLamport:1995"› ›
  assumes "P ∈ downwards.closed"
  shows "next_imp P Q
      = {σ. trace.T (trace.init σ) [] None ∈ Q
          ∧ (∀i. trace.take i σ ∈ P ⟶ trace.take (Suc i) σ ∈ Q)}" (is "?lhs = ?rhs")
proof(rule antisym)
  have "trace.take (Suc i) (trace.T s xs v) ∈ Q"
    if "trace.T s xs v ∈ ?lhs" and "trace.take i (trace.T s xs v) ∈ P"
   for s xs v i
    using that ‹P ∈ downwards.closed›
    by (force simp: next_imp_def trace.less_take_less_eq
              dest: spec[where x="trace.take (Suc i) (trace.T s xs v)"]
              elim: downwards.closed_in)
  then show "?lhs ⊆ ?rhs"
    by (clarsimp simp: trace.split_all next_imp.minimal)
next
  have "trace.T s xs v ∈ ?lhs"
    if minimal: "trace.T s [] None ∈ Q"
   and imp: "∀i. trace.take i (trace.T s xs v) ∈ P ⟶ trace.take (Suc i) (trace.T s xs v) ∈ Q"
   for s xs v
  proof -
    have "trace.take i (trace.T s xs v) ∈ Q"
      if "∀σ''<trace.take i (trace.T s xs v). σ'' ∈ P"
     for i
      using that
    proof(induct i)
      case (Suc i) with imp show ?case
        by (metis le_add2 order_le_less plus_1_eq_Suc trace.take.mono)
    qed (simp add: minimal)
    then show "trace.T s xs v ∈ ?lhs"
      by (clarsimp simp: next_imp_def trace.less_eq_take_def)
  qed
  then show "?rhs ⊆ ?lhs"
    by (clarsimp simp: trace.split_all next_imp.minimal)
qed

text‹

\<^citet>‹‹\S3.5.3› in "AbadiLamport:1995"› assert but do not prove the following connection with
Heyting implication. \<^citet>‹"AbadiMerz:1995"› do. See also
\<^citet>‹‹\S5.3 and \S5.5› in "AbadiMerz:1996"›.

›

lemma Abadi_Merz_Prop_1_subseteq: ―‹ First half of \<^citet>‹‹Proposition~1› in "AbadiMerz:1995"› ›
  fixes P :: "'a::preorder set"
  assumes "P ∈ downwards.closed"
  assumes wf: "wfP ((<) :: 'a relp)"
  shows "next_imp P Q ⊆ downwards.imp (downwards.imp Q P) Q" (is "?lhs ⊆ ?rhs")
proof(rule subsetI)
  fix σ assume "σ ∈ ?lhs" with wf show "σ ∈ ?rhs"
  proof(induct rule: wfp_induct_rule)
    case (less σ)
    have "τ ∈ Q" if "τ ≤ σ" and YYY: "∀σ'≤τ. σ' ∈ Q ⟶ σ' ∈ P" for τ
    proof -
      have "ρ ∈ P" if "ρ < τ" for ρ
      proof -
        from ‹ρ < τ› ‹τ ≤ σ› ‹P ∈ downwards.closed› have "ρ ∈ next_imp P Q"
          by (meson downwards.closed_in next_imp.downwards_closed less.prems less_imp_le)
        with ‹ρ < τ› ‹τ ≤ σ› have "ρ ∈ downwards.imp (downwards.imp Q P) Q"
          using less.hyps less_le_trans by blast
        moreover from ‹ρ < τ›  YYY have "ρ ∈ downwards.imp Q P"
          by (simp add: downwards.imp_def) (meson order.trans order_less_imp_le)
        ultimately show ?thesis by (meson downwards.imp_mp')
      qed
      with that less.prems show ?thesis
        unfolding next_imp_def by blast
    qed
    then show ?case
      unfolding downwards.imp_def by blast
  qed
qed

text‹

The converse holds if either ‹Q› is a safety property or the order is partial.

›

lemma Abadi_Merz_Prop1: ―‹ \<^citet>‹‹Proposition~1› in "AbadiMerz:1995"› and \<^citet>‹‹Proposition~5.2› in "AbadiMerz:1996"› ›
  fixes P :: "'a::preorder set"
  assumes "P ∈ downwards.closed"
  assumes "Q ∈ downwards.closed"
  assumes wf: "wfP ((<) :: 'a relp)"
  shows "next_imp P Q = downwards.imp (downwards.imp Q P) Q" (is "?lhs = ?rhs")
proof(rule antisym[OF next_imp.Abadi_Merz_Prop_1_subseteq[OF assms(1,3)]])
  from ‹Q ∈ downwards.closed› show "?rhs ⊆ ?lhs"
    by (auto simp: next_imp_def downwards.imp_def order.strict_iff_not dest: downwards.closed_in)
qed

lemma Abadi_Lamport_Lemma6: ―‹ \<^citet>‹‹Lemma~6› in "AbadiLamport:1995"› (no proof given there) ›
  fixes P :: "'a::order set"
  assumes "P ∈ downwards.closed"
  assumes wf: "wfP ((<) :: 'a relp)"
  shows "next_imp P Q = downwards.imp (downwards.imp Q P) Q" (is "?lhs = ?rhs")
proof(rule Set.equalityI[OF next_imp.Abadi_Merz_Prop_1_subseteq[OF assms]])
  show "?rhs ⊆ ?lhs"
    unfolding next_imp_def downwards.imp_def by (fastforce simp: le_less elim: downwards.closed_in)
qed

lemmas downwards_imp = next_imp.Abadi_Lamport_Lemma6[OF _ trace.wfP_less]

lemma boolean_implication_le:
  assumes "P ∈ downwards.closed"
  shows "next_imp P Q ⊆ P ❙⟶⇩B Q"
using downwards.closed_conv[OF assms]
by (fastforce simp: next_imp_def boolean_implication.member
             intro: order_less_imp_le)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "spec"›

lift_definition "next_imp" :: "('a, 's, 'v) spec ⇒ ('a, 's, 'v) spec ⇒ ('a, 's, 'v) spec" (infixr ‹❙⟶⇩+› 61) is
  "Next_Imp.next_imp"
by (simp add: next_imp.downwards_imp raw.spec.closed.downwards_closed raw.spec.closed.downwards_imp)

setup ‹Sign.mandatory_path "next_imp"›

lemma heyting: ―‹ fundamental ›
  shows "P ❙⟶⇩+ Q = (Q ❙⟶⇩H P) ❙⟶⇩H Q"
by transfer (simp add: next_imp.downwards_imp raw.spec.closed.downwards_closed)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "singleton"›

lemma next_imp_le_conv:
  fixes P :: "('a, 's, 'v) spec"
  shows "⦉σ⦊ ≤ P ❙⟶⇩+ Q ⟷ (∀σ'≤σ. (∀σ''<σ'. ⦉σ''⦊ ≤ P) ⟶ ⦉σ'⦊ ≤ Q)" (is "?lhs ⟷ ?rhs")
proof(rule iffI)
  show "?lhs ⟹ ?rhs"
    by (force simp: spec.next_imp.heyting spec.singleton.heyting_le_conv)
  note spec.singleton.transfer[transfer_rule]
  show "?rhs ⟹ ?lhs"
  proof(transfer, unfold raw.singleton_def, rule raw.spec.least)
    show "{σ} ⊆ next_imp P Q"
      if "P ∈ raw.spec.closed"
     and "∀σ'≤σ. (∀σ''<σ'. raw.spec.cl {σ''} ⊆ P) ⟶ raw.spec.cl {σ'} ⊆ Q"
     for P Q :: "('a, 's, 'v) trace.t set" and σ
      using that by (auto simp: next_imp_def raw.spec.least_conv
                          dest: order.trans[OF raw.spec.expansive])
    show "next_imp P Q ∈ raw.spec.closed"
      if "P ∈ raw.spec.closed"
     and "Q ∈ raw.spec.closed"
     for P Q :: "('a, 's, 'v) trace.t set"
      using that
      by (simp add: next_imp.downwards_imp raw.spec.closed.downwards_closed raw.spec.closed.downwards_imp)
  qed
qed

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "next_imp"›

lemma mono:
  assumes "x' ≤ x"
  assumes "y ≤ y'"
  shows "x ❙⟶⇩+ y ≤ x' ❙⟶⇩+ y'"
by (simp add: assms heyting.mono spec.next_imp.heyting)

lemma strengthen[strg]:
  assumes "st_ord (¬ F) X X'"
  assumes "st_ord F Y Y'"
  shows "st_ord F (X ❙⟶⇩+ Y) (X' ❙⟶⇩+ Y')"
using assms by (cases F) (auto simp: spec.next_imp.mono)

lemma idempotentR:
  shows "P ❙⟶⇩+ (P ❙⟶⇩+ Q) = P ❙⟶⇩+ Q"
by (simp add: spec.next_imp.heyting heyting heyting.detachment(1) heyting.discharge(2) inf.absorb2
        flip: heyting.curry_conv)

lemma contains:
  assumes "X ≤ Q"
  shows "X ≤ P ❙⟶⇩+ Q"
by (simp add: assms spec.next_imp.heyting heyting.curry le_infI1)

interpretation closure: closure_complete_lattice_class "(❙⟶⇩+) P" for P
by standard
   (metis (no_types, lifting) order.refl order.trans
                              spec.next_imp.idempotentR spec.next_imp.contains spec.next_imp.mono)

lemma InfR:
  shows "x ❙⟶⇩+ ⨅X = ⨅ ((❙⟶⇩+) x ` X)"
by transfer (auto simp: next_imp_def)

lemma SupR_not_empty:
  fixes P :: "(_, _, _) spec"
  assumes "X ≠ {}"
  shows "P ❙⟶⇩+ (⨆x∈X. Q x) = (⨆x∈X. P ❙⟶⇩+ Q x)" (is "?lhs = ?rhs")
proof(rule antisym[OF spec.singleton_le_extI
                      spec.next_imp.closure.Sup_cl_le[where X="Q ` X", simplified image_image]])
  show "⦉σ⦊ ≤ ?rhs" if "⦉σ⦊ ≤ ?lhs" for σ
  proof(cases "⦉σ⦊ ≤ P")
    case True with ‹⦉σ⦊ ≤ ?lhs› show ?thesis
      by (fastforce simp: spec.singleton.next_imp_le_conv
                   intro: order.trans[OF spec.singleton.mono]
                   elim!: order_less_imp_le
                    dest: spec[where x=σ])
  next
    case False show ?thesis
    proof(cases "⦉trace.init σ, [], None⦊ ≤ P")
      case True with ‹¬ ⦉σ⦊ ≤ P›
      obtain j where *: "∀σ''<trace.take (Suc j) σ. ⦉σ''⦊ ≤ P"
                 and **: "¬ ⦉trace.take (Suc j) σ⦊ ≤ P"
        using ex_least_nat_less[where P="λi. ¬⦉trace.take i σ⦊ ≤ P" and n="Suc (length (trace.rest σ))"]
        by (force dest: trace.less_take_less_eq
                  simp: less_Suc_eq_le order.trans[OF spec.singleton.mono]
             simp flip: trace.take.Ex_all)
      from ‹⦉σ⦊ ≤ ?lhs› ** show ?thesis
      by (clarsimp simp: spec.singleton.next_imp_le_conv
                  dest!: spec[where x="trace.take (Suc j) σ"] rev_mp[OF *]
                  elim!: rev_bexI)
          (meson order.trans less_le_not_le spec.singleton.mono trace.less_eq_same_cases trace.less_eq_take)
    next
      case False with ‹X ≠ {}› ‹⦉σ⦊ ≤ ?lhs› show ?thesis
        by (clarsimp simp: spec.singleton.next_imp_le_conv simp flip: ex_in_conv)
           (metis "trace.take.0" trace.less_eq_take_def trace.less_t_def trace.take.sel(1))
    qed
  qed
qed

lemma cont:
  shows "cont Sup (≤) Sup (≤) ((❙⟶⇩+) P)"
by (rule contI) (simp add: spec.next_imp.SupR_not_empty[where Q=id, simplified])

lemma mcont:
  shows "mcont Sup (≤) Sup (≤) ((❙⟶⇩+) P)"
by (simp add: monotoneI mcontI[OF _ spec.next_imp.cont])

lemmas mcont2mcont[cont_intro] = mcont2mcont[OF spec.next_imp.mcont, of luba orda Q P] for luba orda Q P

lemma botL:
  assumes "spec.idle ≤ P"
  shows "⊥ ❙⟶⇩+ P = ⊤"
by (simp add: assms spec.next_imp.heyting spec.eq_iff Heyting.heyting spec.heyting.non_triv)

lemma topL[simp]:
  shows "⊤ ❙⟶⇩+ P = P"
by (simp add: spec.next_imp.heyting)

lemmas topR[simp] = spec.next_imp.closure.cl_top

lemma refl:
  shows "P ❙⟶⇩+ P ≤ P"
by (simp add: spec.next_imp.heyting)

lemma heyting_le:
  shows "P ❙⟶⇩+ Q ≤ P ❙⟶⇩H Q"
by (simp add: spec.next_imp.heyting heyting.discard heyting.mono)

lemma discharge:
  shows "P ⊓ (P ⊓ Q ❙⟶⇩+ R) = P ⊓ (Q ❙⟶⇩+ R)" (is "?thesis1 P Q")
    and "(P ⊓ Q ❙⟶⇩+ R) ⊓ P = P ⊓ (Q ❙⟶⇩+ R)" (is ?thesis2)
    and "Q ⊓ (P ⊓ Q ❙⟶⇩+ R) = Q ⊓ (P ❙⟶⇩+ R)" (is ?thesis3)
    and "(P ⊓ Q ❙⟶⇩+ R) ⊓ Q = Q ⊓ (P ❙⟶⇩+ R)" (is ?thesis4)
proof -
  show "?thesis1 P Q" for P Q
    by (simp add: spec.next_imp.heyting heyting.infR heyting.curry_conv heyting.discard heyting.discharge)
  then show ?thesis2 by (rule inf_commute_conv)
  from ‹?thesis1 Q P› show ?thesis3 by (simp add: ac_simps)
  then show ?thesis4 by (rule inf_commute_conv)
qed

lemma detachment:
  shows "x ⊓ (x ❙⟶⇩+ y) ≤ y"
    and "(x ❙⟶⇩+ y) ⊓ x ≤ y"
by (simp_all add: spec.next_imp.heyting heyting.discard heyting.discharge)

lemma infR:
  shows "P ❙⟶⇩+ Q ⊓ R = (P ❙⟶⇩+ Q) ⊓ (P ❙⟶⇩+ R)"
by (rule antisym[OF spec.next_imp.closure.cl_inf_le])
   (rule spec.singleton_le_extI; clarsimp simp: spec.singleton.next_imp_le_conv)

lemma supL_le:
  shows "x ⊔ y ❙⟶⇩+ z ≤ (x ❙⟶⇩+ z) ⊔ (y ❙⟶⇩+ z)"
by (simp add: le_supI1 spec.next_imp.mono)

lemma heytingL:
  shows "(P ❙⟶⇩H Q) ⊓ (Q ❙⟶⇩+ R) ≤ P ❙⟶⇩+ R"
by (simp add: spec.next_imp.heyting heyting ac_simps)
   (simp add: heyting.rev_trans heyting.discharge flip: inf.assoc)

lemma heytingR:
  shows "(P ❙⟶⇩+ Q) ⊓ (Q ❙⟶⇩H R) ≤ P ❙⟶⇩+ R"
by (simp add: spec.next_imp.heyting heyting ac_simps)
   (simp add: heyting.discharge heyting.trans heyting.uncurry flip: inf.assoc)

lemma heytingL_distrib:
  shows "P ❙⟶⇩H (Q ❙⟶⇩+ R) = (P ⊓ Q) ❙⟶⇩+ (P ❙⟶⇩H R)"
by (metis (no_types, opaque_lifting) heyting.curry_conv heyting.detachment(2) heyting.infR
                                     heyting.refl heyting.swap inf_top_left spec.next_imp.heyting)

lemma trans:
  shows "(P ❙⟶⇩+ Q) ⊓ (Q ❙⟶⇩+ R) ≤ P ❙⟶⇩+ R"
by (meson order.trans Heyting.heyting spec.next_imp.heytingL spec.next_imp.heyting_le)

lemma rev_trans:
  shows "(Q ❙⟶⇩+ R) ⊓ (P ❙⟶⇩+ Q) ≤ P ❙⟶⇩+ R"
by (simp add: inf.commute spec.next_imp.trans)

lemma
  assumes "x' ≤ x"
  shows discharge_leL: "x' ⊓ (x ❙⟶⇩+ y) = x' ⊓ y" (is ?thesis1)
    and discharge_leR: "(x ❙⟶⇩+ y) ⊓ x' = y ⊓ x'" (is ?thesis2)
proof -
  from assms show ?thesis1
    by (metis inf.absorb_iff2 inf_top.right_neutral spec.next_imp.discharge(4) spec.next_imp.topL)
  then show ?thesis2 by (simp add: ac_simps)
qed

lemma invmap:
  shows "spec.invmap af sf vf (P ❙⟶⇩+ Q) = spec.invmap af sf vf P ❙⟶⇩+ spec.invmap af sf vf Q"
by (simp add: spec.next_imp.heyting spec.invmap.heyting)

lemma Abadi_Lamport_Lemma7:
  assumes "Q ⊓ R ≤ P"
  shows "P ❙⟶⇩+ Q ≤ R ❙⟶⇩+ Q"
by (simp add: assms spec.next_imp.heyting Heyting.heyting heyting.detachment(2) heyting.discharge(2))

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "term"›

setup ‹Sign.mandatory_path "none"›

lemma "next_imp":
  shows "spec.term.none (P ❙⟶⇩+ Q) ≤ spec.term.all P ❙⟶⇩+ spec.term.none Q"
by (simp add: spec.next_imp.heyting order.trans[OF spec.term.none.heyting_le] spec.term.all.heyting)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "all"›

lemma "next_imp":
  shows "spec.term.all (P ❙⟶⇩+ Q) = spec.term.all P ❙⟶⇩+ spec.term.all Q"
by (simp add: spec.next_imp.heyting)
   (metis spec.term.all.heyting spec.term.all_none spec.term.heyting_noneL_allR_mono spec.term.none_all)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "closed"›

lemma "next_imp":
  assumes "Q ∈ spec.term.closed _"
  shows "P ❙⟶⇩+ Q ∈ spec.term.closed _"
using assms
by (simp add: spec.next_imp.heyting spec.term.closed.heyting)

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "pre"›

lemma next_imp_eq_heyting:
  assumes "spec.idle ≤ R"
  shows "Q ⊓ spec.pre P ❙⟶⇩+ R = spec.pre P ❙⟶⇩H (Q ❙⟶⇩+ R)" (is "?lhs = ?rhs")
    and "spec.pre P ⊓ Q ❙⟶⇩+ R = spec.pre P ❙⟶⇩H (Q ❙⟶⇩+ R)" (is ?thesis1)
proof -
  show "?lhs = ?rhs"
  proof(rule antisym[OF _ spec.singleton_le_extI])
    show "?lhs ≤ ?rhs"
      by (simp add: heyting spec.next_imp.discharge)
    show "⦉σ⦊ ≤ ?lhs" if "⦉σ⦊ ≤ ?rhs" for σ
      using assms that
      by (clarsimp simp: spec.singleton.next_imp_le_conv spec.singleton.heyting_le_conv
                         spec.singleton.le_conv)
         (metis order.refl append_self_conv2 spec.singleton.idle_le_conv spec.singleton_le_ext_conv
                trace.less(1) trace.less_eqE trace.steps'.simps(1) trace.t.sel(1))
  qed
  then show ?thesis1
    by (simp add: ac_simps)
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›


subsection‹ Compositionality ala Abadi and Merz (and Lamport) \label{sec:abadi_merz-compositionality} ›

text‹

The main theorem for this implication (\<^citet>‹‹Theorem~4› in "AbadiMerz:1995"› and
\<^citet>‹‹Corollary~5.1› in "AbadiMerz:1996"›)
shows how to do assumption/commitment proofs for TLA considered as an
algebraic logic. See also \<^citet>‹"CauCollette:1996"›.

›

setup ‹Sign.mandatory_path "spec"›

lemma Abadi_Lamport_Lemma5:
  shows "(⨅i∈I. P i ❙⟶⇩+ Q i) ≤ (⨅i∈I. P i) ❙⟶⇩+ (⨅i∈I. Q i)"
by (simp add: spec.next_imp.InfR INF_lower INF_superset_mono image_image spec.next_imp.mono)

lemma Abadi_Merz_Prop2_1:
  shows "(P ❙⟶⇩+ Q) ⊓ (P ❙⟶⇩+ (Q ❙⟶⇩H R)) ≤ P ❙⟶⇩+ R"
by (metis heyting.detachment(1) inf_sup_ord(2) spec.next_imp.infR)

lemma Abadi_Merz_Theorem3_5:
  shows "P ❙⟶⇩H (Q ❙⟶⇩H R) ≤ (R ❙⟶⇩+ Q) ❙⟶⇩H (P ❙⟶⇩+ Q)"
by (simp add: heyting order.trans[OF spec.next_imp.heytingL] spec.next_imp.Abadi_Lamport_Lemma7
        flip: heyting.curry_conv)

theorem Abadi_Merz_Theorem4:
  shows "(A ⊓ (⨅i∈I. Cs i) ❙⟶⇩H (⨅i∈I. As i))
       ⊓ (A ❙⟶⇩+ ((⨅i∈I. Cs i) ❙⟶⇩H C))
       ⊓ (⨅i∈I. As i ❙⟶⇩+ Cs i)
        ≤ A ❙⟶⇩+ C" (is "?lhs ≤ ?rhs")
proof -
  have "?lhs ≤ A ❙⟶⇩H (⨅i∈I. Cs i) ❙⟶⇩H (⨅i∈I. As i)"
    by (simp add: heyting.curry_conv inf.coboundedI1)
  then have 2: "?lhs ≤ ((⨅i∈I. As i) ❙⟶⇩+ (⨅i∈I. Cs i)) ❙⟶⇩H (A ❙⟶⇩+ (⨅i∈I. Cs i))"
    by (simp add: heyting.curry_conv inf.coboundedI1 spec.Abadi_Merz_Theorem3_5)
  have 3: "?lhs ≤ (⨅i∈I. As i) ❙⟶⇩+ (⨅i∈I. Cs i)"
    using spec.Abadi_Lamport_Lemma5 le_infI2 by blast
  from 2 3 have "?lhs ≤ A ❙⟶⇩+ (⨅i∈I. Cs i)"
    using heyting.mp by blast
  then show ?thesis
    by - (rule order.trans[OF _ spec.Abadi_Merz_Prop2_1[where Q="⨅ (Cs ` I)"]]; simp add: inf.coboundedI1)
qed

setup ‹Sign.parent_path›
(*<*)

end
(*>*)