Theory Hybrid_Logic

theory Hybrid_Logic imports "HOL-Library.Countable" begin

section ‹Syntax›

datatype ('a, 'b) fm
  = Pro 'a
  | Nom 'b
  | Neg ‹('a, 'b) fm› (‹❙¬ _› [40] 40)
  | Dis ‹('a, 'b) fm› ‹('a, 'b) fm› (infixr ‹❙∨› 30)
  | Dia ‹('a, 'b) fm› (‹❙◇ _› 10)
  | Sat 'b ‹('a, 'b) fm› (‹❙@ _ _› 10)

text ‹We can give other connectives as abbreviations.›

abbreviation Top (‹❙⊤›) where
  ‹❙⊤ ≡ (undefined ❙∨ ❙¬ undefined)›

abbreviation Con (infixr ‹❙∧› 35) where
  ‹p ❙∧ q ≡ ❙¬ (❙¬ p ❙∨ ❙¬ q)›

abbreviation Imp (infixr ‹❙⟶› 25) where
  ‹p ❙⟶ q ≡ ❙¬ (p ❙∧ ❙¬ q)›

abbreviation Box (‹❙□ _› 10) where
  ‹❙□ p ≡ ❙¬ (❙◇ ❙¬ p)›

primrec nominals :: ‹('a, 'b) fm ⇒ 'b set› where
  ‹nominals (Pro x) = {}›
| ‹nominals (Nom i) = {i}›
| ‹nominals (❙¬ p) = nominals p›
| ‹nominals (p ❙∨ q) = nominals p ∪ nominals q›
| ‹nominals (❙◇ p) = nominals p›
| ‹nominals (❙@ i p) = {i} ∪ nominals p›

primrec sub :: ‹('b ⇒ 'c) ⇒ ('a, 'b) fm ⇒ ('a, 'c) fm› where
  ‹sub _ (Pro x) = Pro x›
| ‹sub f (Nom i) = Nom (f i)›
| ‹sub f (❙¬ p) = (❙¬ sub f p)›
| ‹sub f (p ❙∨ q) = (sub f p ❙∨ sub f q)›
| ‹sub f (❙◇ p) = (❙◇ sub f p)›
| ‹sub f (❙@ i p) = (❙@ (f i) (sub f p))›

