# Theory Completeness

```section "Completeness"

theory Completeness
imports Tree Sequents
begin

subsection "pseq: type represents a processed sequent"

type_synonym "atom"  = "(signs * predicate * vbl list)"
type_synonym nform = "(nat * formula)"
type_synonym pseq  = "(atom list * nform list)"

definition
sequent :: "pseq => formula list" where
"sequent = (%(atoms,nforms) . map snd nforms @ map (% (z,p,vs) . FAtom z p vs) atoms)"

definition
pseq :: "formula list => pseq" where
"pseq fs = ([],map (%f.(0,f)) fs)"

definition atoms :: "pseq => atom list" where "atoms = fst"
definition nforms :: "pseq => nform list" where "nforms = snd"

subsection "subs: SATAxiom"

definition
SATAxiom :: "formula list => bool" where
"SATAxiom fs ⟷ (? n vs . FAtom Pos n vs : set fs & FAtom Neg n vs : set fs)"

subsection "subs: a CutFreePC justifiable backwards proof step"

definition
subsFAtom :: "[atom list,(nat * formula) list,signs,predicate,vbl list] => pseq set" where
"subsFAtom atms nAs z P vs = { ((z,P,vs)#atms,nAs) }"

definition
subsFConj :: "[atom list,(nat * formula) list,signs,formula,formula] => pseq set" where
"subsFConj atms nAs z A0 A1 =
(case z of
Pos => { (atms,(0,A0)#nAs),(atms,(0,A1)#nAs) }
| Neg => { (atms,(0,A0)#(0,A1)#nAs) })"

definition
subsFAll :: "[atom list,(nat * formula) list,nat,signs,formula,vbl set] => pseq set" where
"subsFAll atms nAs n z A frees =
(case z of
Pos => { let v = freshVar frees in  (atms,(0,instanceF v A)#nAs) }
| Neg => { (atms,(0,instanceF (X n) A)#nAs @ [(Suc n,FAll Neg A)]) })"

definition
subs :: "pseq => pseq set" where
"subs = (% pseq .
if SATAxiom (sequent pseq) then
{}
else let (atms,nforms) = pseq
in  case nforms of
[]     => {}
| nA#nAs => let (n,A) = nA
in  (case A of
FAtom z P vs  => subsFAtom atms nAs z P vs
| FConj z A0 A1 => subsFConj atms nAs z A0 A1
| FAll  z A     => subsFAll  atms nAs n z A (freeVarsFL (sequent pseq))))"

subsection "proofTree(Gamma) says whether tree(Gamma) is a proof"

definition
proofTree :: "(nat * pseq) set => bool" where
"proofTree A ⟷ bounded A & founded subs (SATAxiom o sequent) A"

subsection "path: considers, contains, costBarrier"

definition
considers :: "[nat => pseq,nat * formula,nat] => bool" where
"considers f nA n = (case (snd (f n)) of [] => False | x#xs => x=nA)"

definition
"contains" :: "[nat => pseq,nat * formula,nat] => bool" where
"contains f nA n ⟷ nA : set (snd (f n))"

definition
costBarrier :: "[nat * formula,pseq] => nat" where
(******
costBarrier justifies: eventually contains ==> eventually considers
with a termination thm, (barrier strictly decreases in |N).
******)
"costBarrier nA = (%(atms,nAs).
let barrier = takeWhile (%x. nA ~= x) nAs
in  let costs = map (exp 3 o size o snd) barrier
in  sumList costs)"

subsection "path: eventually"

(******
Could do this with composable temporal operators, but following paper proof first.
******)

definition
EV :: "[nat => bool] => bool" where
"EV f == (? n . f n)"
(******
This allows blast_tac like searching to be done without hassle
of removing exists rules. (hopefully).
******)

subsection "path: counter model"

definition
counterM :: "(nat => pseq) => object set" where
"counterM f = range obj"

definition
counterEvalP :: "(nat => pseq) => predicate => object list => bool" where
"counterEvalP f = (%p args . ! i . ~(EV (contains f (i,FAtom Pos p (map (X o inv obj) args)))))"

definition
counterModel :: "(nat => pseq) => model" where
"counterModel f = Abs_model (counterM f, counterEvalP f)"

primrec counterAssign :: "vbl => object"
where "counterAssign (X n) = obj n"  (* just deX *)

subsection "subs: finite"

lemma finite_subs: "finite (subs gamma)"
apply(simp add: subs_def subsFAtom_def subsFConj_def subsFAll_def Let_def split_beta split: if_splits list.split formula.split signs.split)
done

lemma fansSubs: "fans subs"
apply(rule fansI) apply(rule, rule finite_subs) done

lemma subs_def2:
"!!gamma.
~ SATAxiom (sequent gamma) ==>
subs gamma = (case nforms gamma of
[]     => {}
| nA#nAs => let (n,A) = nA
in  (case A of
FAtom z P vs  => subsFAtom (atoms gamma) nAs z P vs
| FConj z A0 A1 => subsFConj (atoms gamma) nAs z A0 A1
| FAll  z A     => subsFAll  (atoms gamma) nAs n z A (freeVarsFL (sequent gamma))))"
apply(simp add: subs_def Let_def nforms_def atoms_def split_beta split: list.split)
done

subsection "inherited: proofTree"

lemma proofTree_def2: "proofTree = ( % x . bounded x & founded subs (SATAxiom o sequent) x)"
apply(rule ext)

lemma inheritedProofTree: "inherited subs proofTree"
apply(auto intro: inheritedJoinI inheritedBounded inheritedFounded)
done

lemma proofTreeI: "[| bounded A; founded subs (SATAxiom o sequent) A |] ==> proofTree A"

lemma proofTreeBounded: "proofTree A ==> bounded A"

lemma proofTreeTerminal: "proofTree A ==> (n,delta) : A ==> terminal subs delta ==> SATAxiom (sequent delta)"
apply(simp add: proofTree_def founded_def) apply blast done

subsection "pseq: lemma"

lemma snd_o_Pair: "(snd o (Pair x)) = (% x. x)"
apply(rule ext)
by simp

lemma sequent_pseq: "sequent (pseq fs) = fs"
by (simp add: pseq_def sequent_def snd_o_Pair)

subsection "SATAxiom: proofTree"

lemma SATAxiomTerminal[rule_format]: "SATAxiom (sequent gamma) --> terminal subs gamma"
apply(simp add: subs_def proofTree_def terminal_def founded_def bounded_def)
done

lemma SATAxiomBounded:"SATAxiom (sequent gamma) ==> bounded (tree subs gamma)"
apply(frule SATAxiomTerminal)
apply(subst treeEquation)
apply(simp add: subs_def proofTree_def terminal_def founded_def bounded_def)
done

lemma SATAxiomFounded: "SATAxiom (sequent gamma) ==> founded subs (SATAxiom o sequent) (tree subs gamma)"
apply(frule SATAxiomTerminal)
apply(subst treeEquation)
apply(simp add: subs_def proofTree_def terminal_def founded_def bounded_def)
done

lemma SATAxiomProofTree[rule_format]: "SATAxiom (sequent gamma) --> proofTree (tree subs gamma)"
apply(blast intro: proofTreeI SATAxiomBounded SATAxiomFounded)
done

lemma SATAxiomEq: "(proofTree (tree subs gamma) & terminal subs gamma) = SATAxiom (sequent gamma)"
apply(blast intro: SATAxiomProofTree proofTreeTerminal tree.tree0  SATAxiomTerminal)
done
― ‹FIXME tjr blast sensitive to obj imp vs meta imp for pTT›

subsection "SATAxioms are deductions: - needed"

lemma SAT_deduction: "SATAxiom x ==> x : deductions CutFreePC"
apply(elim exE)
apply(rule_tac x="[FAtom Pos n vs,FAtom Neg n vs]" in inDed_mono)
apply (blast intro!: SATAxiomI rulesInPCs, force)
done

subsection "proofTrees are deductions: subs respects rules - messy start and end"

lemma subsJustified':
notes ss = subs_def2 nforms_def Let_def atoms_def sequent_def subsFAtom_def subsFConj_def subsFAll_def
shows "¬ SATAxiom (sequent (ats, (n, f) # list)) --> ¬ terminal subs (ats, (n, f) # list)
--> (∀sigma∈subs (ats, (n, f) # list). sequent sigma ∈ deductions CutFreePC)
--> sequent (ats, (n, f) # list) ∈ deductions CutFreePC"
apply (rule_tac A=f in formula_signs_cases, clarify) apply(simp add: ss)
apply(rule PermI) apply assumption apply simp_all
apply (rule rulesInPCs, clarify) apply(simp add: ss)
apply(rule PermI) apply assumption apply simp_all
apply (rule rulesInPCs, clarify) apply(simp add: ss) apply(elim conjE)
apply(rule ConjI') apply assumption apply assumption apply(rule rulesInPCs)+
apply(rule DisjI) apply assumption apply(rule rulesInPCs)+
apply(rule AllI) apply assumption apply(rule finiteFreshVar) apply(rule finite_freeVarsFL) apply (rule rulesInPCs, clarify) apply(simp add: ss)
apply(rule ContrI) ― ‹!›
apply(rule_tac w = "X n" in ExI) apply(rule inDed_mono) apply assumption apply force apply(rule rulesInPCs)+
done

lemma subsJustified: "!! gamma. ~ terminal subs gamma
==> ! sigma : subs gamma . sequent sigma : deductions (CutFreePC)
==> sequent gamma : deductions (CutFreePC)"
apply(case_tac "SATAxiom (sequent gamma)")
apply(erule SAT_deduction)
apply(case_tac gamma) apply(rename_tac ats nfs)
apply(case_tac nfs)
apply(simp add: terminal_def subs_def sequent_def Let_def)
apply(case_tac a)
apply(blast intro: subsJustified'[rule_format])
done

subsection "proofTrees are deductions: instance of boundedTreeInduction"

lemmas proofTreeD = proofTree_def [THEN iffD1]

lemma proofTreeDeductionD[rule_format]: "proofTree(tree subs gamma) ⟹ sequent gamma : deductions (CutFreePC)"
apply(rule boundedTreeInduction[OF fansSubs])
apply(erule proofTreeBounded)
apply(rule foundedMono)
apply (force dest: proofTreeD, simp)
apply(blast intro: SAT_deduction foundedMono subsJustified)
apply(blast intro:  subsJustified)
done

subsection "contains, considers:"

lemma contains_def2: "contains f iA n = (iA : set (nforms (f n)))"

lemma considers_def2: "considers f iA n = ( ? nAs . nforms (f n) = iA#nAs)"
apply(simp add: considers_def nforms_def split: list.split) done

lemmas containsI = contains_def2[THEN iffD2]

subsection "path: nforms = [] implies"

lemma nformsNoContains: "[| branch subs gamma f; !n . ~proofTree (tree subs (f n)); nforms (f n) = []  |] ==> ~ contains f iA n"
― ‹FIXME tjr assumptions not required›

lemma nformsTerminal: "nforms (f n) = [] ==> terminal subs (f n)"
apply(simp add: subs_def Let_def terminal_def nforms_def split_beta)
done

lemma nformsStops: "!!f.
[| branch subs gamma f; !n . ~proofTree (tree subs (f n));
nforms (f n) = [] |]
==> nforms (f (Suc n)) = [] & atoms (f (Suc n)) = atoms (f n)"
apply(subgoal_tac "f (Suc n) = f n")
apply simp
apply(blast intro: branchStops nformsTerminal)
done

subsection "path: cases"

lemma terminalNFormCases: "!!f. terminal subs (f n) | (? i A nAs . nforms (f n) = (i,A)#nAs)"
apply (rule disjCI, simp)
apply(rule nformsTerminal)
apply(case_tac "nforms (f n)")
apply simp
apply force
done

lemma cases[elim_format]: "terminal subs (f n) | (¬ (terminal subs (f n) ∧ (? i A nAs . nforms (f n) = (i,A)#nAs)))"
apply(auto elim: terminalNFormCases[elim_format])
done

subsection "path: contains not terminal and propagate condition"

lemma containsNotTerminal: "[| branch subs gamma f; !n . ~proofTree (tree subs (f n)); contains f iA n |] ==> ~ (terminal subs (f n))"
apply(case_tac "SATAxiom (sequent (f n))")
apply(blast dest: SATAxiomEq[THEN iffD2])
apply(drule_tac x=n in spec)
apply (simp add:  subs_def subs_def subsFAtom_def subsFConj_def subsFAll_def Let_def contains_def terminal_def nforms_def split_beta branch_def split: list.split signs.split expand_case_formula, force)
done

lemma containsPropagates: "!!f.
[| branch subs gamma f; !n . ~proofTree (tree subs (f n));
contains f iA n |]
==> contains f iA (Suc n) | considers f iA n"
apply(frule_tac containsNotTerminal) apply force apply force
apply(frule_tac branchSubs) apply assumption
apply(case_tac "considers f iA n") apply simp
apply simp
apply(simp add: contains_def) apply(case_tac "f n") apply simp apply(drule split_list) apply(elim exE conjE) apply simp
apply(case_tac ys)
apply(case_tac "SATAxiom (sequent (f n))") apply(blast dest: iffD2[OF SATAxiomEq])
apply (case_tac aa, simp)
apply(case_tac ba)
apply(rename_tac signs a b)
apply(rename_tac signs a)
done

subsection "path: no consider lemmas"

lemma noConsidersD: "!!f. ~considers f iA n ==> nforms (f n) = x#xs ==> iA ~= x"

lemma considersD: "!!f. considers f iA n ==> ? xs . nforms (f n) = iA#xs"

subsection "path: contains initially"

lemma contains_initially:
"branch subs (pseq gamma) f ⟹ A : set gamma ⟹ (contains f (0,A) 0)"
apply(drule branch0)

lemma contains_initialEVs:
"branch subs (pseq gamma) f ⟹  A : set gamma ⟹ EV (contains f (0,A))"
apply(fast dest: contains_initially) done

subsection "termination: (for EV contains implies EV considers)"

lemmas r = wf_induct[of "measure msrFn", OF wf_measure] for msrFn
lemmas r' = r[simplified measure_def inv_image_def less_than_def less_eq mem_Collect_eq]

lemma r'': "(∀ x. (∀ y. ( ((msrFn::'a ⇒ nat) y) < ((msrFn :: 'a ⇒ nat) x)) ⟶ P y) ⟶ P x) ⟹ P a"
by (blast intro: r' [of _ P])

lemma terminationRule [rule_format]:
"! n. P n --> (~(P (Suc n)) | (P (Suc n) & msrFn (Suc n) < (msrFn::nat => nat) n)) ==> P m --> (? n . P n & ~(P (Suc n)))"
(is "_ ⟹ ?P m")
apply (rule r''[of msrFn "?P" m], blast)
done
― ‹FIXME ugly›

subsection "costBarrier: lemmas"

subsection "costBarrier: exp3 lemmas - bit specific..."

lemma exp3Min: "exp 3 a > 0"
by (induct a, simp, simp)

lemma exp1: "exp 3 (A) + exp 3 (B) < 3 * ((exp 3 A) * (exp 3 B))"
using exp3Min[of A] exp3Min[of B]
apply(case_tac "exp 3 A") apply(simp add: exp3Min)
apply(case_tac "exp 3 B") apply (simp add: exp3Min, simp)
done

lemma exp1': "exp 3 (A) < 3 * ((exp 3 A) * (exp 3 B)) + C"
apply(subgoal_tac "exp 3 (A) < 3 * ((exp 3 A) * (exp 3 B))")
apply arith
apply(case_tac "exp 3 A") using exp3Min[of A] apply arith
apply(case_tac "exp 3 B") using exp3Min[of B] apply arith
apply simp
done

lemma exp2: "Suc 0 < 3 * exp 3 (B)"
using exp3Min[of B]
apply arith
done

lemma expSum: "exp x (a+b) = (exp x a) * (exp x b)"
apply(induct a, auto) done

subsection "costBarrier: decreases whilst contains and unconsiders"

lemma costBarrierDecreases':
notes ss = subs_def2 nforms_def Let_def subsFAtom_def subsFConj_def subsFAll_def costBarrier_def atoms_def exp3Min expSum
shows "~SATAxiom (sequent
(a, (num,fm) # list)) --> iA ~= (num, fm) --> ¬ proofTree (tree subs (a, (num, fm) # list)) --> fSucn : subs (a, (num, fm) # list) --> iA ∈ set list --> costBarrier iA (fSucn) < costBarrier iA (a, (num, fm) # list)"
apply(rule_tac A=fm in formula_signs_cases)
― ‹atoms›
― ‹conj›
apply clarify
apply(erule disjE)
― ‹disj›
apply clarify
― ‹all›
apply clarify
― ‹ex›
apply clarify
done

lemma costBarrierDecreases:
"[| branch subs gamma f;
!n . ~proofTree (tree subs (f n));
contains f iA n;
~(considers f iA) n
|] ==> costBarrier iA (f (Suc n)) < costBarrier iA (f n)"
apply(subgoal_tac "¬ terminal subs (f n)")
apply(subgoal_tac "¬ SATAxiom (sequent (f n))")
apply(subgoal_tac "f (Suc n) ∈ subs (f n)")
apply(frule_tac x=n in spec)
apply(case_tac "f n", simp)
apply(case_tac b, simp)
apply(case_tac aa) apply(rename_tac num fm) apply simp apply(simp add: contains_def considers_def)
apply(rule costBarrierDecreases'[rule_format]) apply force+
apply(rule branchSubs) apply assumption apply assumption
apply(blast dest: SATAxiomTerminal)
apply(blast dest: containsNotTerminal)
done
― ‹FIXME boring splitting etc.›

subsection "path: EV contains implies EV considers"

lemma considersContains: "considers f iA n ⟹ contains f iA n"
apply(cases "snd (f n)", auto) done

lemma containsConsiders: "[| branch subs gamma f; !n . ~ proofTree (tree subs (f n));
EV (contains f iA) |]
==> EV (considers f iA)"
apply(erule exE)
apply(case_tac "considers f iA n") apply force
apply(subgoal_tac "∃n. (contains f iA n ∧ ¬ considers f iA n) ∧
¬ (contains f iA (Suc n) ∧ ¬ considers f iA (Suc n))")
apply(erule exE)
apply(simp, clarify)
apply(case_tac "contains f iA (Suc na)")
apply force apply(force dest!: containsPropagates)
apply(rule_tac msrFn = "%n. costBarrier iA (f n)" and P = "%n. contains f iA n & ~ considers f iA n" in terminationRule)
prefer 2 apply force
apply(case_tac "(contains f iA (Suc na) ∧ ¬ considers f iA (Suc na))")
apply simp apply(erule costBarrierDecreases) apply simp_all
done

subsection "EV contains: common lemma"

lemma lemmA:
"[| branch subs gamma f; ! n. ~ proofTree (tree subs (f n));
EV (contains f (i,A)) |]
==> ? n nAs. ~SATAxiom (sequent (f n)) & (nforms (f n) = (i,A) # nAs & f (Suc n) : subs (f n))"
apply(frule containsConsiders) apply(assumption+)
apply(unfold EV_def)
apply(erule exE, frule considersContains)
apply(unfold considers_def)
apply(case_tac "snd (f n)")
apply force
apply simp
apply(rule_tac x=n in exI)
apply (intro conjI, rule)
apply(blast dest!: SATAxiomEq[THEN iffD2])
apply(rule_tac x=list in exI) apply(simp add: nforms_def)
apply(frule containsNotTerminal) apply force apply(assumption+)
apply(blast dest!: branchSubs)
done

subsection "EV contains: FConj,FDisj,FAll"

lemma EV_disj: "(EV P | EV Q) = EV (λn. P n | Q n)"
apply (unfold EV_def, force) done

lemma evContainsConj: "[| EV (contains f (i,FConj Pos A0 A1));
branch subs gamma f; !n . ~ proofTree (tree subs (f n))
|] ==> EV (contains f (0,A0)) | EV (contains f (0,A1))"
apply(drule lemmA) apply(assumption+)
apply(subgoal_tac "EV (λ n. contains f (0,A0) n | contains f (0,A1) n)")
apply(unfold EV_def)
apply clarify
apply(rename_tac n n' nAs, rule_tac x="Suc n'" in exI)
apply (simp add: contains_def nforms_def, auto)
done

lemma evContainsDisj: "[| EV (contains f (i,FConj Neg A0 A1));
branch subs gamma f; !n . ~ proofTree (tree subs (f n))
|] ==> EV (contains f (0,A0)) & EV (contains f (0,A1))"
apply(drule lemmA) apply(assumption+)
apply(rule conjI)
apply(unfold EV_def)
apply(erule exE) back
apply(rule_tac x="Suc n" in exI)
apply(erule exE) back
apply(rule_tac x="Suc n" in exI)
done

lemma evContainsAll:
"[| EV (contains f (i,FAll Pos body)); branch subs gamma f; !n . ~ proofTree (tree subs (f n))
|]
==> ? v . EV (contains f (0,instanceF v body))"
apply(drule lemmA) apply(assumption+)
apply(erule exE)
apply(rule_tac x="freshVar(freeVarsFL (sequent (f n)))" in exI)
apply(unfold EV_def)
apply(rule_tac x="Suc n" in exI)
done

lemma evContainsEx_instance:
"[| EV (contains f (i,FAll Neg body)); branch subs gamma f; !n . ~ proofTree (tree subs (f n))
|]
==> EV (contains f (0,instanceF (X i) body))"
apply(drule lemmA) apply(assumption+)
apply(erule exE)
apply(unfold EV_def)
apply(rule_tac x="Suc n" in exI)
done

lemma evContainsEx_repeat: "
[| branch subs gamma f; !n . ~ proofTree (tree subs (f n));
EV (contains f (i,FAll Neg body)) |]
==> EV (contains f (Suc i,FAll Neg body))"
apply(drule lemmA) apply(assumption+)
apply(erule exE)
apply(unfold EV_def)
apply(rule_tac x="Suc n" in exI)
done

subsection "EV contains: lemmas (temporal related)"

(******
Should have abstracted to have temporal ops:
EV   : (nat -> bool) -> nat -> bool
AW   : (nat -> bool) -> nat -> bool
NEXT : (nat -> bool) -> nat -> bool
then require:
EV P and EV B imp (\n. A n & B n)

already think have done similar proofs to this one elsewhere,
Q: where? share proofs?
******)

lemma lemma1: "[| P A n ; !A n. P A n --> P A (Suc n) |]
==> P A (n + m)"
apply (induct m, simp, simp)
done

lemma lemma2:
"[| P A n ; P B m ; ! A n. P A n --> P A (Suc n) |]
==> ? n . P A n & P B n"
apply (rule exI[of _ "n+m"], rule)
apply(blast intro!: lemma1)
apply(blast intro!: lemma1)
done

subsection "EV contains: FAtoms"

lemma notTerminalNotSATAxiom: "¬ terminal subs gamma ⟹ ¬ SATAxiom (sequent gamma)"
apply(erule contrapos_nn) apply(erule SATAxiomTerminal) done

lemma notTerminalNforms: "¬ terminal subs (f n) ⟹ nforms (f n) ≠ []"
apply(erule contrapos_nn) apply(erule nformsTerminal) done

lemma atomsPropagate: "[| branch subs gamma f |]
==> x : set (atoms (f n)) --> x : set (atoms (f (Suc n)))"
apply(cases "terminal subs (f n)")
apply(drule branchStops) apply assumption apply simp
apply(drule branchSubs) apply assumption
apply rule apply(frule notTerminalNotSATAxiom)
apply(frule notTerminalNforms)
apply(cases "nforms (f n)") apply simp
apply(case_tac a, auto)
apply(case_tac ba, auto)
apply(rename_tac signs a b)
apply(case_tac signs) apply force apply force
apply(rename_tac signs a)
apply(case_tac signs) apply(force simp: Let_def) apply force
done

subsection "EV contains: FEx cases"

lemma evContainsEx0_allRepeats:
"[| branch subs gamma f; !n . ~ proofTree (tree subs (f n));
EV (contains f (0,FAll Neg A)) |]
==> EV (contains f (i,FAll Neg A))"
apply (induct i, simp)
apply(blast dest!: evContainsEx_repeat)
done

lemma evContainsEx0_allInstances:
"[| branch subs gamma f; !n . ~ proofTree (tree subs (f n));
EV (contains f (0,FAll Neg A)) |]
==> EV (contains f (0,instanceF (X i) A))"
apply(blast dest!: evContainsEx0_allRepeats intro!: evContainsEx_instance)
done

subsection "pseq: creates initial pseq"

lemma containsPSeq0D: "branch subs (pseq fs) f ⟹ contains f (i,A) 0 ⟹ i=0"
apply(drule branch0)
apply (simp add: pseq_def contains_def, blast)
done

subsection "EV contains: contain any (i,FEx y) means contain all (i,FEx y)"

(******
Now, show (Suc i,FEx v A) present means (i,FEx v A) present (or at start).
Assumes initial pseq contains only (0,form) pairs.
------
Show that only way of introducing a (Suc i,FEx_) was from (i,FEx_).
contains n == considers n or contains n+.

Want to find the point where it was introduced.
Have, P true all n or fails at 0 or for a (first) successor.

(!n. P n) | (~P 0) | (P n & ~ P (Suc n))

Instance this with P n = ~(contains ..FEx.. n).
******)

lemma claim: "(A | B | C) = (~C --> ~B --> A)" by auto

lemma natPredCases: "(!n. P n) | (~P 0) | (? n . P n & ~ P (Suc n))"
apply(rule claim[THEN iffD2])
apply(intro impI) apply simp
apply rule apply(induct_tac n) apply auto
done

lemma containsNotTerminal':
"⟦ branch subs gamma f; !n . ~proofTree (tree subs (f n)); contains f iA n ⟧ ⟹ ~ (terminal subs (f n))"
apply (rule containsNotTerminal, auto)
done

lemma notTerminalSucNotTerminal: "⟦ ¬ terminal subs (f (Suc n)); branch subs gamma f ⟧ ⟹ ¬ terminal subs (f n)"
apply(erule contrapos_nn)
apply(rule_tac branchTerminalPropagates[of _ _ _ _ 1, simplified])
apply(assumption+) done
― ‹FIXME move to Tree?›

lemma evContainsExSuc_containsEx:
"[| branch subs (pseq fs) f; !n . ~ proofTree (tree subs (f n));
EV (contains f (Suc i,FAll Neg body)) |]
==> EV (contains f (i,FAll Neg body))"
apply(cut_tac P="%n. ~ contains f (Suc i,FAll Neg body) n" in natPredCases)
apply simp apply(erule disjE)
apply(erule disjE)
apply(blast dest!: containsPSeq0D)
apply(thin_tac "EV _")
apply(erule exE)
apply(erule conjE)
apply(unfold EV_def) apply(rule_tac x=n in exI)
apply(rule considersContains)
apply(frule containsNotTerminal') apply(assumption+)
apply(frule notTerminalSucNotTerminal) apply assumption
apply(thin_tac "¬ terminal x y" for x y)
apply(frule branchSubs) apply assumption
apply(frule notTerminalNforms)
apply(case_tac "SATAxiom (sequent (f n))")
apply(drule SATAxiomTerminal) apply simp
apply(subgoal_tac "(∃i A nAs. nforms (f n) = (i, A) # nAs)")
prefer 2 apply(rule_tac f=f and n=n in cases) apply simp
apply(case_tac "nforms (f n)") apply simp apply(case_tac a, force)
apply(erule exE)+
― ‹shift A into succedent›
apply(rule_tac P="snd (f n) = (ia, A) # nAs" in rev_mp) apply assumption apply(thin_tac "snd (f n) = (ia, A) # nAs")
apply(rule_tac A=A in formula_signs_cases)
apply(auto simp add: subs_def2 nforms_def Let_def subsFAtom_def subsFConj_def subsFAll_def contains_def2 Let_def)
done
― ‹phew, bit precarious, but not too much going on besides unfolding defns. and computing a bit. Need to set simps up›

subsection "EV contains: contain any (i,FEx y) means contain all (i,FEx y)"

lemma evContainsEx_containsEx0:
"[| branch subs (pseq fs) f; !n . ~ proofTree (tree subs (f n)) |]
==> EV (contains f (i,FAll Neg A)) -->
EV (contains f (0,FAll Neg A))"
apply (induct i, simp)
apply(blast dest!: evContainsExSuc_containsEx)
done

lemma evContainsExval:
"[| EV (contains f (i,FAll Neg body)); branch subs (pseq fs) f; !n . ~ proofTree (tree subs (f n))
|]
==> ! v . EV (contains f (0,instanceF v body))"
apply rule apply(induct_tac v)
apply(blast intro!: evContainsEx0_allInstances dest!: evContainsEx_containsEx0)
done

subsection "EV contains: atoms"

lemma atomsInSequentI[rule_format]: "  (z,P,vs) : set (fst ps) -->
FAtom z P vs : set (sequent ps)"
apply(cases ps, force)
done

lemma evContainsAtom1:
"[| branch subs (pseq fs) f; !n . ~ proofTree (tree subs (f n));
EV (contains f (i,FAtom z P vs)) |]
==> ? n . (z,P,vs) : set (fst (f n))"
apply(drule lemmA) apply(assumption+)
apply(erule exE) apply(rule_tac x="Suc n" in exI)

lemmas atomsPropagate'' = atomsPropagate[rule_format]
lemmas atomsPropagate' = atomsPropagate''[simplified atoms_def, simplified]

lemma evContainsAtom:
"[| branch subs (pseq fs) f; !n . ~ proofTree (tree subs (f n));
EV (contains f (i,FAtom z P vs)) |]
==> ? n . (! m . FAtom z P vs : set (sequent (f (n + m))))"
apply(frule evContainsAtom1) apply(assumption+)
apply(erule exE)
apply (rule_tac x=n in exI, rule)
apply(rule atomsInSequentI)
apply (induct_tac m, simp, simp)
apply(rule atomsPropagate') apply(assumption+) done

lemma notEvContainsBothAtoms:
"[| branch subs (pseq fs) f; !n . ~ proofTree (tree subs (f n)) |]
==> ~ EV (contains f (i,FAtom Pos p vs)) |
~ EV (contains f (j,FAtom Neg p vs))"
apply clarify
apply(frule evContainsAtom) apply(assumption+) apply(thin_tac "EV (contains f (j, FAtom Neg p vs))")
apply(frule evContainsAtom) apply(assumption+) apply(thin_tac "EV (contains f (i, FAtom Pos p vs))")
apply(erule_tac exE)+
apply(drule_tac x=na in spec) back
apply(drule_tac x=n in spec) back
apply(subgoal_tac "SATAxiom (sequent (f (n+na)))")
apply(force dest: SATAxiomProofTree)

subsection "counterModel: lemmas"

lemma counterModelInRepn: "(counterM f,counterEvalP f) : model"

lemmas Abs_counterModel_inverse = counterModelInRepn[THEN Abs_model_inverse]

lemma inv_obj_obj: "inv obj (obj n) = n"
using inj_obj apply simp done

lemma map_X_map_counterAssign: "map X (map (inv obj) (map counterAssign xs)) = xs"
apply(simp)
apply(subgoal_tac "(X ∘ (inv obj ∘ counterAssign)) = (% x . x)")
apply simp
apply(rule ext)
apply(case_tac x)
done

lemma objectsCounterModel: "objects (counterModel f) =  { z . ? i . z = obj i }"
by force

lemma inCounterM: "counterAssign v : objects (counterModel f)"
apply(induct v)
by blast

lemma counterAssign_eqI[rule_format]: "x : objects (counterModel f) --> z = X (inv obj x) --> counterAssign z = x"
apply(force simp: objectsCounterModel inj_obj) done

lemma evalPCounterModel: "M = counterModel f ==> evalP M = counterEvalP f"
apply(simp add: evalP_def counterModel_def Abs_counterModel_inverse) done

subsection "counterModel: all path formula value false - step by step"

lemma path_evalF':
notes ss = evalPCounterModel counterEvalP_def map_X_map_counterAssign map_map[symmetric]
and ss1 = instanceF_def evalF_subF_eq comp_vblcase id_def[symmetric]
shows "[| branch subs (pseq fs) f;
!n . ~ proofTree (tree subs (f n))
|] ==> (? i . EV (contains f (i,A))) ⟶ ~(evalF (counterModel f) counterAssign A)"
apply (rule_tac strong_formula_induct, rule)
apply(rule formula_signs_cases)
― ‹atom›
apply(rule, rule)
apply(force dest: notEvContainsBothAtoms)
― ‹conj›
apply(force dest: evContainsConj)
― ‹disj›
apply(force dest: evContainsDisj)
― ‹all›
apply(rule, rule)
apply(erule exE)
apply(drule_tac evContainsAll) apply assumption apply assumption
apply(erule exE)
apply(drule_tac x="(instanceF v f1)" in spec)
apply(erule impE, force simp: size_instance)+
apply simp
apply(rule_tac x="counterAssign v" in bexI) apply simp apply(simp add: inCounterM)
― ‹ex›
apply(rule, rule)
apply(erule exE)
apply(drule_tac evContainsExval) apply assumption apply assumption
apply simp
apply rule
apply(drule_tac x="X i" in spec)
apply(drule_tac x="(instanceF (X i) f1)" in spec)
apply(erule impE, force simp: size_instance)+
done

lemmas path_evalF'' = mp[OF path_evalF']

lemma counterAssignModelAssign: "counterAssign : modelAssigns (counterModel gamma)"
apply (erule rangeE, simp)
apply(rule inCounterM)
done

lemma branch_contains_initially: "branch subs (pseq fs) f ⟹ x : set fs ⟹ contains f (0,x) 0"
done

lemma path_evalF:
"[| branch subs (pseq fs) f;
∀n. ¬ proofTree (tree subs (f n));
x ∈ set fs
|] ==> ¬ evalF (counterModel f) counterAssign x"
apply (rule path_evalF'', assumption, assumption)
apply(rule_tac x=0 in exI) apply(simp add: EV_def)
apply(rule_tac x=0 in exI) apply(simp add: branch_contains_initially)
done

lemma validProofTree: "~proofTree (tree subs (pseq fs)) ==> ~(validS fs)"
apply(subgoal_tac "∃f. branch subs (pseq fs) f ∧ (∀n. ¬ proofTree (tree subs (f n)))")
apply(elim exE conjE)
apply(rule_tac x="counterModel f" in exI)
apply(force dest!: path_evalF)
apply(rule counterAssignModelAssign)
apply(rule failingBranchExistence)
apply(rule inheritedProofTree)
apply (rule fansSubs, assumption)
done

lemma adequacy[simplified sequent_pseq]: "validS fs ==> (sequent (pseq fs)) : deductions CutFreePC"
apply(rule proofTreeDeductionD)
apply(rule ccontr)
apply(force dest!: validProofTree)
done

end
```