(* skeleton argument of decidability of ticket entailment *)
decidability = konig + LRisbcca + LTitca + pi + tau +
consts
concl_unique :: "'f dertree => bool"
irredundant :: "'f dertree => bool"
mk_irred :: "'f dertree => 'f dertree"
mk_tRfree :: "('f multiset, 'f) sequent dertree trf"
mk_lctr_irred :: "('f multiset, 'f) sequent dertree trf"
defs
(* at the moment, use SOME; may need to use a defn that reflects the
construction used in proving tRfree_thm *)
mk_tRfree_def "mk_tRfree dt ==
SOME dtf. valid (LRit - tR) dtf & conclDT dtf = conclDT dt"
primrec
cu_Der "concl_unique (Der f dts) = (~ (f :# dt_contentss dts))"
cu_Unf "concl_unique (Unf f) = True"
defs
irredundant_def "irredundant dt == allDT concl_unique dt"
(* transforming a derivation to a irredundant derivation *)
defs
(* definition follows ex_lctr_irred_lem, useful when valid LRitsb dt *)
mk_lctr_irred_def "mk_lctr_irred dt == @dtr. lctr_irred dtr &
valid LRitsb dtr & conclDT dtr = conclDT dt & heightDT dtr <= heightDT dt"
rules (* ASSUMED, NOT PROVED *)
(* tau : every derivation in LRit can be translated to a derivation in LTitc,
(don't actually need this), tau gives a set of valid derivations *)
tau_valid "tdt : tau dt ==> valid LRit dt ==> valid LTitc tdt"
(* to be any use in decidability, tau must return a finite set of derivations *)
tau_finite "finite (tau dt)"
(* need to ensure that tau translates a derivation in LRit to
every possible derivation in LTitc, or at least, to a set which includes
one in LTit, if there is such a one *)
tau_pi "valid LTit dt ==> dt : tau (pi dt)"
(* then, can get all irredundant valid proof trees for LRitsb,
translate them to LTitc in all possible ways, and see if any are in LTit *)
(* but notice, that pi dt is a tree in LRit, the decidability algorithm
starts with (all possible cases of) a tree in LRitsb, so we actually want *)
tau_irr_sb_pi "valid LTit dt ==>
dt : tau (mk_tRfree (dest_sb (mk_lctr_irred (mk_sb (pi dt)))))"
(* once we have changed pi dt by turning it into a LRitsb proof (and then
making it irredundant) to get pdt', how will we ensure that tau pdt'
contains dt? For tau pdt to simply return all proofs "similar" to pdt
may not be sufficient since mk_irred (mk_sb (pi dt)) (or, in particular,
mk_sb (pi dt)) may not be "similar" to pi dt *)
end