Quelle  Next_Imp.thy

(*<*)
theory Next_Imp
imports
  Safety_Logic
begin

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

text‹

  was apparently well-known in the mid-1990s (see, e.g.,
 🍋‹‹\S4› in "XuCauCollette:1994"› and
  references therein), Heyting implication is inadequate for a
  refinement story. (We show it is strong enough for a
  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
  (at least) because the composition theorem for Heyting
  (\S\ref{sec:abadi_plotkin}) is not termination sensitive.)

  therefore follow 🍋‹"AbadiLamport:1995"› by developing a stronger implication
 ‹P \⟶₊ Q› with the intuitive semantics that the consequent ‹Q› holds for at least one
  beyond the antecedent ‹P›. This is some kind of step indexing.

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

 :
 ▪ 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

  references:
 ▪ 🍋‹"Maier:2001"›

 ›

definition "next_imp" :: "'a::preorder set ==> 'a set ==> 'a set" where ―‹ 🍋‹‹\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 🍋‹"CauCollette:1996"›, 🍋‹‹\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‹

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

 ›

lemma Abadi_Merz_Prop_1_subseteq: ―‹ First half of 🍋‹‹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‹

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

 ›

lemma Abadi_Merz_Prop1: ―‹ 🍋‹‹Proposition~1› in "AbadiMerz:1995"› and 🍋‹‹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: ―‹ 🍋‹‹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 \<longrightarrow>_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 \<longrightarrow>₊ Q = (Q \<longrightarrow>_H P) \<longrightarrow>_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 \<longrightarrow>₊ 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 \<longrightarrow>₊ y ≤ x' \<longrightarrow>₊ 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 \<longrightarrow>₊ Y) (X' \<longrightarrow>₊ Y')"
using assms by (cases F) (auto simp: spec.next_imp.mono)

lemma idempotentR:
  shows "P \<longrightarrow>₊ (P \<longrightarrow>₊ Q) = P \<longrightarrow>₊ 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 \<longrightarrow>₊ Q"
by (simp add: assms spec.next_imp.heyting heyting.curry le_infI1)

interpretation closure: closure_complete_lattice_class "(\<longrightarrow>₊) 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 \<longrightarrow>₊ ⊓X = ⊓ ((\<longrightarrow>₊) x ` X)"
by transfer (auto simp: next_imp_def)

lemma SupR_not_empty:
  fixes P :: "(_, _, _) spec"
  assumes "X ≠ {}"
  shows "P \<longrightarrow>₊ (⊔x∈X. Q x) = (⊔x∈X. P \<longrightarrow>₊ 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 (≤) ((\<longrightarrow>₊) P)"
by (rule contI) (simp add: spec.next_imp.SupR_not_empty[where Q=id, simplified])

lemma mcont:
  shows "mcont Sup (≤) Sup (≤) ((\<longrightarrow>₊) 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 "⊥ \<longrightarrow>₊ P = ⊤"
by (simp add: assms spec.next_imp.heyting spec.eq_iff Heyting.heyting spec.heyting.non_triv)

lemma topL[simp]:
  shows "⊤ \<longrightarrow>₊ P = P"
by (simp add: spec.next_imp.heyting)

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

lemma refl:
  shows "P \<longrightarrow>₊ P ≤ P"
by (simp add: spec.next_imp.heyting)

lemma heyting_le:
  shows "P \<longrightarrow>₊ Q ≤ P \<longrightarrow>_H Q"
by (simp add: spec.next_imp.heyting heyting.discard heyting.mono)

lemma discharge:
  shows "P ⊓ (P ⊓ Q \<longrightarrow>₊ R) = P ⊓ (Q \<longrightarrow>₊ R)" (is "?thesis1 P Q")
    and "(P ⊓ Q \<longrightarrow>₊ R) ⊓ P = P ⊓ (Q \<longrightarrow>₊ R)" (is ?thesis2)
    and "Q ⊓ (P ⊓ Q \<longrightarrow>₊ R) = Q ⊓ (P \<longrightarrow>₊ R)" (is ?thesis3)
    and "(P ⊓ Q \<longrightarrow>₊ R) ⊓ Q = Q ⊓ (P \<longrightarrow>₊ 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 \<longrightarrow>₊ y) ≤ y"
    and "(x \<longrightarrow>₊ y) ⊓ x ≤ y"
by (simp_all add: spec.next_imp.heyting heyting.discard heyting.discharge)

