Theory OInvariants

(*  Title:       OInvariants.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Open reachability and invariance"

theory OInvariants
imports Invariants
begin

subsection "Open reachability"

text ‹
  By convention, the states of an open automaton are pairs. The first component is considered
  to be the global state and the second is the local state.

  A state is `open reachable' under @{term S} and @{term U} if it is the initial state, or it
  is the destination of a transition---where the global components satisfy @{term S}---from an
  open reachable state, or it is the destination of an interleaved environment step where the
  global components satisfy @{term U}.
›

inductive_set oreachable
  :: "('g × 'l, 'a) automaton
      ⇒ ('g ⇒ 'g ⇒ 'a ⇒ bool)
      ⇒ ('g ⇒ 'g ⇒ bool)
      ⇒ ('g × 'l) set"
  for A  :: "('g × 'l, 'a) automaton"
  and S  :: "'g ⇒ 'g ⇒ 'a ⇒ bool"
  and U  :: "'g ⇒ 'g ⇒ bool"
where
    oreachable_init: "s ∈ init A ⟹ s ∈ oreachable A S U"
  | oreachable_local: "⟦ s ∈ oreachable A S U; (s, a, s') ∈ trans A; S (fst s) (fst s') a ⟧
                        ⟹ s' ∈ oreachable A S U"
  | oreachable_other: "⟦ s ∈ oreachable A S U; U (fst s) σ' ⟧
                        ⟹ (σ', snd s) ∈ oreachable A S U"

lemma oreachable_local' [elim]:
  assumes "(σ, p) ∈ oreachable A S U"
      and "((σ, p), a, (σ', p')) ∈ trans A"
      and "S σ σ' a"
    shows "(σ', p') ∈ oreachable A S U"
  using assms by (metis fst_conv oreachable.oreachable_local)

lemma oreachable_other' [elim]:
  assumes "(σ, p) ∈ oreachable A S U"
      and "U σ σ'"
    shows "(σ', p) ∈ oreachable A S U"
  proof -
    from ‹U σ σ'› have "U (fst (σ, p)) σ'" by simp
    with ‹(σ, p) ∈ oreachable A S U› have "(σ', snd (σ, p)) ∈ oreachable A S U"
      by (rule oreachable_other)
    thus "(σ', p) ∈ oreachable A S U" by simp
  qed

lemma oreachable_pair_induct [consumes, case_names init other local]:
  assumes "(σ, p) ∈ oreachable A S U"
      and "⋀σ p. (σ, p) ∈ init A ⟹ P σ p"
      and "(⋀σ p σ'. ⟦ (σ, p) ∈ oreachable A S U; P σ p; U σ σ' ⟧ ⟹ P σ' p)"
      and "(⋀σ p σ' p' a. ⟦ (σ, p) ∈ oreachable A S U; P σ p;
                            ((σ, p), a, (σ', p')) ∈ trans A; S σ σ' a ⟧ ⟹ P σ' p')"
    shows "P σ p"
  using assms (1) proof (induction "(σ, p)" arbitrary: σ p)
    fix σ p
    assume "(σ, p) ∈ init A"
    with assms(2) show "P σ p" .
  next
    fix s σ'
    assume "s ∈ oreachable A S U"
       and "U (fst s) σ'"
       and IH: "⋀σ p. s = (σ, p) ⟹ P σ p"
    from this(1) obtain σ p where "s = (σ, p)"
                              and "(σ, p) ∈ oreachable A S U"
      by (metis surjective_pairing)
    note this(2)
    moreover from IH and ‹s = (σ, p)› have "P σ p" .
    moreover from ‹U (fst s) σ'› and ‹s = (σ, p)› have "U σ σ'" by simp
    ultimately have "P σ' p" by (rule assms(3))
    with ‹s = (σ, p)› show "P σ' (snd s)" by simp
  next
    fix s a σ' p'
    assume "s ∈ oreachable A S U"
       and tr: "(s, a, (σ', p')) ∈ trans A"
       and "S (fst s) (fst (σ', p')) a"
       and IH: "⋀σ p. s = (σ, p) ⟹ P σ p"
    from this(1) obtain σ p where "s = (σ, p)"
                              and "(σ, p) ∈ oreachable A S U"
      by (metis surjective_pairing)
    note this(2)
    moreover from IH ‹s = (σ, p)› have "P σ p" .
    moreover from tr and ‹s = (σ, p)› have "((σ, p), a, (σ', p')) ∈ trans A" by simp
    moreover from ‹S (fst s) (fst (σ', p')) a› and ‹s = (σ, p)› have "S σ σ' a" by simp
    ultimately show "P σ' p'" by (rule assms(4))
  qed

lemma oreachable_weakenE [elim]:
  assumes "s ∈ oreachable A PS PU"
      and PSQS: "⋀s s' a. PS s s' a ⟹ QS s s' a"
      and PUQU: "⋀s s'.   PU s s'   ⟹ QU s s'"
    shows "s ∈ oreachable A QS QU"
  using assms(1)
  proof (induction)
    fix s assume "s ∈ init A"
    thus "s ∈ oreachable A QS QU" ..
  next
    fix s a s'
    assume "s ∈ oreachable A QS QU"
       and "(s, a, s') ∈ trans A"
       and "PS (fst s) (fst s') a"
    from ‹PS (fst s) (fst s') a› have "QS (fst s) (fst s') a" by (rule PSQS)
    with ‹s ∈ oreachable A QS QU› and ‹(s, a, s') ∈ trans A› show "s' ∈ oreachable A QS QU" ..
  next
    fix s g'
    assume "s ∈ oreachable A QS QU"
       and "PU (fst s) g'"
    from ‹PU (fst s) g'› have "QU (fst s) g'" by (rule PUQU)
    with ‹s ∈ oreachable A QS QU› show "(g', snd s) ∈ oreachable A QS QU" ..
  qed

definition
  act :: "('a ⇒ bool) ⇒ 's ⇒ 's ⇒ 'a ⇒ bool"
where
  "act I ≡ (λ_ _. I)"

lemma act_simp [iff]: "act I s s' a = I a"
  unfolding act_def ..

lemma reachable_in_oreachable [elim]:
    fixes s
  assumes "s ∈ reachable A I"
    shows "s ∈ oreachable A (act I) U"
  unfolding act_def using assms proof induction
    fix s
    assume "s ∈ init A"
    thus "s ∈ oreachable A (λ_ _. I) U" ..
  next
    fix s a s'
    assume "s ∈ oreachable A (λ_ _. I) U"
       and "(s, a, s') ∈ trans A"
       and "I a"
    thus "s' ∈ oreachable A (λ_ _. I) U"
      by (rule oreachable_local)
  qed

subsection "Open Invariance"

definition oinvariant
  :: "('g × 'l, 'a) automaton
      ⇒ ('g ⇒ 'g ⇒ 'a ⇒ bool) ⇒ ('g ⇒ 'g ⇒ bool)
      ⇒ (('g × 'l) ⇒ bool) ⇒ bool"
  ("_ ⊨ (1'((1_),/ (1_) →')/ _)" [100, 0, 0, 9] 8)
where
  "(A ⊨ (S, U →) P) = (∀s∈oreachable A S U. P s)"

lemma oinvariantI [intro]:
    fixes T TI S U P
  assumes init: "⋀s. s ∈ init A ⟹ P s"
      and other: "⋀g g' l.
                  ⟦ (g, l) ∈ oreachable A S U; P (g, l); U g g' ⟧ ⟹ P (g', l)"
      and local: "⋀s a s'.
                  ⟦ s ∈ oreachable A S U; P s; (s, a, s') ∈ trans A; S (fst s) (fst s') a ⟧ ⟹ P s'"
    shows "A ⊨ (S, U →) P"
  unfolding oinvariant_def
  proof
       fix s
    assume "s ∈ oreachable A S U"
      thus "P s"
    proof induction
      fix s assume "s ∈ init A"
      thus "P s" by (rule init)
    next
      fix s a s'
      assume "s ∈ oreachable A S U"
         and "P s"
         and "(s, a, s') ∈ trans A"
         and "S (fst s) (fst s') a"
        thus "P s'" by (rule local)
     next
       fix s g'
       assume "s ∈ oreachable A S U"
          and "P s"
          and "U (fst s) g'"
         thus "P (g', snd s)"
           by - (rule other [where g="fst s"], simp_all)
    qed
  qed

lemma oinvariant_oreachableI:
  assumes "⋀σ s. (σ, s)∈oreachable A S U ⟹ P (σ, s)"
  shows "A ⊨ (S, U →) P"
  using assms unfolding oinvariant_def by auto

lemma oinvariant_pairI [intro]:
  assumes init: "⋀σ p. (σ, p) ∈ init A ⟹ P (σ, p)"
      and local: "⋀σ p σ' p' a.
                   ⟦ (σ, p) ∈ oreachable A S U; P (σ, p); ((σ, p), a, (σ', p')) ∈ trans A;
                     S σ σ' a ⟧ ⟹ P (σ', p')"
      and other: "⋀σ σ' p.
                  ⟦ (σ, p) ∈ oreachable A S U; P (σ, p); U σ σ' ⟧ ⟹ P (σ', p)"
    shows "A ⊨ (S, U →) P"
  by (rule oinvariantI)
     (clarsimp | erule init | erule(3) local | erule(2) other)+

lemma oinvariantD [dest]:
  assumes "A ⊨ (S, U →) P"
      and "s ∈ oreachable A S U"
    shows "P s"
  using assms unfolding oinvariant_def
  by clarsimp

lemma oinvariant_initD [dest, elim]:
  assumes invP: "A ⊨ (S, U →) P"
      and init: "s ∈ init A"
    shows "P s"
  proof -
    from init have "s ∈ oreachable A S U" ..
    with invP show ?thesis ..
  qed

lemma oinvariant_weakenE [elim!]:
  assumes invP: "A ⊨ (PS, PU →) P"
      and PQ:   "⋀s. P s ⟹ Q s"
      and QSPS: "⋀s s' a. QS s s' a ⟹ PS s s' a"
      and QUPU: "⋀s s'.   QU s s'   ⟹ PU s s'"
    shows       "A ⊨ (QS, QU →) Q"
  proof
    fix s
    assume "s ∈ init A"
    with invP have "P s" ..
    thus "Q s" by (rule PQ)
  next
    fix σ p σ' p' a
    assume "(σ, p) ∈ oreachable A QS QU"
       and "((σ, p), a, (σ', p')) ∈ trans A"
       and "QS σ σ' a"
    from this(3) have "PS σ σ' a" by (rule QSPS)
    from ‹(σ, p) ∈ oreachable A QS QU› and QSPS QUPU have "(σ, p) ∈ oreachable A PS PU" ..
    hence "(σ', p') ∈ oreachable A PS PU" using ‹((σ, p), a, (σ', p')) ∈ trans A› and ‹PS σ σ' a› ..
    with invP have "P (σ', p')" ..
    thus "Q (σ', p')" by (rule PQ)
  next
    fix σ σ' p
    assume "(σ, p) ∈ oreachable A QS QU"
       and "Q (σ, p)"
       and "QU σ σ'"
    from ‹QU σ σ'› have "PU σ σ'" by (rule QUPU)
    from ‹(σ, p) ∈ oreachable A QS QU› and QSPS QUPU have "(σ, p) ∈ oreachable A PS PU" ..
    hence "(σ', p) ∈ oreachable A PS PU" using ‹PU σ σ'› ..
    with invP have "P (σ', p)" ..
    thus "Q (σ', p)" by (rule PQ)
  qed

lemma oinvariant_weakenD [dest]:
  assumes "A ⊨ (S', U' →) P"
      and "(σ, p) ∈ oreachable A S U"
      and weakenS: "⋀s s' a. S s s' a ⟹ S' s s' a"
      and weakenU: "⋀s s'. U s s' ⟹ U' s s'"
    shows "P (σ, p)"
  proof -
    from ‹(σ, p) ∈ oreachable A S U› have "(σ, p) ∈ oreachable A S' U'"
      by (rule oreachable_weakenE)
         (erule weakenS, erule weakenU)
    with ‹A ⊨ (S', U' →) P› show "P (σ, p)" ..
  qed

lemma close_open_invariant:
  assumes oinv: "A ⊨ (act I, U →) P"
    shows "A ⊫ (I →) P"
  proof
    fix s
    assume "s ∈ init A"
    with oinv show "P s" ..
  next
    fix ξ p ξ' p' a
    assume sr: "(ξ, p) ∈ reachable A I"
       and step: "((ξ, p), a, (ξ', p')) ∈ trans A"
       and "I a"
    hence "(ξ', p') ∈ reachable A I" ..
    hence "(ξ', p') ∈ oreachable A (act I) U" ..
    with oinv show "P (ξ', p')" ..
  qed

definition local_steps :: "((('i ⇒ 's1) × 'l1) × 'a × ('i ⇒ 's2) × 'l2) set ⇒ 'i set ⇒ bool"
where "local_steps T J ≡
   (∀σ ζ s a σ' s'. ((σ, s), a, (σ', s')) ∈ T ∧ (∀j∈J. ζ j = σ j)
   ⟶ (∃ζ'. (∀j∈J. ζ' j = σ' j) ∧ ((ζ, s), a, (ζ', s')) ∈ T))"

lemma local_stepsI [intro!]:
  assumes "⋀σ ζ s a σ' ζ' s'. ⟦ ((σ, s), a, (σ', s')) ∈ T; ∀j∈J. ζ j = σ j ⟧
                               ⟹ (∃ζ'. (∀j∈J. ζ' j = σ' j) ∧ ((ζ, s), a, (ζ', s')) ∈ T)"
    shows "local_steps T J"
  unfolding local_steps_def using assms by clarsimp

lemma local_stepsE [elim, dest]:
  assumes "local_steps T J"
      and "((σ, s), a, (σ', s')) ∈ T"
      and "∀j∈J. ζ j = σ j"
    shows "∃ζ'. (∀j∈J. ζ' j = σ' j) ∧ ((ζ, s), a, (ζ', s')) ∈ T"
  using assms unfolding local_steps_def by blast

definition other_steps :: "(('i ⇒ 's) ⇒ ('i ⇒ 's) ⇒ bool) ⇒ 'i set ⇒ bool"
where "other_steps U J ≡ ∀σ σ'. U σ σ' ⟶ (∀j∈J. σ' j = σ j)"

lemma other_stepsI [intro!]:
  assumes "⋀σ σ' j. ⟦ U σ σ'; j ∈ J ⟧ ⟹ σ' j = σ j"
    shows "other_steps U J"
  using assms unfolding other_steps_def by simp

lemma other_stepsE [elim]:
  assumes "other_steps U J"
      and "U σ σ'"
    shows "∀j∈J. σ' j = σ j"
  using assms unfolding other_steps_def by simp

definition subreachable
where "subreachable A U J ≡ ∀I. ∀s ∈ oreachable A (λs s'. I) U.
                                  (∃σ. (∀j∈J. σ j = (fst s) j) ∧ (σ, snd s) ∈ reachable A I)"

lemma subreachableI [intro]:
  assumes "local_steps (trans A) J"
      and "other_steps U J"
    shows "subreachable A U J"
  unfolding subreachable_def
  proof (rule, rule)
    fix I s
    assume "s ∈ oreachable A (λs s'. I) U"
    thus "(∃σ. (∀j∈J. σ j = (fst s) j) ∧ (σ, snd s) ∈ reachable A I)"
    proof induction
      fix s
      assume "s ∈ init A"
      hence "(fst s, snd s) ∈ reachable A I"
        by simp (rule reachable_init)
      moreover have "∀j∈J. (fst s) j = (fst s) j"
        by simp
      ultimately show "∃σ. (∀j∈J. σ j = (fst s) j) ∧ (σ, snd s) ∈ reachable A I"
        by auto
    next
      fix s a s'
      assume "∃σ. (∀j∈J. σ j = (fst s) j) ∧ (σ, snd s) ∈ reachable A I"
         and "(s, a, s') ∈ trans A"
         and "I a"
      then obtain ζ where "∀j∈J. ζ j = (fst s) j"
                      and "(ζ, snd s) ∈ reachable A I" by auto

      from ‹(s, a, s') ∈ trans A› have "((fst s, snd s), a, (fst s', snd s')) ∈ trans A"
        by simp
      with ‹local_steps (trans A) J› obtain ζ' where "∀j∈J. ζ' j = (fst s') j"
                                                 and "((ζ, snd s), a, (ζ', snd s')) ∈ trans A"
        using ‹∀j∈J. ζ j = (fst s) j› by - (drule(2) local_stepsE, clarsimp)
      from ‹(ζ, snd s) ∈ reachable A I›
       and ‹((ζ, snd s), a, (ζ', snd s')) ∈ trans A›
       and ‹I a›
       have "(ζ', snd s') ∈ reachable A I" ..

      with ‹∀j∈J. ζ' j = (fst s') j›
        show "∃σ. (∀j∈J. σ j = (fst s') j) ∧ (σ, snd s') ∈ reachable A I" by auto
    next
      fix s σ'
      assume "∃σ. (∀j∈J. σ j = (fst s) j) ∧ (σ, snd s) ∈ reachable A I"
         and "U (fst s) σ'"
      then obtain σ where "∀j∈J. σ j = (fst s) j"
                      and "(σ, snd s) ∈ reachable A I" by auto
      from ‹other_steps U J› and ‹U (fst s) σ'› have "∀j∈J. σ' j = (fst s) j"
        by - (erule(1) other_stepsE)
      with ‹∀j∈J. σ j = (fst s) j› have "∀j∈J. σ j = σ' j"
        by clarsimp
      with ‹(σ, snd s) ∈ reachable A I›
       show "∃σ. (∀j∈J. σ j = fst (σ', snd s) j) ∧ (σ, snd (σ', snd s)) ∈ reachable A I"
         by auto
    qed
  qed

lemma subreachableE [elim]:
  assumes "subreachable A U J"
      and "s ∈ oreachable A (λs s'. I) U"
    shows "∃σ. (∀j∈J. σ j = (fst s) j) ∧ (σ, snd s) ∈ reachable A I"
  using assms unfolding subreachable_def by simp

lemma subreachableE_pair [elim]:
  assumes "subreachable A U J"
      and "(σ, s) ∈ oreachable A (λs s'. I) U"
    shows "∃ζ. (∀j∈J. ζ j = σ j) ∧ (ζ, s) ∈ reachable A I"
  using assms unfolding subreachable_def by (metis fst_conv snd_conv)

lemma subreachable_otherE [elim]:
  assumes "subreachable A U J"
      and "(σ, l) ∈ oreachable A (λs s'. I) U"
      and "U σ σ'"
    shows "∃ζ'. (∀j∈J. ζ' j = σ' j) ∧ (ζ', l) ∈ reachable A I"
  proof -
    from ‹(σ, l) ∈ oreachable A (λs s'. I) U› and ‹U σ σ'›
      have "(σ', l) ∈ oreachable A (λs s'. I) U"
      by - (rule oreachable_other')
    with ‹subreachable A U J› show ?thesis
      by auto
  qed

lemma open_closed_invariant:
    fixes J
  assumes "A ⊫ (I →) P"
      and "subreachable A U J"
      and localp: "⋀σ σ' s. ⟦ ∀j∈J. σ' j = σ j; P (σ', s) ⟧ ⟹ P (σ, s)"
    shows "A ⊨ (act I, U →) P"
  proof (rule, simp_all only: act_def)
    fix s
    assume "s ∈ init A"
    with ‹A ⊫ (I →) P› show "P s" ..
  next
    fix s a s'
    assume "s ∈ oreachable A (λ_ _. I) U"
       and "P s"
       and "(s, a, s') ∈ trans A"
       and "I a"
    hence "s' ∈ oreachable A (λ_ _. I) U"
      by (metis oreachable_local)
    with ‹subreachable A U J› obtain σ'
      where "∀j∈J. σ' j = (fst s') j"
        and "(σ', snd s') ∈ reachable A I"
        by (metis subreachableE)
    from ‹A ⊫ (I →) P› and ‹(σ', snd s') ∈ reachable A I› have "P (σ', snd s')" ..
    with ‹∀j∈J. σ' j = (fst s') j› show "P s'"
      by (metis localp prod.collapse)
  next
    fix g g' l
    assume or: "(g, l) ∈ oreachable A (λs s'. I) U"
       and "U g g'"
       and "P (g, l)"
    from ‹subreachable A U J› and or and ‹U g g'›
      obtain gg' where "∀j∈J. gg' j = g' j"
                   and "(gg', l) ∈ reachable A I"
        by (auto dest!: subreachable_otherE)
    from ‹A ⊫ (I →) P› and ‹(gg', l) ∈ reachable A I›
      have "P (gg', l)" ..
    with ‹∀j∈J. gg' j = g' j› show "P (g', l)"
      by (rule localp)
  qed

lemma oinvariant_anyact:
  assumes "A ⊨ (act TT, U →) P"
    shows "A ⊨ (S, U →) P"                             
  using assms by rule auto

definition
  ostep_invariant
  :: "('g × 'l, 'a) automaton
      ⇒ ('g ⇒ 'g ⇒ 'a ⇒ bool) ⇒ ('g ⇒ 'g ⇒ bool)
      ⇒ (('g × 'l, 'a) transition ⇒ bool) ⇒ bool"
  ("_ ⊨⇩A (1'((1_),/ (1_) →')/ _)" [100, 0, 0, 9] 8)
where
  "(A ⊨⇩A (S, U →) P) =
     (∀s∈oreachable A S U. (∀a s'. (s, a, s') ∈ trans A ∧ S (fst s) (fst s') a ⟶ P (s, a, s')))"

lemma ostep_invariant_def':
  "(A ⊨⇩A (S, U →) P) = (∀s∈oreachable A S U.
                           (∀a s'. (s, a, s') ∈ trans A ∧ S (fst s) (fst s') a ⟶ P (s, a, s')))"
  unfolding ostep_invariant_def by auto

lemma ostep_invariantI [intro]:
  assumes *: "⋀σ s a σ' s'. ⟦ (σ, s)∈oreachable A S U; ((σ, s), a, (σ', s')) ∈ trans A; S σ σ' a ⟧
                             ⟹ P ((σ, s), a, (σ', s'))"
    shows "A ⊨⇩A (S, U →) P"
  unfolding ostep_invariant_def
  using assms by auto

lemma ostep_invariantD [dest]:
  assumes "A ⊨⇩A (S, U →) P"
      and "(σ, s)∈oreachable A S U"
      and "((σ, s), a, (σ', s')) ∈ trans A"
      and "S σ σ' a"
    shows "P ((σ, s), a, (σ', s'))"
  using assms unfolding ostep_invariant_def' by clarsimp

lemma ostep_invariantE [elim]:
  assumes "A ⊨⇩A (S, U →) P"
      and "(σ, s)∈oreachable A S U"
      and "((σ, s), a, (σ', s')) ∈ trans A"
      and "S σ σ' a"
      and "P ((σ, s), a, (σ', s')) ⟹ Q"
    shows "Q"
  using assms by auto

lemma ostep_invariant_weakenE [elim!]:
  assumes invP: "A ⊨⇩A (PS, PU →) P"
      and PQ:   "⋀t. P t ⟹ Q t"
      and QSPS: "⋀σ σ' a. QS σ σ' a ⟹ PS σ σ' a"
      and QUPU: "⋀σ σ'.   QU σ σ'   ⟹ PU σ σ'"
    shows       "A ⊨⇩A (QS, QU →) Q"
  proof
    fix σ s σ' s' a
    assume "(σ, s) ∈ oreachable A QS QU"
       and "((σ, s), a, (σ', s')) ∈ trans A"
       and "QS σ σ' a"
    from ‹QS σ σ' a› have "PS σ σ' a" by (rule QSPS)
    from ‹(σ, s) ∈ oreachable A QS QU› have "(σ, s) ∈ oreachable A PS PU" using QSPS QUPU ..
    with invP have "P ((σ, s), a, (σ', s'))" using ‹((σ, s), a, (σ', s')) ∈ trans A› ‹PS σ σ' a› ..
    thus "Q ((σ, s), a, (σ', s'))" by (rule PQ)
  qed

lemma ostep_invariant_weaken_with_invariantE [elim]:
  assumes pinv: "A ⊨ (S, U →) P"
      and qinv: "A ⊨⇩A (S, U →) Q"
      and wr: "⋀σ s a σ' s'. ⟦ P (σ, s); P (σ', s'); Q ((σ, s), a, (σ', s')); S σ σ' a ⟧
                              ⟹ R ((σ, s), a, (σ', s'))"
    shows "A ⊨⇩A (S, U →) R"
  proof
    fix σ s a σ' s'
    assume sr: "(σ, s) ∈ oreachable A S U"
       and tr: "((σ, s), a, (σ', s')) ∈ trans A"
       and "S σ σ' a"
    hence "(σ', s') ∈ oreachable A S U" ..
    with pinv have "P (σ', s')" ..
    from pinv and sr have "P (σ, s)" ..
    from qinv sr tr ‹S σ σ' a› have "Q ((σ, s), a, (σ', s'))" ..
    with ‹P (σ, s)› and ‹P (σ', s')› show "R ((σ, s), a, (σ', s'))" using ‹S σ σ' a› by (rule wr)
  qed

lemma ostep_to_invariantI:
  assumes sinv: "A ⊨⇩A (S, U →) Q"
      and init: "⋀σ s. (σ, s) ∈ init A ⟹ P (σ, s)"
      and local: "⋀σ s σ' s' a.
                    ⟦ (σ, s) ∈ oreachable A S U;
                      P (σ, s);
                      Q ((σ, s), a, (σ', s'));
                      S σ σ' a ⟧ ⟹ P (σ', s')"
      and other: "⋀σ σ' s. ⟦ (σ, s) ∈ oreachable A S U; U σ σ'; P (σ, s) ⟧ ⟹ P (σ', s)"
    shows "A ⊨ (S, U →) P"
  proof
    fix σ s assume "(σ, s) ∈ init A" thus "P (σ, s)" by (rule init)
  next
    fix σ s σ' s' a
    assume "(σ, s) ∈ oreachable A S U"
       and "P (σ, s)"
       and "((σ, s), a, (σ', s')) ∈ trans A"
       and "S σ σ' a"
      show "P (σ', s')"
    proof -
      from sinv and ‹(σ, s)∈oreachable A S U› and ‹((σ, s), a, (σ', s')) ∈ trans A› and ‹S σ σ' a›
        have "Q ((σ, s), a, (σ', s'))" ..
      with ‹(σ, s)∈oreachable A S U› and ‹P (σ, s)› show "P (σ', s')"
        using ‹S σ σ' a› by (rule local)
    qed
  next
    fix σ σ' l
    assume "(σ, l) ∈ oreachable A S U"
       and "U σ σ'"
       and "P (σ, l)"
      thus "P (σ', l)" by (rule other)
  qed

lemma open_closed_step_invariant:
  assumes "A ⊫⇩A (I →) P"
      and "local_steps (trans A) J"
      and "other_steps U J"
      and localp: "⋀σ ζ a σ' ζ' s s'.
                   ⟦ ∀j∈J. σ j = ζ j; ∀j∈J. σ' j = ζ' j; P ((σ, s), a, (σ', s')) ⟧
                   ⟹ P ((ζ, s), a, (ζ', s'))"
    shows "A ⊨⇩A (act I, U →) P"
  proof
    fix σ s a σ' s'
    assume or: "(σ, s) ∈ oreachable A (act I) U"
       and tr: "((σ, s), a, (σ', s')) ∈ trans A"
       and "act I σ σ' a"
    from ‹act I σ σ' a› have "I a" ..
    from ‹local_steps (trans A) J› and ‹other_steps U J› have "subreachable A U J" ..
    then obtain ζ where "∀j∈J. ζ j = σ j"
                    and "(ζ, s) ∈ reachable A I"
      using or unfolding act_def
        by (auto dest!: subreachableE_pair)

     from ‹local_steps (trans A) J› and tr and ‹∀j∈J. ζ j = σ j›
       obtain ζ' where "∀j∈J. ζ' j = σ' j"
                   and "((ζ, s), a, (ζ', s')) ∈ trans A"
       by auto

    from ‹A ⊫⇩A (I →) P› and ‹(ζ, s) ∈ reachable A I›
                          and ‹((ζ, s), a, (ζ', s')) ∈ trans A›
                          and ‹I a›
      have "P ((ζ, s), a, (ζ', s'))" ..
    with ‹∀j∈J. ζ j = σ j› and ‹∀j∈J. ζ' j = σ' j› show "P ((σ, s), a, (σ', s'))"
      by (rule localp)
  qed

lemma oinvariant_step_anyact:
  assumes "p ⊨⇩A (act TT, U →) P"
    shows "p ⊨⇩A (S, U →) P"
  using assms by rule auto

subsection "Standard assumption predicates "

text ‹otherwith›

definition otherwith :: "('s ⇒ 's ⇒ bool)
                          ⇒ 'i set
                          ⇒ (('i ⇒ 's) ⇒ 'a ⇒ bool)
                          ⇒ ('i ⇒ 's) ⇒ ('i ⇒ 's) ⇒ 'a ⇒ bool"
where "otherwith Q I P σ σ' a ≡ (∀i. i∉I ⟶ Q (σ i) (σ' i)) ∧ P σ a"

lemma otherwithI [intro]:
  assumes other: "⋀j. j∉I ⟹ Q (σ j) (σ' j)"
      and sync:  "P σ a"
    shows "otherwith Q I P σ σ' a"
  unfolding otherwith_def using assms by simp

lemma otherwithE [elim]:
  assumes "otherwith Q I P σ σ' a"
      and "⟦ P σ a; ∀j. j∉I ⟶ Q (σ j) (σ' j) ⟧ ⟹ R σ σ' a"
    shows "R σ σ' a"
  using assms unfolding otherwith_def by simp

lemma otherwith_actionD [dest]:
  assumes "otherwith Q I P σ σ' a"
    shows "P σ a"
  using assms by auto

lemma otherwith_syncD [dest]:
  assumes "otherwith Q I P σ σ' a"
    shows "∀j. j∉I ⟶ Q (σ j) (σ' j)"
  using assms by auto

lemma otherwithEI [elim]:
  assumes "otherwith P I PO σ σ' a"
      and "⋀σ a. PO σ a ⟹ QO σ a"
    shows "otherwith P I QO σ σ' a"
  using assms(1) unfolding otherwith_def
  by (clarsimp elim!: assms(2))

lemma all_but:
  assumes "⋀ξ. S ξ ξ"
      and "σ' i = σ i"
      and "∀j. j ≠ i ⟶ S (σ j) (σ' j)"
    shows "∀j. S (σ j) (σ' j)"
  using assms by metis

lemma all_but_eq [dest]:
  assumes "σ' i = σ i"
      and "∀j. j ≠ i ⟶ σ j = σ' j"
    shows "σ = σ'"
  using assms by - (rule ext, metis)

text ‹other›

definition other :: "('s ⇒ 's ⇒ bool) ⇒ 'i set ⇒ ('i ⇒ 's) ⇒ ('i ⇒ 's) ⇒ bool"
where "other P I σ σ' ≡ ∀i. if i∈I then σ' i = σ i else P (σ i) (σ' i)"

lemma otherI [intro]:
  assumes local: "⋀i. i∈I ⟹ σ' i = σ i"
      and other: "⋀j. j∉I ⟹ P (σ j) (σ' j)"
    shows "other P I σ σ'"
  using assms unfolding other_def by clarsimp

lemma otherE [elim]:
  assumes "other P I σ σ'"
      and "⟦ ∀i∈I. σ' i = σ i; ∀j. j∉I ⟶ P (σ j) (σ' j) ⟧ ⟹ R σ σ'"
    shows "R σ σ'"
  using assms unfolding other_def by simp

lemma other_localD [dest]:
  "other P {i} σ σ' ⟹ σ' i = σ i"
  by auto

lemma other_otherD [dest]:
  "other P {i} σ σ' ⟹ ∀j. j≠i ⟶ P (σ j) (σ' j)"
  by auto

lemma other_bothE [elim]:
  assumes "other P {i} σ σ'"
  obtains "σ' i = σ i" and "∀j. j≠i ⟶ P (σ j) (σ' j)"
  using assms by auto

lemma weaken_local [elim]:
  assumes "other P I σ σ'"
      and PQ: "⋀ξ ξ'. P ξ ξ' ⟹ Q ξ ξ'"
    shows "other Q I σ σ'"
  using assms unfolding other_def by auto

definition global :: "((nat ⇒ 's) ⇒ bool) ⇒ (nat ⇒ 's) × 'local ⇒ bool"
where "global P ≡ (λ(σ, _). P σ)"

lemma globalsimp [simp]: "global P s = P (fst s)"
  unfolding global_def by (simp split: prod.split)

definition globala :: "((nat ⇒ 's, 'action) transition ⇒ bool)
                       ⇒ ((nat ⇒ 's) × 'local, 'action) transition ⇒ bool"
where "globala P ≡ (λ((σ, _), a, (σ', _)). P (σ, a, σ'))"

lemma globalasimp [simp]: "globala P s = P (fst (fst s), fst (snd s), fst (snd (snd s)))"
  unfolding globala_def by (simp split: prod.split)

end