(* proof of finiteness part of decidability of ticket entailment *)
sb_finite = decidability +
(* given a set of sequents (eg a branch of a proof tree),
define the well-founded relation which will show the branch finite *)
types
'fml branch = "(nat => ('fml multiset, 'fml) sequent)"
consts
ussu :: "'fml branch => nat => ('fml set, 'fml) sequent set"
mk_brr1 :: "formula branch * nat => (formula set * formula) set"
br_rel2 :: "(formula branch * nat) relation"
allsseqs :: "(formula multiset, formula) sequent =>
(formula set * formula) set"
defs
(* set of underlying fml set/succ in branch *)
ussu_def "ussu br n == ap_ant set_of ` br ` {i. i <= n}"
allsseqs_def "allsseqs seq ==
let allsubfmls = UNION (fmls_of seq) subfmls in
Pow allsubfmls <*> allsubfmls"
primrec
(* set of underlying fml set/succ not represented in branch *)
mk_brr1_def "mk_brr1 (br, n) = allsseqs (br 0) - seq_pair ` ussu br n"
inductive "br_rel2"
intrs
I "lctr_irred (dt_of_branch br n1) ==> ussu br n1 = ussu br n2 ==>
n2 < n1 ==> ((br, n1), (br, n2)) : br_rel2"
rules (* ASSUMED, NOT PROVED *)
(* the process of creating irredundant proof trees using rules of LRitsb
is finite, thus trying to find a valid (no premises) one is finite,
making LRit decidable *)
LRitsb_finite
"finite {dt. allDT (frgs LRitsb) dt & lctr_irred dt & conclDT dt = c}"
(* one form of Kripke's lemma *)
Kripke "(ALL n. lctr_irred (dt_of_branch br n)) ==>
finite {n. ap_ant set_of (br n) = seq}"
end