lemma infR:
  shows "P \<longrightarrow>₊ Q ⊓ R = (P \<longrightarrow>₊ Q) ⊓ (P \<longrightarrow>₊ 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 \<longrightarrow>₊ z ≤ (x \<longrightarrow>₊ z) ⊔ (y \<longrightarrow>₊ z)"
by (simp add: le_supI1 spec.next_imp.mono)

lemma heytingL:
  shows "(P \<longrightarrow>_H Q) ⊓ (Q \<longrightarrow>₊ R) ≤ P \<longrightarrow>₊ 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 \<longrightarrow>₊ Q) ⊓ (Q \<longrightarrow>_H R) ≤ P \<longrightarrow>₊ 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 \<longrightarrow>_H (Q \<longrightarrow>₊ R) = (P ⊓ Q) \<longrightarrow>₊ (P \<longrightarrow>_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 \<longrightarrow>₊ Q) ⊓ (Q \<longrightarrow>₊ R) ≤ P \<longrightarrow>₊ R"
by (meson order.trans Heyting.heyting spec.next_imp.heytingL spec.next_imp.heyting_le)

lemma rev_trans:
  shows "(Q \<longrightarrow>₊ R) ⊓ (P \<longrightarrow>₊ Q) ≤ P \<longrightarrow>₊ R"
by (simp add: inf.commute spec.next_imp.trans)

lemma
  assumes "x' ≤ x"
  shows discharge_leL: "x' ⊓ (x \<longrightarrow>₊ y) = x' ⊓ y" (is ?thesis1)
    and discharge_leR: "(x \<longrightarrow>₊ 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 \<longrightarrow>₊ Q) = spec.invmap af sf vf P \<longrightarrow>₊ 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 \<longrightarrow>₊ Q ≤ R \<longrightarrow>₊ 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 \<longrightarrow>₊ Q) ≤ spec.term.all P \<longrightarrow>₊ 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 \<longrightarrow>₊ Q) = spec.term.all P \<longrightarrow>₊ 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 \<longrightarrow>₊ 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 \<longrightarrow>₊ R = spec.pre P \<longrightarrow>_H (Q \<longrightarrow>₊ R)" (is "?lhs = ?rhs")
    and "spec.pre P ⊓ Q \<longrightarrow>₊ R = spec.pre P \<longrightarrow>_H (Q \<longrightarrow>₊ 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‹

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

 ›

setup ‹Sign.mandatory_path "spec"›

lemma Abadi_Lamport_Lemma5:
  shows "(⊓i∈I. P i \<longrightarrow>₊ Q i) ≤ (⊓i∈I. P i) \<longrightarrow>₊ (⊓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 \<longrightarrow>₊ Q) ⊓ (P \<longrightarrow>₊ (Q \<longrightarrow>_H R)) ≤ P \<longrightarrow>₊ R"
by (metis heyting.detachment(1) inf_sup_ord(2) spec.next_imp.infR)

lemma Abadi_Merz_Theorem3_5:
  shows "P \<longrightarrow>_H (Q \<longrightarrow>_H R) ≤ (R \<longrightarrow>₊ Q) \<longrightarrow>_H (P \<longrightarrow>₊ 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) \<longrightarrow>_H (⊓i∈I. As i))
       ⊓ (A \<longrightarrow>₊ ((⊓i∈I. Cs i) \<longrightarrow>_H C))
       ⊓ (⊓i∈I. As i \<longrightarrow>₊ Cs i)
        ≤ A \<longrightarrow>₊ C" (is "?lhs ≤ ?rhs")
proof -
  have "?lhs ≤ A \<longrightarrow>_H (⊓i∈I. Cs i) \<longrightarrow>_H (⊓i∈I. As i)"
    by (simp add: heyting.curry_conv inf.coboundedI1)
  then have 2: "?lhs ≤ ((⊓i∈I. As i) \<longrightarrow>₊ (⊓i∈I. Cs i)) \<longrightarrow>_H (A \<longrightarrow>₊ (⊓i∈I. Cs i))"
    by (simp add: heyting.curry_conv inf.coboundedI1 spec.Abadi_Merz_Theorem3_5)
  have 3: "?lhs ≤ (⊓i∈I. As i) \<longrightarrow>₊ (⊓i∈I. Cs i)"
    using spec.Abadi_Lamport_Lemma5 le_infI2 by blast
  from 2 3 have "?lhs ≤ A \<longrightarrow>₊ (⊓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
(*>*)