# Theory Hybrid_Logic

theory Hybrid_Logic imports  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

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)

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

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

mapi_branch (mapper f ({(length branch, length ps)}  xs)) ((ps, a) # branch) =
mapi_branch (mapper f xs) ((ps, a) # branch)

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

Dup p i ((ps, a) # branch) xs  Dup p i ((q # ps, a) # branch) xs
using Dup_block[where ps'=[_]] by simp

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

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
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)
moreover have (length branch, length ps)  xs
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