lemma sub_nominals: ‹nominals (sub f p) = f ` nominals p›
  by (induct p) auto

lemma sub_id: ‹sub id p = p›
  by (induct p) simp_all

lemma sub_upd_fresh: ‹i ∉ nominals p ⟹ sub (f(i := j)) p = sub f p›
  by (induct p) auto

section ‹Semantics›

text ‹
  Type variable ‹'w› stands for the set of worlds and ‹'a› for the set of propositional symbols.
  The accessibility relation is given by ‹R› and the valuation by ‹V›.
  The mapping from nominals to worlds is an extra argument ‹g› to the semantics.›

datatype ('w, 'a) model =
  Model (R: ‹'w ⇒ 'w set›) (V: ‹'w ⇒ 'a ⇒ bool›)

primrec semantics
  :: ‹('w, 'a) model ⇒ ('b ⇒ 'w) ⇒ 'w ⇒ ('a, 'b) fm ⇒ bool›
  (‹_, _, _ ⊨ _› [50, 50, 50] 50) where
  ‹(M, _, w ⊨ Pro x) = V M w x›
| ‹(_, g, w ⊨ Nom i) = (w = g i)›
| ‹(M, g, w ⊨ ❙¬ p) = (¬ M, g, w ⊨ p)›
| ‹(M, g, w ⊨ (p ❙∨ q)) = ((M, g, w ⊨ p) ∨ (M, g, w ⊨ q))›
| ‹(M, g, w ⊨ ❙◇ p) = (∃v ∈ R M w. M, g, v ⊨ p)›
| ‹(M, g, _ ⊨ ❙@ i p) = (M, g, g i ⊨ p)›

lemma ‹M, g, w ⊨ ❙⊤›
  by simp

lemma semantics_fresh:
  ‹i ∉ nominals p ⟹ (M, g, w ⊨ p) = (M, g(i := v), w ⊨ p)›
  by (induct p arbitrary: w) auto

subsection ‹Examples›

abbreviation is_named :: ‹('w, 'b) model ⇒ bool› where
  ‹is_named M ≡ ∀w. ∃a. V M a = w›

abbreviation reflexive :: ‹('w, 'b) model ⇒ bool› where
  ‹reflexive M ≡ ∀w. w ∈ R M w›

abbreviation irreflexive :: ‹('w, 'b) model ⇒ bool› where
  ‹irreflexive M ≡ ∀w. w ∉ R M w›

abbreviation symmetric :: ‹('w, 'b) model ⇒ bool› where
  ‹symmetric M ≡ ∀v w. w ∈ R M v ⟷ v ∈ R M w›

abbreviation asymmetric :: ‹('w, 'b) model ⇒ bool› where
  ‹asymmetric M ≡ ∀v w. ¬ (w ∈ R M v ∧ v ∈ R M w)›

abbreviation transitive :: ‹('w, 'b) model ⇒ bool› where
  ‹transitive M ≡ ∀v w x. w ∈ R M v ∧ x ∈ R M w ⟶ x ∈ R M v›

abbreviation universal :: ‹('w, 'b) model ⇒ bool› where
  ‹universal M ≡ ∀v w. v ∈ R M w›

lemma ‹irreflexive M ⟹ M, g, w ⊨ ❙@ i ❙¬ (❙◇ Nom i)›
proof -
  assume ‹irreflexive M›
  then have ‹g i ∉ R M (g i)›
    by simp
  then have ‹¬ M, g, g i ⊨ ❙◇ Nom i›
    by simp
  then have ‹M, g, g i ⊨ ❙¬ (❙◇ Nom i)›
    by simp
  then show ‹M, g, w ⊨ ❙@ i ❙¬ (❙◇ Nom i)›
    by simp
qed

text ‹We can automatically show some characterizations of frames by pure axioms.›

lemma ‹irreflexive M = (∀g w. M, g, w ⊨ ❙@ i ❙¬ (❙◇ Nom i))›
  by auto

lemma ‹asymmetric M = (∀g w. M, g, w ⊨ ❙@ i (❙□ ❙¬ (❙◇ Nom i)))›
  by auto

lemma ‹universal M = (∀g w. M, g, w ⊨ ❙◇ Nom i)›
  by auto

section ‹Tableau›

text ‹
  A block is defined as a list of formulas paired with an opening nominal.
  The opening nominal is not necessarily in the list.
  A branch is a list of blocks.
›

type_synonym ('a, 'b) block = ‹('a, 'b) fm list × 'b›
type_synonym ('a, 'b) branch = ‹('a, 'b) block list›

abbreviation member_list :: ‹'a ⇒ 'a list ⇒ bool› (‹_ ∈. _› [51, 51] 50) where
  ‹x ∈. xs ≡ x ∈ set xs›

text ‹The predicate ‹on› presents the opening nominal as appearing on the block.›

primrec on :: ‹('a, 'b) fm ⇒ ('a, 'b) block ⇒ bool› (‹_ on _› [51, 51] 50) where
  ‹p on (ps, i) = (p ∈. ps ∨ p = Nom i)›

syntax
  "_Ballon" :: ‹pttrn ⇒ 'a set ⇒ bool ⇒ bool› (‹(3∀(_/on_)./ _)› [0, 0, 10] 10)
  "_Bexon" :: ‹pttrn ⇒ 'a set ⇒ bool ⇒ bool› (‹(3∃(_/on_)./ _)› [0, 0, 10] 10)

syntax_consts
  "_Ballon" ⇌ All and
  "_Bexon" ⇌ Ex

translations
  "∀p on A. P" ⇀ "∀p. p on A ⟶ P"
  "∃p on A. P" ⇀ "∃p. p on A ∧ P"

abbreviation list_nominals :: ‹('a, 'b) fm list ⇒ 'b set› where
  ‹list_nominals ps ≡ (⋃p ∈ set ps. nominals p)›

primrec block_nominals :: ‹('a, 'b) block ⇒ 'b set› where
  ‹block_nominals (ps, i) = {i} ∪ list_nominals ps›

definition branch_nominals :: ‹('a, 'b) branch ⇒ 'b set› where
  ‹branch_nominals branch ≡ (⋃block ∈ set branch. block_nominals block)›

abbreviation at_in_branch :: ‹('a, 'b) fm ⇒ 'b ⇒ ('a, 'b) branch ⇒ bool› where
  ‹at_in_branch p a branch ≡ ∃ps. (ps, a) ∈. branch ∧ p on (ps, a)›

notation at_in_branch (‹_ at _ in _› [51, 51, 51] 50)

definition new :: ‹('a, 'b) fm ⇒ 'b ⇒ ('a, 'b) branch ⇒ bool› where
  ‹new p a branch ≡ ¬ p at a in branch›

definition witnessed :: ‹('a, 'b) fm ⇒ 'b ⇒ ('a, 'b) branch ⇒ bool› where
  ‹witnessed p a branch ≡ ∃i. (❙@ i p) at a in branch ∧ (❙◇ Nom i) at a in branch›

text ‹
  A branch has a closing tableau iff it is contained in the following inductively defined set.
  In that case I call the branch closeable.
  The first argument on the left of the turnstile, ‹A›, is a fixed set of nominals restricting Nom.
  This set rules out the copying of nominals and accessibility formulas introduced by DiaP.
  The second argument is "potential", used to restrict the GoTo rule.
›

inductive STA :: ‹'b set ⇒ nat ⇒ ('a, 'b) branch ⇒ bool› (‹_, _ ⊢ _› [50, 50, 50] 50)
  for A :: ‹'b set› where
    Close:
    ‹p at i in branch ⟹ (❙¬ p) at i in branch ⟹
     A, n ⊢ branch›
  | Neg:
    ‹(❙¬ ❙¬ p) at a in (ps, a) # branch ⟹
     new p a ((ps, a) # branch) ⟹
     A, Suc n ⊢ (p # ps, a) # branch ⟹
     A, n ⊢ (ps, a) # branch›
  | DisP:
    ‹(p ❙∨ q) at a in (ps, a) # branch ⟹
     new p a ((ps, a) # branch) ⟹ new q a ((ps, a) # branch) ⟹
     A, Suc n ⊢ (p # ps, a) # branch ⟹ A, Suc n ⊢ (q # ps, a) # branch ⟹
     A, n ⊢ (ps, a) # branch›
  | DisN:
    ‹(❙¬ (p ❙∨ q)) at a in (ps, a) # branch ⟹
     new (❙¬ p) a ((ps, a) # branch) ∨ new (❙¬ q) a ((ps, a) # branch) ⟹
     A, Suc n ⊢ ((❙¬ q) # (❙¬ p) # ps, a) # branch ⟹
     A, n ⊢ (ps, a) # branch›
  | DiaP:
    ‹(❙◇ p) at a in (ps, a) # branch ⟹
     i ∉ A ∪ branch_nominals ((ps, a) # branch) ⟹
     ∄a. p = Nom a ⟹ ¬ witnessed p a ((ps, a) # branch) ⟹
     A, Suc n ⊢ ((❙@ i p) # (❙◇ Nom i) # ps, a) # branch ⟹
     A, n ⊢ (ps, a) # branch›
  | DiaN:
    ‹(❙¬ (❙◇ p)) at a in (ps, a) # branch ⟹
     (❙◇ Nom i) at a in (ps, a) # branch ⟹
     new (❙¬ (❙@ i p)) a ((ps, a) # branch) ⟹
     A, Suc n ⊢ ((❙¬ (❙@ i p)) # ps, a) # branch ⟹
     A, n ⊢ (ps, a) # branch›
  | SatP:
    ‹(❙@ a p) at b in (ps, a) # branch ⟹
     new p a ((ps, a) # branch) ⟹
     A, Suc n ⊢ (p # ps, a) # branch ⟹
     A, n ⊢ (ps, a) # branch›
  | SatN:
    ‹(❙¬ (❙@ a p)) at b in (ps, a) # branch ⟹
     new (❙¬ p) a ((ps, a) # branch) ⟹
     A, Suc n ⊢ ((❙¬ p) # ps, a) # branch ⟹
     A, n ⊢ (ps, a) # branch›
  | GoTo:
    ‹i ∈ branch_nominals branch ⟹
     A, n ⊢ ([], i) # branch ⟹
     A, Suc n ⊢ branch›
  | Nom:
    ‹p at b in (ps, a) # branch ⟹ Nom a at b in (ps, a) # branch ⟹
     ∀i. p = Nom i ∨ p = (❙◇ Nom i) ⟶ i ∈ A ⟹
     new p a ((ps, a) # branch) ⟹
     A, Suc n ⊢ (p # ps, a) # branch ⟹
     A, n ⊢ (ps, a) # branch›

abbreviation STA_ex_potential :: ‹'b set ⇒ ('a, 'b) branch ⇒ bool› (‹_ ⊢ _› [50, 50] 50) where
  ‹A ⊢ branch ≡ ∃n. A, n ⊢ branch›

lemma STA_Suc: ‹A, n ⊢ branch ⟹ A, Suc n ⊢ branch›
  by (induct n branch rule: STA.induct) (simp_all add: STA.intros)

text ‹A verified derivation in the calculus.›

lemma
  fixes i
  defines ‹p ≡ ❙¬ (❙@ i (Nom i))›
  shows ‹A, Suc n ⊢ [([p], a)]›
proof -
  have ‹i ∈ branch_nominals [([p], a)]›
    unfolding p_def branch_nominals_def by simp
  then have ?thesis if ‹A,  n ⊢ [([], i), ([p], a)]›
    using that GoTo by fast
  moreover have ‹new (❙¬ Nom i) i [([], i), ([p], a)]›
    unfolding p_def new_def by auto
  moreover have ‹(❙¬ (❙@ i (Nom i))) at a in [([], i), ([p], a)]›
    unfolding p_def by fastforce
  ultimately have ?thesis if ‹A, Suc n ⊢ [([❙¬ Nom i], i), ([p], a)]›
    using that SatN by fast
  then show ?thesis
    by (meson Close list.set_intros(1) on.simps)
qed

section ‹Soundness›

text ‹
  An ‹i›-block is satisfied by a model ‹M› and assignment ‹g› if all formulas on the block
    are true under ‹M› at the world ‹g i›
  A branch is satisfied by a model and assignment if all blocks on it are.
›

primrec block_sat :: ‹('w, 'a) model ⇒ ('b ⇒ 'w) ⇒ ('a, 'b) block ⇒ bool›
  (‹_, _ ⊨⇩B _› [50, 50] 50) where
  ‹(M, g ⊨⇩B (ps, i)) = (∀p on (ps, i). M, g, g i ⊨ p)›

abbreviation branch_sat ::
  ‹('w, 'a) model ⇒ ('b ⇒ 'w) ⇒ ('a, 'b) branch ⇒ bool›
  (‹_, _ ⊨⇩Θ _› [50, 50] 50) where
  ‹M, g ⊨⇩Θ branch ≡ ∀(ps, i) ∈ set branch. M, g ⊨⇩B (ps, i)›

lemma block_nominals:
  ‹p on block ⟹ i ∈ nominals p ⟹ i ∈ block_nominals block›
  by (induct block) auto

lemma block_sat_fresh:
  assumes ‹M, g ⊨⇩B block› ‹i ∉ block_nominals block›
  shows ‹M, g(i := v) ⊨⇩B block›
  using assms
proof (induct block)
  case (Pair ps a)
  then have ‹∀p on (ps, a). i ∉ nominals p›
    using block_nominals by fast
  moreover have ‹i ≠ a›
    using calculation by simp
  ultimately have ‹∀p on (ps, a). M, g(i := v), (g(i := v)) a ⊨ p›
    using Pair semantics_fresh by fastforce
  then show ?case
    by (meson block_sat.simps)
qed

lemma branch_sat_fresh:
  assumes ‹M, g ⊨⇩Θ branch› ‹i ∉ branch_nominals branch›
  shows ‹M, g(i := v) ⊨⇩Θ branch›
  using assms using block_sat_fresh unfolding branch_nominals_def by fast

text ‹If a branch has a derivation then it cannot be satisfied.›

lemma soundness': ‹A, n ⊢ branch ⟹ M, g ⊨⇩Θ branch ⟹ False›
proof (induct n branch arbitrary: g rule: STA.induct)
  case (Close p i branch)
  then have ‹M, g, g i ⊨ p› ‹M, g, g i ⊨ ❙¬ p›
    by fastforce+
  then show ?case
    by simp
next
  case (Neg p a ps branch)
  have ‹M, g, g a ⊨ p›
    using Neg(1, 5) by fastforce
  then have ‹M, g ⊨⇩Θ (p # ps, a) # branch›
    using Neg(5) by simp
  then show ?case
    using Neg(4) by blast
next
  case (DisP p q a ps branch)
  consider ‹M, g, g a ⊨ p› | ‹M, g, g a ⊨ q›
    using DisP(1, 8) by fastforce
  then consider
    ‹M, g ⊨⇩Θ (p # ps, a) # branch› |
    ‹M, g ⊨⇩Θ (q # ps, a) # branch›
    using DisP(8) by auto
  then show ?case
    using DisP(5, 7) by metis
next
  case (DisN p q a ps branch)
  have ‹M, g, g a ⊨ ❙¬ p› ‹M, g, g a ⊨ ❙¬ q›
    using DisN(1, 5) by fastforce+
  then have ‹M, g ⊨⇩Θ ((❙¬ q) # (❙¬ p) # ps, a) # branch›
    using DisN(5) by simp
  then show ?case
    using DisN(4) by blast
next
  case (DiaP p a ps branch i)
  then have *: ‹M, g ⊨⇩B (ps, a)›
    by simp

  have ‹i ∉ nominals p›
    using DiaP(1-2) unfolding branch_nominals_def by fastforce

  have ‹M, g, g a ⊨ ❙◇ p›
    using DiaP(1, 7) by fastforce
  then obtain v where ‹v ∈ R M (g a)› ‹M, g, v ⊨ p›
    by auto
  then have ‹M, g(i := v), v ⊨ p›
    using ‹i ∉ nominals p› semantics_fresh by metis
  then have ‹M, g(i := v), g a ⊨ ❙@ i p›
    by simp
  moreover have ‹M, g(i := v), g a ⊨ ❙◇ Nom i›
    using ‹v ∈ R M (g a)› by simp
  moreover have ‹M, g(i := v) ⊨⇩Θ (ps, a) # branch›
    using DiaP(2, 7) branch_sat_fresh by fast
  moreover have ‹i ∉ block_nominals (ps, a)›
    using DiaP(2) unfolding branch_nominals_def by simp
  then have ‹∀p on (ps, a). M, g(i := v), g a ⊨ p›
    using * semantics_fresh by fastforce
  ultimately have
    ‹M, g(i := v) ⊨⇩Θ ((❙@ i p) # (❙◇ Nom i) # ps, a) # branch›
    by auto
  then show ?case
    using DiaP by blast
next
  case (DiaN p a ps branch i)
  have ‹M, g, g a ⊨ ❙¬ (❙◇ p)› ‹M, g, g a ⊨ ❙◇ Nom i›
    using DiaN(1-2, 6) by fastforce+
  then have ‹M, g, g a ⊨ ❙¬ (❙@ i p)›
    by simp
  then have ‹M, g ⊨⇩Θ ((❙¬ (❙@ i p)) # ps, a) # branch›
    using DiaN(6) by simp
  then show ?thesis
    using DiaN(5) by blast
next
  case (SatP a p b ps branch)
  have ‹M, g, g a ⊨ p›
    using SatP(1, 5) by fastforce
  then have ‹M, g ⊨⇩Θ (p # ps, a) # branch›
    using SatP(5) by simp
  then show ?case
    using SatP(4) by blast
next
  case (SatN a p b ps branch)
  have ‹M, g, g a ⊨ ❙¬ p›
    using SatN(1, 5) by fastforce
  then have ‹M, g ⊨⇩Θ ((❙¬ p) # ps, a) # branch›
    using SatN(5) by simp
  then show ?case
    using SatN(4) by blast
next
  case (GoTo i branch)
  then show ?case
    by auto
next
  case (Nom p b ps a branch)
  have ‹M, g, g b ⊨ p› ‹M, g, g b ⊨ Nom a›
    using Nom(1-2, 7) by fastforce+
  moreover have ‹M, g ⊨⇩B (ps, a)›
    using Nom(7) by simp
  ultimately have ‹M, g ⊨⇩B (p # ps, a)›
    by simp
  then have ‹M, g ⊨⇩Θ (p # ps, a) # branch›
    using Nom(7) by simp
  then show ?case
    using Nom(6) by blast
qed

lemma block_sat: ‹∀p on block. M, g, w ⊨ p ⟹ M, g ⊨⇩B block›
  by (induct block) auto

lemma branch_sat:
  assumes ‹∀(ps, i) ∈ set branch. ∀p on (ps, i). M, g, w ⊨ p›
  shows ‹M, g ⊨⇩Θ branch›
  using assms block_sat by fast

lemma soundness:
  assumes ‹A, n ⊢ branch›
  shows ‹∃block ∈ set branch. ∃p on block. ¬ M, g, w ⊨ p›
  using assms soundness' branch_sat by fast

corollary ‹¬ A, n ⊢ []›
  using soundness by fastforce

theorem soundness_fresh:
  assumes ‹A, n ⊢ [([❙¬ p], i)]› ‹i ∉ nominals p›
  shows ‹M, g, w ⊨ p›
proof -
  from assms(1) have ‹M, g, g i ⊨ p› for g
    using soundness by fastforce
  then have ‹M, g(i := w), (g(i := w)) i ⊨ p›
    by blast
  then have ‹M, g(i := w), w ⊨ p›
    by simp
  then have ‹M, g(i := g i), w ⊨ p›
    using assms(2) semantics_fresh by metis
  then show ?thesis
    by simp
qed

section ‹No Detours›

text ‹
  We only need to spend initial potential when we apply GoTo twice in a row.
  Otherwise another rule will have been applied in-between that justifies the GoTo.
  Therefore, by filtering out detours we can close any closeable branch starting from
    a single unit of potential.
›

primrec nonempty :: ‹('a, 'b) block ⇒ bool› where
  ‹nonempty (ps, i) = (ps ≠ [])›

lemma nonempty_Suc:
  assumes
    ‹A, n ⊢ (ps, a) # filter nonempty left @ right›
    ‹q at a in (ps, a) # filter nonempty left @ right› ‹q ≠ Nom a›
  shows ‹A, Suc n ⊢ filter nonempty ((ps, a) # left) @ right›
proof (cases ps)
  case Nil
  then have ‹a ∈ branch_nominals (filter nonempty left @ right)›
    unfolding branch_nominals_def using assms(2-3) by fastforce
  then show ?thesis
    using assms(1) Nil GoTo by auto
next
  case Cons
  then show ?thesis
    using assms(1) STA_Suc by auto
qed

lemma STA_nonempty:
  ‹A, n ⊢ left @ right ⟹ A, Suc m ⊢ filter nonempty left @ right›
proof (induct n ‹left @ right› arbitrary: left right rule: STA.induct)
  case (Close p i n)
  have ‹(❙¬ p) at i in filter nonempty left @ right›
    using Close(2) by fastforce
  moreover from this have ‹p at i in filter nonempty left @ right›
    using Close(1) by fastforce
  ultimately show ?case
    using STA.Close by fast
next
  case (Neg p a ps branch n)
  then show ?case
  proof (cases left)
    case Nil
    then have ‹A, Suc m ⊢ (p # ps, a) # branch›
      using Neg(4) by fastforce
    then have ‹A, m ⊢ (ps, a) # branch›
      using Neg(1-2) STA.Neg by fast
    then show ?thesis
      using Nil Neg(5) STA_Suc by auto
  next
    case (Cons _ left')
    then have ‹A, Suc m ⊢ (p # ps, a) # filter nonempty left' @ right›
      using Neg(4)[where left=‹_ # left'›] Neg(5) by fastforce
    moreover have *: ‹(❙¬ ❙¬ p) at a in (ps, a) # filter nonempty left' @ right›
      using Cons Neg(1, 5) by fastforce
    moreover have ‹new p a ((ps, a) # filter nonempty left' @ right)›
      using Cons Neg(2, 5) unfolding new_def by auto
    ultimately have ‹A, m ⊢ (ps, a) # filter nonempty left' @ right›
      using STA.Neg by fast
    then have ‹A, Suc m ⊢ filter nonempty ((ps, a) # left') @ right›
      using * nonempty_Suc by fast
    then show ?thesis
      using Cons Neg(5) by auto
  qed
next
  case (DisP p q a ps branch n)
  then show ?case
  proof (cases left)
    case Nil
    then have ‹A, Suc m ⊢ (p # ps, a) # branch› ‹A, Suc m ⊢ (q # ps, a) # branch›
      using DisP(5, 7) by fastforce+
    then have ‹A, m ⊢ (ps, a) # branch›
      using DisP(1-3) STA.DisP by fast
    then show ?thesis
      using Nil DisP(8) STA_Suc by auto
  next
    case (Cons _ left')
    then have
      ‹A, Suc m ⊢ (p # ps, a) # filter nonempty left' @ right›
      ‹A, Suc m ⊢ (q # ps, a) # filter nonempty left' @ right›
      using DisP(5, 7)[where left=‹_ # left'›] DisP(8) by fastforce+
    moreover have *: ‹(p ❙∨ q) at a in (ps, a) # filter nonempty left' @ right›
      using Cons DisP(1, 8) by fastforce
    moreover have
      ‹new p a ((ps, a) # filter nonempty left' @ right)›
      ‹new q a ((ps, a) # filter nonempty left' @ right)›
      using Cons DisP(2-3, 8) unfolding new_def by auto
    ultimately have ‹A, m ⊢ (ps, a) # filter nonempty left' @ right›
      using STA.DisP by fast
    then have ‹A, Suc m ⊢ filter nonempty ((ps, a) # left') @ right›
      using * nonempty_Suc by fast
    then show ?thesis
      using Cons DisP(8) by auto
  qed
next
  case (DisN p q a ps branch n)
  then show ?case
  proof (cases left)
    case Nil
    then have ‹A, Suc m ⊢ ((❙¬ q) # (❙¬ p) # ps, a) # branch›
      using DisN(4) by fastforce
    then have ‹A, m ⊢ (ps, a) # branch›
      using DisN(1-2) STA.DisN by fast
    then show ?thesis
      using Nil DisN(5) STA_Suc by auto
  next
    case (Cons _ left')
    then have ‹A, Suc m ⊢ ((❙¬ q) # (❙¬ p) # ps, a) # filter nonempty left' @ right›
      using DisN(4)[where left=‹_ # left'›] DisN(5) by fastforce
    moreover have *: ‹(❙¬ (p ❙∨ q)) at a in (ps, a) # filter nonempty left' @ right›
      using Cons DisN(1, 5) by fastforce
    moreover consider
      ‹new (❙¬ p) a ((ps, a) # filter nonempty left' @ right)› |
      ‹new (❙¬ q) a ((ps, a) # filter nonempty left' @ right)›
      using Cons DisN(2, 5) unfolding new_def by auto
    ultimately have ‹A, m ⊢ (ps, a) # filter nonempty left' @ right›
      using STA.DisN by metis
    then have ‹A, Suc m ⊢ filter nonempty ((ps, a) # left') @ right›
      using * nonempty_Suc by fast
    then show ?thesis
      using Cons DisN(5) by auto
  qed
next
  case (DiaP p a ps branch i n)
  then show ?case
  proof (cases left)
    case Nil
    then have ‹A, Suc m ⊢ ((❙@ i p) # (❙◇ Nom i) # ps, a) # branch›
      using DiaP(6) by fastforce
    then have ‹A, m ⊢ (ps, a) # branch›
      using DiaP(1-4) STA.DiaP by fast
    then show ?thesis
      using Nil DiaP(7) STA_Suc by auto
  next
    case (Cons _ left')
    then have ‹A, Suc m ⊢ ((❙@ i p) # (❙◇ Nom i) # ps, a) # filter nonempty left' @ right›
      using DiaP(6)[where left=‹_ # left'›] DiaP(7) by fastforce
    moreover have *: ‹(❙◇ p) at a in (ps, a) # filter nonempty left' @ right›
      using Cons DiaP(1, 7) by fastforce
    moreover have ‹i ∉ A ∪ branch_nominals ((ps, a) # filter nonempty left' @ right)›
      using Cons DiaP(2, 7) unfolding branch_nominals_def by auto
    moreover have ‹¬ witnessed p a ((ps, a) # filter nonempty left' @ right)›
      using Cons DiaP(4, 7) unfolding witnessed_def by auto
    ultimately have ‹A, m ⊢ (ps, a) # filter nonempty left' @ right›
      using DiaP(3) STA.DiaP by fast
    then have ‹A, Suc m ⊢ filter nonempty ((ps, a) # left') @ right›
      using * nonempty_Suc by fast
    then show ?thesis
      using Cons DiaP(7) by auto
  qed
next
  case (DiaN p a ps branch i n)
  then show ?case
  proof (cases left)
    case Nil
    then have ‹A, Suc m ⊢ ((❙¬ (❙@ i p)) # ps, a) # branch›
      using DiaN(5) by fastforce
    then have ‹A, m ⊢ (ps, a) # branch›
      using DiaN(1-3) STA.DiaN by fast
    then show ?thesis
      using Nil DiaN(6) STA_Suc by auto
  next
    case (Cons _ left')
    then have ‹A, Suc m ⊢ ((❙¬ (❙@ i p)) # ps, a) # filter nonempty left' @ right›
      using DiaN(5)[where left=‹_ # left'›] DiaN(6) by fastforce
    moreover have *: ‹(❙¬ (❙◇ p)) at a in (ps, a) # filter nonempty left' @ right›
      using Cons DiaN(1, 6) by fastforce
    moreover have *: ‹(❙◇ Nom i) at a in (ps, a) # filter nonempty left' @ right›
      using Cons DiaN(2, 6) by fastforce
    moreover have ‹new (❙¬ (❙@ i p)) a ((ps, a) # filter nonempty left' @ right)›
      using Cons DiaN(3, 6) unfolding new_def by auto
    ultimately have ‹A, m ⊢ (ps, a) # filter nonempty left' @ right›
      using STA.DiaN by fast
    then have ‹A, Suc m ⊢ filter nonempty ((ps, a) # left') @ right›
      using * nonempty_Suc by fast
    then show ?thesis
      using Cons DiaN(6) by auto
  qed
next
  case (SatP a p b ps branch n)
  then show ?case
  proof (cases left)
    case Nil
    then have ‹A, Suc m ⊢ (p # ps, a) # branch›
      using SatP(4) by fastforce
    then have ‹A, m ⊢ (ps, a) # branch›
      using SatP(1-2) STA.SatP by fast
    then show ?thesis
      using Nil SatP(5) STA_Suc by auto
  next
    case (Cons _ left')
    then have ‹A, Suc m ⊢ (p # ps, a) # filter nonempty left' @ right›
      using SatP(4)[where left=‹_ # left'›] SatP(5) by fastforce
    moreover have ‹(❙@ a p) at b in (ps, a) # filter nonempty left' @ right›
      using Cons SatP(1, 5) by fastforce
    moreover have ‹new p a ((ps, a) # filter nonempty left' @ right)›
      using Cons SatP(2, 5) unfolding new_def by auto
    ultimately have *: ‹A, m ⊢ (ps, a) # filter nonempty left' @ right›
      using STA.SatP by fast
    then have ‹A, Suc m ⊢ filter nonempty ((ps, a) # left') @ right›
    proof (cases ps)
      case Nil
      then have ‹a ∈ branch_nominals (filter nonempty left' @ right)›
        unfolding branch_nominals_def using SatP(1, 5) Cons by fastforce
      then show ?thesis
        using * Nil GoTo by fastforce
    next
      case Cons
      then show ?thesis
        using * STA_Suc by auto
    qed
    then show ?thesis
      using Cons SatP(5) by auto
  qed
next
  case (SatN a p b ps branch n)
  then show ?case
  proof (cases left)
    case Nil
    then have ‹A, Suc m ⊢ ((❙¬ p) # ps, a) # branch›
      using SatN(4) by fastforce
    then have ‹A, m ⊢ (ps, a) # branch›
      using SatN(1-2) STA.SatN by fast
    then show ?thesis
      using Nil SatN(5) STA_Suc by auto
  next
    case (Cons _ left')
    then have ‹A, Suc m ⊢ ((❙¬ p) # ps, a) # filter nonempty left' @ right›
      using SatN(4)[where left=‹_ # left'›] SatN(5) by fastforce
    moreover have ‹(❙¬ (❙@ a p)) at b in (ps, a) # filter nonempty left' @ right›
      using Cons SatN(1, 5) by fastforce
    moreover have ‹new (❙¬ p) a ((ps, a) # filter nonempty left' @ right)›
      using Cons SatN(2, 5) unfolding new_def by auto
    ultimately have *: ‹A, m ⊢ (ps, a) # filter nonempty left' @ right›
      using STA.SatN by fast
    then have ‹A, Suc m ⊢ filter nonempty ((ps, a) # left') @ right›
    proof (cases ps)
      case Nil
      then have ‹a ∈ branch_nominals (filter nonempty left' @ right)›
        unfolding branch_nominals_def using SatN(1, 5) Cons by fastforce
      then show ?thesis
        using * Nil GoTo by fastforce
    next
      case Cons
      then show ?thesis
        using * STA_Suc by auto
    qed
    then show ?thesis
      using Cons SatN(5) by auto
  qed
next
  case (GoTo i n)
  show ?case
    using GoTo(3)[where left=‹([], i) # left›] by simp
next
  case (Nom p b ps a branch n)
  then show ?case
  proof (cases left)
    case Nil
    then have ‹A, Suc m ⊢ (p # ps, a) # branch›
      using Nom(6) by fastforce
    then have ‹A, m ⊢ (ps, a) # branch›
      using Nom(1-4) STA.Nom by metis
    then show ?thesis
      using Nil Nom(7) STA_Suc by auto
  next
    case (Cons _ left')
    then have ‹A, Suc m ⊢ (p # ps, a) # filter nonempty left' @ right›
      using Nom(6)[where left=‹_ # left'›] Nom(7) by fastforce
    moreover have
      ‹p at b in (ps, a) # filter nonempty left' @ right› and a:
      ‹Nom a at b in (ps, a) # filter nonempty left' @ right›
      using Cons Nom(1-2, 7) by simp_all (metis empty_iff empty_set)+
    moreover have ‹new p a ((ps, a) # filter nonempty left' @ right)›
      using Cons Nom(4, 7) unfolding new_def by auto
    ultimately have *: ‹A, m ⊢ (ps, a) # filter nonempty left' @ right›
      using Nom(3) STA.Nom by metis
    then have ‹A, Suc m ⊢ filter nonempty ((ps, a) # left') @ right›
    proof (cases ps)
      case Nil
      moreover have ‹a ≠ b›
        using Nom(1, 4) unfolding new_def by blast
      ultimately have ‹a ∈ branch_nominals (filter nonempty left' @ right)›
        using a unfolding branch_nominals_def by fastforce
      then show ?thesis
        using * Nil GoTo by auto
    next
      case Cons
      then show ?thesis
        using * STA_Suc by auto
    qed
    then show ?thesis
      using Cons Nom(7) by auto
  qed
qed

theorem STA_potential: ‹A, n ⊢ branch ⟹ A, Suc m ⊢ branch›
  using STA_nonempty[where left=‹[]›] by auto

corollary STA_one: ‹A, n ⊢ branch ⟹ A, 1 ⊢ branch›
  using STA_potential by auto

subsection ‹Free GoTo›

text ‹The above result allows us to prove a version of GoTo that works "for free."›

lemma GoTo':
  assumes ‹A, Suc n ⊢ ([], i) # branch› ‹i ∈ branch_nominals branch›
  shows ‹A, Suc n ⊢ branch›
  using assms GoTo STA_potential by fast

section ‹Indexed Mapping›

text ‹This section contains some machinery for showing admissible rules.›

subsection ‹Indexing›

text ‹
  We use pairs of natural numbers to index into the branch.
  The first component specifies the block and the second specifies the formula on that block.
  We index from the back to ensure that indices are stable
    under the addition of new formulas and blocks.
›

primrec rev_nth :: ‹'a list ⇒ nat ⇒ 'a option› (infixl ‹!.› 100) where
  ‹[] !. v = None›
| ‹(x # xs) !. v = (if length xs = v then Some x else xs !. v)›

lemma rev_nth_last: ‹xs !. 0 = Some x ⟹ last xs = x›
  by (induct xs) auto

lemma rev_nth_zero: ‹(xs @ [x]) !. 0 = Some x›
  by (induct xs) auto

lemma rev_nth_snoc: ‹(xs @ [x]) !. Suc v = Some y ⟹ xs !. v = Some y›
  by (induct xs) auto

lemma rev_nth_Suc: ‹(xs @ [x]) !. Suc v = xs !. v›
  by (induct xs) auto

lemma rev_nth_bounded: ‹v < length xs ⟹ ∃x. xs !. v = Some x›
  by (induct xs) simp_all

lemma rev_nth_Cons: ‹xs !. v = Some y ⟹ (x # xs) !. v = Some y›
proof (induct xs arbitrary: v rule: rev_induct)
  case (snoc a xs)
  then show ?case
  proof (induct v)
    case (Suc v)
    then have ‹xs !. v = Some y›
      using rev_nth_snoc by fast
    then have ‹(x # xs) !. v = Some y›
      using Suc(2) by blast
    then show ?case
      using Suc(3) by auto
  qed simp
qed simp

lemma rev_nth_append: ‹xs !. v = Some y ⟹ (ys @ xs) !. v = Some y›
  using rev_nth_Cons[where xs=‹_ @ xs›] by (induct ys) simp_all

lemma rev_nth_mem: ‹block ∈. branch ⟷ (∃v. branch !. v = Some block)›
proof
  assume ‹block ∈. branch›
  then show ‹∃v. branch !. v = Some block›
  proof (induct branch)
    case (Cons block' branch)
    then show ?case
    proof (cases ‹block = block'›)
      case False
      then have ‹∃v. branch !. v = Some block›
        using Cons by simp
      then show ?thesis
        using rev_nth_Cons by fast
    qed auto
  qed simp
next
  assume ‹∃v. branch !. v = Some block›
  then show ‹block ∈. branch›
  proof (induct branch)
    case (Cons block' branch)
    then show ?case
      by simp (metis option.sel)
  qed simp
qed

lemma rev_nth_on: ‹p on (ps, i) ⟷ (∃v. ps !. v = Some p) ∨ p = Nom i›
  by (simp add: rev_nth_mem)

lemma rev_nth_Some: ‹xs !. v = Some y ⟹ v < length xs›
proof (induct xs arbitrary: v rule: rev_induct)
  case (snoc x xs)
  then show ?case
    by (induct v) (simp_all, metis rev_nth_snoc)
qed simp

lemma index_Cons:
  assumes ‹((ps, a) # branch) !. v = Some (qs, b)› ‹qs !. v' = Some q›
  shows ‹∃qs'. ((p # ps, a) # branch) !. v = Some (qs', b) ∧ qs' !. v' = Some q›
proof -
  have
    ‹((p # ps, a) # branch) !. v = Some (qs, b) ∨
     ((p # ps, a) # branch) !. v = Some (p # qs, b)›
    using assms(1) by auto
  moreover have ‹qs !. v' = Some q› ‹(p # qs) !. v' = Some q›
    using assms(2) rev_nth_Cons by fast+
  ultimately show ?thesis
    by fastforce
qed

subsection ‹Mapping›

primrec mapi :: ‹(nat ⇒ 'a ⇒ 'b) ⇒ 'a list ⇒ 'b list› where
  ‹mapi f [] = []›
| ‹mapi f (x # xs) = f (length xs) x # mapi f xs›

primrec mapi_block ::
  ‹(nat ⇒ ('a, 'b) fm ⇒ ('a, 'b) fm) ⇒ (('a, 'b) block ⇒ ('a, 'b) block)› where
  ‹mapi_block f (ps, i) = (mapi f ps, i)›

definition mapi_branch ::
  ‹(nat ⇒ nat ⇒ ('a, 'b) fm ⇒ ('a, 'b) fm) ⇒ (('a, 'b) branch ⇒ ('a, 'b) branch)› where
  ‹mapi_branch f branch ≡ mapi (λv. mapi_block (f v)) branch›

abbreviation mapper ::
  ‹(('a, 'b) fm ⇒ ('a, 'b) fm) ⇒
   (nat × nat) set ⇒ nat ⇒ nat ⇒ ('a, 'b) fm ⇒ ('a, 'b) fm› where
  ‹mapper f xs v v' p ≡ (if (v, v') ∈ xs then f p else p)›

lemma mapi_block_add_oob:
  assumes ‹length ps ≤ v'›
  shows
    ‹mapi_block (mapper f ({(v, v')} ∪ xs) v) (ps, i) =
     mapi_block (mapper f xs v) (ps, i)›
  using assms by (induct ps) simp_all

lemma mapi_branch_add_oob:
  assumes ‹length branch ≤ v›
  shows
    ‹mapi_branch (mapper f ({(v, v')} ∪ xs)) branch =
     mapi_branch (mapper f xs) branch›
  unfolding mapi_branch_def using assms by (induct branch) simp_all

lemma mapi_branch_head_add_oob:
  ‹mapi_branch (mapper f ({(length branch, length ps)} ∪ xs)) ((ps, a) # branch) =
   mapi_branch (mapper f xs) ((ps, a) # branch)›
  using mapi_branch_add_oob[where branch=branch] unfolding mapi_branch_def
  using mapi_block_add_oob[where ps=ps] by simp

lemma mapi_branch_mem:
  assumes ‹(ps, i) ∈. branch›
  shows ‹∃v. (mapi (f v) ps, i) ∈. mapi_branch f branch›
  unfolding mapi_branch_def using assms by (induct branch) auto

lemma rev_nth_mapi_branch:
  assumes ‹branch !. v = Some (ps, a)›
  shows ‹(mapi (f v) ps, a) ∈. mapi_branch f branch›
  unfolding mapi_branch_def using assms
  by (induct branch) (simp_all, metis mapi_block.simps option.inject)

lemma rev_nth_mapi_block:
  assumes ‹ps !. v' = Some p›
  shows ‹f v' p on (mapi f ps, a)›
  using assms by (induct ps) (simp_all, metis option.sel)

lemma mapi_append:
  ‹mapi f (xs @ ys) = mapi (λv. f (v + length ys)) xs @ mapi f ys›
  by (induct xs) simp_all

lemma mapi_block_id: ‹mapi_block (mapper f {} v) (ps, i) = (ps, i)›
  by (induct ps) auto

lemma mapi_branch_id: ‹mapi_branch (mapper f {}) branch = branch›
  unfolding mapi_branch_def using mapi_block_id by (induct branch) auto

lemma length_mapi: ‹length (mapi f xs) = length xs›
  by (induct xs) auto

lemma mapi_rev_nth:
  assumes ‹xs !. v = Some x›
  shows ‹mapi f xs !. v = Some (f v x)›
  using assms
proof (induct xs arbitrary: v)
  case (Cons y xs)
  have *: ‹mapi f (y # xs) = f (length xs) y # mapi f xs›
    by simp
  show ?case
  proof (cases ‹v = length xs›)
    case True
    then have ‹mapi f (y # xs) !. v = Some (f (length xs) y)›
      using length_mapi * by (metis rev_nth.simps(2))
    then show ?thesis
      using Cons.prems True by auto
  next
    case False
    then show ?thesis
      using * Cons length_mapi by (metis rev_nth.simps(2))
  qed
qed simp

section ‹Duplicate Formulas›

subsection ‹Removable indices›

abbreviation ‹proj ≡ Equiv_Relations.proj›

definition all_is :: ‹('a, 'b) fm ⇒ ('a, 'b) fm list ⇒ nat set ⇒ bool› where
  ‹all_is p ps xs ≡ ∀v ∈ xs. ps !. v = Some p›

definition is_at :: ‹('a, 'b) fm ⇒ 'b ⇒ ('a, 'b) branch ⇒ nat ⇒ nat ⇒ bool› where
  ‹is_at p i branch v v' ≡ ∃ps. branch !. v = Some (ps, i) ∧ ps !. v' = Some p›

text ‹This definition is slightly complicated by the inability to index the opening nominal.›

definition is_elsewhere :: ‹('a, 'b) fm ⇒ 'b ⇒ ('a, 'b) branch ⇒ (nat × nat) set ⇒ bool› where
  ‹is_elsewhere p i branch xs ≡ ∃w w' ps. (w, w') ∉ xs ∧
    branch !. w = Some (ps, i) ∧ (p = Nom i ∨ ps !. w' = Some p)›

definition Dup :: ‹('a, 'b) fm ⇒ 'b ⇒ ('a, 'b) branch ⇒ (nat × nat) set ⇒ bool› where
  ‹Dup p i branch xs ≡ ∀(v, v') ∈ xs.
    is_at p i branch v v' ∧ is_elsewhere p i branch xs›

lemma Dup_all_is:
  assumes ‹Dup p i branch xs› ‹branch !. v = Some (ps, a)›
  shows ‹all_is p ps (proj xs v)›
  using assms unfolding Dup_def is_at_def all_is_def proj_def by auto

lemma Dup_branch:
  ‹Dup p i branch xs ⟹ Dup p i (extra @ branch) xs›
  unfolding Dup_def is_at_def is_elsewhere_def using rev_nth_append by fast

lemma Dup_block:
  assumes ‹Dup p i ((ps, a) # branch) xs›
  shows ‹Dup p i ((ps' @ ps, a) # branch) xs›
  unfolding Dup_def
proof safe
  fix v v'
  assume ‹(v, v') ∈ xs›
  then show ‹is_at p i ((ps' @ ps, a) # branch) v v'›
    using assms rev_nth_append unfolding Dup_def is_at_def by fastforce
next
  fix v v'
  assume ‹(v, v') ∈ xs›
  then obtain w w' qs where
    ‹(w, w') ∉ xs› ‹((ps, a) # branch) !. w = Some (qs, i)›
    ‹p = Nom i ∨ qs !. w' = Some p›
    using assms unfolding Dup_def is_elsewhere_def by blast
  then have
    ‹∃qs. ((ps' @ ps, a) # branch) !. w = Some (qs, i) ∧
     (p = Nom i ∨ qs !. w' = Some p)›
    using rev_nth_append by fastforce
  then show ‹is_elsewhere p i ((ps' @ ps, a) # branch) xs›
    unfolding is_elsewhere_def using ‹(w, w') ∉ xs› by blast
qed

definition only_touches :: ‹'b ⇒ ('a, 'b) branch ⇒ (nat × nat) set ⇒ bool› where
  ‹only_touches i branch xs ≡ ∀(v, v') ∈ xs. ∀ps a. branch !. v = Some (ps, a) ⟶ i = a›

lemma Dup_touches: ‹Dup p i branch xs ⟹ only_touches i branch xs›
  unfolding Dup_def is_at_def only_touches_def by auto

lemma only_touches_opening:
  assumes ‹only_touches i branch xs› ‹(v, v') ∈ xs› ‹branch !. v = Some (ps, a)›
  shows ‹i = a›
  using assms unfolding only_touches_def is_at_def by auto

lemma Dup_head:
  ‹Dup p i ((ps, a) # branch) xs ⟹ Dup p i ((q # ps, a) # branch) xs›
  using Dup_block[where ps'=‹[_]›] by simp

lemma Dup_head_oob':
  assumes ‹Dup p i ((ps, a) # branch) xs›
  shows ‹(length branch, k + length ps) ∉ xs›
  using assms rev_nth_Some unfolding Dup_def is_at_def by fastforce

lemma Dup_head_oob:
  assumes ‹Dup p i ((ps, a) # branch) xs›
  shows ‹(length branch, length ps) ∉ xs›
  using assms Dup_head_oob'[where k=0] by fastforce

subsection ‹Omitting formulas›

primrec omit :: ‹nat set ⇒ ('a, 'b) fm list ⇒ ('a, 'b) fm list› where
  ‹omit xs [] = []›
| ‹omit xs (p # ps) = (if length ps ∈ xs then omit xs ps else p # omit xs ps)›

primrec omit_block :: ‹nat set ⇒ ('a, 'b) block ⇒ ('a, 'b) block› where
  ‹omit_block xs (ps, a) = (omit xs ps, a)›

definition omit_branch :: ‹(nat × nat) set ⇒ ('a, 'b) branch ⇒ ('a, 'b) branch› where
  ‹omit_branch xs branch ≡ mapi (λv. omit_block (proj xs v)) branch›

lemma omit_mem: ‹ps !. v = Some p ⟹ v ∉ xs ⟹ p ∈. omit xs ps›
proof (induct ps)
  case (Cons q ps)
  then show ?case
    by (cases ‹v = length ps›) simp_all
qed simp

lemma omit_id: ‹omit {} ps = ps›
  by (induct ps) auto

lemma omit_block_id: ‹omit_block {} block = block›
  using omit_id by (cases block) simp

lemma omit_branch_id: ‹omit_branch {} branch = branch›
  unfolding omit_branch_def proj_def using omit_block_id
  by (induct branch) fastforce+

lemma omit_branch_mem_diff_opening:
  assumes ‹only_touches i branch xs› ‹(ps, a) ∈. branch› ‹i ≠ a›
  shows ‹(ps, a) ∈. omit_branch xs branch›
proof -
  obtain v where v: ‹branch !. v = Some (ps, a)›
    using assms(2) rev_nth_mem by fast
  then have ‹omit_branch xs branch !. v = Some (omit (proj xs v) ps, a)›
    unfolding omit_branch_def by (simp add: mapi_rev_nth)
  then have *: ‹(omit (proj xs v) ps, a) ∈. omit_branch xs branch›
    using rev_nth_mem by fast
  moreover have ‹proj xs v = {}›
    unfolding proj_def using assms(1, 3) v only_touches_opening by fast
  then have ‹omit (proj xs v) ps = ps›
    using omit_id by auto
  ultimately show ?thesis
    by simp
qed

lemma Dup_omit_branch_mem_same_opening:
  assumes ‹Dup p i branch xs› ‹p at i in branch›
  shows ‹p at i in omit_branch xs branch›
proof -
  obtain ps where ps: ‹(ps, i) ∈. branch› ‹p on (ps, i)›
    using assms(2) by blast
  then obtain v where v: ‹branch !. v = Some (ps, i)›
    using rev_nth_mem by fast
  then have ‹omit_branch xs branch !. v = Some (omit (proj xs v) ps, i)›
    unfolding omit_branch_def by (simp add: mapi_rev_nth)
  then have *: ‹(omit (proj xs v) ps, i) ∈. omit_branch xs branch›
    using rev_nth_mem by fast

  consider
    v' where ‹ps !. v' = Some p› ‹(v, v') ∈ xs› |
    v' where ‹ps !. v' = Some p› ‹(v, v') ∉ xs› |
    ‹p = Nom i›
    using ps v rev_nth_mem by fastforce
  then show ?thesis
  proof cases
    case (1 v')
    then obtain qs w w' where qs:
      ‹(w, w') ∉ xs› ‹branch !. w = Some (qs, i)› ‹p = Nom i ∨ qs !. w' = Some p›
      using assms(1) unfolding Dup_def is_elsewhere_def by blast
    then have ‹omit_branch xs branch !. w = Some (omit (proj xs w) qs, i)›
      unfolding omit_branch_def by (simp add: mapi_rev_nth)
    then have ‹(omit (proj xs w) qs, i) ∈. omit_branch xs branch›
      using rev_nth_mem by fast
    moreover have ‹p on (omit (proj xs w) qs, i)›
      unfolding proj_def using qs(1, 3) omit_mem by fastforce
    ultimately show ?thesis
      by blast
  next
    case (2 v')
    then show ?thesis
      using * omit_mem unfolding proj_def
      by (metis Image_singleton_iff on.simps)
  next
    case 3
    then show ?thesis
      using * by auto
  qed
qed

lemma omit_del:
  assumes ‹p ∈. ps› ‹p ∉ set (omit xs ps)›
  shows ‹∃v. ps !. v = Some p ∧ v ∈ xs›
  using assms omit_mem rev_nth_mem by metis

lemma omit_all_is:
  assumes ‹all_is p ps xs› ‹q ∈. ps› ‹q ∉ set (omit xs ps)›
  shows ‹q = p›
  using assms omit_del unfolding all_is_def by fastforce

definition all_is_branch :: ‹('a, 'b) fm ⇒ 'b ⇒ ('a, 'b) branch ⇒ (nat × nat) set ⇒ bool› where
  ‹all_is_branch p i branch xs ≡ ∀(v, v') ∈ xs. v < length branch ⟶ is_at p i branch v v'›

lemma all_is_branch:
  ‹all_is_branch p i branch xs ⟹ branch !. v = Some (ps, a) ⟹ all_is p ps (proj xs v)›
  unfolding all_is_branch_def is_at_def all_is_def proj_def using rev_nth_Some by fastforce

lemma Dup_all_is_branch: ‹Dup p i branch xs ⟹ all_is_branch p i branch xs›
  unfolding all_is_branch_def Dup_def by fast

lemma omit_branch_mem_diff_formula:
  assumes ‹all_is_branch p i branch xs› ‹q at i in branch› ‹p ≠ q›
  shows ‹q at i in omit_branch xs branch›
proof -
  obtain ps where ps: ‹(ps, i) ∈. branch› ‹q on (ps, i)›
    using assms(2) by blast
  then obtain v where v: ‹branch !. v = Some (ps, i)›
    using rev_nth_mem by fast
  then have ‹omit_branch xs branch !. v = Some (omit (proj xs v) ps, i)›
    unfolding omit_branch_def by (simp add: mapi_rev_nth)
  then have *: ‹(omit (proj xs v) ps, i) ∈. omit_branch xs branch›
    using rev_nth_mem by fast
  moreover have ‹all_is p ps (proj xs v)›
    using assms(1) v all_is_branch by fast
  then have ‹q on (omit (proj xs v) ps, i)›
    using ps assms(3) omit_all_is by auto
  ultimately show ?thesis
    by blast
qed

lemma Dup_omit_branch_mem:
  assumes ‹Dup p i branch xs› ‹q at a in branch›
  shows ‹q at a in omit_branch xs branch›
  using assms omit_branch_mem_diff_opening Dup_touches Dup_omit_branch_mem_same_opening
    omit_branch_mem_diff_formula Dup_all_is_branch by fast

lemma omit_set: ‹set (omit xs ps) ⊆ set ps›
  by (induct ps) auto

lemma on_omit: ‹p on (omit xs ps, i) ⟹ p on (ps, i)›
  using omit_set by auto

lemma all_is_set:
  assumes ‹all_is p ps xs›
  shows ‹{p} ∪ set (omit xs ps) = {p} ∪ set ps›
  using assms omit_all_is omit_set unfolding all_is_def by fast

lemma all_is_list_nominals:
  assumes ‹all_is p ps xs›
  shows ‹nominals p ∪ list_nominals (omit xs ps) = nominals p ∪ list_nominals ps›
  using assms all_is_set by fastforce

lemma all_is_block_nominals:
  assumes ‹all_is p ps xs›
  shows ‹nominals p ∪ block_nominals (omit xs ps, i) = nominals p ∪ block_nominals (ps, i)›
  using assms by (simp add: all_is_list_nominals)

lemma all_is_branch_nominals':
  assumes ‹all_is_branch p i branch xs›
  shows
    ‹nominals p ∪ branch_nominals (omit_branch xs branch) =
     nominals p ∪ branch_nominals branch›
proof -
  have ‹∀(v, v') ∈ xs. v < length branch ⟶ is_at p i branch v v'›
    using assms unfolding all_is_branch_def is_at_def by auto
  then show ?thesis
  proof (induct branch)
    case Nil
    then show ?case
      unfolding omit_branch_def by simp
  next
    case (Cons block branch)
    then show ?case
    proof (cases block)
      case (Pair ps a)
      have ‹∀(v, v') ∈ xs. v < length branch ⟶ is_at p i branch v v'›
        using Cons(2) rev_nth_Cons unfolding is_at_def by auto
      then have
        ‹nominals p ∪ branch_nominals (omit_branch xs branch) =
         nominals p ∪ branch_nominals branch›
        using Cons(1) by blast
      then have
        ‹nominals p ∪ branch_nominals (omit_branch xs ((ps, a) # branch)) =
         nominals p ∪ block_nominals (omit (proj xs (length branch)) ps, a) ∪
          branch_nominals branch›
        unfolding branch_nominals_def omit_branch_def by auto
      moreover have ‹all_is p ps (proj xs (length branch))›
        using Cons(2) Pair unfolding proj_def all_is_def is_at_def by auto
      then have
        ‹nominals p ∪ block_nominals (omit (proj xs (length branch)) ps, a) =
         nominals p ∪ block_nominals (ps, a)›
        using all_is_block_nominals by fast
      then have
        ‹nominals p ∪ block_nominals (omit_block (proj xs (length branch)) (ps, a)) =
         nominals p ∪ block_nominals (ps, a)›
        by simp
      ultimately have
        ‹nominals p ∪ branch_nominals (omit_branch xs ((ps, a) # branch)) =
          nominals p ∪ block_nominals (ps, a) ∪ branch_nominals branch›
        by auto
      then show ?thesis
        unfolding branch_nominals_def using Pair by auto
    qed
  qed
qed

lemma Dup_branch_nominals:
  assumes ‹Dup p i branch xs›
  shows ‹branch_nominals (omit_branch xs branch) = branch_nominals branch›
proof (cases ‹xs = {}›)
  case True
  then show ?thesis
    using omit_branch_id by metis
next
  case False
  with assms obtain ps w w' where
    ‹(w, w') ∉ xs› ‹branch !. w = Some (ps, i)› ‹p = Nom i ∨ ps !. w' = Some p›
    unfolding Dup_def is_elsewhere_def by fast
  then have *: ‹(ps, i) ∈. branch› ‹p on (ps, i)›
    using rev_nth_mem rev_nth_on by fast+
  then have ‹nominals p ⊆ branch_nominals branch›
    unfolding branch_nominals_def using block_nominals by fast
  moreover obtain ps' where
    ‹(ps', i) ∈. omit_branch xs branch› ‹p on (ps', i)›
    using assms * Dup_omit_branch_mem by fast
  then have ‹nominals p ⊆ branch_nominals (omit_branch xs branch)›
    unfolding branch_nominals_def using block_nominals by fast
  moreover have
    ‹nominals p ∪ branch_nominals (omit_branch xs branch) =
     nominals p ∪ branch_nominals branch›
    using assms all_is_branch_nominals' Dup_all_is_branch by fast
  ultimately show ?thesis
    by blast
qed

lemma omit_branch_mem_dual:
  assumes ‹p at i in omit_branch xs branch›
  shows ‹p at i in branch›
proof -
  obtain ps where ps: ‹(ps, i) ∈. omit_branch xs branch› ‹p on (ps, i)›
    using assms(1) by blast
  then obtain v where v: ‹omit_branch xs branch !. v = Some (ps, i)›
    using rev_nth_mem unfolding omit_branch_def by fast
  then have ‹v < length (omit_branch xs branch)›
    using rev_nth_Some by fast
  then have ‹v < length branch›
    unfolding omit_branch_def using length_mapi by metis
  then obtain ps' i' where ps': ‹branch !. v = Some (ps', i')›
    using rev_nth_bounded by (metis surj_pair)
  then have ‹omit_branch xs branch !. v = Some (omit (proj xs v) ps', i')›
    unfolding omit_branch_def by (simp add: mapi_rev_nth)
  then have ‹ps = omit (proj xs v) ps'› ‹i = i'›
    using v by simp_all
  then have ‹p on (ps', i)›
    using ps omit_set by auto
  moreover have ‹(ps', i) ∈. branch›
    using ps' ‹i = i'› rev_nth_mem by fast
  ultimately show ?thesis
    using ‹ps = omit (proj xs v) ps'› by blast
qed

lemma witnessed_omit_branch:
  assumes ‹witnessed p a (omit_branch xs branch)›
  shows ‹witnessed p a branch›
proof -
  obtain ps qs i where
    ps: ‹(ps, a) ∈. omit_branch xs branch› ‹(❙@ i p) on (ps, a)› and
    qs: ‹(qs, a) ∈. omit_branch xs branch› ‹(❙◇ Nom i) on (qs, a)›
    using assms unfolding witnessed_def by blast
  from ps obtain ps' where
    ‹(ps', a) ∈. branch› ‹(❙@ i p) on (ps', a)›
    using omit_branch_mem_dual by fast
  moreover from qs obtain qs' where
    ‹(qs', a) ∈. branch› ‹(❙◇ Nom i) on (qs', a)›
    using omit_branch_mem_dual by fast
  ultimately show ?thesis
    unfolding witnessed_def by blast
qed

lemma new_omit_branch:
  assumes ‹new p a branch›
  shows ‹new p a (omit_branch xs branch)›
  using assms omit_branch_mem_dual unfolding new_def by fast

lemma omit_oob:
  assumes ‹length ps ≤ v›
  shows ‹omit ({v} ∪ xs) ps = omit xs ps›
  using assms by (induct ps) simp_all

lemma omit_branch_oob:
  assumes ‹length branch ≤ v›
  shows ‹omit_branch ({(v, v')} ∪ xs) branch = omit_branch xs branch›
  using assms
proof (induct branch)
  case Nil
  then show ?case
    unfolding omit_branch_def by simp
next
  case (Cons block branch)
  let ?xs = ‹({(v, v')} ∪ xs)›
  show ?case
  proof (cases block)
    case (Pair ps a)
    then have
      ‹omit_branch ?xs ((ps, a) # branch) =
        (omit (proj ?xs (length branch)) ps, a) # omit_branch xs branch›
      using Cons unfolding omit_branch_def by simp
    moreover have ‹proj ?xs (length branch) = proj xs (length branch)›
      using Cons(2) unfolding proj_def by auto
    ultimately show ?thesis
      unfolding omit_branch_def by simp
  qed
qed

subsection ‹Induction›

lemma STA_Dup:
  assumes ‹A, n ⊢ branch› ‹Dup q i branch xs›
  shows ‹A, n ⊢ omit_branch xs branch›
  using assms
proof (induct n branch)
  case (Close p i' branch n)
  have ‹p at i' in omit_branch xs branch›
    using Close(1, 3) Dup_omit_branch_mem by fast
  moreover have ‹(❙¬ p) at i' in omit_branch xs branch›
    using Close(2, 3) Dup_omit_branch_mem by fast
  ultimately show ?case
    using STA.Close by fast
next
  case (Neg p a ps branch n)
  have ‹A, Suc n ⊢ omit_branch xs ((p # ps, a) # branch)›
    using Neg(4-) Dup_head by fast
  moreover have ‹(length branch, length ps) ∉ xs›
    using Neg(5) Dup_head_oob by fast
  ultimately have
    ‹A, Suc n ⊢ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch›
    unfolding omit_branch_def proj_def by simp
  moreover have ‹(❙¬ ❙¬ p) at a in omit_branch xs ((ps, a) # branch)›
    using Neg(1, 5) Dup_omit_branch_mem by fast
  moreover have ‹new p a (omit_branch xs ((ps, a) # branch))›
    using Neg(2) new_omit_branch by fast
  ultimately show ?case
    by (simp add: omit_branch_def STA.Neg)
next
  case (DisP p q a ps branch n)
  have
    ‹A, Suc n ⊢ omit_branch xs ((p # ps, a) # branch)›
    ‹A, Suc n ⊢ omit_branch xs ((q # ps, a) # branch)›
    using DisP(4-) Dup_head by fast+
  moreover have ‹(length branch, length ps) ∉ xs›
    using DisP(8) Dup_head_oob by fast
  ultimately have
    ‹A, Suc n ⊢ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch›
    ‹A, Suc n ⊢ (q # omit (proj xs (length branch)) ps, a) # omit_branch xs branch›
    unfolding omit_branch_def proj_def by simp_all
  moreover have ‹(p ❙∨ q) at a in omit_branch xs ((ps, a) # branch)›
    using DisP(1, 8) Dup_omit_branch_mem by fast
  moreover have ‹new p a (omit_branch xs ((ps, a) # branch))›
    using DisP(2) new_omit_branch by fast
  moreover have ‹new q a (omit_branch xs ((ps, a) # branch))›
    using DisP(3) new_omit_branch by fast
  ultimately show ?case
    by (simp add: omit_branch_def STA.DisP)
next
  case (DisN p q a ps branch n)
  have ‹A, Suc n ⊢ omit_branch xs (((❙¬ q) # (❙¬ p) # ps, a) # branch)›
    using DisN(4-) Dup_block[where ps'=‹[_, _]›] by fastforce
  moreover have ‹(length branch, length ps) ∉ xs›
    using DisN(5) Dup_head_oob by fast
  moreover have ‹(length branch, 1 + length ps) ∉ xs›
    using DisN(5) Dup_head_oob' by fast
  ultimately have
    ‹A, Suc n ⊢ ((❙¬ q) # (❙¬ p) # omit (proj xs (length branch)) ps, a) #
      omit_branch xs branch›
    unfolding omit_branch_def proj_def by simp
  moreover have ‹(❙¬ (p ❙∨ q)) at a in omit_branch xs ((ps, a) # branch)›
    using DisN(1, 5) Dup_omit_branch_mem by fast
  moreover have
    ‹new (❙¬ p) a (omit_branch xs ((ps, a) # branch)) ∨
     new (❙¬ q) a (omit_branch xs ((ps, a) # branch))›
    using DisN(2) new_omit_branch by fast
  ultimately show ?case
    by (simp add: omit_branch_def STA.DisN)
next
  case (DiaP p a ps branch i n)
  have ‹A, Suc n ⊢ omit_branch xs (((❙@ i p) # (❙◇ Nom i) # ps, a) # branch)›
    using DiaP(4-) Dup_block[where ps'=‹[_, _]›] by fastforce
  moreover have ‹(length branch, length ps) ∉ xs›
    using DiaP(7) Dup_head_oob by fast
  moreover have ‹(length branch, 1+ length ps) ∉ xs›
    using DiaP(7) Dup_head_oob' by fast
  ultimately have
    ‹A, Suc n ⊢ ((❙@ i p) # (❙◇ Nom i) # omit (proj xs (length branch)) ps, a) #
      omit_branch xs branch›
    unfolding omit_branch_def proj_def by simp
  moreover have ‹(❙◇ p) at a in omit_branch xs ((ps, a) # branch)›
    using DiaP(1, 7) Dup_omit_branch_mem by fast
  moreover have ‹i ∉ A ∪ branch_nominals (omit_branch xs ((ps, a) # branch))›
    using DiaP(2, 7) Dup_branch_nominals by fast
  moreover have ‹¬ witnessed p a (omit_branch xs ((ps, a) # branch))›
    using DiaP(4) witnessed_omit_branch by fast
  ultimately show ?case
    using DiaP(3) by (simp add: omit_branch_def STA.DiaP)
next
  case (DiaN p a ps branch i n)
  have ‹A, Suc n ⊢ omit_branch xs (((❙¬ (❙@ i p)) # ps, a) # branch)›
    using DiaN(4-) Dup_head by fast
  moreover have ‹(length branch, length ps) ∉ xs›
    using DiaN(6) Dup_head_oob by fast
  ultimately have
    ‹A, Suc n ⊢ ((❙¬ (❙@ i p)) # omit (proj xs (length branch)) ps, a) #
      omit_branch xs branch›
    unfolding omit_branch_def proj_def by simp
  moreover have ‹(❙¬ (❙◇ p)) at a in omit_branch xs ((ps, a) # branch)›
    using DiaN(1, 6) Dup_omit_branch_mem by fast
  moreover have ‹(❙◇ Nom i) at a in omit_branch xs ((ps, a) # branch)›
    using DiaN(2, 6) Dup_omit_branch_mem by fast
  moreover have ‹new (❙¬ (❙@ i p)) a (omit_branch xs ((ps, a) # branch))›
    using DiaN(3) new_omit_branch by fast
  ultimately show ?case
    by (simp add: omit_branch_def STA.DiaN)
next
  case (SatP a p b ps branch n)
  have ‹A, Suc n ⊢ omit_branch xs ((p # ps, a) # branch)›
    using SatP(4-) Dup_head by fast
  moreover have ‹(length branch, length ps) ∉ xs›
    using SatP(5) Dup_head_oob by fast
  ultimately have
    ‹A, Suc n ⊢ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch›
    unfolding omit_branch_def proj_def by simp
  moreover have ‹(❙@ a p) at b in omit_branch xs ((ps, a) # branch)›
    using SatP(1, 5) Dup_omit_branch_mem by fast
  moreover have ‹new p a (omit_branch xs ((ps, a) # branch))›
    using SatP(2) new_omit_branch by fast
  ultimately show ?case
    by (simp add: omit_branch_def STA.SatP)
next
  case (SatN a p b ps branch n)
  have ‹A, Suc n ⊢ omit_branch xs (((❙¬ p) # ps, a) # branch)›
    using SatN(4-) Dup_head by fast
  moreover have ‹(length branch, length ps) ∉ xs›
    using SatN(5) Dup_head_oob by fast
  ultimately have
    ‹A, Suc n ⊢ ((❙¬ p) # omit (proj xs (length branch)) ps, a) # omit_branch xs branch›
    unfolding omit_branch_def proj_def by simp
  moreover have ‹(❙¬ (❙@ a p)) at b in omit_branch xs ((ps, a) # branch)›
    using SatN(1, 5) Dup_omit_branch_mem by fast
  moreover have ‹new (❙¬ p) a (omit_branch xs ((ps, a) # branch))›
    using SatN(2) new_omit_branch by fast
  ultimately show ?case
    by (simp add: omit_branch_def STA.SatN)
next
  case (GoTo i branch n)
  then have ‹A, n ⊢ omit_branch xs (([], i) # branch)›
    using Dup_branch[where extra=‹[([], i)]›] by fastforce
  then have ‹A, n ⊢ ([], i) # omit_branch xs branch›
    unfolding omit_branch_def by simp
  moreover have ‹i ∈ branch_nominals (omit_branch xs branch)›
    using GoTo(1, 4) Dup_branch_nominals by fast
  ultimately show ?case
    unfolding omit_branch_def by (simp add: STA.GoTo)
next
  case (Nom p b ps a branch n)
  have ‹A, Suc n ⊢ omit_branch xs ((p # ps, a) # branch)›
    using Nom(4-) Dup_head by fast
  moreover have ‹(length branch, length ps) ∉ xs›
    using Nom(7) Dup_head_oob by fast
  ultimately have
    ‹A, Suc n ⊢ (p # omit (proj xs (length branch)) ps, a) # omit_branch xs branch›
    unfolding omit_branch_def proj_def by simp
  moreover have ‹p at b in omit_branch xs ((ps, a) # branch)›
    using Nom(1, 7) Dup_omit_branch_mem by fast
  moreover have ‹Nom a at b in omit_branch xs ((ps, a) # branch)›
    using Nom(2, 7) Dup_omit_branch_mem by fast
  moreover have ‹new p a (omit_branch xs ((ps, a) # branch))›
    using Nom(4) new_omit_branch by fast
  ultimately show ?case
    using Nom(3) by (simp add: omit_branch_def STA.Nom)
qed

theorem Dup:
  assumes ‹A, n ⊢ (p # ps, a) # branch› ‹¬ new p a ((ps, a) # branch)›
  shows ‹A, n ⊢ (ps, a) # branch›
proof -
  obtain qs where qs:
    ‹(qs, a) ∈. (ps, a) # branch› ‹p on (qs, a)›
    using assms(2) unfolding new_def by blast

  let ?xs = ‹{(length branch, length ps)}›

  have *: ‹is_at p a ((p # ps, a) # branch) (length branch) (length ps)›
    unfolding is_at_def by simp

  have ‹Dup p a ((p # ps, a) # branch) ?xs›
  proof (cases ‹p = Nom a›)
    case True
    moreover have ‹((p # ps, a) # branch) !. length branch = Some (p # ps, a)›
      by simp
    moreover have ‹p on (p # ps, a)›
      by simp
    ultimately have ‹is_elsewhere p a ((p # ps, a) # branch) ?xs›
      unfolding is_elsewhere_def using assms(2) rev_nth_Some
      by (metis (mono_tags, lifting) Pair_inject less_le singletonD)
    then show ?thesis
      unfolding Dup_def using * by blast
  next
    case false: False
    then show ?thesis
    proof (cases ‹ps = qs›)
      case True
      then obtain w' where w': ‹qs !. w' = Some p›
        using qs(2) false rev_nth_mem by fastforce
      then have ‹(p # ps) !. w' = Some p›
        using True rev_nth_Cons by fast
      moreover have ‹((p # ps, a) # branch) !. length branch = Some (p # ps, a)›
        by simp
      moreover have ‹(length branch, w') ∉ ?xs›
        using True w' rev_nth_Some by fast
      ultimately have ‹is_elsewhere p a ((p # ps, a) # branch) ?xs›
        unfolding is_elsewhere_def by fast
      then show ?thesis
        unfolding Dup_def using * by fast
    next
      case False
      then obtain w where w: ‹branch !. w = Some (qs, a)›
        using qs(1) rev_nth_mem by fastforce
      moreover obtain w' where w': ‹qs !. w' = Some p›
        using qs(2) false rev_nth_mem by fastforce
      moreover have ‹(w, w') ∉ ?xs›
        using rev_nth_Some w by fast
      ultimately have ‹is_elsewhere p a ((p # ps, a) # branch) ?xs›
        unfolding is_elsewhere_def using rev_nth_Cons by fast
      then show ?thesis
        unfolding Dup_def using * by fast
    qed
  qed

  then have ‹A, n ⊢ omit_branch ?xs ((p # ps, a) # branch)›
    using assms(1) STA_Dup by fast
  then have ‹A, n ⊢ (omit (proj ?xs (length branch)) ps, a) # omit_branch ?xs branch›
    unfolding omit_branch_def proj_def by simp
  moreover have ‹omit_branch ?xs branch = omit_branch {} branch›
    using omit_branch_oob by auto
  then have ‹omit_branch ?xs branch = branch›
    using omit_branch_id by simp
  moreover have ‹proj ?xs (length branch) = {length ps}›
    unfolding proj_def by blast
  then have ‹omit (proj ?xs (length branch)) ps = omit {} ps›
    using omit_oob by auto
  then have ‹omit (proj ?xs (length branch)) ps = ps›
    using omit_id by simp
  ultimately show ?thesis
    by simp
qed

subsection ‹Unrestricted rules›

lemma STA_add: ‹A, n ⊢ branch ⟹ A, m + n ⊢ branch›
  using STA_Suc by (induct m) auto

lemma STA_le: ‹A, n ⊢ branch ⟹ n ≤ m ⟹ A, m ⊢ branch›
  using STA_add by (metis le_add_diff_inverse2)

lemma Neg':
  assumes
    ‹(❙¬ ❙¬ p) at a in (ps, a) # branch›
    ‹A, n ⊢ (p # ps, a) # branch›
  shows ‹A, n ⊢ (ps, a) # branch›
  using assms Neg Dup STA_Suc by metis

lemma DisP':
  assumes
    ‹(p ❙∨ q) at a in (ps, a) # branch›
    ‹A, n ⊢ (p # ps, a) # branch› ‹A, n ⊢ (q # ps, a) # branch›
  shows ‹A, n ⊢ (ps, a) # branch›
proof (cases ‹new p a ((ps, a) # branch) ∧ new q a ((ps, a) # branch)›)
  case True
  moreover have ‹A, Suc n ⊢ (p # ps, a) # branch› ‹A,  Suc n ⊢ (q # ps, a) # branch›
    using assms(2-3) STA_Suc by fast+
  ultimately show ?thesis
    using assms(1) DisP by fast
next
  case False
  then show ?thesis
    using assms Dup by fast
qed

lemma DisP'':
  assumes
    ‹(p ❙∨ q) at a in (ps, a) # branch›
    ‹A, n ⊢ (p # ps, a) # branch› ‹A, m ⊢ (q # ps, a) # branch›
  shows ‹A, max n m ⊢ (ps, a) # branch›
proof (cases ‹n ≤ m›)
  case True
  then have ‹A, m ⊢ (p # ps, a) # branch›
    using assms(2) STA_le by blast
  then show ?thesis
    using assms True by (simp add: DisP' max.absorb2)
next
  case False
  then have ‹A, n ⊢ (q # ps, a) # branch›
    using assms(3) STA_le by fastforce
  then show ?thesis
    using assms False by (simp add: DisP' max.absorb1)
qed

lemma DisN':
  assumes
    ‹(❙¬ (p ❙∨ q)) at a in (ps, a) # branch›
    ‹A, n ⊢ ((❙¬ q) # (❙¬ p) # ps, a) # branch›
  shows ‹A, n ⊢ (ps, a) # branch›
proof (cases ‹new (❙¬ q) a ((ps, a) # branch) ∨ new (❙¬ p) a ((ps, a) # branch)›)
  case True
  then show ?thesis
    using assms DisN STA_Suc by fast
next
  case False
  then show ?thesis
    using assms Dup
    by (metis (no_types, lifting) list.set_intros(1-2) new_def on.simps set_ConsD)
qed

lemma DiaP':
  assumes
    ‹(❙◇ p) at a in (ps, a) # branch›
    ‹i ∉ A ∪ branch_nominals ((ps, a) # branch)›
    ‹∄a. p = Nom a›
    ‹¬ witnessed p a ((ps, a) # branch)›
    ‹A, n ⊢ ((❙@ i p) # (❙◇ Nom i) # ps, a) # branch›
  shows ‹A, n ⊢ (ps, a) # branch›
  using assms DiaP STA_Suc by fast

lemma DiaN':
  assumes
    ‹(❙¬ (❙◇ p)) at a in (ps, a) # branch›
    ‹(❙◇ Nom i) at a in (ps, a) # branch›
    ‹A, n ⊢ ((❙¬ (❙@ i p)) # ps, a) # branch›
  shows ‹A, n ⊢ (ps, a) # branch›
  using assms DiaN Dup STA_Suc by fast

lemma SatP':
  assumes
    ‹(❙@ a p) at b in (ps, a) # branch›
    ‹A, n ⊢ (p # ps, a) # branch›
  shows ‹A, n ⊢ (ps, a) # branch›
  using assms SatP Dup STA_Suc by fast

lemma SatN':
  assumes
    ‹(❙¬ (❙@ a p)) at b in (ps, a) # branch›
    ‹A, n ⊢ ((❙¬ p) # ps, a) # branch›
  shows ‹A, n ⊢ (ps, a) # branch›
  using assms SatN Dup STA_Suc by fast

lemma Nom':
  assumes
    ‹p at b in (ps, a) # branch›
    ‹Nom a at b in (ps, a) # branch›
    ‹∀i. p = Nom i ∨ p = (❙◇ Nom i) ⟶ i ∈ A›
    ‹A, n ⊢ (p # ps, a) # branch›
  shows ‹A, n ⊢ (ps, a) # branch›
proof (cases ‹new p a ((ps, a) # branch)›)
  case True
  moreover have ‹A, Suc n ⊢ (p # ps, a) # branch›
    using assms(4) STA_Suc by blast
  ultimately show ?thesis
    using assms(1-3) Nom by metis
next
  case False
  then show ?thesis
    using assms Dup by fast
qed

section ‹Substitution›

lemma finite_nominals: ‹finite (nominals p)›
  by (induct p) simp_all

lemma finite_block_nominals: ‹finite (block_nominals block)›
  using finite_nominals by (induct block) auto

lemma finite_branch_nominals: ‹finite (branch_nominals branch)›
  unfolding branch_nominals_def by (induct branch) (auto simp: finite_block_nominals)

abbreviation sub_list :: ‹('b ⇒ 'c) ⇒ ('a, 'b) fm list ⇒ ('a, 'c) fm list› where
  ‹sub_list f ps ≡ map (sub f) ps›

primrec sub_block :: ‹('b ⇒ 'c) ⇒ ('a, 'b) block ⇒ ('a, 'c) block› where
  ‹sub_block f (ps, i) = (sub_list f ps, f i)›

definition sub_branch :: ‹('b ⇒ 'c) ⇒ ('a, 'b) branch ⇒ ('a, 'c) branch› where
  ‹sub_branch f blocks ≡ map (sub_block f) blocks›

lemma sub_block_mem: ‹p on block ⟹ sub f p on sub_block f block›
  by (induct block) auto

lemma sub_branch_mem:
  assumes ‹(ps, i) ∈. branch›
  shows ‹(sub_list f ps, f i) ∈. sub_branch f branch›
  unfolding sub_branch_def using assms image_iff by fastforce

lemma sub_block_nominals: ‹block_nominals (sub_block f block) = f ` block_nominals block›
  by (induct block) (auto simp: sub_nominals)

