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)

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 #