lemma sub_branch_nominals:
  ‹branch_nominals (sub_branch f branch) = f ` branch_nominals branch›
  unfolding branch_nominals_def sub_branch_def
  by (induct branch) (auto simp: sub_block_nominals)

lemma sub_list_id: ‹sub_list id ps = ps›
  using sub_id by (induct ps) auto

lemma sub_block_id: ‹sub_block id block = block›
  using sub_list_id by (induct block) auto

lemma sub_branch_id: ‹sub_branch id branch = branch›
  unfolding sub_branch_def using sub_block_id by (induct branch) auto

lemma sub_block_upd_fresh:
  assumes ‹i ∉ block_nominals block›
  shows ‹sub_block (f(i := j)) block = sub_block f block›
  using assms by (induct block) (auto simp add: sub_upd_fresh)

lemma sub_branch_upd_fresh:
  assumes ‹i ∉ branch_nominals branch›
  shows ‹sub_branch (f(i := j)) branch = sub_branch f branch›
  using assms unfolding branch_nominals_def sub_branch_def
  by (induct branch) (auto simp: sub_block_upd_fresh)

lemma sub_comp: ‹sub f (sub g p) = sub (f o g) p›
  by (induct p) simp_all

lemma sub_list_comp: ‹sub_list f (sub_list g ps) = sub_list (f o g) ps›
  using sub_comp by (induct ps) auto

lemma sub_block_comp: ‹sub_block f (sub_block g block) = sub_block (f o g) block›
  using sub_list_comp by (induct block) simp_all

lemma sub_branch_comp:
  ‹sub_branch f (sub_branch g branch) = sub_branch (f o g) branch›
  unfolding sub_branch_def using sub_block_comp by (induct branch) fastforce+

lemma swap_id: ‹(id(i := j, j := i)) o (id(i := j, j := i)) = id›
  by auto

lemma at_in_sub_branch:
  assumes ‹p at i in (ps, a) # branch›
  shows ‹sub f p at f i in (sub_list f ps, f a) # sub_branch f branch›
  using assms sub_branch_mem by fastforce

lemma sub_still_allowed:
  assumes ‹∀i. p = Nom i ∨ p = (❙◇ Nom i) ⟶ i ∈ A›
  shows ‹sub f p = Nom i ∨ sub f p = (❙◇ Nom i) ⟶ i ∈ f ` A›
proof safe
  assume ‹sub f p = Nom i›
  then obtain i' where i': ‹p = Nom i'› ‹f i' = i›
    by (cases p) simp_all
  then have ‹i' ∈ A›
    using assms by fast
  then show ‹i ∈ f ` A›
    using i' by fast
next
  assume ‹sub f p = (❙◇ Nom i)›
  then obtain i' where i': ‹p = (❙◇ Nom i')› ‹f i' = i›
  proof (induct p)
    case (Dia q)
    then show ?case
      by (cases q) simp_all
  qed simp_all
  then have ‹i' ∈ A›
    using assms by fast
  then show ‹i ∈ f ` A›
    using i' by fast
qed

text ‹
  If a branch has a closing tableau then so does any branch obtained by renaming nominals
    as long as the substitution leaves some nominals free.
  This is always the case for substitutions that do not change the type of nominals.
  Since some formulas on the renamed branch may no longer be new, they do not contribute any
    potential and so we existentially quantify over the potential needed to close the new branch.
  We assume that the set of allowed nominals ‹A› is finite such that we can obtain a free nominal.
›

lemma STA_sub':
  fixes f :: ‹'b ⇒ 'c›
  assumes ‹⋀(f :: 'b ⇒ 'c) i A. finite A ⟹ i ∉ A ⟹ ∃j. j ∉ f ` A›
    ‹finite A› ‹A, n ⊢ branch›
  shows ‹f ` A ⊢ sub_branch f branch›
  using assms(3-)
proof (induct n branch arbitrary: f rule: STA.induct)
  case (Close p i branch n)
  have ‹sub f p at f i in sub_branch f branch›
    using Close(1) sub_branch_mem by fastforce
  moreover have ‹(❙¬ sub f p) at f i in sub_branch f branch›
    using Close(2) sub_branch_mem by force
  ultimately show ?case
    using STA.Close by fast
next
  case (Neg p a ps branch n f)
  then have ‹f ` A ⊢ (sub f p # sub_list f ps, f a) # sub_branch f branch›
    unfolding sub_branch_def by simp
  moreover have ‹(❙¬ ❙¬ sub f p) at f a in (sub_list f ps, f a) # sub_branch f branch›
    using Neg(1) at_in_sub_branch by (metis (no_types, opaque_lifting) sub.simps(3))
  ultimately have ‹f ` A ⊢ (sub_list f ps, f a) # sub_branch f branch›
    using Neg' by fast
  then show ?case
    unfolding sub_branch_def by simp
next
  case (DisP p q a ps branch n)
  then have
    ‹f ` A ⊢ (sub f p # sub_list f ps, f a) # sub_branch f branch›
    ‹f ` A ⊢ (sub f q # sub_list f ps, f a) # sub_branch f branch›
    unfolding sub_branch_def by simp_all
  moreover have ‹(sub f p ❙∨ sub f q) at f a in (sub_list f ps, f a) # sub_branch f branch›
    using DisP(1) at_in_sub_branch by (metis (no_types, opaque_lifting) sub.simps(4))
  ultimately have ‹f ` A ⊢ (sub_list f ps, f a) # sub_branch f branch›
    using DisP'' by fast
  then show ?case
    unfolding sub_branch_def by simp
next
  case (DisN p q a ps branch n)
  then have ‹f ` A ⊢ ((❙¬ sub f q) # (❙¬ sub f p) # sub_list f ps, f a) # sub_branch f branch›
    unfolding sub_branch_def by simp
  moreover have ‹(❙¬ (sub f p ❙∨ sub f q)) at f a in (sub_list f ps, f a) # sub_branch f branch›
    using DisN(1) at_in_sub_branch by (metis (no_types, opaque_lifting) sub.simps(3-4))
  ultimately have ‹f ` A ⊢ (sub_list f ps, f a) # sub_branch f branch›
    using DisN' by fast
  then show ?case
    unfolding sub_branch_def by simp
next
  case (DiaP p a ps branch i n)
  have ‹i ∉ A›
    using DiaP(2) by simp

  show ?case
  proof (cases ‹witnessed (sub f p) (f a) (sub_branch f ((ps, a) # branch))›)
    case True
    then obtain i' where
      rs: ‹(❙@ i' (sub f p)) at f a in (sub_list f ps, f a) # sub_branch f branch› and
      ts: ‹(❙◇ Nom i') at f a in (sub_list f ps, f a) # sub_branch f branch›
      unfolding sub_branch_def witnessed_def by auto
    from rs have rs':
      ‹(❙@ i' (sub f p)) at f a in ((❙◇ Nom i') # sub_list f ps, f a) # sub_branch f branch›
      by fastforce

    let ?f = ‹f(i := i')›
    let ?branch = ‹sub_branch ?f branch›
    have ‹sub_branch ?f ((ps, a) # branch) = sub_branch f ((ps, a) # branch)›
      using DiaP(2) sub_branch_upd_fresh by fast
    then have **: ‹sub_list ?f ps = sub_list f ps› ‹?f a = f a› ‹?branch = sub_branch f branch›
      unfolding sub_branch_def by simp_all

    have p: ‹sub ?f p = sub f p›
      using DiaP(1-2) sub_upd_fresh unfolding branch_nominals_def by fastforce

    have ‹?f ` A ⊢ sub_branch ?f (((❙@ i p) # (❙◇ Nom i) # ps, a) # branch)›
      using DiaP(6) by blast
    then have
      ‹?f ` A ⊢ ((❙@ (?f i) (sub ?f p)) # (❙◇ Nom (?f i)) # sub_list ?f ps, ?f a) # ?branch›
      unfolding sub_branch_def by fastforce
    then have
      ‹?f ` A ⊢ ((❙@ i' (sub f p)) # (❙◇ Nom i') # sub_list f ps, f a) # sub_branch f branch›
      using p ** by simp
    then have ‹?f ` A ⊢ ((❙◇ Nom i') # sub_list f ps, f a) # sub_branch f branch›
      using rs' by (meson Dup new_def)
    then have ‹?f ` A ⊢ (sub_list f ps, f a) # sub_branch f branch›
      using ts by (meson Dup new_def)
    moreover have ‹?f ` A = f ` A›
      using ‹i ∉ A› by auto
    ultimately show ?thesis
      unfolding sub_branch_def by auto
  next
    case False
    have ‹finite (branch_nominals ((ps, a) # branch))›
      by (simp add: finite_branch_nominals)
    then have ‹finite (A ∪ branch_nominals ((ps, a) # branch))›
      using ‹finite A› by simp
    then obtain j where *: ‹j ∉ f ` (A ∪ branch_nominals ((ps, a) # branch))›
      using DiaP(2) assms by metis
    then have ‹j ∉ f ` A›
      by blast

    let ?f = ‹f(i := j)›
    let ?branch = ‹sub_branch ?f branch›
    have **: ‹sub_branch ?f ((ps, a) # branch) = sub_branch f ((ps, a) # branch)›
      using DiaP(2) sub_branch_upd_fresh by fast
    then have ***: ‹sub_list ?f ps = sub_list f ps› ‹?f a = f a› ‹?branch = sub_branch f branch›
      unfolding sub_branch_def by simp_all
    moreover have p: ‹sub ?f p = sub f p›
      using DiaP(1-2) sub_upd_fresh unfolding branch_nominals_def by fastforce
    ultimately have ‹¬ witnessed (sub ?f p) (?f a) (sub_branch ?f ((ps, a) # branch))›
      using False ** by simp
    then have w: ‹¬ witnessed (sub ?f p) (?f a) ((sub_list ?f ps, ?f a) # ?branch)›
      unfolding sub_branch_def by simp

    have f: ‹?f ` A = f ` A›
      using ‹i ∉ A› by auto

    have ‹?f ` A ⊢ sub_branch ?f (((❙@ i p) # (❙◇ Nom i) # ps, a) # branch)›
      using DiaP(6) by blast
    then have ‹f ` A ⊢ ((❙@ (?f i) (sub ?f p)) # (❙◇ Nom (?f i)) # sub_list ?f ps, ?f a) # ?branch›
      unfolding sub_branch_def using f by simp
    moreover have ‹sub ?f (❙◇ p) at ?f a in (sub_list ?f ps, ?f a) # sub_branch ?f branch›
      using DiaP(1) at_in_sub_branch by fast
    then have ‹(❙◇ sub ?f p) at ?f a in (sub_list ?f ps, ?f a) # sub_branch ?f branch›
      by simp
    moreover have ‹∄a. sub ?f p = Nom a›
      using DiaP(3) by (cases p) simp_all
    moreover have ‹j ∉ f ` (branch_nominals ((ps, a) # branch))›
      using * by blast
    then have ‹?f i ∉ branch_nominals ((sub_list ?f ps, ?f a) # ?branch)›
      using ** sub_branch_nominals unfolding sub_branch_def
      by (metis fun_upd_same list.simps(9) sub_block.simps)
    ultimately have ‹f ` A ⊢ (sub_list ?f ps, ?f a) # ?branch›
      using w DiaP' ‹j ∉ f ` A› by (metis Un_iff fun_upd_same)
    then show ?thesis
      using *** unfolding sub_branch_def by simp
  qed
next
  case (DiaN p a ps branch i n)
  then have ‹f ` A ⊢ ((❙¬ (❙@ (f i) (sub f p))) # sub_list f ps, f a) # sub_branch f branch›
    unfolding sub_branch_def by simp
  moreover have ‹(❙¬ (❙◇ sub f p)) at f a in (sub_list f ps, f a) # sub_branch f branch›
    using DiaN(1) at_in_sub_branch by (metis (no_types, opaque_lifting) sub.simps(3, 5))
  moreover have ‹(❙◇ Nom (f i)) at f a in (sub_list f ps, f a) # sub_branch f branch›
    using DiaN(2) at_in_sub_branch by (metis (no_types, opaque_lifting) sub.simps(2, 5))
  ultimately have ‹f ` A ⊢ (sub_list f ps, f a) # sub_branch f branch›
    using DiaN' by fast
  then show ?case
    unfolding sub_branch_def by simp
next
  case (SatP a p b ps branch n)
  then have ‹f ` A ⊢ (sub f p # sub_list f ps, f a) # sub_branch f branch›
    unfolding sub_branch_def by simp
  moreover have ‹(❙@ (f a) (sub f p)) at f b in (sub_list f ps, f a) # sub_branch f branch›
    using SatP(1) at_in_sub_branch by (metis (no_types, opaque_lifting) sub.simps(6))
  ultimately have ‹f ` A ⊢ (sub_list f ps, f a) # sub_branch f branch›
    using SatP' by fast
  then show ?case
    unfolding sub_branch_def by simp
next
  case (SatN a p b ps branch n)
  then have ‹f ` A ⊢ ((❙¬ sub f p) # sub_list f ps, f a) # sub_branch f branch›
    unfolding sub_branch_def by simp
  moreover have ‹(❙¬ (❙@ (f a) (sub f p))) at f b in (sub_list f ps, f a) # sub_branch f branch›
    using SatN(1) at_in_sub_branch by (metis (no_types, opaque_lifting) sub.simps(3, 6))
  ultimately have ‹f ` A ⊢ (sub_list f ps, f a) # sub_branch f branch›
    using SatN' by fast
  then show ?case
    unfolding sub_branch_def by simp
next
  case (GoTo i branch n)
  then have ‹f ` A ⊢ ([], f i) # sub_branch f branch›
    unfolding sub_branch_def by simp
  moreover have ‹f i ∈ branch_nominals (sub_branch f branch)›
    using GoTo(1) sub_branch_nominals by fast
  ultimately show ?case
    using STA.GoTo by fast
next
  case (Nom p b ps a branch n)
  then have ‹f ` A ⊢ sub_branch f ((p # ps, a) # branch)›
    by blast
  then have ‹f ` A ⊢ (sub f p # sub_list f ps, f a) # sub_branch f branch›
    unfolding sub_branch_def by simp
  moreover have ‹sub f p at f b in (sub_list f ps, f a) # sub_branch f branch›
    using Nom(1) at_in_sub_branch by fast
  moreover have ‹Nom (f a) at f b in (sub_list f ps, f a) # sub_branch f branch›
    using Nom(2) at_in_sub_branch by (metis (no_types, opaque_lifting) sub.simps(2))
  moreover have ‹∀i. sub f p = Nom i ∨ sub f p = (❙◇ Nom i) ⟶ i ∈ f ` A›
    using Nom(3) sub_still_allowed by metis
  ultimately have ‹f ` A ⊢ (sub_list f ps, f a) # sub_branch f branch›
    using Nom' by metis
  then show ?case
    unfolding sub_branch_def by simp
qed

lemma ex_fresh_gt:
  fixes f :: ‹'b ⇒ 'c›
  assumes ‹∃g :: 'c ⇒ 'b. surj g› ‹finite A› ‹i ∉ A›
  shows ‹∃j. j ∉ f ` A›
proof (rule ccontr)
  assume ‹∄j. j ∉ f ` A›
  moreover obtain g :: ‹'c ⇒ 'b› where ‹surj g›
    using assms(1) by blast
  ultimately show False
    using assms(2-3)
    by (metis UNIV_I UNIV_eq_I card_image_le card_seteq finite_imageI image_comp subsetI)
qed

corollary STA_sub_gt:
  fixes f :: ‹'b ⇒ 'c›
  assumes ‹∃g :: 'c ⇒ 'b. surj g› ‹A ⊢ branch›
    ‹finite A› ‹∀i ∈ branch_nominals branch. f i ∈ f ` A ⟶ i ∈ A›
  shows ‹f ` A ⊢ sub_branch f branch›
  using assms ex_fresh_gt STA_sub' by metis

corollary STA_sub_inf:
  fixes f :: ‹'b ⇒ 'c›
  assumes ‹infinite (UNIV :: 'c set)› ‹A ⊢ branch›
    ‹finite A› ‹∀i ∈ branch_nominals branch. f i ∈ f ` A ⟶ i ∈ A›
  shows ‹f ` A ⊢ sub_branch f branch›
proof -
  have ‹finite A ⟹ ∃j. j ∉ f ` A› for A and f :: ‹'b ⇒ 'c›
    using assms(1) ex_new_if_finite by blast
  then show ?thesis
    using assms(2-) STA_sub' by metis
qed

corollary STA_sub:
  fixes f :: ‹'b ⇒ 'b›
  assumes ‹A ⊢ branch› ‹finite A›
  shows ‹f ` A ⊢ sub_branch f branch›
proof -
  have ‹finite A ⟹ i ∉ A ⟹ ∃j. j ∉ f ` A› for i A and f :: ‹'b ⇒ 'b›
    by (metis card_image_le card_seteq finite_imageI subsetI)
  then show ?thesis
    using assms STA_sub' by metis
qed

subsection ‹Unrestricted ‹(❙◇)› rule›

lemma DiaP'':
  assumes
    ‹(❙◇ p) at a in (ps, a) # branch›
    ‹i ∉ A ∪ branch_nominals ((ps, a) # branch)› ‹∄a. p = Nom a›
    ‹finite A›
    ‹A ⊢ ((❙@ i p) # (❙◇ Nom i) # ps, a) # branch›
  shows ‹A ⊢ (ps, a) # branch›
proof (cases ‹witnessed p a ((ps, a) # branch)›)
  case True
  then obtain i' where
    rs: ‹(❙@ i' p) at a in (ps, a) # branch› and
    ts: ‹(❙◇ Nom i') at a in (ps, a) # branch›
    unfolding witnessed_def by blast
  then have rs':
    ‹(❙@ i' p) at a in ((❙◇ Nom i') # ps, a) # branch›
    by fastforce

  let ?f = ‹id(i := i')›

  have ‹?f ` A ⊢ sub_branch ?f (((❙@ i p) # (❙◇ Nom i) # ps, a) # branch)›
    using assms(4-5) STA_sub by blast
  then have ‹?f ` A ⊢ ((❙@ i' (sub ?f p)) # (❙◇ Nom i') # sub_list ?f ps, ?f a) #
      sub_branch ?f branch›
    unfolding sub_branch_def by simp
  moreover have ‹i ∉ nominals p› ‹i ∉ list_nominals ps› ‹i ≠ a› ‹i ∉ branch_nominals branch›
    using assms(1-3) unfolding branch_nominals_def by fastforce+
  then have ‹sub ?f p = p›
    by (simp add: sub_id sub_upd_fresh)
  moreover have ‹sub_list ?f ps = ps›
    using ‹i ∉ list_nominals ps› by (simp add: map_idI sub_id sub_upd_fresh)
  moreover have ‹?f a = a›
    using ‹i ≠ a› by simp
  moreover have ‹sub_branch ?f branch = branch›
    using ‹i ∉ branch_nominals branch› by (simp add: sub_branch_id sub_branch_upd_fresh)
  ultimately have ‹?f ` A ⊢ ((❙@ i' p) # (❙◇ Nom i') # ps, a) # branch›
    by simp
  then have ‹?f ` A ⊢ ((❙◇ Nom i') # ps, a) # branch›
    using rs' by (meson Dup new_def)
  then have ‹?f ` A ⊢ (ps, a) # branch›
    using ts by (meson Dup new_def)
  moreover have ‹?f ` A = A›
    using assms(2) by auto
  ultimately show ?thesis
    by simp
next
  case False
  then show ?thesis
    using assms DiaP' STA_Suc by fast
qed

section ‹Structural Properties›

lemma block_nominals_branch:
  assumes ‹block ∈. branch›
  shows ‹block_nominals block ⊆ branch_nominals branch›
  unfolding branch_nominals_def using assms by blast

lemma sub_block_fresh:
  assumes ‹i ∉ branch_nominals branch› ‹block ∈. branch›
  shows ‹sub_block (f(i := j)) block = sub_block f block›
  using assms block_nominals_branch sub_block_upd_fresh by fast

lemma list_down_induct [consumes 1, case_names Start Cons]:
  assumes ‹∀y ∈ set ys. Q y› ‹P (ys @ xs)›
    ‹⋀y xs. Q y ⟹ P (y # xs) ⟹ P xs›
  shows ‹P xs›
  using assms by (induct ys) auto

text ‹
  If the last block on a branch has opening nominal ‹a› and the last formulas on that block
   occur on another block alongside nominal ‹a›, then we can drop those formulas.
›

lemma STA_drop_prefix:
  assumes ‹set ps ⊆ set qs› ‹(qs, a) ∈. branch› ‹A, n ⊢ (ps @ ps', a) # branch›
  shows ‹A, n ⊢ (ps', a) # branch›
proof -
  have ‹∀p ∈ set ps. p on (qs, a)›
    using assms(1) by auto
  then show ?thesis
  proof (induct ps' rule: list_down_induct)
    case Start
    then show ?case
      using assms(3) .
  next
    case (Cons p ps)
    then show ?case
      using assms(2) by (meson Dup new_def list.set_intros(2))
  qed
qed

text ‹We can drop a block if it is subsumed by another block.›

lemma STA_drop_block:
  assumes
    ‹set ps ⊆ set ps'› ‹(ps', a) ∈. branch›
    ‹A, n ⊢ (ps, a) # branch›
  shows ‹A, Suc n ⊢ branch›
  using assms
proof (induct branch)
  case Nil
  then show ?case
    by simp
next
  case (Cons block branch)
  then show ?case
  proof (cases block)
    case (Pair qs b)
    then have ‹A, n ⊢ ([], a) # (qs, b) # branch›
      using Cons(2-4) STA_drop_prefix[where branch=‹(qs, b) # branch›] by simp
    moreover have ‹a ∈ branch_nominals ((qs, b) # branch)›
      unfolding branch_nominals_def using Cons(3) Pair by fastforce
    ultimately have ‹A, Suc n ⊢ (qs, b) # branch›
      by (simp add: GoTo)
    then show ?thesis
      using Pair Dup by fast
  qed
qed

lemma STA_drop_block':
  assumes ‹A, n ⊢ (ps, a) # branch› ‹(ps, a) ∈. branch›
  shows ‹A, Suc n ⊢ branch›
  using assms STA_drop_block by fastforce

lemma sub_branch_image: ‹set (sub_branch f branch) = sub_block f ` set branch›
  unfolding sub_branch_def by simp

lemma sub_block_repl:
  assumes ‹j ∉ block_nominals block›
  shows ‹i ∉ block_nominals (sub_block (id(i := j, j := i)) block)›
  using assms by (simp add: image_iff sub_block_nominals)

lemma sub_branch_repl:
  assumes ‹j ∉ branch_nominals branch›
  shows ‹i ∉ branch_nominals (sub_branch (id(i := j, j := i)) branch)›
  using assms by (simp add: image_iff sub_branch_nominals)

text ‹If a finite set of blocks has a closing tableau then so does any finite superset.›

lemma STA_struct:
  fixes branch :: ‹('a, 'b) branch›
  assumes
    inf: ‹infinite (UNIV :: 'b set)› and fin: ‹finite A› and
    ‹A, n ⊢ branch› ‹set branch ⊆ set branch'›
  shows ‹A ⊢ branch'›
  using assms(3-)
proof (induct n branch arbitrary: branch' rule: STA.induct)
  case (Close p i branch n)
  then show ?case
    using STA.Close by fast
next
  case (Neg p a ps branch n)
  have ‹A ⊢ (p # ps, a) # branch'›
    using Neg(4-) by (simp add: subset_code(1))
  moreover have ‹(❙¬ ❙¬ p) at a in (ps, a) # branch'›
    using Neg(1, 5) by auto
  ultimately have ‹A ⊢ (ps, a) # branch'›
    using Neg' by fast
  moreover have ‹(ps, a) ∈. branch'›
    using Neg(5) by simp
  ultimately show ?case
    using STA_drop_block' by fast
next
  case (DisP p q a ps branch n)
  have ‹A ⊢ (p # ps, a) # branch'› ‹A ⊢ (q # ps, a) # branch'›
    using DisP(5, 7-) by (simp_all add: subset_code(1))
  moreover have ‹(p ❙∨ q) at a in (ps, a) # branch'›
    using DisP(1, 8) by auto
  ultimately have ‹A ⊢ (ps, a) # branch'›
    using DisP'' by fast
  moreover have ‹(ps, a) ∈. branch'›
    using DisP(8) by simp
  ultimately show ?case
    using STA_drop_block' by fast
next
  case (DisN p q a ps branch n)
  have ‹A ⊢ ((❙¬ q) # (❙¬ p) # ps, a)# branch'›
    using DisN(4-) by (simp add: subset_code(1))
  moreover have ‹(❙¬ (p ❙∨ q)) at a in (ps, a) # branch'›
    using DisN(1, 5) by auto
  ultimately have ‹A ⊢ (ps, a) # branch'›
    using DisN' by fast
  moreover have ‹(ps, a) ∈. branch'›
    using DisN(5) by simp
  ultimately show ?case
    using STA_drop_block' by fast
next
  case (DiaP p a ps branch i n)
  have ‹finite (A ∪ branch_nominals branch')›
    using fin by (simp add: finite_branch_nominals)
  then obtain j where j: ‹j ∉ A ∪ branch_nominals branch'›
    using assms ex_new_if_finite by blast
  then have j': ‹j ∉ branch_nominals ((ps, a) # branch)›
    using DiaP(7) unfolding branch_nominals_def by blast

  let ?f = ‹id(i := j, j := i)›
  let ?branch' = ‹sub_branch ?f branch'›
  have branch': ‹sub_branch ?f ?branch' = branch'›
    using sub_branch_comp sub_branch_id swap_id by metis

  have ‹i ∉ branch_nominals ((ps, a) # branch)›
    using DiaP(2) by blast
  then have branch: ‹sub_branch ?f ((ps, a) # branch) = (ps, a) # branch›
    using DiaP(2) j' sub_branch_id sub_branch_upd_fresh by metis
  moreover have
    ‹set (sub_branch ?f ((ps, a) # branch)) ⊆ set ?branch'›
    using DiaP(7) sub_branch_image by blast
  ultimately have *: ‹set ((ps, a) # branch) ⊆ set ?branch'›
    unfolding sub_branch_def by auto

  have ‹i ∉ block_nominals (ps, a)›
    using DiaP unfolding branch_nominals_def by simp
  moreover have ‹i ∉ branch_nominals ?branch'›
    using j sub_branch_repl by fast
  ultimately have i: ‹i ∉ branch_nominals ((ps, a) # ?branch')›
    unfolding branch_nominals_def by simp

  have ‹?f ` A = A›
    using DiaP(2) j by auto

  have ‹A ⊢ ((❙@ i p) # (❙◇ Nom i) # ps, a) # ?branch'›
    using DiaP(6) *
    by (metis (no_types, lifting) subset_code(1) insert_mono list.set(2) set_subset_Cons)
  moreover have ‹(❙◇ p) at a in (ps, a) # ?branch'›
    using DiaP(1, 7) * by (meson set_subset_Cons subset_code(1))
  ultimately have ‹A ⊢ (ps, a) # ?branch'›
    using inf DiaP(2-3) fin i DiaP'' by (metis Un_iff)
  then have ‹?f ` A ⊢ sub_branch ?f ((ps, a) # ?branch')›
    using STA_sub fin by blast
  then have ‹A ⊢ (ps, a) # branch'›
    using ‹?f ` A = A› branch' branch unfolding sub_branch_def by simp
  moreover have ‹(ps, a) ∈. branch'›
    using ‹set ((ps, a) # branch) ⊆ set branch'› by simp
  ultimately show ?case
    using STA_drop_block' by fast
next
  case (DiaN p a ps branch i n)
  have ‹A ⊢ ((❙¬ (❙@ i p)) # ps, a) # branch'›
    using DiaN(5-) by (simp add: subset_code(1))
  moreover have
    ‹(❙¬ (❙◇ p)) at a in (ps, a) # branch'›
    ‹(❙◇ Nom i) at a in (ps, a) # branch'›
    using DiaN(1-2, 6) by auto
  ultimately have ‹A ⊢ (ps, a) # branch'›
    using DiaN' by fast
  moreover have ‹(ps, a) ∈. branch'›
    using DiaN(6) by simp
  ultimately show ?case
    using STA_drop_block' by fast
next
  case (SatP a p b ps branch n)
  have ‹A ⊢ (p # ps, a) # branch'›
    using SatP(4-) by (simp add: subset_code(1))
  moreover have ‹(❙@ a p) at b in (ps, a) # branch'›
    using SatP(1, 5) by auto
  ultimately have ‹A ⊢ (ps, a) # branch'›
    using SatP' by fast
  moreover have ‹(ps, a) ∈. branch'›
    using SatP(5) by simp
  ultimately show ?case
    using STA_drop_block' by fast
next
  case (SatN a p b ps branch n)
  have ‹A ⊢ ((❙¬ p) # ps, a) # branch'›
    using SatN(4-) by (simp add: subset_code(1))
  moreover have ‹(❙¬ (❙@ a p)) at b in (ps, a) # branch'›
    using SatN(1, 5) by auto
  ultimately have ‹A ⊢ (ps, a) # branch'›
    using SatN' by fast
  moreover have ‹(ps, a) ∈. branch'›
    using SatN(5) by simp
  ultimately show ?case
    using STA_drop_block' by fast
next
  case (GoTo i branch n)
  then have ‹A ⊢ ([], i) # branch'›
    by (simp add: subset_code(1))
  moreover have ‹i ∈ branch_nominals branch'›
    using GoTo(1, 4) unfolding branch_nominals_def by auto
  ultimately show ?case
    using GoTo(2) STA.GoTo by fast
next
  case (Nom p b ps a branch n)
  have ‹A ⊢ (p # ps, a) # branch'›
    using Nom(6-) by (simp add: subset_code(1))
  moreover have ‹p at b in (ps, a) # branch'›
    using Nom(1, 7) by auto
  moreover have ‹Nom a at b in (ps, a) # branch'›
    using Nom(2, 7) by auto
  ultimately have ‹A ⊢ (ps, a) # branch'›
    using Nom(3) Nom' by metis
  moreover have ‹(ps, a) ∈. branch'›
    using Nom(7) by simp
  ultimately show ?case
    using STA_drop_block' by fast
qed

text ‹
  If a branch has a closing tableau then we can replace the formulas of the last block
  on that branch with any finite superset and still obtain a closing tableau.
›

lemma STA_struct_block:
  fixes branch :: ‹('a, 'b) branch›
  assumes
    inf: ‹infinite (UNIV :: 'b set)› and fin: ‹finite A› and
    ‹A, n ⊢ (ps, a) # branch› ‹set ps ⊆ set ps'›
  shows ‹A ⊢ (ps', a) # branch›
  using assms(3-)
proof (induct n ‹(ps, a) # branch› arbitrary: ps ps' rule: STA.induct)
  case (Close p i n ts ts')
  then have ‹p at i in (ts', a) # branch› ‹(❙¬ p) at i in (ts', a) # branch›
    by auto
  then show ?case
    using STA.Close by fast
next
  case (Neg p ps n)
  then have ‹(❙¬ ❙¬ p) at a in (ps', a) # branch›
    by auto
  moreover have ‹A ⊢ (p # ps', a) # branch›
    using Neg(4-) by (simp add: subset_code(1))
  ultimately show ?case
    using Neg' by fast
next
  case (DisP p q ps n)
  then have ‹(p ❙∨ q) at a in (ps', a) # branch›
    by auto
  moreover have ‹A ⊢ (p # ps', a) # branch› ‹A ⊢ (q # ps', a) # branch›
    using DisP(5, 7-) by (simp_all add: subset_code(1))
  ultimately show ?case
    using DisP'' by fast
next
  case (DisN p q ps n)
  then have ‹(❙¬ (p ❙∨ q)) at a in (ps', a) # branch›
    by auto
  moreover have ‹A ⊢ ((❙¬ q) # (❙¬ p) # ps', a) # branch›
    using DisN(4-) by (simp add: subset_code(1))
  ultimately show ?case
    using DisN' by fast
next
  case (DiaP p ps i n)
  have ‹finite (A ∪ branch_nominals ((ps', a) # branch))›
    using fin finite_branch_nominals by blast
  then obtain j where j: ‹j ∉ A ∪ branch_nominals ((ps', a) # branch)›
    using assms ex_new_if_finite by blast
  then have j': ‹j ∉ block_nominals (ps, a)›
    using DiaP.prems unfolding branch_nominals_def by auto

  let ?f = ‹id(i := j, j := i)›
  let ?ps' = ‹sub_list ?f ps'›
  have ps': ‹sub_list ?f ?ps' = ps'›
    using sub_list_comp sub_list_id swap_id by metis

  have ‹i ∉ block_nominals (ps, a)›
    using DiaP(1-2) unfolding branch_nominals_def by simp
  then have ps: ‹sub_block ?f (ps, a) = (ps, a)›
    using j' sub_block_id sub_block_upd_fresh by metis
  moreover have ‹set (sub_list ?f ps) ⊆ set (sub_list ?f ps')›
    using ‹set ps ⊆ set ps'› by auto
  ultimately have *: ‹set ps ⊆ set ?ps'›
    by simp

  have ‹i ∉ branch_nominals branch›
    using DiaP unfolding branch_nominals_def by simp
  moreover have ‹j ∉ branch_nominals branch›
    using j unfolding branch_nominals_def by simp
  ultimately have branch: ‹sub_branch ?f branch = branch›
    using sub_branch_id sub_branch_upd_fresh by metis

  have ‹i ≠ a› ‹j ≠ a›
    using DiaP j unfolding branch_nominals_def by simp_all
  then have ‹?f a = a›
    by simp
  moreover have ‹j ∉ block_nominals (ps', a)›
    using j unfolding branch_nominals_def by simp
  ultimately have ‹i ∉ block_nominals (?ps', a)›
    using sub_block_repl[where block=‹(ps', a)› and i=i and j=j] by simp

  have ‹?f ` A = A›
    using DiaP(2) j by auto

  have ‹(❙◇ p) at a in (?ps', a) # branch›
    using DiaP(1) * by fastforce
  moreover have ‹A ⊢ ((❙@ i p) # (❙◇ Nom i) # ?ps', a) # branch›
    using * DiaP(6) fin by (simp add: subset_code(1))
  moreover have ‹i ∉ A ∪ branch_nominals ((?ps', a) # branch)›
    using DiaP(2) ‹i ∉ block_nominals (?ps', a)› unfolding branch_nominals_def by simp
  ultimately have ‹A ⊢ (?ps', a) # branch›
    using DiaP(3) fin DiaP'' by metis
  then have ‹?f ` A ⊢ sub_branch ?f ((?ps', a) # branch)›
    using STA_sub fin by blast
  then have ‹A ⊢ (sub_list ?f ?ps', ?f a) # sub_branch ?f branch›
    unfolding sub_branch_def using ‹?f ` A = A› by simp
  then show ?case
    using ‹?f a = a› ps' branch by simp
next
  case (DiaN p ps i n)
  then have
    ‹(❙¬ (❙◇ p)) at a in (ps', a) # branch›
    ‹(❙◇ Nom i) at a in (ps', a) # branch›
    by auto
  moreover have ‹A ⊢ ((❙¬ (❙@ i p)) # ps', a) # branch›
    using DiaN(5-) by (simp add: subset_code(1))
  ultimately show ?case
    using DiaN' by fast
next
  case (SatP p b ps n)
  then have ‹(❙@ a p) at b in (ps', a) # branch›
    by auto
  moreover have ‹A ⊢ (p # ps', a) # branch›
    using SatP(4-) by (simp add: subset_code(1))
  ultimately show ?case
    using SatP' by fast
next
  case (SatN p b ps n)
  then have ‹(❙¬ (❙@ a p)) at b in (ps', a) # branch›
    by auto
  moreover have ‹A ⊢ ((❙¬ p) # ps', a) # branch›
    using SatN(4-) by (simp add: subset_code(1))
  ultimately show ?case
    using SatN' by fast
next
  case (GoTo i n ps)
  then have ‹A, Suc n ⊢ (ps, a) # branch›
    using STA.GoTo by fast
  then obtain m where ‹A, m ⊢ (ps, a) # (ps', a) # branch›
    using inf fin STA_struct[where branch'=‹(ps, a) # _ # _›] by fastforce
  then have ‹A, Suc m ⊢ (ps', a) # branch›
    using GoTo(4) by (simp add: STA_drop_block[where a=a])
  then show ?case
    by blast
next
  case (Nom p b ps n)
  have ‹p at b in (ps', a) # branch›
    using Nom(1, 7) by auto
  moreover have ‹Nom a at b in (ps', a) # branch›
    using Nom(2, 7) by auto
  moreover have ‹A ⊢ (p # ps', a) # branch›
    using Nom(6-) by (simp add: subset_code(1))
  ultimately show ?case
    using Nom(3) Nom' by metis
qed

section ‹Bridge›

text ‹
  We define a ‹descendants k i branch› relation on sets of indices.
  The sets are built on the index of a ‹❙◇ Nom k› on an ‹i›-block in ‹branch› and can be extended
    by indices of formula occurrences that can be thought of as descending from
    that ‹❙◇ Nom k› by application of either the ‹(❙¬ ❙◇)› or ‹Nom› rule.

  We show that if we have nominals ‹j› and ‹k› on the same block in a closeable branch,
  then the branch obtained by the following transformation is also closeable:
  For every index ‹v›, if the formula at ‹v› is ‹❙◇ Nom k›, replace it by ‹❙◇ Nom j› and
    if it is ‹❙¬ (❙@ k p)› replace it by ‹❙¬ (❙@ j p)›.
  There are no other cases.

  From this transformation we can show admissibility of the Bridge rule under the assumption
    that ‹j› is an allowed nominal.
›

subsection ‹Replacing›

abbreviation bridge' :: ‹'b ⇒ 'b ⇒ ('a, 'b) fm ⇒ ('a, 'b) fm› where
  ‹bridge' k j p ≡ case p of
    (❙◇ Nom k') ⇒ (if k = k' then (❙◇ Nom j) else (❙◇ Nom k'))
  | (❙¬ (❙@ k' q)) ⇒ (if k = k' then (❙¬ (❙@ j q)) else (❙¬ (❙@ k' q)))
  | p ⇒ p›

abbreviation bridge ::
  ‹'b ⇒ 'b ⇒ (nat × nat) set ⇒ nat ⇒ nat ⇒ ('a, 'b) fm ⇒ ('a, 'b) fm› where
  ‹bridge k j ≡ mapper (bridge' k j)›

lemma bridge_on_Nom:
  ‹Nom i on (ps, a) ⟹ Nom i on (mapi (bridge k j xs v) ps, a)›
  by (induct ps) auto

lemma bridge'_nominals:
  ‹nominals (bridge' k j p) ∪ {k, j} = nominals p ∪ {k, j}›
proof (induct p)
  case (Neg p)
  then show ?case by (cases p) auto
next
  case (Dia p)
  then show ?case by (cases p) auto
qed auto

lemma bridge_nominals:
  ‹nominals (bridge k j xs v v' p) ∪ {k, j} = nominals p ∪ {k, j}›
proof (cases ‹(v, v') ∈ xs›)
  case True
  then have ‹nominals (bridge k j xs v v' p) = nominals (bridge' k j p)›
    by simp
  then show ?thesis
    using bridge'_nominals by metis
qed simp

lemma bridge_block_nominals:
  ‹block_nominals (mapi_block (bridge k j xs v) (ps, a)) ∪ {k, j} =
   block_nominals (ps, a) ∪ {k, j}›
proof (induct ps)
  case Nil
  then show ?case
    by simp
next
  case (Cons p ps)
  have ‹?case ⟷
    (nominals (bridge k j xs v (length ps) p)) ∪
    (block_nominals (mapi_block (bridge k j xs v) (ps, a)) ∪ {k, j}) =
    (nominals p) ∪ (block_nominals (ps, a) ∪ {k, j})›
    by simp
  also have ‹… ⟷
    (nominals (bridge k j xs v (length ps) p) ∪ {k, j}) ∪
    (block_nominals (mapi_block (bridge k j xs v) (ps, a)) ∪ {k, j}) =
    (nominals p ∪ {k, j}) ∪ (block_nominals (ps, a) ∪ {k, j})›
    by blast
  moreover have
    ‹nominals (bridge k j xs v (length ps) p) ∪ {k, j} = nominals p ∪ {k, j}›
    using bridge_nominals by metis
  moreover note Cons
  ultimately show ?case
    by argo
qed

lemma bridge_branch_nominals:
  ‹branch_nominals (mapi_branch (bridge k j xs) branch) ∪ {k, j} =
   branch_nominals branch ∪ {k, j}›
proof (induct branch)
  case Nil
  then show ?case
    unfolding branch_nominals_def mapi_branch_def
    by simp
next
  case (Cons block branch)
  have ‹?case ⟷
    (block_nominals (mapi_block (bridge k j xs (length branch)) block)) ∪
    (branch_nominals (mapi_branch (bridge k j xs) branch) ∪ {k, j}) =
    (block_nominals block) ∪ (branch_nominals branch ∪ {k, j})›
    unfolding branch_nominals_def mapi_branch_def by simp
  also have ‹… ⟷
    (block_nominals (mapi_block (bridge k j xs (length branch)) block) ∪ {k, j}) ∪
    (branch_nominals (mapi_branch (bridge k j xs) branch) ∪ {k, j}) =
    (block_nominals block ∪ {k, j}) ∪ (branch_nominals branch ∪ {k, j})›
    by blast
  moreover have
    ‹block_nominals (mapi_block (bridge k j xs (length branch)) block) ∪ {k, j} =
     block_nominals block ∪ {k, j}›
    using bridge_block_nominals[where ps=‹fst block› and a=‹snd block›] by simp
  ultimately show ?case
    using Cons by argo
qed

lemma at_in_mapi_branch:
  assumes ‹p at a in branch› ‹p ≠ Nom a›
  shows ‹∃v v'. f v v' p at a in mapi_branch f branch›
  using assms by (meson mapi_branch_mem rev_nth_mapi_block rev_nth_on)

lemma nom_at_in_bridge:
  fixes k j xs
  defines ‹f ≡ bridge k j xs›
  assumes ‹Nom i at a in branch›
  shows ‹Nom i at a in mapi_branch f branch›
proof -
  obtain qs where qs: ‹(qs, a) ∈. branch› ‹Nom i on (qs, a)›
    using assms(2) by blast
  then obtain l where ‹(mapi (f l) qs, a) ∈. mapi_branch f branch›
    using mapi_branch_mem by fast
  moreover have ‹Nom i on (mapi (f l) qs, a)›
    unfolding f_def using qs(2) by (induct qs) auto
  ultimately show ?thesis
    by blast
qed

lemma nominals_mapi_branch_bridge:
  assumes ‹Nom k at j in branch›
  shows ‹branch_nominals (mapi_branch (bridge k j xs) branch) = branch_nominals branch›
proof -
  let ?f = ‹bridge k j xs›
  have ‹Nom k at j in mapi_branch ?f branch›
    using assms nom_at_in_bridge by fast
  then have
    ‹j ∈ branch_nominals (mapi_branch ?f branch)›
    ‹k ∈ branch_nominals (mapi_branch ?f branch)›
    unfolding branch_nominals_def by fastforce+
  moreover have ‹j ∈ branch_nominals branch› ‹k ∈ branch_nominals branch›
    using assms unfolding branch_nominals_def by fastforce+
  moreover have
    ‹branch_nominals (mapi_branch ?f branch) ∪ {k, j} = branch_nominals branch ∪ {k, j}›
    using bridge_branch_nominals by metis
  ultimately show ?thesis
    by blast
qed

lemma bridge_proper_dia:
  assumes ‹∄a. p = Nom a›
  shows ‹bridge k j xs v v' (❙◇ p) = (❙◇ p)›
  using assms by (induct p) simp_all

lemma bridge_compl_cases:
  fixes k j xs v v' w w' p
  defines ‹q ≡ bridge k j xs v v' p› and ‹q' ≡ bridge k j xs w w' (❙¬ p)›
  shows
    ‹(q = (❙◇ Nom j) ∧ q' = (❙¬ (❙◇ Nom k))) ∨
 (∃r. q = (❙¬ (❙@ j r)) ∧ q' = (❙¬ ❙¬ (❙@ k r))) ∨
 (∃r. q = (❙@ k r) ∧ q' = (❙¬ (❙@ j r))) ∨
     (q = p ∧ q' = (❙¬ p))›
proof (cases p)
  case (Neg p)
  then show ?thesis
    by (cases p) (simp_all add: q_def q'_def)
next
  case (Dia p)
  then show ?thesis
    by (cases p) (simp_all add: q_def q'_def)
qed (simp_all add: q_def q'_def)

subsection ‹Descendants›

inductive descendants :: ‹'b ⇒ 'b ⇒ ('a, 'b) branch ⇒ (nat × nat) set ⇒ bool› where
  Initial:
  ‹branch !. v = Some (qs, i) ⟹ qs !. v' = Some (❙◇ Nom k) ⟹
    descendants k i branch {(v, v')}›
| Derived:
  ‹branch !. v = Some (qs, a) ⟹ qs !. v' = Some (❙¬ (❙@ k p)) ⟹
    descendants k i branch xs ⟹ (w, w') ∈ xs ⟹
    branch !. w = Some (rs, a) ⟹ rs !. w' = Some (❙◇ Nom k) ⟹
    descendants k i branch ({(v, v')} ∪ xs)›
| Copied:
  ‹branch !. v = Some (qs, a) ⟹ qs !. v' = Some p ⟹
    descendants k i branch xs ⟹ (w, w') ∈ xs ⟹
    branch !. w = Some (rs, b) ⟹ rs !. w' = Some p ⟹
    Nom a at b in branch ⟹
    descendants k i branch ({(v, v')} ∪ xs)›

lemma descendants_initial:
  assumes ‹descendants k i branch xs›
  shows ‹∃(v, v') ∈ xs. ∃ps.
    branch !. v = Some (ps, i) ∧ ps !. v' = Some (❙◇ Nom k)›
  using assms by (induct k i branch xs rule: descendants.induct) simp_all

lemma descendants_bounds_fst:
  assumes ‹descendants k i branch xs› ‹(v, v') ∈ xs›
  shows ‹v < length branch›
  using assms rev_nth_Some
  by (induct k i branch xs rule: descendants.induct) fast+

lemma descendants_bounds_snd:
  assumes ‹descendants k i branch xs› ‹(v, v') ∈ xs› ‹branch !. v = Some (ps, a)›
  shows ‹v' < length ps›
  using assms
  by (induct k i branch xs rule: descendants.induct) (auto simp: rev_nth_Some)

lemma descendants_branch:
  ‹descendants k i branch xs ⟹ descendants k i (extra @ branch) xs›
proof (induct k i branch xs rule: descendants.induct)
  case (Initial branch v qs i v' k)
  then show ?case
    using rev_nth_append descendants.Initial by fast
next
  case (Derived branch v qs a v' k p i xs w w' rs)
  then have
    ‹(extra @ branch) !. v = Some (qs, a)›
    ‹(extra @ branch) !. w = Some (rs, a)›
    using rev_nth_append by fast+
  then show ?case
    using Derived(2, 4-5, 7) descendants.Derived by fast
next
  case (Copied branch v qs a v' p k i xs w w' rs b)
  then have
    ‹(extra @ branch) !. v = Some (qs, a)›
    ‹(extra @ branch) !. w = Some (rs, b)›
    using rev_nth_append by fast+
  moreover have ‹Nom a at b in (extra @ branch)›
    using Copied(8) by auto
  ultimately show ?case
    using Copied(2-4, 5-7) descendants.Copied by fast
qed

lemma descendants_block:
  assumes ‹descendants k i ((ps, a) # branch) xs›
  shows ‹descendants k i ((ps' @ ps, a) # branch) xs›
  using assms
proof (induct k i ‹(ps, a) # branch› xs arbitrary: ps a branch rule: descendants.induct)
  case (Initial v qs i v' k)
  have
    ‹((ps' @ ps, a) # branch) !. v = Some (qs, i) ∨
     ((ps' @ ps, a) # branch) !. v = Some (ps' @ qs, i)›
    using Initial(1) by auto
  moreover have
    ‹qs !. v' = Some (❙◇ Nom k)› ‹(ps' @ qs) !. v' = Some (❙◇ Nom k)›
    using Initial(2) rev_nth_append by simp_all
  ultimately show ?case
    using descendants.Initial by fast
next
  case (Derived v qs a' v' k p i xs w w' rs)
  have
    ‹((ps' @ ps, a) # branch) !. v = Some (qs, a') ∨
     ((ps' @ ps, a) # branch) !. v = Some (ps' @ qs, a')›
    using Derived(1) by auto
  moreover have
    ‹qs !. v' = Some (❙¬ (❙@ k p))› ‹(ps' @ qs) !. v' = Some (❙¬ (❙@ k p))›
    using Derived(2) rev_nth_append by simp_all
  moreover have
    ‹((ps' @ ps, a) # branch) !. w = Some (rs, a') ∨
     ((ps' @ ps, a) # branch) !. w = Some (ps' @ rs, a')›
    using ‹((ps, a) # branch) !. w = Some (rs, a')› by auto
  moreover have
    ‹rs !. w' = Some (❙◇ Nom k)› ‹(ps' @ rs) !. w' = Some (❙◇ Nom k)›
    using Derived(7) rev_nth_append by simp_all
  ultimately show ?case
    using Derived(4-5) descendants.Derived by fast
next
  case (Copied v qs a' v' p k i xs w w' rs b)
  have
    ‹((ps' @ ps, a) # branch) !. v = Some (qs, a') ∨
     ((ps' @ ps, a) # branch) !. v = Some (ps' @ qs, a')›
    using Copied(1) by auto
  moreover have ‹qs !. v' = Some p› ‹(ps' @ qs) !. v' = Some p›
    using Copied(2) rev_nth_append by simp_all
  moreover have
    ‹((ps' @ ps, a) # branch) !. w = Some (rs, b) ∨
     ((ps' @ ps, a) # branch) !. w = Some (ps' @ rs, b)›
    using Copied(6) by auto
  moreover have ‹rs !. w' = Some p› ‹(ps' @ rs) !. w' = Some p›
    using Copied(7) rev_nth_append by simp_all
  moreover have
    ‹((ps' @ ps, a) # branch) !. w = Some (rs, b) ∨
     ((ps' @ ps, a) # branch) !. w = Some (ps' @ rs, b)›
    using Copied(6) by auto
  moreover have ‹rs !. w' = Some p› ‹(ps' @ rs) !. w' = Some p›
    using Copied(7) rev_nth_append by simp_all
  moreover have ‹Nom a' at b in (ps' @ ps, a) # branch›
    using Copied(8) by fastforce
  ultimately show ?case
    using Copied(4-5) descendants.Copied[where branch=‹(ps' @ ps, a) # branch›] by blast
qed

lemma descendants_no_head:
  assumes ‹descendants k i ((ps, a) # branch) xs›
  shows ‹descendants k i ((p # ps, a) # branch) xs›
  using assms descendants_block[where ps'=‹[_]›] by simp

lemma descendants_types:
  assumes
    ‹descendants k i branch xs› ‹(v, v') ∈ xs›
    ‹branch !. v = Some (ps, a)› ‹ps !. v' = Some p›
  shows ‹p = (❙◇ Nom k) ∨ (∃q. p = (❙¬ (❙@ k q)))›
  using assms by (induct k i branch xs arbitrary: v v' ps a) fastforce+

lemma descendants_oob_head':
  assumes ‹descendants k i ((ps, a) # branch) xs›
  shows ‹(length branch, m + length ps) ∉ xs›
  using assms descendants_bounds_snd by fastforce

lemma descendants_oob_head:
  assumes ‹descendants k i ((ps, a) # branch) xs›
  shows ‹(length branch, length ps) ∉ xs›
  using assms descendants_oob_head'[where m=0] by fastforce

subsection ‹Induction›

text ‹
  We induct over an arbitrary set of indices.
  That way, we can determine in each case whether the extension gets replaced or not
    by manipulating the set before applying the induction hypothesis.
›

lemma STA_bridge':
  fixes a :: 'b
  assumes
    inf: ‹infinite (UNIV :: 'b set)› and fin: ‹finite A› and ‹j ∈ A›
    ‹A, n ⊢ (ps, a) # branch›
    ‹descendants k i ((ps, a) # branch) xs›
    ‹Nom k at j in branch›
  shows ‹A ⊢ mapi_branch (bridge k j xs) ((ps, a) # branch)›
  using assms(4-)
proof (induct n ‹(ps, a) # branch› arbitrary: ps a branch xs rule: STA.induct)
  case (Close p i' n)
  let ?f = ‹bridge k j xs›
  let ?branch = ‹mapi_branch ?f ((ps, a) # branch)›

  obtain qs where qs: ‹(qs, i') ∈. (ps, a) # branch› ‹p on (qs, i')›
    using Close(1) by blast
  obtain rs where rs: ‹(rs, i') ∈. (ps, a) # branch› ‹(❙¬ p) on (rs, i')›
    using Close(2) by blast

  obtain v where v: ‹(mapi (?f v) qs, i') ∈. ?branch›
    using qs mapi_branch_mem by fast
  obtain w where w: ‹(mapi (?f w) rs, i') ∈. ?branch›
    using rs mapi_branch_mem by fast

  have k: ‹Nom k at j in ?branch›
    using Close(4) nom_at_in_bridge unfolding mapi_branch_def by fastforce

  show ?case
  proof (cases ‹∃a. p = Nom a›)
    case True
    then have ‹p on (mapi (?f v) qs, i')›
      using qs bridge_on_Nom by fast
    moreover have ‹(❙¬ p) on (mapi (?f w) rs, i')›
      using rs(2) True by (induct rs) auto
    ultimately show ?thesis
      using v w STA.Close by fast
  next
    case False
    then obtain v' where ‹qs !. v' = Some p›
      using qs rev_nth_on by fast
    then have qs': ‹(?f v v' p) on (mapi (?f v) qs, i')›
      using rev_nth_mapi_block by fast

    then obtain w' where ‹rs !. w' = Some (❙¬ p)›
      using rs rev_nth_on by fast
    then have rs': ‹(?f w w' (❙¬ p)) on (mapi (?f w) rs, i')›
      using rev_nth_mapi_block by fast

    obtain q q' where q: ‹?f v v' p = q› and q': ‹?f w w' (❙¬ p) = q'›
      by simp_all
    then consider
      (dia) ‹q = (❙◇ Nom j)› ‹q' = (❙¬ (❙◇ Nom k))› |
      (satn)‹∃r. q = (❙¬ (❙@ j r)) ∧ q' = (❙¬ ❙¬ (❙@ k r))› |
      (sat) ‹∃r. q = (❙@ k r) ∧ q' = (❙¬ (❙@ j r))› |
      (old) ‹q = p› ‹q' = (❙¬ p)›
      using bridge_compl_cases by fast
    then show ?thesis
    proof cases
      case dia
      then have *:
        ‹(❙◇ Nom j) on (mapi (?f v) qs, i')›
        ‹(❙¬ (❙◇ Nom k)) on (mapi (?f w) rs, i')›
        using q qs' q' rs' by simp_all

      have ‹i' ∈ branch_nominals ?branch›
        unfolding branch_nominals_def using v by fastforce
      then have ?thesis if ‹A ⊢ ([], i') # ?branch›
        using that GoTo by fast
      moreover have ‹(mapi (?f v) qs, i') ∈. ([], i') # ?branch›
        using v by simp
      moreover have ‹(mapi (?f w) rs, i') ∈. ([], i') # ?branch›
        using w by simp
      ultimately have ?thesis if ‹A ⊢ ([❙¬ (❙@ j (Nom k))], i') # ?branch›
        using that * by (meson DiaN')
      moreover have ‹j ∈ branch_nominals (([❙¬ (❙@ j (Nom k))], i') # ?branch)›
        unfolding branch_nominals_def by simp
      ultimately have ?thesis if ‹A ⊢ ([], j) # ([❙¬ (❙@ j (Nom k))], i') # ?branch›
        using that GoTo by fast
      moreover have ‹(❙¬ (❙@ j (Nom k))) at i' in ([], j) # ([❙¬ (❙@ j (Nom k))], i') # ?branch›
        by fastforce
      ultimately have ?thesis if ‹A ⊢ ([❙¬ Nom k], j) # ([❙¬ (❙@ j (Nom k))], i') # ?branch›
        using that SatN' by fast
      moreover have ‹Nom k at j in ([❙¬ Nom k], j) # ([❙¬ (❙@ j (Nom k))], i') # ?branch›
        using k by fastforce
      moreover have ‹(❙¬ Nom k) at j in ([❙¬ Nom k], j) # ([❙¬ (❙@ j (Nom k))], i') # ?branch›
        by fastforce
      ultimately show ?thesis
        using STA.Close by fast
    next
      case satn
      then obtain r where *:
        ‹(❙¬ (❙@ j r)) on (mapi (?f v) qs, i')›
        ‹(❙¬ ❙¬ (❙@ k r)) on (mapi (?f w) rs, i')›
        using q qs' q' rs' by auto

      have ‹i' ∈ branch_nominals ?branch›
        unfolding branch_nominals_def using v by fastforce
      then have ?thesis if ‹A ⊢ ([], i') # ?branch›
        using that GoTo by fast
      moreover have ‹(mapi (?f w) rs, i') ∈. ([], i') # ?branch›
        using w by simp
      ultimately have ?thesis if ‹A ⊢ ([❙@ k r], i') # ?branch›
        using that *(2) by (meson Neg')
      moreover have ‹j ∈ branch_nominals (([❙@ k r], i') # ?branch)›
        unfolding branch_nominals_def using k by fastforce
      ultimately have ?thesis if ‹A ⊢ ([], j) # ([❙@ k r], i') # ?branch›
        using that GoTo by fast
      moreover have ‹(❙¬ (❙@ j r)) at i' in ([], j) # ([❙@ k r], i') # ?branch›
        using *(1) v by auto
      ultimately have ?thesis if ‹A ⊢ ([❙¬ r], j) # ([❙@ k r], i') # ?branch›
        using that SatN' by fast
      moreover have ‹k ∈ branch_nominals (([❙¬ r], j) # ([❙@ k r], i') # ?branch)›
        unfolding branch_nominals_def using k by fastforce
      ultimately have ?thesis if ‹A ⊢ ([], k) # ([❙¬ r], j) # ([❙@ k r], i') # ?branch›
        using that GoTo by fast
      moreover have ‹(❙@ k r) at i' in ([], k) # ([❙¬ r], j) # ([❙@ k r], i') # ?branch›
        by fastforce
      ultimately have ?thesis if ‹A ⊢ ([r], k) # ([❙¬ r], j) # ([❙@ k r], i') # ?branch›
        using that SatP' by fast
      moreover have
        ‹Nom k at j in ([r], k) # ([❙¬ r], j) # ([❙@ k r], i') # ?branch›
        ‹(❙¬ r) at j in ([r], k) # ([❙¬ r], j) # ([❙@ k r], i') # ?branch›
        using k by fastforce+
      ultimately have ?thesis if ‹A ⊢ ([❙¬ r, r], k) # ([❙¬ r], j) # ([❙@ k r], i') # ?branch›
        using that by (meson Nom' fm.distinct(21) fm.simps(18))
      moreover have
        ‹r at k in ([❙¬ r, r], k) # ([❙¬ r], j) # ([❙@ k r], i') # ?branch›
        ‹(❙¬ r) at k in ([❙¬ r, r], k) # ([❙¬ r], j) # ([❙@ k r], i') # ?branch›
        by fastforce+
      ultimately show ?thesis
        using STA.Close by fast
    next
      case sat
      then obtain r where *:
        ‹(❙@ k r) on (mapi (?f v) qs, i')›
        ‹(❙¬ (❙@ j r)) on (mapi (?f w) rs, i')›
        using q qs' q' rs' by auto

      have ‹j ∈ branch_nominals ?branch›
        unfolding branch_nominals_def using k by fastforce
      then have ?thesis if ‹A ⊢ ([], j) # ?branch›
        using that GoTo by fast
      moreover have ‹(❙¬ (❙@ j r)) at i' in ([], j) # ?branch›
        using *(2) w by auto
      ultimately have ?thesis if ‹A ⊢ ([❙¬ r], j) # ?branch›
        using that by (meson SatN')
      moreover have ‹k ∈ branch_nominals (([❙¬ r], j) # ?branch)›
        unfolding branch_nominals_def using k by fastforce
      ultimately have ?thesis if ‹A ⊢ ([], k) # ([❙¬ r], j) # ?branch›
        using that GoTo by fast
      moreover have ‹(❙@ k r) at i' in ([], k) # ([❙¬ r], j) # ?branch›
        using *(1) v by auto
      ultimately have ?thesis if ‹A ⊢ ([r], k) # ([❙¬ r], j) # ?branch›
        using that SatP' by fast
      moreover have
        ‹Nom k at j in ([r], k) # ([❙¬ r], j) # ?branch›
        ‹(❙¬ r) at j in ([r], k) # ([❙¬ r], j) # ?branch›
        using k by fastforce+
      ultimately have ?thesis if ‹A ⊢ ([❙¬ r, r], k) # ([❙¬ r], j) # ?branch›
        using that by (meson Nom' fm.distinct(21) fm.simps(18))
      moreover have
        ‹r at k in ([❙¬ r, r], k) # ([❙¬ r], j) # ?branch›
        ‹(❙¬ r) at k in ([❙¬ r, r], k) # ([❙¬ r], j) # ?branch›
        by fastforce+
      ultimately show ?thesis
        using STA.Close by fast
    next
      case old
      then have ‹p on (mapi (?f v) qs, i')› ‹(❙¬ p) on (mapi (?f w) rs, i')›
        using q qs' q' rs' by simp_all
      then show ?thesis
        using v w STA.Close[where p=p and i=i'] by fast
    qed
  qed
next
  case (Neg p a ps branch n)
  let ?f = ‹bridge k j xs›
  have p: ‹?f l l' (❙¬ ❙¬ p) = (❙¬ ❙¬ p)› for l l'
    by simp

  have ‹descendants k i ((p # ps, a) # branch) xs›
    using Neg(5) descendants_no_head by fast
  then have ‹A ⊢ mapi_branch ?f ((p # ps, a) # branch)›
    using Neg(4-) by blast
  moreover have ‹(length branch, length ps) ∉ xs›
    using Neg(5) descendants_oob_head by fast
  ultimately have ‹A ⊢ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    unfolding mapi_branch_def by simp
  moreover have ‹∃l l'. ?f l l' (❙¬ ❙¬ p) at a in mapi_branch ?f ((ps, a) # branch)›
    using Neg(1) at_in_mapi_branch by fast
  then have ‹(❙¬ ❙¬ p) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    unfolding mapi_branch_def using p by simp
  ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    using Neg' by fast
  then show ?case
    unfolding mapi_branch_def by auto
next
  case (DisP p q a ps branch n)
  let ?f = ‹bridge k j xs›
  have p: ‹?f l l' (p ❙∨ q) = (p ❙∨ q)› for l l'
    by simp

  have
    ‹descendants k i ((p # ps, a) # branch) xs›
    ‹descendants k i ((q # ps, a) # branch) xs›
    using DisP(8) descendants_no_head by fast+
  then have
    ‹A ⊢ mapi_branch ?f ((p # ps, a) # branch)›
    ‹A ⊢ mapi_branch ?f ((q # ps, a) # branch)›
    using DisP(5-) by blast+
  moreover have ‹(length branch, length ps) ∉ xs›
    using DisP(8) descendants_oob_head by fast
  ultimately have
    ‹A ⊢ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    ‹A ⊢ (q # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    unfolding mapi_branch_def by simp_all
  moreover have ‹∃l l'. ?f l l' (p ❙∨ q) at a in mapi_branch ?f ((ps, a) # branch)›
    using DisP(1) at_in_mapi_branch by fast
  then have ‹(p ❙∨ q) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    unfolding mapi_branch_def using p by simp
  ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    using DisP'' by fast
  then show ?case
    unfolding mapi_branch_def by auto
next
  case (DisN p q a ps branch n)
  let ?f = ‹bridge k j xs›
  have p: ‹?f l l' (❙¬ (p ❙∨ q)) = (❙¬ (p ❙∨ q))› for l l'
    by simp

  have ‹descendants k i (((❙¬ p) # ps, a) # branch) xs›
    using DisN(5) descendants_no_head by fast
  then have ‹descendants k i (((❙¬ q) # (❙¬ p) # ps, a) # branch) xs›
    using descendants_no_head by fast
  then have ‹A ⊢ mapi_branch ?f (((❙¬ q) # (❙¬ p) # ps, a) # branch)›
    using DisN(4-) by blast
  moreover have ‹(length branch, length ps) ∉ xs›
    using DisN(5) descendants_oob_head by fast
  moreover have ‹(length branch, 1 + length ps) ∉ xs›
    using DisN(5) descendants_oob_head' by fast
  ultimately have ‹A ⊢ ((❙¬ q) # (❙¬ p) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    unfolding mapi_branch_def by simp
  moreover have ‹∃l l'. ?f l l' (❙¬ (p ❙∨ q)) at a in mapi_branch ?f ((ps, a) # branch)›
    using DisN(1) at_in_mapi_branch by fast
  then have ‹(❙¬ (p ❙∨ q)) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    unfolding mapi_branch_def using p by simp
  ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    using DisN' by fast
  then show ?case
    unfolding mapi_branch_def by auto
next
  case (DiaP p a ps branch i' n)
  let ?f = ‹bridge k j xs›
  have p: ‹?f l l' (❙◇ p) = (❙◇ p)› for l l'
    using DiaP(3) bridge_proper_dia by fast

  have ‹branch_nominals (mapi_branch ?f ((ps, a) # branch)) = branch_nominals ((ps, a) # branch)›
    using DiaP(8-) nominals_mapi_branch_bridge[where j=j and k=k and branch=‹(ps, a) # branch›]
    by auto
  then have i':
    ‹i' ∉ A ∪ branch_nominals ((mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)›
    unfolding mapi_branch_def using DiaP(2) by simp

  have 1: ‹?f (length branch) (1 + length ps) (❙@ i' p) = (❙@ i' p)›
    by simp
  have ‹i' ≠ k›
    using DiaP(2, 8) unfolding branch_nominals_def by fastforce
  then have 2: ‹?f (length branch) (length ps) (❙◇ Nom i') = (❙◇ Nom i')›
    by simp

  have ‹i' ≠ j›
    using DiaP(2, 8) unfolding branch_nominals_def by fastforce
  moreover have ‹descendants k i (((❙@ i' p) # (❙◇ Nom i') # ps, a) # branch) xs›
    using DiaP(7) descendants_block[where ps'=‹[_, _]›] by fastforce
  ultimately have ‹A ⊢ mapi_branch ?f (((❙@ i' p) # (❙◇ Nom i') # ps, a) # branch)›
    using DiaP(4-) by blast
  then have ‹A ⊢ ((❙@ i' p) # (❙◇ Nom i') # mapi (?f (length branch)) ps, a) #
      mapi_branch ?f branch›
    unfolding mapi_branch_def using 1 by (simp add: 2)
  moreover have ‹∃l l'. ?f l l' (❙◇ p) at a in mapi_branch ?f ((ps, a) # branch)›
    using DiaP(1) at_in_mapi_branch by fast
  then have ‹(❙◇ p) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    unfolding mapi_branch_def using p by simp
  ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    using i' DiaP(3) fin DiaP'' by fast
  then show ?case
    unfolding mapi_branch_def by simp
next
  case (DiaN p a ps branch i' n)
  have p: ‹bridge k j xs l l' (❙¬ (❙◇ p)) = (❙¬ (❙◇ p))› for xs l l'
    by simp

  obtain rs where rs: ‹(rs, a) ∈. (ps, a) # branch› ‹(❙◇ Nom i') on (rs, a)›
    using DiaN(2) by fast
  obtain v where v: ‹((ps, a) # branch) !. v = Some (rs, a)›
    using rs(1) rev_nth_mem by fast
  obtain v' where v': ‹rs !. v' = Some (❙◇ Nom i')›
    using rs(2) rev_nth_on by fast

  show ?case
  proof (cases ‹(v, v') ∈ xs›)
    case True
    then have ‹i' = k›
      using DiaN(6) v v' descendants_types by fast

    let ?xs = ‹{(length branch, length ps)} ∪ xs›
    let ?f = ‹bridge k j ?xs›
    let ?branch = ‹((❙¬ (❙@ i' p)) # ps, a) # branch›

    obtain rs' where
      ‹(((❙¬ (❙@ k p)) # ps, a) # branch) !. v = Some (rs', a)›
      ‹rs' !. v' = Some (❙◇ Nom i')›
      using v v' index_Cons by fast
    moreover have ‹descendants k i (((❙¬ (❙@ k p)) # ps, a) # branch) xs›
      using DiaN(6) descendants_block[where ps'=‹[_]›] by fastforce
    moreover have ‹?branch !. length branch = Some ((❙¬ (❙@ k p)) # ps, a)›
      using ‹i' = k› by simp
    moreover have ‹((❙¬ (❙@ k p)) # ps) !. length ps = Some (❙¬ (❙@ k p))›
      by simp
    ultimately have ‹descendants k i (((❙¬ (❙@ k p)) # ps, a) # branch) ?xs›
      using True ‹i' = k› Derived[where branch=‹_ # branch›] by simp

    then have ‹A ⊢ mapi_branch ?f (((❙¬ (❙@ k p)) # ps, a) # branch)›
      using ‹i' = k› DiaN(5-) by blast
    then have ‹A ⊢ ((❙¬ (❙@ j p)) # mapi (?f (length branch)) ps, a) #
        mapi_branch (bridge k j ?xs) branch›
      unfolding mapi_branch_def using ‹i' = k› by simp
    moreover have ‹∃l l'. ?f l l' (❙¬ (❙◇ p)) at a in mapi_branch ?f ((ps, a) # branch)›
      using DiaN(1) at_in_mapi_branch by fast
    then have ‹(❙¬ (❙◇ p)) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      unfolding mapi_branch_def using p[where xs=‹?xs›] by simp
    moreover have ‹(mapi (?f v) rs, a) ∈. mapi_branch ?f ((ps, a) # branch)›
      using v rev_nth_mapi_branch by fast
    then have ‹(mapi (?f v) rs, a) ∈
        set ((mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)›
      unfolding mapi_branch_def by simp
    moreover have ‹?f v v' (❙◇ Nom i') on (mapi (?f v) rs, a)›
      using v' rev_nth_mapi_block by fast
    then have ‹(❙◇ Nom j) on (mapi (?f v) rs, a)›
      using True ‹i' = k› by simp
    ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      by (meson DiaN')
    then have ‹A ⊢ (mapi (bridge k j xs (length branch)) ps, a) #
        mapi_branch (bridge k j xs) branch›
      using mapi_branch_head_add_oob[where branch=branch and ps=ps] unfolding mapi_branch_def
      by simp
    then show ?thesis
      unfolding mapi_branch_def by simp
  next
    case False
    let ?f = ‹bridge k j xs›

    have ‹descendants k i (((❙¬ (❙@ i' p)) # ps, a) # branch) xs›
      using DiaN(6) descendants_no_head by fast
    then have ‹A ⊢ mapi_branch ?f (((❙¬ (❙@ i' p)) # ps, a) # branch)›
      using DiaN(5-) by blast
    moreover have ‹(length branch, length ps) ∉ xs›
      using DiaN(6) descendants_oob_head by fast
    ultimately have ‹A ⊢ ((❙¬ (❙@ i' p)) # mapi (?f (length branch)) ps, a) #
        mapi_branch ?f branch›
      unfolding mapi_branch_def by simp
    moreover have ‹∃l l'. ?f l l' (❙¬ (❙◇ p)) at a in mapi_branch ?f ((ps, a) # branch)›
      using DiaN(1) at_in_mapi_branch by fast
    then have ‹(❙¬ (❙◇ p)) at a in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      unfolding mapi_branch_def using p[where xs=‹xs›] by simp
    moreover have ‹(mapi (?f v) rs, a) ∈. mapi_branch ?f ((ps, a) # branch)›
      using v rev_nth_mapi_branch by fast
    then have ‹(mapi (?f v) rs, a) ∈
        set ((mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)›
      unfolding mapi_branch_def by simp
    moreover have ‹?f v v' (❙◇ Nom i') on (mapi (?f v) rs, a)›
      using v' rev_nth_mapi_block by fast
    then have ‹(❙◇ Nom i') on (mapi (?f v) rs, a)›
      using False by simp
    ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      by (meson DiaN')
    then show ?thesis
      unfolding mapi_branch_def by simp
  qed
next
  case (SatP a p b ps branch n)
  let ?f = ‹bridge k j xs›
  have p: ‹?f l l' (❙@ a p) = (❙@ a p)› for l l'
    by simp

  have ‹descendants k i ((p # ps, a) # branch) xs›
    using SatP(5) descendants_no_head by fast
  then have ‹A ⊢ mapi_branch ?f ((p # ps, a) # branch)›
    using SatP(4-) by blast
  moreover have ‹(length branch, length ps) ∉ xs›
    using SatP(5) descendants_oob_head by fast
  ultimately have ‹A ⊢ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    unfolding mapi_branch_def by simp
  moreover have ‹∃l l'. ?f l l' (❙@ a p) at b in mapi_branch ?f ((ps, a) # branch)›
    using SatP(1) at_in_mapi_branch by fast
  then have ‹(❙@ a p) at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    unfolding mapi_branch_def using p by simp
  ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
    using SatP' by fast
  then show ?case
    unfolding mapi_branch_def by simp
next
  case (SatN a p b ps branch n)
  obtain qs where qs: ‹(qs, b) ∈. (ps, a) # branch› ‹(❙¬ (❙@ a p)) on (qs, b)›
    using SatN(1) by fast
  obtain v where v: ‹((ps, a) # branch) !. v = Some (qs, b)›
    using qs(1) rev_nth_mem by fast
  obtain v' where v': ‹qs !. v' = Some (❙¬ (❙@ a p))›
    using qs(2) rev_nth_on by fast

  show ?case
  proof (cases ‹(v, v') ∈ xs›)
    case True
    then have ‹a = k›
      using SatN(5) v v' descendants_types by fast

    let ?f = ‹bridge k j xs›
    let ?branch = ‹((❙¬ p) # ps, a) # branch›
    have p: ‹?f v v' (❙¬ (❙@ k p)) = (❙¬ (❙@ j p))›
      using True by simp

    obtain rs' where
      ‹?branch !. v = Some (rs', b)›
      ‹rs' !. v' = Some (❙¬ (❙@ k p))›
      using v v' ‹a = k› index_Cons by fast
    have ‹descendants k i ?branch xs›
      using SatN(5) descendants_no_head by fast
    then have ‹A ⊢ mapi_branch ?f ?branch›
      using ‹a = k› SatN(4-) by blast
    moreover have ‹(length branch, length ps) ∉ xs›
      using SatN(5) descendants_oob_head by fast
    ultimately have ‹A ⊢ ((❙¬ p) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      unfolding mapi_branch_def using ‹a = k› by simp
    moreover have ‹set (((❙¬ p) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch) ⊆
        set (((❙¬ p) # mapi (?f (length branch)) ps, a) # ([❙¬ p], j) # mapi_branch ?f branch)›
      by auto
    ultimately have *:
      ‹A ⊢ ((❙¬ p) # mapi (?f (length branch)) ps, a) # ([❙¬ p], j) # mapi_branch ?f branch›
      using inf fin STA_struct by fastforce

    have k: ‹Nom k at j in mapi_branch ?f ((ps, a) # branch)›
      using SatN(6) nom_at_in_bridge unfolding mapi_branch_def by fastforce

    have ‹(mapi (?f v) qs, b) ∈. mapi_branch ?f ((ps, a) # branch)›
      using v rev_nth_mapi_branch by fast
    moreover have ‹?f v v' (❙¬ (❙@ k p)) on (mapi (?f v) qs, b)›
      using v' ‹a = k› rev_nth_mapi_block by fast
    then have ‹(❙¬ (❙@ j p)) on (mapi (?f v) qs, b)›
      using p by simp
    ultimately have satn: ‹(❙¬ (❙@ j p)) at b in mapi_branch ?f ((ps, a) # branch)›
      by blast

    have ‹j ∈ branch_nominals (mapi_branch ?f ((ps, a) # branch))›
      unfolding branch_nominals_def using k by fastforce
    then have ?thesis if ‹A ⊢ ([], j) # mapi_branch ?f ((ps, a) # branch)›
      using that GoTo by fast
    moreover have ‹(❙¬ (❙@ j p)) at b in ([], j) # mapi_branch ?f ((ps, a) # branch)›
      using satn by auto
    ultimately have ?thesis if ‹A ⊢ ([❙¬ p], j) # mapi_branch ?f ((ps, a) # branch)›
      using that SatN' by fast
    then have ?thesis if ‹A ⊢ ([❙¬ p], j) # mapi_branch ?f ((ps, a) # branch)›
      using that SatN' by fast
    then have ?thesis if
      ‹A ⊢ ([❙¬ p], j) # (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      using that unfolding mapi_branch_def by simp
    moreover have ‹set ((mapi (?f (length branch)) ps, a) # ([❙¬ p], j) # mapi_branch ?f branch) ⊆
        set (([❙¬ p], j) # (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)›
      by auto
    ultimately have ?thesis if
      ‹A ⊢ (mapi (?f (length branch)) ps, a) # ([❙¬ p], j) # mapi_branch ?f branch›
      using that inf fin STA_struct by blast
    moreover have
      ‹Nom k at j in (mapi (?f (length branch)) ps, a) # ([❙¬ p], j) # mapi_branch ?f branch›
      using k unfolding mapi_branch_def by auto
    moreover have
      ‹(❙¬ p) at j in (mapi (?f (length branch)) ps, a) # ([❙¬ p], j) # mapi_branch ?f branch›
      by fastforce
    ultimately have ?thesis if
      ‹A ⊢ ((❙¬ p) # mapi (?f (length branch)) ps, a) # ([❙¬ p], j) # mapi_branch ?f branch›
      using that ‹a = k› by (meson Nom' fm.distinct(21) fm.simps(18))
    then show ?thesis
      using * by blast
  next
    case False
    let ?f = ‹bridge k j xs›

    have ‹descendants k i (((❙¬ p) # ps, a) # branch) xs›
      using SatN(5) descendants_no_head by fast
    then have ‹A ⊢ mapi_branch (bridge k j xs) (((❙¬ p) # ps, a) # branch)›
      using SatN(4-) by blast
    moreover have ‹(length branch, length ps) ∉ xs›
      using SatN(5) descendants_oob_head by fast
    ultimately have ‹A ⊢ ((❙¬ p) # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      unfolding mapi_branch_def by simp
    moreover have ‹(mapi (?f v) qs, b) ∈. mapi_branch ?f ((ps, a) # branch)›
      using v rev_nth_mapi_branch by fast
    then have ‹(mapi (?f v) qs, b) ∈
        set ((mapi (?f (length branch)) ps, a) # mapi_branch ?f branch)›
      unfolding mapi_branch_def by simp
    moreover have ‹?f v v' (❙¬ (❙@ a p)) on (mapi (?f v) qs, b)›
      using v' rev_nth_mapi_block by fast
    then have ‹(❙¬ (❙@ a p)) on (mapi (?f v) qs, b)›
      using False by simp
    ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      by (meson SatN')
    then show ?thesis
      unfolding mapi_branch_def by simp
  qed
next
  case (GoTo i' n ps a branch)
  let ?f = ‹bridge k j xs›

  have ‹descendants k i (([], i') # (ps, a) # branch) xs›
    using GoTo(4) descendants_branch[where extra=‹[_]›] by simp
  then have ‹A ⊢ mapi_branch ?f (([], i') # (ps, a) # branch)›
    using GoTo(3, 5-) by auto
  then have ‹A ⊢ ([], i') # mapi_branch ?f ((ps, a) # branch)›
    unfolding mapi_branch_def by simp
  moreover have
    ‹branch_nominals (mapi_branch ?f ((ps, a) # branch)) = branch_nominals ((ps, a) # branch)›
    using GoTo(5-) nominals_mapi_branch_bridge[where j=j and k=k and branch=‹(ps, a) # branch›]
    by auto
  then have ‹i' ∈ branch_nominals (mapi_branch (bridge k j xs) ((ps, a) # branch))›
    using GoTo(1) by blast
  ultimately show ?case
    using STA.GoTo by fast
next
  case (Nom p b ps a branch n)
  show ?case
  proof (cases ‹∃j. p = Nom j›)
    case True
    let ?f = ‹bridge k j xs›

    have ‹descendants k i ((p # ps, a) # branch) xs›
      using Nom(7) descendants_block[where ps'=‹[p]›] by simp
    then have ‹A ⊢ mapi_branch ?f ((p # ps, a) # branch)›
      using Nom(6-) by blast
    moreover have ‹?f (length branch) (length ps) p = p›
      using True by auto
    ultimately have ‹A ⊢ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      unfolding mapi_branch_def by simp
    moreover have ‹p at b in mapi_branch ?f ((ps, a) # branch)›
      using Nom(1) True nom_at_in_bridge by fast
    then have ‹p at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      unfolding mapi_branch_def by simp
    moreover have ‹Nom a at b in mapi_branch ?f ((ps, a) # branch)›
      using Nom(2) True nom_at_in_bridge by fast
    then have ‹Nom a at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      unfolding mapi_branch_def by simp
    ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
      by (meson Nom' Nom.hyps(3))
    then show ?thesis
      unfolding mapi_branch_def by simp
  next
    case False
    obtain qs where qs: ‹(qs, b) ∈. (ps, a) # branch› ‹p on (qs, b)›
      using Nom(1) by blast
    obtain v where v: ‹((ps, a) # branch) !. v = Some (qs, b)›
      using qs(1) rev_nth_mem by fast
    obtain v' where v': ‹qs !. v' = Some p›
      using qs(2) False rev_nth_on by fast

    show ?thesis
    proof (cases ‹(v, v') ∈ xs›)
      case True
      let ?xs = ‹{(length branch, length ps)} ∪ xs›
      let ?f = ‹bridge k j ?xs›

      let ?p = ‹bridge' k j p›
      have p: ‹?f v v' p = ?p›
        using True by simp

      consider (dia) ‹p = (❙◇ Nom k)› | (satn) q where ‹p = (❙¬ (❙@ k q))› | (old) ‹?p = p›
        by (meson Nom.prems(1) True descendants_types v v')
      then have A: ‹∀i. ?p = Nom i ∨ ?p = (❙◇ Nom i) ⟶ i ∈ A›
        using Nom(3) ‹j ∈ A› by cases simp_all

      obtain qs' where
        ‹((p # ps, a) # branch) !. v = Some (qs', b)›
        ‹qs' !. v' = Some p›
        using v v' index_Cons by fast
      moreover have ‹Nom a at b in (p # ps, a) # branch›
        using Nom(2) by fastforce
      moreover have ‹descendants k i ((p # ps, a) # branch) xs›
        using Nom(7) descendants_block[where ps'=‹[p]›] by simp
      moreover have
        ‹((p # ps, a) # branch) !. length branch = Some (p # ps, a)›
        ‹(p # ps) !. length ps = Some p›
        by simp_all
      ultimately have ‹descendants k i ((p # ps, a) # branch) ?xs›
        using True Copied by fast
      then have ‹A ⊢ mapi_branch ?f ((p # ps, a) # branch)›
        using Nom(6-) by blast
      then have ‹A ⊢ (?p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
        unfolding mapi_branch_def by simp

      moreover have ‹(mapi (?f v) qs, b) ∈. mapi_branch ?f ((ps, a) # branch)›
        using v rev_nth_mapi_branch by fast
      then have ‹(mapi (?f v) qs, b) ∈. (mapi (?f (length branch)) ps, a) #
          mapi_branch ?f branch›
        unfolding mapi_branch_def by simp
      moreover have ‹?f v v' p on (mapi (?f v) qs, b)›
        using v v' rev_nth_mapi_block by fast
      then have ‹?p on (mapi (?f v) qs, b)›
        using p by simp

      moreover have ‹Nom a at b in mapi_branch ?f ((ps, a) # branch)›
        using Nom(2) nom_at_in_bridge by fast
      then have ‹Nom a at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
        unfolding mapi_branch_def by simp
      ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
        using A by (meson Nom' Nom(3))
      then have ‹A ⊢ (mapi (bridge k j xs (length branch)) ps, a) #
          mapi_branch (bridge k j xs) branch›
        using mapi_branch_head_add_oob[where branch=branch and ps=ps]
        unfolding mapi_branch_def by simp
      then show ?thesis
        unfolding mapi_branch_def by simp
    next
      case False
      let ?f = ‹bridge k j xs›

      have ‹descendants k i ((p # ps, a) # branch) xs›
        using Nom(7) descendants_no_head by fast
      then have ‹A ⊢ mapi_branch ?f ((p # ps, a) # branch)›
        using Nom(6-) by blast
      moreover have ‹(length branch, length ps) ∉ xs›
        using Nom(7) descendants_oob_head by fast
      ultimately have ‹A ⊢ (p # mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
        unfolding mapi_branch_def by simp

      moreover have ‹(mapi (?f v) qs, b) ∈. mapi_branch ?f ((ps, a) # branch)›
        using v rev_nth_mapi_branch by fast
      then have ‹(mapi (?f v) qs, b) ∈. (mapi (?f (length branch)) ps, a) #
          mapi_branch ?f branch›
        unfolding mapi_branch_def by simp
      moreover have ‹?f v v' p on (mapi (?f v) qs, b)›
        using v v' rev_nth_mapi_block by fast
      then have ‹p on (mapi (?f v) qs, b)›
        using False by simp
      moreover have ‹Nom a at b in mapi_branch ?f ((ps, a) # branch)›
        using Nom(2) nom_at_in_bridge by fast
      then have ‹Nom a at b in (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
        unfolding mapi_branch_def by simp
      ultimately have ‹A ⊢ (mapi (?f (length branch)) ps, a) # mapi_branch ?f branch›
        by (meson Nom' Nom(3))
      then show ?thesis
        unfolding mapi_branch_def by simp
    qed
  qed
qed

lemma STA_bridge:
  fixes i :: 'b
  assumes
    inf: ‹infinite (UNIV :: 'b set)› and
    ‹A ⊢ branch› ‹descendants k i branch xs›
    ‹Nom k at j in branch›
    ‹finite A› ‹j ∈ A›
  shows ‹A ⊢ mapi_branch (bridge k j xs) branch›
proof -
  have ‹A ⊢ ([], j) # branch›
    using assms(2, 5-6) inf STA_struct[where branch'=‹([], j) # branch›] by auto
  moreover have ‹descendants k i (([], j) # branch) xs›
    using assms(3) descendants_branch[where extra=‹[_]›] by fastforce
  ultimately have ‹A ⊢ mapi_branch (bridge k j xs) (([], j) # branch)›
    using STA_bridge' inf assms(3-) by fast
  then have *: ‹A ⊢ ([], j) # mapi_branch (bridge k j xs) branch›
    unfolding mapi_branch_def by simp
  have ‹branch_nominals (mapi_branch (bridge k j xs) branch) = branch_nominals branch›
    using nominals_mapi_branch_bridge assms(4-) by fast
  moreover have ‹j ∈ branch_nominals branch›
    using assms(4) unfolding branch_nominals_def by fastforce
  ultimately have ‹j ∈ branch_nominals (mapi_branch (bridge k j xs) branch)›
    by simp
  then show ?thesis
    using * GoTo by fast
qed

subsection ‹Derivation›

theorem Bridge:
  fixes i :: 'b
  assumes inf: ‹infinite (UNIV :: 'b set)› and fin: ‹finite A› and ‹j ∈ A›
    ‹Nom k at j in (ps, i) # branch› ‹(❙◇ Nom j) at i in (ps, i) # branch›
    ‹A ⊢ ((❙◇ Nom k) # ps, i) # branch›
  shows ‹A ⊢ (ps, i) # branch›
proof -
  let ?xs = ‹{(length branch, length ps)}›

  have ‹descendants k i (((❙◇ Nom k) # ps, i) # branch) ?xs›
    using Initial by force
  moreover have ‹Nom k at j in ((❙◇ Nom k) # ps, i) # branch›
    using assms(4) by fastforce
  ultimately have ‹A ⊢ mapi_branch (bridge k j ?xs) (((❙◇ Nom k) # ps, i) # branch)›
    using STA_bridge inf fin assms(3, 6) by fast
  then have ‹A ⊢ ((❙◇ Nom j) # mapi (bridge k j ?xs (length branch)) ps, i) #
      mapi_branch (bridge k j ?xs) branch›
    unfolding mapi_branch_def by simp
  moreover have ‹mapi_branch (bridge k j {(length branch, length ps)}) branch =
      mapi_branch (bridge k j {}) branch›
    using mapi_branch_add_oob[where xs=‹{}›] by fastforce
  moreover have ‹mapi (bridge k j ?xs (length branch)) ps =
    mapi (bridge k j {} (length branch)) ps›
    using mapi_block_add_oob[where xs=‹{}› and ps=ps] by simp
  ultimately have ‹A ⊢ ((❙◇ Nom j) # ps, i) # branch›
    using mapi_block_id[where ps=ps] mapi_branch_id[where branch=branch] by simp
  then show ?thesis
    using Dup assms(5) by (metis new_def)
qed

section ‹Completeness›

subsection ‹Hintikka›

abbreviation at_in_set :: ‹('a, 'b) fm ⇒ 'b ⇒ ('a, 'b) block set ⇒ bool› where
  ‹at_in_set p a S ≡ ∃ps. (ps, a) ∈ S ∧ p on (ps, a)›

notation at_in_set (‹_ at _ in'' _› [51, 51, 51] 50)

text ‹
  A set of blocks is Hintikka if it satisfies the following requirements.
  Intuitively, if it corresponds to an exhausted open branch
    with respect to the fixed set of allowed nominals ‹A›.
  For example, we only require symmetry, "if ‹j› occurs at ‹i› then ‹i› occurs at ‹j›" if ‹i ∈ A›.
›

locale Hintikka =
  fixes A :: ‹'b set› and H :: ‹('a, 'b) block set› assumes
    ProP: ‹Nom j at i in' H ⟹ Pro x at j in' H ⟹ ¬ (❙¬ Pro x) at i in' H› and
    NomP: ‹Nom a at i in' H ⟹ ¬ (❙¬ Nom a) at i in' H› and
    NegN: ‹(❙¬ ❙¬ p) at i in' H ⟹ p at i in' H› and
    DisP: ‹(p ❙∨ q) at i in' H ⟹ p at i in' H ∨ q at i in' H› and
    DisN: ‹(❙¬ (p ❙∨ q)) at i in' H ⟹ (❙¬ p) at i in' H ∧ (❙¬ q) at i in' H› and
    DiaP: ‹∄a. p = Nom a ⟹ (❙◇ p) at i in' H ⟹
      ∃j. (❙◇ Nom j) at i in' H ∧ (❙@ j p) at i in' H› and
    DiaN: ‹(❙¬ (❙◇ p)) at i in' H ⟹ (❙◇ Nom j) at i in' H ⟹ (❙¬ (❙@ j p)) at i in' H› and
    SatP: ‹(❙@ i p) at a in' H ⟹ p at i in' H› and
    SatN: ‹(❙¬ (❙@ i p)) at a in' H ⟹ (❙¬ p) at i in' H› and
    GoTo: ‹i ∈ nominals p ⟹ ∃a. p at a in' H ⟹ ∃ps. (ps, i) ∈ H› and
    Nom: ‹∀a. p = Nom a ∨ p = (❙◇ Nom a) ⟶ a ∈ A ⟹
      p at i in' H ⟹ Nom j at i in' H ⟹ p at j in' H›

text ‹
  Two nominals ‹i› and ‹j› are equivalent in respect to a Hintikka set ‹H› if
    ‹H› contains an ‹i›-block with ‹j› on it.
  This is an equivalence relation on the names in ‹H› intersected with the allowed nominals ‹A›.
›

definition hequiv :: ‹('a, 'b) block set ⇒ 'b ⇒ 'b ⇒ bool› where
  ‹hequiv H i j ≡ Nom j at i in' H›

abbreviation hequiv_rel :: ‹'b set ⇒ ('a, 'b) block set ⇒ ('b × 'b) set› where
  ‹hequiv_rel A H ≡ {(i, j) |i j. hequiv H i j ∧ i ∈ A ∧ j ∈ A}›

definition names :: ‹('a, 'b) block set ⇒ 'b set› where
  ‹names H ≡ {i |ps i. (ps, i) ∈ H}›

lemma hequiv_refl: ‹i ∈ names H ⟹ hequiv H i i›
  unfolding hequiv_def names_def by simp

lemma hequiv_refl': ‹(ps, i) ∈ H ⟹ hequiv H i i›
  using hequiv_refl unfolding names_def by fastforce

lemma hequiv_sym':
  assumes ‹Hintikka A H› ‹i ∈ A› ‹hequiv H i j›
  shows ‹hequiv H j i›
proof -
  have ‹i ∈ A ⟶ Nom i at i in' H ⟶ Nom j at i in' H ⟶ Nom i at j in' H› for i j
    using assms(1) Hintikka.Nom by fast
  then show ?thesis
    using assms(2-) unfolding hequiv_def by auto
qed

lemma hequiv_sym: ‹Hintikka A H ⟹ i ∈ A ⟹ j ∈ A ⟹ hequiv H i j ⟷ hequiv H j i›
  by (meson hequiv_sym')

lemma hequiv_trans:
  assumes ‹Hintikka A H› ‹i ∈ A› ‹k ∈ A› ‹hequiv H i j› ‹hequiv H j k›
  shows ‹hequiv H i k›
proof -
  have ‹hequiv H j i›
    by (meson assms(1-2, 4) hequiv_sym')
  moreover have ‹k ∈ A ⟶ Nom k at j in' H ⟶ Nom i at j in' H ⟶ Nom k at i in' H› for i k j
    using assms(1) Hintikka.Nom by fast
  ultimately show ?thesis
    using assms(3-) unfolding hequiv_def by blast
qed

lemma hequiv_names: ‹hequiv H i j ⟹ i ∈ names H›
  unfolding hequiv_def names_def by blast

lemma hequiv_names_rel:
  assumes ‹Hintikka A H›
  shows ‹hequiv_rel A H ⊆ names H × names H›
  using assms hequiv_names hequiv_sym by fast

lemma hequiv_refl_rel:
  assumes ‹Hintikka A H›
  shows ‹refl_on (names H ∩ A) (hequiv_rel A H)›
  unfolding refl_on_def using assms hequiv_refl hequiv_names_rel by fast

lemma hequiv_sym_rel: ‹Hintikka A H ⟹ sym (hequiv_rel A H)›
  unfolding sym_def using hequiv_sym by fast

lemma hequiv_trans_rel: ‹Hintikka B A ⟹ trans (hequiv_rel B A)›
  unfolding trans_def using hequiv_trans by fast

lemma hequiv_rel:
  assumes "Hintikka A H"
  shows ‹equiv (names H ∩ A) (hequiv_rel A H)›
proof (rule equivI)
  show "hequiv_rel A H ⊆ (names H ∩ A) × (names H ∩ A)"
    using hequiv_names_rel[OF ‹Hintikka A H›] by blast
next
  show "refl_on (names H ∩ A) (hequiv_rel A H)"
    using hequiv_refl_rel[OF ‹Hintikka A H›] .
next
  show "sym (hequiv_rel A H)"
    using hequiv_sym_rel[OF ‹Hintikka A H›] .
next
  show "trans (hequiv_rel A H)"
    using hequiv_trans_rel[OF ‹Hintikka A H›] .
qed

lemma nominal_in_names:
  assumes ‹Hintikka A H› ‹∃block ∈ H. i ∈ block_nominals block›
  shows ‹i ∈ names H›
  using assms Hintikka.GoTo unfolding names_def by fastforce

subsubsection ‹Named model›

text ‹
  Given a Hintikka set ‹H›, a formula ‹p› on a block in ‹H› and a set of allowed nominals ‹A›
    which contains all "root-like" nominals in ‹p› we construct a model that satisfies ‹p›.

  The worlds of our model are sets of equivalent nominals and
    nominals are assigned to the equivalence class of an equivalent allowed nominal.
  This definition resembles the "ur-father" notion.

  From a world ‹is›, we can reach a world ‹js› iff there is an ‹i ∈ is› and a ‹j ∈ js› s.t.
    there is an ‹i›-block in ‹H› with ‹❙◇ Nom j› on it.

  A propositional symbol ‹p› is true in a world ‹is› if there exists an ‹i ∈ is› s.t.
    ‹p› occurs on an ‹i›-block in ‹H›.
 ›

definition assign :: ‹'b set ⇒ ('a, 'b) block set ⇒ 'b ⇒ 'b set› where
  ‹assign A H i ≡ if ∃a. a ∈ A ∧ Nom a at i in' H
    then proj (hequiv_rel A H) (SOME a. a ∈ A ∧ Nom a at i in' H)
    else {i}›

definition reach :: ‹'b set ⇒ ('a, 'b) block set ⇒ 'b set ⇒ 'b set set› where
  ‹reach A H is ≡ {assign A H j |i j. i ∈ is ∧ (❙◇ Nom j) at i in' H}›

definition val :: ‹('a, 'b) block set ⇒ 'b set ⇒ 'a ⇒ bool› where
  ‹val H is x ≡ ∃i ∈ is. Pro x at i in' H›

lemma ex_assignment:
  assumes ‹Hintikka A H›
  shows ‹assign A H i ≠ {}›
proof (cases ‹∃b. b ∈ A ∧ Nom b at i in' H›)
  case True
  let ?b = ‹SOME b. b ∈ A ∧ Nom b at i in' H›
  have *: ‹?b ∈ A ∧ Nom ?b at i in' H›
    using someI_ex True .
  moreover from this have ‹hequiv H ?b ?b›
    using assms block_nominals nominal_in_names hequiv_refl
    by (metis (no_types, lifting) nominals.simps(2) singletonI)
  ultimately show ?thesis
    unfolding assign_def proj_def by auto
next
  case False
  then show ?thesis
    unfolding assign_def by auto
qed

lemma ur_closure:
  assumes ‹Hintikka A H› ‹p at i in' H› ‹∀a. p = Nom a ∨ p = (❙◇ Nom a) ⟶ a ∈ A›
  shows ‹∀a ∈ assign A H i. p at a in' H›
proof (cases ‹∃b. b ∈ A ∧ Nom b at i in' H›)
  case True
  let ?b = ‹SOME b. b ∈ A ∧ Nom b at i in' H›
  have *: ‹?b ∈ A ∧ Nom ?b at i in' H›
    using someI_ex True .
  then have ‹p at ?b in' H›
    using assms by (meson Hintikka.Nom)
  then have ‹p at a in' H› if ‹hequiv H ?b a› for a
    using that assms(1, 3) unfolding hequiv_def by (meson Hintikka.Nom)
  moreover have ‹assign A H i = proj (hequiv_rel A H) ?b›
    unfolding assign_def using True by simp
  ultimately show ?thesis
    unfolding proj_def by blast
next
  case False
  then show ?thesis
    unfolding assign_def using assms by auto
qed

lemma ur_closure':
  assumes ‹Hintikka A H› ‹p at i in' H› ‹∀a. p = Nom a ∨ p = (❙◇ Nom a) ⟶ a ∈ A›
  shows ‹∃a ∈ assign A H i. p at a in' H›
proof -
  obtain a where ‹a ∈ assign A H i›
    using assms(1) ex_assignment by fast
  then show ?thesis
    using assms ur_closure[where i=i] by blast
qed

lemma mem_hequiv_rel: ‹a ∈ proj (hequiv_rel A H) b ⟹ a ∈ A›
  unfolding proj_def by blast

lemma hequiv_proj:
  assumes ‹Hintikka A H›
    ‹Nom a at i in' H› ‹a ∈ A› ‹Nom b at i in' H› ‹b ∈ A›
  shows ‹proj (hequiv_rel A H) a = proj (hequiv_rel A H) b›
proof -
  have ‹equiv (names H ∩ A) (hequiv_rel A H)›
    using assms(1) hequiv_rel by fast
  moreover have ‹{a, b} ⊆ names H ∩ A›
    using assms(1-5) nominal_in_names by fastforce
  moreover have ‹Nom b at a in' H›
    using assms(1-2, 4-5) Hintikka.Nom by fast
  then have ‹hequiv H a b›
    unfolding hequiv_def by simp
  ultimately show ?thesis
    by (simp add: proj_iff)
qed

lemma hequiv_proj_opening:
  assumes ‹Hintikka A H› ‹Nom a at i in' H› ‹a ∈ A› ‹i ∈ A›
  shows ‹proj (hequiv_rel A H) a = proj (hequiv_rel A H) i›
  using hequiv_proj assms by fastforce

lemma assign_proj_refl:
  assumes ‹Hintikka A H› ‹Nom i at i in' H› ‹i ∈ A›
  shows ‹assign A H i = proj (hequiv_rel A H) i›
proof -
  let ?a = ‹SOME a. a ∈ A ∧ Nom a at i in' H›
  have ‹∃a. a ∈ A ∧ Nom a at i in' H›
    using assms(2-3) by fast
  with someI_ex have *: ‹?a ∈ A ∧ Nom ?a at i in' H› .
  then have ‹assign A H i = proj (hequiv_rel A H) ?a›
    unfolding assign_def by auto
  then show ?thesis
    unfolding assign_def
    using hequiv_proj * assms by fast
qed

lemma assign_named:
  assumes ‹Hintikka A H› ‹i ∈ proj (hequiv_rel A H) a›
  shows ‹i ∈ names H›
  using assms unfolding proj_def by simp (meson hequiv_names hequiv_sym')

lemma assign_unique:
  assumes ‹Hintikka A H› ‹a ∈ assign A H i›
  shows ‹assign A H a = assign A H i›
proof (cases ‹∃b. b ∈ A ∧ Nom b at i in' H›)
  case True
  let ?b = ‹SOME b. b ∈ A ∧ Nom b at i in' H›
  have *: ‹?b ∈ A ∧ Nom ?b at i in' H›
    using someI_ex True .

  have **: ‹assign A H i = proj (hequiv_rel A H) ?b›
    unfolding assign_def using True by simp
  moreover from this have ‹Nom a at a in' H›
    using assms assign_named unfolding names_def by fastforce
  ultimately have ‹assign A H a = proj (hequiv_rel A H) a›
    using assms assign_proj_refl mem_hequiv_rel by fast
  with ** show ?thesis
    unfolding proj_def using assms
    by simp (meson hequiv_sym' hequiv_trans)
next
  case False
  then have ‹assign A H i = {i}›
    unfolding assign_def by auto
  then have ‹a = i›
    using assms(2) by simp
  then show ?thesis
    by simp
qed

lemma assign_val:
  assumes
    ‹Hintikka A H› ‹Pro x at a in' H› ‹(❙¬ Pro x) at i in' H›
    ‹a ∈ assign A H i› ‹i ∈ names H›
  shows False
  using assms Hintikka.ProP ur_closure by fastforce

lemma Hintikka_model:
  assumes ‹Hintikka A H›
  shows
    ‹p at i in' H ⟹ nominals p ⊆ A ⟹
        Model (reach A H) (val H), assign A H, assign A H i ⊨ p›
    ‹(❙¬ p) at i in' H ⟹ nominals p ⊆ A ⟹
      ¬ Model (reach A H) (val H), assign A H, assign A H i ⊨ p›
proof (induct p arbitrary: i)
  fix i
  case (Pro x)
  assume ‹Pro x at i in' H›
  then show ‹Model (reach A H) (val H), assign A H, assign A H i ⊨ Pro x›
    using assms(1) ur_closure' unfolding val_def by fastforce
next
  fix i
  case (Pro x)
  assume ‹(❙¬ Pro x) at i in' H›
  then have ‹∄a. a ∈ assign A H i ∧ Pro x at a in' H›
    using assms(1) assign_val unfolding names_def by fast
  then have ‹¬ val H (assign A H i) x›
    unfolding proj_def val_def hequiv_def by simp
  then show ‹¬ Model (reach A H) (val H), assign A H, assign A H i ⊨ Pro x›
    by simp
next
  fix i
  case (Nom a)
  assume *: ‹Nom a at i in' H› ‹nominals (Nom a) ⊆ A›

  let ?b = ‹SOME b. b ∈ A ∧ Nom b at i in' H›
  let ?c = ‹SOME b. b ∈ A ∧ Nom b at a in' H›

  have ‹a ∈ A›
    using *(2) by simp
  then have ‹∃b. b ∈ A ∧ Nom b at i in' H›
    using * by fast
  with someI_ex have b: ‹?b ∈ A ∧ Nom ?b at i in' H› .
  then have ‹assign A H i = proj (hequiv_rel A H) ?b›
    unfolding assign_def by auto
  also have ‹proj (hequiv_rel A H) ?b = proj (hequiv_rel A H) a›
    using hequiv_proj assms(1) b * ‹a ∈ A› by fast

  also have ‹Nom a at a in' H›
    using * ‹a ∈ A› assms(1) Hintikka.Nom by fast
  then have ‹∃c. c ∈ A ∧ Nom c at a in' H›
    using ‹a ∈ A› by blast
  with someI_ex have c: ‹?c ∈ A ∧ Nom ?c at a in' H› .
  then have ‹assign A H a = proj (hequiv_rel A H) ?c›
    unfolding assign_def by auto
  then have ‹proj (hequiv_rel A H) a = assign A H a›
    using hequiv_proj_opening assms(1) ‹a ∈ A› c by fast

  finally have ‹assign A H i = assign A H a› .
  then show ‹Model (reach A H) (val H), assign A H, assign A H i ⊨ Nom a›
    by simp
next
  fix i
  case (Nom a)
  assume *: ‹(❙¬ Nom a) at i in' H› ‹nominals (Nom a) ⊆ A›
  then have ‹a ∈ A›
    by simp

  have ‹hequiv H a a›
    using hequiv_refl * nominal_in_names assms(1) by fastforce
  obtain j where j: ‹j ∈ assign A H i› ‹(❙¬ Nom a) at j in' H›
    using ur_closure' assms(1) * by fastforce
  then have ‹¬ Nom a at j in' H›
    using assms(1) Hintikka.NomP by fast

  moreover have ‹∀b ∈ assign A H a. Nom a at b in' H›
    using assms ‹a ∈ A› ‹hequiv H a a› ur_closure unfolding hequiv_def by fast
  ultimately have ‹assign A H a ≠ assign A H i›
    using j by blast
  then show ‹¬ Model (reach A H) (val H), assign A H, assign A H i ⊨ Nom a›
    by simp
next
  fix i
  case (Neg p)
  moreover assume ‹(❙¬ p) at i in' H› ‹nominals (❙¬ p) ⊆ A›
  ultimately show ‹Model (reach A H) (val H), assign A H, assign A H i ⊨ ❙¬ p›
    by simp
next
  fix i
  case (Neg p)
  moreover assume *: ‹(❙¬ ❙¬ p) at i in' H›
  then have ‹p at i in' H›
    using assms(1) Hintikka.NegN by fast
  moreover assume ‹nominals (❙¬ p) ⊆ A›
  moreover from this * have ‹∀a. p = (❙◇ Nom a) ⟶ a ∈ A›
    by auto
  ultimately show ‹¬ Model (reach A H) (val H), assign A H, assign A H i ⊨ ❙¬ p›
    using assms(1) by auto
next
  fix i
  case (Dis p q)
  moreover assume *: ‹(p ❙∨ q) at i in' H›
  then have ‹p at i in' H ∨ q at i in' H›
    using assms(1) Hintikka.DisP by fast
  moreover assume ‹nominals (p ❙∨ q) ⊆ A›
  moreover from this * have ‹∀a. p = (❙◇ Nom a) ⟶ a ∈ A› ‹∀a. q = (❙◇ Nom a) ⟶ a ∈ A›
    by auto
  ultimately show ‹Model (reach A H) (val H), assign A H, assign A H i ⊨ (p ❙∨ q)›
    by simp metis
next
  fix i
  case (Dis p q)
  moreover assume *: ‹(❙¬ (p ❙∨ q)) at i in' H›
  then have ‹(❙¬ p) at i in' H› ‹(❙¬ q) at i in' H›
    using assms(1) Hintikka.DisN by fast+
  moreover assume ‹nominals (p ❙∨ q) ⊆ A›
  moreover from this * have ‹∀a. p = (❙◇ Nom a) ⟶ a ∈ A› ‹∀a. q = (❙◇ Nom a) ⟶ a ∈ A›
    by auto
  ultimately show ‹¬ Model (reach A H) (val H), assign A H, assign A H i ⊨ (p ❙∨ q)›
    by auto
next
  fix i
  case (Dia p)
  assume *: ‹(❙◇ p) at i in' H› ‹nominals (❙◇ p) ⊆ A›
  with * have p: ‹∀a. p = (❙◇ Nom a) ⟶ a ∈ A›
    by auto

  show ‹Model (reach A H) (val H), assign A H, assign A H i ⊨ ❙◇ p›
  proof (cases ‹∃j. p = Nom j›)
    case True
    then obtain j where j: ‹p = Nom j› ‹j ∈ A›
      using *(2) by auto
    then obtain a where a: ‹a ∈ assign A H i› ‹(❙◇ Nom j) at a in' H›
      using ur_closure' assms(1) ‹(❙◇ p) at i in' H› by fast

    from j have ‹(❙◇ Nom j) at i in' H›
      using *(1) by simp
    then have ‹(❙◇ Nom j) at a in' H›
      using ur_closure assms(1) a(2) by fast
    then have ‹assign A H j ∈ reach A H (assign A H i)›
      unfolding reach_def using a(1) by fast
    then show ?thesis
      using j(1) by simp
  next
    case False
    then obtain a where a: ‹a ∈ assign A H i› ‹(❙◇ p) at a in' H›
      using ur_closure' assms(1) ‹(❙◇ p) at i in' H› by fast
    then have ‹∃j. (❙◇ Nom j) at a in' H ∧ (❙@ j p) at a in' H›
      using False assms ‹(❙◇ p) at i in' H› by (meson Hintikka.DiaP)
    then obtain j where j: ‹(❙◇ Nom j) at a in' H› ‹(❙@ j p) at a in' H›
      by blast

    from j(2) have ‹p at j in' H›
      using assms(1) Hintikka.SatP by fast
    then have ‹Model (reach A H) (val H), assign A H, assign A H j ⊨ p›
      using Dia p *(2) by simp
    moreover have ‹assign A H j ∈ reach A H (assign A H i)›
      unfolding reach_def using a(1) j(1) by blast
    ultimately show ?thesis
      by auto
  qed
next
  fix i
  case (Dia p)
  assume *: ‹(❙¬ (❙◇ p)) at i in' H› ‹nominals (❙◇ p) ⊆ A›
  then obtain a where a: ‹a ∈ assign A H i› ‹(❙¬ (❙◇ p)) at a in' H›
    using ur_closure' assms(1) by fast
  {
    fix j b
    assume ‹(❙◇ Nom j) at b in' H› ‹b ∈ assign A H a›
    moreover have ‹(❙¬ (❙◇ p)) at b in' H›
      using a(2) assms(1) calculation(2) ur_closure by fast
    ultimately have ‹(❙¬ (❙@ j p)) at b in' H›
      using assms(1) Hintikka.DiaN by fast
    then have ‹(❙¬ p) at j in' H›
      using assms(1) Hintikka.SatN by fast
    then have ‹¬ Model (reach A H) (val H), assign A H, assign A H j ⊨ p›
      using Dia *(2) by simp
  }
  then have ‹¬ Model (reach A H) (val H), assign A H, assign A H a ⊨ ❙◇ p›
    unfolding reach_def by auto
  moreover have ‹assign A H a = assign A H i›
    using assms(1) a assign_unique by fast
  ultimately show ‹¬ Model (reach A H) (val H), assign A H, assign A H i ⊨ ❙◇ p›
    by simp
next
  fix i
  case (Sat j p)
  assume ‹(❙@ j p) at i in' H› ‹nominals (❙@ j p) ⊆ A›
  moreover from this have ‹∀a. p = (❙◇ Nom a) ⟶ a ∈ A›
    by auto
  moreover have ‹p at j in' H› if ‹∃a. (❙@ j p) at a in' H›
    using that assms(1) Hintikka.SatP by fast
  ultimately show ‹Model (reach A H) (val H), assign A H, assign A H i ⊨ ❙@ j p›
    using Sat by auto
next
  fix i
  case (Sat j p)
  assume ‹(❙¬ (❙@ j p)) at i in' H› ‹nominals (❙@ j p) ⊆ A›
  moreover from this have ‹∀a. p = (❙◇ Nom a) ⟶ a ∈ A›
    by auto
  moreover have ‹(❙¬ p) at j in' H› if ‹∃a. (❙¬ (❙@ j p)) at a in' H›
    using that assms(1) Hintikka.SatN by fast
  ultimately show ‹¬ Model (reach A H) (val H), assign A H, assign A H i ⊨ ❙@ j p›
    using Sat by fastforce
qed

subsection ‹Lindenbaum-Henkin›

text ‹
  A set of blocks is consistent if no finite subset can be derived.
  Given a consistent set of blocks we are going to extend it to be
    saturated and maximally consistent and show that is then Hintikka.
  All definitions are with respect to the set of allowed nominals.
›

definition consistent :: ‹'b set ⇒ ('a, 'b) block set ⇒ bool› where
  ‹consistent A S ≡ ∄S'. set S' ⊆ S ∧ A ⊢ S'›

instance fm :: (countable, countable) countable
  by countable_datatype

definition proper_dia :: ‹('a, 'b) fm ⇒ ('a, 'b) fm option› where
  ‹proper_dia p ≡ case p of (❙◇ p) ⇒ (if ∄a. p = Nom a then Some p else None) | _ ⇒ None›

lemma proper_dia: ‹proper_dia p = Some q ⟹ p = (❙◇ q) ∧ (∄a. q = Nom a)›
  unfolding proper_dia_def by (cases p) (simp_all, metis option.discI option.inject)

text ‹The following function witnesses each ‹❙◇ p› in a fresh world.›

primrec witness_list :: ‹('a, 'b) fm list ⇒ 'b set ⇒ ('a, 'b) fm list› where
  ‹witness_list [] _ = []›
| ‹witness_list (p # ps) used =
    (case proper_dia p of
      None ⇒ witness_list ps used
    | Some q ⇒
        let i = SOME i. i ∉ used
        in (❙@ i q) # (❙◇ Nom i) # witness_list ps ({i} ∪ used))›

primrec witness :: ‹('a, 'b) block ⇒ 'b set ⇒ ('a, 'b) block› where
  ‹witness (ps, a) used = (witness_list ps used, a)›

lemma witness_list:
  ‹proper_dia p = Some q ⟹ witness_list (p # ps) used =
    (let i = SOME i. i ∉ used
     in (❙@ i q) # (❙◇ Nom i) # witness_list ps ({i} ∪ used))›
  by simp

primrec extend ::
  ‹'b set ⇒ ('a, 'b) block set ⇒ (nat ⇒ ('a, 'b) block) ⇒ nat ⇒ ('a, 'b) block set› where
  ‹extend A S f 0 = S›
| ‹extend A S f (Suc n) =
    (if ¬ consistent A ({f n} ∪ extend A S f n)
     then extend A S f n
     else
      let used = A ∪ (⋃block ∈ {f n} ∪ extend A S f n. block_nominals block)
      in {f n, witness (f n) used} ∪ extend A S f n)›

definition Extend ::
  ‹'b set ⇒ ('a, 'b) block set ⇒ (nat ⇒ ('a, 'b) block) ⇒ ('a, 'b) block set› where
  ‹Extend A S f ≡ (⋃n. extend A S f n)›

lemma extend_chain: ‹extend A S f n ⊆ extend A S f (Suc n)›
  by auto

lemma extend_mem: ‹S ⊆ extend A S f n›
  by (induct n) auto

lemma Extend_mem: ‹S ⊆ Extend A S f›
  unfolding Extend_def using extend_mem by fast

subsubsection ‹Consistency›

lemma split_list:
  ‹set A ⊆ {x} ∪ X ⟹ x ∈. A ⟹ ∃B. set (x # B) = set A ∧ x ∉ set B›
  by simp (metis Diff_insert_absorb mk_disjoint_insert set_removeAll)

lemma consistent_drop_single:
  fixes a :: 'b
  assumes
    inf: ‹infinite (UNIV :: 'b set)› and
    fin: ‹finite A› and
    cons: ‹consistent A ({(p # ps, a)} ∪ S)›
  shows ‹consistent A ({(ps, a)} ∪ S)›
  unfolding consistent_def
proof
  assume ‹∃S'. set S' ⊆ {(ps, a)} ∪ S ∧ A ⊢ S'›
  then obtain S' n where ‹set S' ⊆ {(ps, a)} ∪ S› ‹(ps, a) ∈. S'› ‹A, n ⊢ S'›
    using assms unfolding consistent_def by blast
  then obtain S'' where ‹set ((ps, a) # S'') = set S'› ‹(ps, a) ∉ set S''›
    using split_list by metis
  then have ‹A ⊢ (ps, a) # S''›
    using inf fin STA_struct ‹A, n ⊢ S'› by blast
  then have ‹A ⊢ (p # ps, a) # S''›
    using inf fin STA_struct_block[where ps'=‹p # ps›] by fastforce
  moreover have ‹set ((p # ps, a) # S'') ⊆ {(p # ps, a)} ∪ S›
    using ‹(ps, a) ∉ set S''› ‹set ((ps, a) # S'') = set S'› ‹set S' ⊆ {(ps, a)} ∪ S› by auto
  ultimately show False
    using cons unfolding consistent_def by blast
qed

lemma consistent_drop_block: ‹consistent A ({block} ∪ S) ⟹ consistent A S›
  unfolding consistent_def by blast

lemma inconsistent_weaken: ‹¬ consistent A S ⟹ S ⊆ S' ⟹ ¬ consistent A S'›
  unfolding consistent_def by blast

lemma finite_nominals_set: ‹finite S ⟹ finite (⋃block ∈ S. block_nominals block)›
  by (induct S rule: finite_induct) (simp_all add: finite_block_nominals)

lemma witness_list_used:
  fixes i :: 'b
  assumes inf: ‹infinite (UNIV :: 'b set)› and ‹finite used› ‹i ∉ list_nominals ps›
  shows ‹i ∉ list_nominals (witness_list ps ({i} ∪ used))›
  using assms(2-)
proof (induct ps arbitrary: used)
  case (Cons p ps)
  then show ?case
  proof (cases ‹proper_dia p›)
    case (Some q)
    let ?j = ‹SOME j. j ∉ {i} ∪ used›
    have ‹finite ({i} ∪ used)›
      using ‹finite used› by simp
    then have ‹∃j. j ∉ {i} ∪ used›
      using inf ex_new_if_finite by metis
    then have j: ‹?j ∉ {i} ∪ used›
      using someI_ex by metis

    have ‹witness_list (p # ps) ({i} ∪ used) =
        (❙@ ?j q) # (❙◇ Nom ?j) # witness_list ps ({?j} ∪ ({i} ∪ used))›
      using Some witness_list by metis
    then have *: ‹list_nominals (witness_list (p # ps) ({i} ∪ used)) =
        {?j} ∪ nominals q ∪ list_nominals (witness_list ps ({?j} ∪ ({i} ∪ used)))›
      by simp

    have ‹finite ({?j} ∪ used)›
      using ‹finite used› by simp
    moreover have ‹i ∉ list_nominals ps›
      using ‹i ∉ list_nominals (p # ps)› by simp
    ultimately have ‹i ∉ list_nominals (witness_list ps ({i} ∪ ({?j} ∪ used)))›
      using Cons by metis
    moreover have ‹{i} ∪ ({?j} ∪ used) = {?j} ∪ ({i} ∪ used)›
      by blast
    moreover have ‹i ≠ ?j›
      using j by auto
    ultimately have ‹i ∈ list_nominals (witness_list (p # ps) ({i} ∪ used)) ⟷ i ∈ nominals q›
      using * by simp
    moreover have ‹i ∉ nominals q›
      using Cons(3) Some proper_dia by fastforce
    ultimately show ?thesis
      by blast
  qed simp
qed simp

lemma witness_used:
  fixes i :: 'b
  assumes inf: ‹infinite (UNIV :: 'b set)› and
    ‹finite used› ‹i ∉ block_nominals block›
  shows ‹i ∉ block_nominals (witness block ({i} ∪ used))›
  using assms witness_list_used by (induct block) fastforce

lemma consistent_witness_list:
  fixes a :: 'b
  assumes inf: ‹infinite (UNIV :: 'b set)› and ‹consistent A S›
    ‹(ps, a) ∈ S› ‹finite used› ‹A ∪ ⋃ (block_nominals ` S) ⊆ used›
  shows ‹consistent A ({(witness_list ps used, a)} ∪ S)›
  using assms(2-)
proof (induct ps arbitrary: used S)
  case Nil
  then have ‹{(witness_list [] used, a)} ∪ S = S›
    by auto
  moreover have ‹finite {}› ‹{} ∩ used = {}›
    by simp_all
  ultimately show ?case
    using ‹consistent A S› by simp
next
  case (Cons p ps)
  have fin: ‹finite A›
    using assms(4-5) finite_subset by fast
  have ‹{(p # ps, a)} ∪ S = S›
    using ‹(p # ps, a) ∈ S› by blast
  then have ‹consistent A ({(p # ps, a)} ∪ S)›
    using ‹consistent A S› by simp
  then have ‹consistent A ({(ps, a)} ∪ S)›
    using inf fin consistent_drop_single by fast
  moreover have ‹(ps, a) ∈ {(ps, a)} ∪ S›
    by simp
  moreover have ‹A ∪ ⋃ (block_nominals ` ({(ps, a)} ∪ S)) ⊆ extra ∪ used› for extra
    using ‹(p # ps, a) ∈ S› ‹A ∪ ⋃ (block_nominals ` S) ⊆ used› by fastforce
  moreover have ‹finite (extra ∪ used)› if ‹finite extra› for extra
    using that ‹finite used› by blast
  ultimately have cons:
    ‹consistent A ({(witness_list ps (extra ∪ used), a)} ∪ ({(ps, a)} ∪ S))›
    if ‹finite extra› for extra
    using that Cons by metis

  show ?case
  proof (cases ‹proper_dia p›)
    case None
    then have ‹witness_list (p # ps) used = witness_list ps used›
      by auto
    moreover have ‹consistent A ({(witness_list ps used, a)} ∪ ({(ps, a)} ∪ S))›
      using cons[where extra=‹{}›] by simp
    then have ‹consistent A ({(witness_list ps used, a)} ∪ S)›
      using consistent_drop_block[where block=‹(ps, a)›] by auto
    ultimately show ?thesis
      by simp
  next
    case (Some q)
    let ?i = ‹SOME i. i ∉ used›
    have ‹∃i. i ∉ used›
      using ex_new_if_finite inf ‹finite used› .
    with someI_ex have ‹?i ∉ used› .
    then have i: ‹?i ∉ ⋃ (block_nominals ` S)›
      using Cons by auto
    then have ‹?i ∉ block_nominals (p # ps, a)›
      using Cons by blast

    let ?tail = ‹witness_list ps ({?i} ∪ used)›

    have ‹consistent A ({(?tail, a)} ∪ ({(ps, a)} ∪ S))›
      using cons[where extra=‹{?i}›] by blast
    then have *: ‹consistent A ({(?tail, a)} ∪ S)›
      using consistent_drop_block[where block=‹(ps, a)›] by simp

    have ‹witness_list (p # ps) used = (❙@ ?i q) # (❙◇ Nom ?i) # ?tail›
      using Some witness_list by metis
    moreover have ‹consistent A ({((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a)} ∪ S)›
      unfolding consistent_def
    proof
      assume ‹∃S'. set S' ⊆ {((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a)} ∪ S ∧ A ⊢ S'›
      then obtain S' n where
        ‹A, n ⊢ S'› and S':
        ‹set S' ⊆ {((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a)} ∪ S›
        ‹((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a) ∈. S'›
        using * unfolding consistent_def by blast
      then obtain S'' where S'':
        ‹set (((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a) # S'') = set S'›
        ‹((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a) ∉ set S''›
        using split_list[where x=‹((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a)›] by blast
      then have ‹A ⊢ ((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a) # S''›
        using inf ‹finite A› STA_struct ‹A, n ⊢ S'› by blast
      moreover have ‹set (((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a) # S'') ⊆
        set (((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a) # (p # ps, a) # S'')›
        by auto
      ultimately have **: ‹A ⊢ ((❙@ ?i q) # (❙◇ Nom ?i) # ?tail, a) # (p # ps, a) # S''›
        using inf ‹finite A› STA_struct by blast

      have ‹?i ∉ block_nominals (?tail, a)›
        using inf ‹finite used› ‹?i ∉ block_nominals (p # ps, a)› witness_used by fastforce
      moreover have ‹?i ∉ branch_nominals S''›
        unfolding branch_nominals_def using i S' S'' by auto
      ultimately have ‹?i ∉ branch_nominals ((?tail, a) # (p # ps, a) # S'')›
        using ‹?i ∉ block_nominals (p # ps, a)› unfolding branch_nominals_def
        by simp
      then have ‹?i ∉ A ∪ branch_nominals ((?tail, a) # (p # ps, a) # S'')›
        using ‹?i ∉ used› Cons.prems(4) by blast

      moreover have ‹∄a. q = Nom a›
        using Some proper_dia by blast
      moreover have ‹(p # ps, a) ∈. (?tail, a) # (p # ps, a) # S''›
        by simp
      moreover have ‹p = (❙◇ q)›
        using Some proper_dia by blast
      then have ‹(❙◇ q) on (p # ps, a)›
        by simp
      ultimately have ‹A ⊢ (?tail, a) # (p # ps, a) # S''›
        using ** ‹finite A› DiaP'' by fast
      moreover have ‹set ((p # ps, a) # S'') ⊆ S›
        using Cons(3) S' S'' by auto
      ultimately show False
        using * unfolding consistent_def by (simp add: subset_Un_eq)
    qed
    ultimately show ?thesis
      by simp
  qed
qed

lemma consistent_witness:
  fixes block :: ‹('a, 'b) block›
  assumes ‹infinite (UNIV :: 'b set)›
    ‹consistent A S› ‹finite (⋃ (block_nominals ` S))› ‹block ∈ S› ‹finite A›
  shows ‹consistent A ({witness block (A ∪ ⋃ (block_nominals ` S))} ∪ S)›
  using assms consistent_witness_list by (cases block) fastforce

lemma consistent_extend:
  fixes S :: ‹('a, 'b) block set›
  assumes inf: ‹infinite (UNIV :: 'b set)› and fin: ‹finite A› and
    ‹consistent A (extend A S f n)› ‹finite (⋃ (block_nominals ` extend A S f n))›
  shows ‹consistent A (extend A S f (Suc n))›
proof (cases ‹consistent A ({f n} ∪ extend A S f n)›)
  case True
  let ?used = ‹A ∪ (⋃block ∈ {f n} ∪ extend A S f n. block_nominals block)›
  have *: ‹extend A S f (n + 1) = {f n, witness (f n) ?used} ∪ extend A S f n›
    using True by simp

  have ‹consistent A ({f n} ∪ extend A S f n)›
    using True by simp
  moreover have ‹finite ((⋃ (block_nominals ` ({f n} ∪ extend A S f n))))›
    using ‹finite (⋃ (block_nominals ` extend A S f n))› finite_nominals_set by force
  moreover have ‹f n ∈ {f n} ∪ extend A S f n›
    by simp
  ultimately have ‹consistent A ({witness (f n) ?used} ∪ ({f n} ∪ extend A S f n))›
    using inf fin consistent_witness by blast
  then show ?thesis
    using * by simp
next
  case False
  then show ?thesis
    using assms(3) by simp
qed

lemma finite_nominals_extend:
  assumes ‹finite (⋃ (block_nominals ` S))›
  shows ‹finite (⋃ (block_nominals ` extend A S f n))›
  using assms by (induct n) (auto simp add: finite_block_nominals)

lemma consistent_extend':
  fixes S :: ‹('a, 'b) block set›
  assumes ‹infinite (UNIV :: 'b set)› ‹finite A› ‹consistent A S› ‹finite (⋃ (block_nominals ` S))›
  shows ‹consistent A (extend A S f n)›
  using assms
proof (induct n)
  case (Suc n)
  then show ?case
    by (metis consistent_extend finite_nominals_extend)
qed simp

lemma UN_finite_bound:
  assumes ‹finite A› ‹A ⊆ (⋃n. f n)›
  shows ‹∃m :: nat. A ⊆ (⋃n ≤ m. f n)›
  using assms
proof (induct A rule: finite_induct)
  case (insert x A)
  then obtain m where ‹A ⊆ (⋃n ≤ m. f n)›
    by fast
  then have ‹A ⊆ (⋃n ≤ (m + k). f n)› for k
    by fastforce
  moreover obtain m' where ‹x ∈ f m'›
    using insert(4) by blast
  ultimately have ‹{x} ∪ A ⊆ (⋃n ≤ m + m'. f n)›
    by auto
  then show ?case
    by blast
qed simp

lemma extend_bound: ‹(⋃n ≤ m. extend A S f n) = extend A S f m›
proof (induct m)
  case (Suc m)
  have ‹⋃ (extend A S f ` {..Suc m}) = ⋃ (extend A S f ` {..m}) ∪ extend A S f (Suc m)›
    using atMost_Suc by auto
  also have ‹… = extend A S f m ∪ extend A S f (Suc m)›
    using Suc by blast
  also have ‹… = extend A S f (Suc m)›
    using extend_chain by blast
  finally show ?case
    by simp
qed simp

lemma consistent_Extend:
  fixes S :: ‹('a, 'b) block set›
  assumes inf: ‹infinite (UNIV :: 'b set)› and ‹finite A›
    ‹consistent A S› ‹finite (⋃ (block_nominals ` S))›
  shows ‹consistent A (Extend A S f)›
  unfolding Extend_def
proof (rule ccontr)
  assume ‹¬ consistent A (⋃ (range (extend A S f)))›
  then obtain S' n where *:
    ‹A, n ⊢ S'›
    ‹set S' ⊆ (⋃n. extend A S f n)›
    unfolding consistent_def by blast
  moreover have ‹finite (set S')›
    by simp
  ultimately obtain m where ‹set S' ⊆ (⋃n ≤ m. extend A S f n)›
    using UN_finite_bound by metis
  then have ‹set S' ⊆ extend A S f m›
    using extend_bound by blast
  moreover have ‹consistent A (extend A S f m)›
    using assms consistent_extend' by blast
  ultimately show False
    unfolding consistent_def using * by blast
qed

subsubsection ‹Maximality›

text ‹A set of blocks is maximally consistent if any proper extension makes it inconsistent.›

definition maximal :: ‹'b set ⇒ ('a, 'b) block set ⇒ bool› where
  ‹maximal A S ≡ consistent A S ∧ (∀block. block ∉ S ⟶ ¬ consistent A ({block} ∪ S))›

lemma extend_not_mem:
  ‹f n ∉ extend A S f (Suc n) ⟹ ¬ consistent A ({f n} ∪ extend A S f n)›
  by (metis Un_insert_left extend.simps(2) insertI1)

lemma maximal_Extend:
  fixes S :: ‹('a, 'b) block set›
  assumes inf: ‹infinite (UNIV :: 'b set)› and ‹finite A›
    ‹consistent A S› ‹finite (⋃ (block_nominals ` S))› ‹surj f›
  shows ‹maximal A (Extend A S f)›
proof (rule ccontr)
  assume ‹¬ maximal A (Extend A S f)›
  then obtain block where
    ‹block ∉ Extend A S f› ‹consistent A ({block} ∪ Extend A S f)›
    unfolding maximal_def using assms consistent_Extend by metis
  obtain n where n: ‹f n = block›
    using ‹surj f› unfolding surj_def by metis
  then have ‹block ∉ extend A S f (Suc n)›
    using ‹block ∉ Extend A S f› extend_chain unfolding Extend_def by blast
  then have ‹¬ consistent A ({block} ∪ extend A S f n)›
    using n extend_not_mem by blast
  moreover have ‹block ∉ extend A S f n›
    using ‹block ∉ extend A S f (Suc n)› extend_chain by blast
  then have ‹{block} ∪ extend A S f n ⊆ {block} ∪ Extend A S f›
    unfolding Extend_def by blast
  ultimately have ‹¬ consistent A ({block} ∪ Extend A S f)›
    using inconsistent_weaken by blast
  then show False
    using ‹consistent A ({block} ∪ Extend A S f)› by simp
qed

subsubsection ‹Saturation›

text ‹A set of blocks is saturated if every ‹❙◇ p› is witnessed.›

definition saturated :: ‹('a, 'b) block set ⇒ bool› where
  ‹saturated S ≡ ∀p i. (❙◇ p) at i in' S ⟶ (∄a. p = Nom a) ⟶
    (∃j. (❙@ j p) at i in' S ∧ (❙◇ Nom j) at i in' S)›

lemma witness_list_append:
  ‹∃extra. witness_list (ps @ qs) used = witness_list ps used @ witness_list qs (extra ∪ used)›
proof (induct ps arbitrary: used)
  case Nil
  then show ?case
    by (metis Un_absorb append_self_conv2 witness_list.simps(1))
next
  case (Cons p ps)
  show ?case
  proof (cases ‹∃q. proper_dia p = Some q›)
    case True
    let ?i = ‹SOME i. i ∉ used›
    from True obtain q where q: ‹proper_dia p = Some q›
      by blast
    moreover have ‹(p # ps) @ qs = p # (ps @ qs)›
      by simp
    ultimately have
      ‹witness_list ((p # ps) @ qs) used = (❙@ ?i q) # (❙◇ Nom ?i) #
       witness_list (ps @ qs) ({?i} ∪ used)›
      using witness_list by metis
    then have
      ‹∃extra. witness_list ((p # ps) @ qs) used = (❙@ ?i q) # (❙◇ Nom ?i) #
        witness_list ps ({?i} ∪ used) @ witness_list qs (extra ∪ ({?i} ∪ used))›
      using Cons by metis
    moreover have ‹(❙@ ?i q) # (❙◇ Nom ?i) # witness_list ps ({?i} ∪ used) =
        witness_list (p # ps) used›
      using q witness_list by metis
    ultimately have ‹∃extra. witness_list ((p # ps) @ qs) used =
        witness_list (p # ps) used @ witness_list qs (extra ∪ ({?i} ∪ used))›
      by (metis append_Cons)
    then have ‹∃extra. witness_list ((p # ps) @ qs) used =
        witness_list (p # ps) used @ witness_list qs (({?i} ∪ extra) ∪ used)›
      by simp
    then show ?thesis
      by blast
  qed (simp add: Cons)
qed

lemma ex_witness_list:
  assumes ‹p ∈. ps› ‹proper_dia p = Some q›
  shows ‹∃i. {❙@ i q, ❙◇ Nom i} ⊆ set (witness_list ps used)›
  using ‹p ∈. ps›
proof (induct ps arbitrary: used)
  case (Cons a ps)
  then show ?case
  proof (induct ‹a = p›)
    case True
    then have
      ‹∃i. witness_list (a # ps) used = (❙@ i q) # (❙◇ Nom i) #
        witness_list ps ({i} ∪ used)›
      using ‹proper_dia p = Some q› witness_list by metis
    then show ?case
      by auto
  next
    case False
    then have ‹∃i. {❙@ i q, ❙◇ Nom i} ⊆ set (witness_list ps (extra ∪ used))› for extra
      by simp
    moreover have ‹∃extra. witness_list (a # ps) used =
        witness_list [a] used @ witness_list ps (extra ∪ used)›
      using witness_list_append[where ps=‹[_]›] by simp
    ultimately show ?case
      by fastforce
  qed
qed simp

lemma saturated_Extend:
  fixes S :: ‹('a, 'b) block set›
  assumes inf: ‹infinite (UNIV :: 'b set)› and fin: ‹finite A› and
    ‹consistent A S› ‹finite (⋃ (block_nominals ` S))› ‹surj f›
  shows ‹saturated (Extend A S f)›
  unfolding saturated_def
proof safe
  fix ps i p
  assume ‹(ps, i) ∈ Extend A S f› ‹(❙◇ p) on (ps, i)› ‹∄a. p = Nom a›
  obtain n where n: ‹f n = (ps, i)›
    using ‹surj f› unfolding surj_def by metis

  let ?used = ‹A ∪ (⋃block ∈ {f n} ∪ extend A S f n. block_nominals block)›

  have ‹extend A S f n ⊆ Extend A S f›
    unfolding Extend_def by auto
  moreover have ‹consistent A (Extend A S f)›
    using assms consistent_Extend by blast
  ultimately have ‹consistent A ({(ps, i)} ∪ extend A S f n)›
    using ‹(ps, i) ∈ Extend A S f› inconsistent_weaken by blast
  then have ‹extend A S f (Suc n) = {f n, witness (f n) ?used} ∪ extend A S f n›
    using n ‹(❙◇ p) on (ps, i)› by auto
  then have ‹witness (f n) ?used ∈ Extend A S f›
    unfolding Extend_def by blast
  then have *: ‹(witness_list ps ?used, i) ∈ Extend A S f›
    using n by simp

  have ‹(❙◇ p) ∈. ps›
    using ‹(❙◇ p) on (ps, i)› by simp
  moreover have ‹proper_dia (❙◇ p) = Some p›
    unfolding proper_dia_def using ‹∄a. p = Nom a› by simp
  ultimately have ‹∃j.
      (❙@ j p) on (witness_list ps ?used, i) ∧
      (❙◇ Nom j) on (witness_list ps ?used, i)›
    using ex_witness_list by fastforce
  then show ‹∃j.
      (∃qs. (qs, i) ∈ Extend A S f ∧ (❙@ j p) on (qs, i)) ∧
      (∃rs. (rs, i) ∈ Extend A S f ∧ (❙◇ Nom j) on (rs, i))›
    using * by blast
qed

subsection ‹Smullyan-Fitting›

lemma Hintikka_Extend:
  fixes S :: ‹('a, 'b) block set›
  assumes inf: ‹infinite (UNIV :: 'b set)› and fin: ‹finite A› and
    ‹maximal A S› ‹consistent A S› ‹saturated S›
  shows ‹Hintikka A S›
  unfolding Hintikka_def
proof safe
  fix x i j ps qs rs
  assume
    ps: ‹(ps, i) ∈ S› ‹Nom j on (ps, i)› and
    qs: ‹(qs, j) ∈ S› ‹Pro x on (qs, j)› and
    rs: ‹(rs, i) ∈ S› ‹(❙¬ Pro x) on (rs, i)›
  then have ‹¬ A, n ⊢ [(qs, j), (ps, i), (rs, i)]› for n
    using ‹consistent A S› unfolding consistent_def by simp
  moreover have ‹A, n ⊢ [((❙¬ Pro x) # qs, j), (ps, i), (rs, i)]› for n
    using qs(2) Close
    by (metis (no_types, lifting) list.set_intros(1) on.simps set_subset_Cons subsetD)
  then have ‹A, n ⊢ [(qs, j), (ps, i), (rs, i)]› for n
    using ps(2) rs(2)
    by (meson Nom' fm.distinct(21) fm.simps(18) list.set_intros(1) set_subset_Cons subsetD)
  ultimately show False
    by blast
next
  fix a i ps qs
  assume
    ps: ‹(ps, i) ∈ S› ‹Nom a on (ps, i)› and
    qs: ‹(qs, i) ∈ S› ‹(❙¬ Nom a) on (qs, i)›
  then have ‹¬ A , n ⊢ [(ps, i), (qs, i)]› for n
    using ‹consistent A S› unfolding consistent_def by simp
  moreover have ‹A, n ⊢ [(ps, i), (qs, i)]› for n
    using ps(2) qs(2) by (meson Close list.set_intros(1) set_subset_Cons subset_code(1))
  ultimately show False
    by blast
next
  fix p i ps
  assume ps: ‹(ps, i) ∈ S› ‹(❙¬ ❙¬ p) on (ps, i)›
  show ‹p at i in' S›
  proof (rule ccontr)
    assume ‹¬ p at i in' S›
    then obtain S' n where
      ‹A, n ⊢ S'› and S': ‹set S' ⊆ {(p # ps, i)} ∪ S› and ‹(p # ps, i) ∈. S'›
      using ‹maximal A S› unfolding maximal_def consistent_def
      by (metis insert_is_Un list.set_intros(1) on.simps subset_insert)
    then obtain S'' where S'':
      ‹set ((p # ps, i) # S'') = set S'› ‹(p # ps, i) ∉ set S''›
      using split_list[where x=‹(p # ps, i)›] by blast
    then have ‹A ⊢ (p # ps, i) # S''›
      using inf fin STA_struct ‹A, n ⊢ S'› by blast
    then have ‹A ⊢ (ps, i) # S''›
      using ps by (meson Neg' list.set_intros(1))
    moreover have ‹set ((ps, i) # S'') ⊆ S›
      using S' S'' ps by auto
    ultimately show False
      using ‹consistent A S› unfolding consistent_def by blast
  qed
next
  fix p q i ps
  assume ps: ‹(ps, i) ∈ S› ‹(p ❙∨ q) on (ps, i)› and *: ‹¬ q at i in' S›
  show ‹p at i in' S›
  proof (rule ccontr)
    assume ‹¬ p at i in' S›
    then obtain Sp' np where
      ‹A, np ⊢ Sp'› and Sp': ‹set Sp' ⊆ {(p # ps, i)} ∪ S› and ‹(p # ps, i) ∈. Sp'›
      using ‹maximal A S› unfolding maximal_def consistent_def
      by (metis insert_is_Un list.set_intros(1) on.simps subset_insert)
    then obtain Sp'' where Sp'':
      ‹set ((p # ps, i) # Sp'') = set Sp'› ‹(p # ps, i) ∉ set Sp''›
      using split_list[where x=‹(p # ps, i)›] by blast
    then have ‹A ⊢ (p # ps, i) # Sp''›
      using ‹A, np ⊢ Sp'› inf fin STA_struct by blast

    obtain Sq' nq where
      ‹A, nq ⊢ Sq'› and Sq': ‹set Sq' ⊆ {(q # ps, i)} ∪ S› and ‹(q # ps, i) ∈. Sq'›
      using * ‹maximal A S› unfolding maximal_def consistent_def
      by (metis insert_is_Un list.set_intros(1) on.simps subset_insert)
    then obtain Sq'' where Sq'':
      ‹set ((q # ps, i) # Sq'') = set Sq'› ‹(q # ps, i) ∉ set Sq''›
      using split_list[where x=‹(q # ps, i)›] by blast
    then have ‹A ⊢ (q # ps, i) # Sq''›
      using ‹A, nq ⊢ Sq'› inf fin STA_struct by blast

    obtain S'' where S'': ‹set S'' = set Sp'' ∪ set Sq''›
      by (meson set_union)
    then have
      ‹set ((p # ps, i) # Sp'') ⊆ set ((p # ps, i) # S'')›
      ‹set ((q # ps, i) # Sq'') ⊆ set ((q # ps, i) # S'')›
      by auto
    then have ‹A ⊢ (p # ps, i) # S''› ‹A ⊢ (q # ps, i) # S''›
      using ‹A ⊢ (p # ps, i) # Sp''› ‹A ⊢ (q # ps, i) # Sq''› inf fin STA_struct by blast+
    then have ‹A ⊢ (ps, i) # S''›
      using ps by (meson DisP'' list.set_intros(1))
    moreover have ‹set ((ps, i) # S'') ⊆ S›
      using ps Sp' Sp'' Sq' Sq'' S'' by auto
    ultimately show False
      using ‹consistent A S› unfolding consistent_def by blast
  qed
next
  fix p q i ps
  assume ps: ‹(ps, i) ∈ S› ‹(❙¬ (p ❙∨ q)) on (ps, i)›
  show ‹(❙¬ p) at i in' S›
  proof (rule ccontr)
    assume ‹¬ (❙¬ p) at i in' S›
    then obtain S' where
      ‹A ⊢ S'› and
      S': ‹set S' ⊆ {((❙¬ q) # (❙¬ p) # ps, i)} ∪ S› and
      ‹((❙¬ q) # (❙¬ p) # ps, i) ∈. S'›
      using ‹maximal A S› unfolding maximal_def consistent_def
      by (metis (mono_tags, lifting) insert_is_Un insert_subset list.simps(15) on.simps
          set_subset_Cons subset_insert)
    then obtain S'' where S'':
      ‹set (((❙¬ q) # (❙¬ p) # ps, i) # S'') = set S'›
      ‹((❙¬ q) # (❙¬ p) # ps, i) ∉ set S''›
      using split_list[where x=‹((❙¬ q) # (❙¬ p) # ps, i)›] by blast
    then have ‹A ⊢ ((❙¬ q) # (❙¬ p) # ps, i) # S''›
      using inf fin STA_struct ‹A ⊢ S'› by blast
    then have ‹A ⊢ (ps, i) # S''›
      using ps by (meson DisN' list.set_intros(1))
    moreover have ‹set ((ps, i) # S'') ⊆ S›
      using S' S'' ps by auto
    ultimately show False
      using ‹consistent A S› unfolding consistent_def by blast
  qed
next
  fix p q i ps
  assume ps: ‹(ps, i) ∈ S› ‹(❙¬ (p ❙∨ q)) on (ps, i)›
  show ‹(❙¬ q) at i in' S›
  proof (rule ccontr)
    assume ‹¬ (❙¬ q) at i in' S›
    then obtain S' where
      ‹A ⊢ S'› and
      S': ‹set S' ⊆ {((❙¬ q) # (❙¬ p) # ps, i)} ∪ S› and
      ‹((❙¬ q) # (❙¬ p) # ps, i) ∈. S'›
      using ‹maximal A S› unfolding maximal_def consistent_def
      by (metis (mono_tags, lifting) insert_is_Un insert_subset list.simps(15) on.simps
          set_subset_Cons subset_insert)
    then obtain S'' where S'':
      ‹set (((❙¬ q) # (❙¬ p) # ps, i) # S'') = set S'›
      ‹((❙¬ q) # (❙¬ p) # ps, i) ∉ set S''›
      using split_list[where x=‹((❙¬ q) # (❙¬ p) # ps, i)›] by blast
    then have ‹A ⊢ ((❙¬ q) # (❙¬ p) # ps, i) # S''›
      using inf fin STA_struct ‹A ⊢ S'› by blast
    then have ‹A ⊢ (ps, i) # S''›
      using ps by (meson DisN' list.set_intros(1))
    moreover have ‹set ((ps, i) # S'') ⊆ S›
      using S' S'' ps by auto
    ultimately show False
      using ‹consistent A S› unfolding consistent_def by blast
  qed
next
  fix p i ps
  assume ‹∄a. p = Nom a› ‹(ps, i) ∈ S› ‹(❙◇ p) on (ps, i)›
  then show ‹∃j. (❙◇ Nom j) at i in' S ∧ (❙@ j p) at i in' S›
    using ‹saturated S› unfolding saturated_def by blast
next
  fix p i j ps qs
  assume
    ps: ‹(ps, i) ∈ S› ‹(❙¬ (❙◇ p)) on (ps, i)› and
    qs: ‹(qs, i) ∈ S› ‹(❙◇ Nom j) on (qs, i)›
  show ‹(❙¬ (❙@ j p)) at i in' S›
  proof (rule ccontr)
    assume ‹¬ (❙¬ (❙@ j p)) at i in' S›
    then obtain S' n where
      ‹A, n ⊢ S'› and S': ‹set S' ⊆ {([❙¬ (❙@ j p)], i)} ∪ S› and ‹([❙¬ (❙@ j p)], i) ∈. S'›
      using ‹maximal A S› unfolding maximal_def consistent_def
      by (metis insert_is_Un list.set_intros(1) on.simps subset_insert)
    then obtain S'' where S'':
      ‹set (([❙¬ (❙@ j p)], i) # S'') = set S'› ‹([❙¬ (❙@ j p)], i) ∉ set S''›
      using split_list[where x=‹([❙¬ (❙@ j p)], i)›] by blast
    then have ‹A ⊢ ([❙¬ (❙@ j p)], i) # S''›
      using inf fin STA_struct ‹A, n ⊢ S'› by blast
    then have ‹A ⊢ ([❙¬ (❙@ j p)], i) # (ps, i) # (qs, i) # S''›
      using inf fin STA_struct[where branch'=‹([_], _) # (ps, i) # (qs, i) # S''›] ‹A, n ⊢ S'›
      by fastforce
    then have ‹A ⊢ ([], i) # (ps, i) # (qs, i) # S''›
      using ps(2) qs(2) by (meson DiaN' list.set_intros(1) set_subset_Cons subset_iff)
    moreover have ‹i ∈ branch_nominals ((ps, i) # (qs, i) # S'')›
      unfolding branch_nominals_def by simp
    ultimately have ‹A ⊢ (ps, i) # (qs, i) # S''›
      using GoTo by fast
    moreover have ‹set ((ps, i) # (qs, i) # S'') ⊆ S›
      using S' S'' ps qs by auto
    ultimately show False
      using ‹consistent A S› unfolding consistent_def by blast
  qed
next
  fix p i ps a
  assume ps: ‹(ps, a) ∈ S› ‹(❙@ i p) on (ps, a)›
  show ‹p at i in' S›
  proof (rule ccontr)
    assume ‹¬ p at i in' S›
    then obtain S' n where
      ‹A, n ⊢ S'› and S': ‹set S' ⊆ {([p], i)} ∪ S› and ‹([p], i) ∈. S'›
      using ‹maximal A S› unfolding maximal_def consistent_def
      by (metis insert_is_Un list.set_intros(1) on.simps subset_insert)
    then obtain S'' where S'':
      ‹set (([p], i) # S'') = set S'› ‹([p], i) ∉ set S''›
      using split_list[where x=‹([p], i)›] by blast
    then have ‹A ⊢ ([p], i) # S''›
      using inf fin STA_struct ‹A, n ⊢ S'› by blast
    moreover have ‹set (([p], i) # S'') ⊆ set (([p], i) # (ps, a) # S'')›
      by auto
    ultimately have ‹A ⊢ ([p], i) # (ps, a) # S''›
      using inf fin STA_struct ‹A, n ⊢ S'› by blast
    then have ‹A ⊢ ([], i) # (ps, a) # S''›
      using ps by (metis SatP' insert_iff list.simps(15))
    moreover have ‹i ∈ branch_nominals ((ps, a) # S'')›
      using ps unfolding branch_nominals_def by fastforce
    ultimately have ‹A ⊢ (ps, a) # S''›
      using GoTo by fast
    moreover have ‹set ((ps, a) # S'') ⊆ S›
      using S' S'' ps by auto
    ultimately show False
      using ‹consistent A S› unfolding consistent_def by blast
  qed
next
  fix p i ps a
  assume ps: ‹(ps, a) ∈ S› ‹(❙¬ (❙@ i p)) on (ps, a)›
  show ‹(❙¬ p) at i in' S›
  proof (rule ccontr)
    assume ‹¬ (❙¬ p) at i in' S›
    then obtain S' n where
      ‹A, n ⊢ S'› and S': ‹set S' ⊆ {([❙¬ p], i)} ∪ S› and ‹([❙¬ p], i) ∈. S'›
      using ‹maximal A S› unfolding maximal_def consistent_def
      by (metis insert_is_Un list.set_intros(1) on.simps subset_insert)
    then obtain S'' where S'':
      ‹set (([❙¬ p], i) # S'') = set S'› ‹([❙¬ p], i) ∉ set S''›
      using split_list[where x=‹([❙¬ p], i)›] by blast
    then have ‹A ⊢ ([❙¬ p], i) # S''›
      using inf fin STA_struct ‹A, n ⊢ S'› by blast
    then have ‹A ⊢ ([❙¬ p], i) # (ps, a) # S''›
      using inf fin STA_struct[where branch'=‹([❙¬ p], i) # _ # S''›] ‹A, n ⊢ S'›
      by fastforce
    then have ‹A ⊢ ([], i) # (ps, a) # S''›
      using ps by (metis SatN' insert_iff list.simps(15))
    moreover have ‹i ∈ branch_nominals ((ps, a) # S'')›
      using ps unfolding branch_nominals_def by fastforce
    ultimately have ‹A ⊢ (ps, a) # S''›
      using GoTo by fast
    moreover have ‹set ((ps, a) # S'') ⊆ S›
      using S' S'' ps by auto
    ultimately show False
      using ‹consistent A S› unfolding consistent_def by blast
  qed
next
  fix p i ps a
  assume i: ‹i ∈ nominals p› and ps: ‹(ps, a) ∈ S› ‹p on (ps, a)›
  show ‹∃qs. (qs, i) ∈ S›
  proof (rule ccontr)
    assume ‹∄qs. (qs, i) ∈ S›
    then obtain S' n where
      ‹A, n ⊢ S'› and S': ‹set S' ⊆ {([], i)} ∪ S› and ‹([], i) ∈. S'›
      using ‹maximal A S› unfolding maximal_def consistent_def
      by (metis insert_is_Un subset_insert)
    then obtain S'' where S'':
      ‹set (([], i) # S'') = set S'› ‹([], i) ∉ set S''›
      using split_list[where x=‹([], i)›] by blast
    then have ‹A ⊢ ([], i) # (ps, a) # S''›
      using inf fin STA_struct[where branch'=‹([], i) # (ps, a) # S''›] ‹A, n ⊢ S'› by fastforce
    moreover have ‹i ∈ branch_nominals ((ps, a) # S'')›
      using i ps unfolding branch_nominals_def by auto
    ultimately have ‹A ⊢ (ps, a) # S''›
      using GoTo by fast
    moreover have ‹set ((ps, a) # S'') ⊆ S›
      using S' S'' ps by auto
    ultimately show False
      using ‹consistent A S› unfolding consistent_def by blast
  qed
next
  fix p i j ps qs
  assume
    p: ‹∀a. p = Nom a ∨ p = (❙◇ Nom a) ⟶ a ∈ A› and
    ps: ‹(ps, i) ∈ S› ‹p on (ps, i)› and
    qs: ‹(qs, i) ∈ S› ‹Nom j on (qs, i)›

  show ‹p at j in' S›
  proof (rule ccontr)
    assume ‹∄rs. (rs, j) ∈ S ∧ p on (rs, j)›
    then obtain S' n where
      ‹A, n ⊢ S'› and S': ‹set S' ⊆ {([p], j)} ∪ S› and ‹([p], j) ∈. S'›
      using ‹maximal A S› unfolding maximal_def consistent_def
      by (metis insert_is_Un list.set_intros(1) on.simps subset_insert)
    then obtain S'' where S'':
      ‹set (([p], j) # S'') = set S'› ‹([p], j) ∉ set S''›
      using split_list[where x=‹([p], j)›] by blast
    then have ‹A ⊢ ([p], j) # S''›
      using inf fin STA_struct ‹A, n ⊢ S'› by blast
    then have ‹A ⊢ ([p], j) # (ps, i) # (qs, i) # S''›
      using inf fin STA_struct[where branch'=‹([_], _) # (ps, i) # (qs, i) # S''›] ‹A, n ⊢ S'›
      by fastforce
    then have ‹A ⊢ ([], j) # (ps, i) # (qs, i) # S''›
      using ps(2) qs(2) p by (meson Nom' in_mono list.set_intros(1) set_subset_Cons)
    moreover have ‹j ∈ branch_nominals ((ps, i) # (qs, i) # S'')›
      using qs(2) unfolding branch_nominals_def by fastforce
    ultimately have ‹A ⊢ (ps, i) # (qs, i) # S''›
      using GoTo by fast
    moreover have ‹set ((ps, i) # (qs, i) # S'') ⊆ S›
      using S' S'' ps qs by auto
    ultimately show False
      using ‹consistent A S› unfolding consistent_def by blast
  qed
qed

subsection ‹Result›

theorem completeness:
  fixes p :: ‹('a :: countable, 'b :: countable) fm›
  assumes
    inf: ‹infinite (UNIV :: 'b set)› and
    valid: ‹∀(M :: ('b set, 'a) model) g w. M, g, w ⊨ p›
  shows ‹nominals p, 1 ⊢ [([❙¬ p], i)]›
proof -
  let ?A = ‹nominals p›

  have ‹?A ⊢ [([❙¬ p], i)]›
  proof (rule ccontr)
    assume ‹¬ ?A ⊢ [([❙¬ p], i)]›
    moreover have ‹finite ?A›
      using finite_nominals by blast
    ultimately have *: ‹consistent ?A {([❙¬ p], i)}›
      unfolding consistent_def using STA_struct inf
      by (metis empty_set list.simps(15))

    let ?S = ‹Extend ?A {([❙¬ p], i)} from_nat›
    have ‹finite {([❙¬ p], i)}›
      by simp
    then have fin: ‹finite (⋃ (block_nominals ` {([❙¬ p], i)}))›
      using finite_nominals_set by blast

    have ‹consistent ?A ?S›
      using consistent_Extend inf * fin ‹finite ?A› by blast
    moreover have ‹maximal ?A ?S›
      using maximal_Extend inf * fin by fastforce
    moreover have ‹saturated ?S›
      using saturated_Extend inf * fin by fastforce
    ultimately have ‹Hintikka ?A ?S›
      using Hintikka_Extend inf ‹finite ?A› by blast
    moreover have ‹([❙¬ p], i) ∈ ?S›
      using Extend_mem by blast
    moreover have ‹(❙¬ p) on ([❙¬ p], i)›
      by simp
    ultimately have ‹¬ Model (reach ?A ?S) (val ?S), assign ?A ?S, assign ?A ?S i ⊨ p›
      using Hintikka_model(2) by fast
    then show False
      using valid by blast
  qed
  then show ?thesis
    using STA_one by fast
qed

text ‹
  We arbitrarily fix nominal and propositional symbols to be natural numbers
  (any countably infinite type suffices) and
  define validity as truth in all models with sets of natural numbers as worlds.
  We show below that this implies validity for any type of worlds.
›

abbreviation
  ‹valid p ≡ ∀(M :: (nat set, nat) model) (g :: nat ⇒ _) w. M, g, w ⊨ p›

text ‹
  A formula is valid iff its negation has a closing tableau from a fresh world.
  We can assume a single unit of potential and take the allowed nominals to be the root nominals.
›

theorem main:
  assumes ‹i ∉ nominals p›
  shows ‹valid p ⟷ nominals p, 1 ⊢ [([❙¬ p], i)]›
proof
  assume ‹valid p›
  then show ‹nominals p, 1 ⊢ [([❙¬ p], i)]›
    using completeness by blast
next
  assume ‹nominals p, 1 ⊢ [([❙¬ p], i)]›
  then show ‹valid p›
    using assms soundness_fresh by fast
qed

text ‹The restricted validity implies validity in general.›

theorem valid_semantics:
  ‹valid p ⟶ M, g, w ⊨ p›
proof
  assume ‹valid p›
  then have ‹i ∉ nominals p ⟹ nominals p ⊢ [([❙¬ p], i)]› for i
    using main by blast
  moreover have ‹∃i. i ∉ nominals p›
    by (simp add: finite_nominals ex_new_if_finite)
  ultimately show ‹M, g, w ⊨ p›
    using soundness_fresh by fast
qed

end