# HG changeset patch # User paulson # Date 1092997209 -7200 # Node ID c7af682b9ee5f256996affa247ef25a204a2b242 # Parent c5c4884634b7e4783e9b90e1bcf2c8c42b29e5dc fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon diff -r c5c4884634b7 -r c7af682b9ee5 TFL/casesplit.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/TFL/casesplit.ML Fri Aug 20 12:20:09 2004 +0200 @@ -0,0 +1,310 @@ +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) +(* Title: TFL/casesplit.ML + Author: Lucas Dixon, University of Edinburgh + lucas.dixon@ed.ac.uk + Date: 17 Aug 2004 +*) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) +(* DESCRIPTION: + + A structure that defines a tactic to program case splits. + + casesplit_free : + string * Term.type -> int -> Thm.thm -> Thm.thm Seq.seq + + casesplit_name : + string -> int -> Thm.thm -> Thm.thm Seq.seq + + These use the induction theorem associated with the recursive data + type to be split. + + The structure includes a function to try and recursively split a + conjecture into a list sub-theorems: + + splitto : Thm.thm list -> Thm.thm -> Thm.thm +*) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) + +(* logic-specific *) +signature CASE_SPLIT_DATA = +sig + val dest_Trueprop : Term.term -> Term.term + val mk_Trueprop : Term.term -> Term.term + val read_cterm : Sign.sg -> string -> Thm.cterm +end; + +(* for HOL *) +structure CaseSplitData_HOL : CASE_SPLIT_DATA = +struct +val dest_Trueprop = HOLogic.dest_Trueprop; +val mk_Trueprop = HOLogic.mk_Trueprop; +val read_cterm = HOLogic.read_cterm; +end; + + +signature CASE_SPLIT = +sig + (* failure to find a free to split on *) + exception find_split_exp of string + + (* getting a case split thm from the induction thm *) + val case_thm_of_ty : Sign.sg -> Term.typ -> Thm.thm + val cases_thm_of_induct_thm : Thm.thm -> Thm.thm + + (* case split tactics *) + val casesplit_free : + string * Term.typ -> int -> Thm.thm -> Thm.thm Seq.seq + val casesplit_name : string -> int -> Thm.thm -> Thm.thm Seq.seq + + (* finding a free var to split *) + val find_term_split : + Term.term * Term.term -> (string * Term.typ) Library.option + val find_thm_split : + Thm.thm -> int -> Thm.thm -> (string * Term.typ) Library.option + val find_thms_split : + Thm.thm list -> int -> Thm.thm -> (string * Term.typ) Library.option + + (* try to recursively split conjectured thm to given list of thms *) + val splitto : Thm.thm list -> Thm.thm -> Thm.thm + + (* for use with the recdef package *) + val derive_init_eqs : + Sign.sg -> + (Thm.thm * int) list -> Term.term list -> (Thm.thm * int) list +end; + +functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = +struct + +(* beta-eta contract the theorem *) +fun beta_eta_contract thm = + let + val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm + val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2 + in thm3 end; + +(* make a casethm from an induction thm *) +val cases_thm_of_induct_thm = + Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i))); + +(* get the case_thm (my version) from a type *) +fun case_thm_of_ty sgn ty = + let + val dtypestab = DatatypePackage.get_datatypes_sg sgn; + val ty_str = case ty of + Type(ty_str, _) => ty_str + | TFree(s,_) => raise ERROR_MESSAGE + ("Free type: " ^ s) + | TVar((s,i),_) => raise ERROR_MESSAGE + ("Free variable: " ^ s) + val dt = case (Symtab.lookup (dtypestab,ty_str)) + of Some dt => dt + | None => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str) + in + cases_thm_of_induct_thm (#induction dt) + end; + +(* + val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t; +*) + + +(* for use when there are no prems to the subgoal *) +(* does a case split on the given variable *) +fun mk_casesplit_goal_thm sgn (vstr,ty) gt = + let + val x = Free(vstr,ty) + val abst = Abs(vstr, ty, Term.abstract_over (x, gt)); + + val ctermify = Thm.cterm_of sgn; + val ctypify = Thm.ctyp_of sgn; + val case_thm = case_thm_of_ty sgn ty; + + val abs_ct = ctermify abst; + val free_ct = ctermify x; + + val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm)); + + val tsig = Sign.tsig_of sgn; + val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm); + val (Pv, Dv, type_insts) = + case (Thm.concl_of case_thm) of + (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => + (Pv, Dv, + Vartab.dest (Type.typ_match tsig (Vartab.empty, (Dty, ty)))) + | _ => raise ERROR_MESSAGE ("not a valid case thm"); + val type_cinsts = map (apsnd ctypify) type_insts; + val cPv = ctermify (Sign.inst_term_tvars sgn type_insts Pv); + val cDv = ctermify (Sign.inst_term_tvars sgn type_insts Dv); + in + (beta_eta_contract + (case_thm + |> Thm.instantiate (type_cinsts, []) + |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))) + end; + + +(* for use when there are no prems to the subgoal *) +(* does a case split on the given variable (Free fv) *) +fun casesplit_free fv i th = + let + val gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th)); + val sgn = Thm.sign_of_thm th; + in + Tactic.rtac (mk_casesplit_goal_thm sgn fv gt) i th + end; + +(* for use when there are no prems to the subgoal *) +(* does a case split on the given variable *) +fun casesplit_name vstr i th = + let + val gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th)); + val freets = Term.term_frees gt; + fun getter x = let val (n,ty) = Term.dest_Free x in + if vstr = n then Some (n,ty) else None end; + val (n,ty) = case Library.get_first getter freets + of Some (n, ty) => (n, ty) + | _ => raise ERROR_MESSAGE ("no such variable " ^ vstr); + val sgn = Thm.sign_of_thm th; + in + Tactic.rtac (mk_casesplit_goal_thm sgn (n,ty) gt) i th + end; + + +(* small example: +Goal "P (x :: nat) & (C y --> Q (y :: nat))"; +by (rtac (thm "conjI") 1); +val th = topthm(); +val i = 2; +val vstr = "y"; + +by (casesplit_name "y" 2); + +val th = topthm(); +val i = 1; +val th' = casesplit_name "x" i th; +*) + + +(* the find_XXX_split functions are simply doing a lightwieght (I +think) term matching equivalent to find where to do the next split *) + +(* assuming two twems are identical except for a free in one at a +subterm, or constant in another, ie assume that one term is a plit of +another, then gives back the free variable that has been split. *) +exception find_split_exp of string +fun find_term_split (Free v, _ $ _) = Some v + | find_term_split (Free v, Const _) = Some v + | find_term_split (Free v, Abs _) = Some v (* do we really want this case? *) + | find_term_split (a $ b, a2 $ b2) = + (case find_term_split (a, a2) of + None => find_term_split (b,b2) + | vopt => vopt) + | find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) = + find_term_split (t1, t2) + | find_term_split (Const (x,ty), Const(x2,ty2)) = + if x = x2 then None else (* keep searching *) + raise find_split_exp (* stop now *) + "Terms are not identical upto a free varaible! (Consts)" + | find_term_split (Bound i, Bound j) = + if i = j then None else (* keep searching *) + raise find_split_exp (* stop now *) + "Terms are not identical upto a free varaible! (Bound)" + | find_term_split (a, b) = + raise find_split_exp (* stop now *) + "Terms are not identical upto a free varaible! (Other)"; + +(* assume that "splitth" is a case split form of subgoal i of "genth", +then look for a free variable to split, breaking the subgoal closer to +splitth. *) +fun find_thm_split splitth i genth = + find_term_split (Logic.get_goal (Thm.prop_of genth) i, + Thm.concl_of splitth) handle find_split_exp _ => None; + +(* as above but searches "splitths" for a theorem that suggest a case split *) +fun find_thms_split splitths i genth = + Library.get_first (fn sth => find_thm_split sth i genth) splitths; + + +(* split the subgoal i of "genth" until we get to a member of +splitths. Assumes that genth will be a general form of splitths, that +can be case-split, as needed. Otherwise fails. Note: We assume that +all of "splitths" are aplit to the same level, and thus it doesn't +matter which one we choose to look for the next split. Simply add +search on splitthms and plit variable, to change this. *) +(* Note: possible efficiency measure: when a case theorem is no longer +useful, drop it? *) +(* Note: This should not be a separate tactic but integrated into the +case split done during recdef's case analysis, this would avoid us +having to (re)search for variables to split. *) +fun splitto splitths genth = + let + val _ = assert (not (null splitths)) "splitto: no given splitths"; + val sgn = Thm.sign_of_thm genth; + + (* check if we are a member of splitths - FIXME: quicker and + more flexible with discrim net. *) + fun solve_by_splitth th split = biresolution false [(false,split)] 1 th; + + fun split th = + (case find_thms_split splitths 1 th of + None => raise ERROR_MESSAGE "splitto: cannot find variable to split on" + | Some v => + let + val gt = Data.dest_Trueprop (nth_elem(0, Thm.prems_of th)); + val split_thm = mk_casesplit_goal_thm sgn v gt; + val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm; + in + expf (map recsplitf subthms) + end) + + and recsplitf th = + (* note: multiple unifiers! we only take the first element, + probably fine -- there is probably only one anyway. *) + (case Library.get_first (Seq.pull o solve_by_splitth th) splitths of + None => split th + | Some (solved_th, more) => solved_th) + in + recsplitf genth + end; + + +(* Note: We dont do this if wf conditions fail to be solved, as each +case may have a different wf condition - we could group the conditions +togeather and say that they must be true to solve the general case, +but that would hide from the user which sub-case they were related +to. Probably this is not important, and it would work fine, but I +prefer leaving more fine grain control to the user. *) + +(* derive eqs, assuming strict, ie the rules have no assumptions = all + the well-foundness conditions have been solved. *) +local + fun get_related_thms i = + mapfilter ((fn (r,x) => if x = i then Some r else None)); + + fun solve_eq (th, [], i) = + raise ERROR_MESSAGE "derive_init_eqs: missing rules" + | solve_eq (th, [a], i) = (a, i) + | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th,i); +in +fun derive_init_eqs sgn rules eqs = + let + val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o Data.mk_Trueprop) + eqs + in + (rev o map solve_eq) + (Library.foldln + (fn (e,i) => + (curry (op ::)) (e, (get_related_thms (i - 1) rules), i - 1)) + eqths []) + end; +end; +(* + val (rs_hwfc, unhidefs) = Library.split_list (map hide_prems rules) + (map2 (op |>) (ths, expfs)) +*) + +end; + + +structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL); diff -r c5c4884634b7 -r c7af682b9ee5 TFL/isand.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/TFL/isand.ML Fri Aug 20 12:20:09 2004 +0200 @@ -0,0 +1,241 @@ +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) +(* Title: TFL/isand.ML + Author: Lucas Dixon, University of Edinburgh + lucas.dixon@ed.ac.uk + Date: 6 Aug 2004 +*) +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) +(* DESCRIPTION: + + Natural Deduction tools + + For working with Isbaelle theorem in a natural detuction style, + ie, not having to deal with meta level quantified varaibles, + instead, we work with newly introduced frees, and hide the + "all"'s, exporting results from theorems proved with the frees, to + solve the all cases of the previous goal. + + Note: A nice idea: allow esxporting to solve any subgoal, thus + allowing the interleaving of proof, or provide a structure for the + ordering of proof, thus allowing proof attempts in parrelle, but + recording the order to apply things in. +*) + +structure IsaND = +struct + +(* Solve *some* subgoal of "th" directly by "sol" *) +(* Note: this is probably what Markus ment to do upon export of a +"show" but maybe he used RS/rtac intead, which would wrongly lead to +failing if there are premices to the shown goal. *) +fun solve_with sol th = + let fun solvei 0 = Seq.empty + | solvei i = + Seq.append (bicompose false (false,sol,0) i th, + solvei (i - 1)) + in + solvei (Thm.nprems_of th) + end; + + +(* fix parameters of a subgoal "i", as free variables, and create an +exporting function that will use the result of this proved goal to +show the goal in the original theorem. + +Note, an advantage of this over Isar is that it supports instantiation +of unkowns in the earlier theorem, ie we can do instantiation of meta +vars! *) +fun fix_alls' i th = + let + val t = (prop_of th); + val names = Term.add_term_names (t,[]); + val gt = Logic.get_goal t i; + val body = Term.strip_all_body gt; + val alls = rev (Term.strip_all_vars gt); + val fvs = map Free + ((Term.variantlist (map fst alls, names)) + ~~ (map snd alls)); + val sgn = Thm.sign_of_thm th; + val ctermify = Thm.cterm_of sgn; + val cfvs = rev (map ctermify fvs); + + val body' = (subst_bounds (fvs,body)); + val gthi0 = Thm.trivial (ctermify body'); + + (* Given a thm justifying subgoal i, solve subgoal i *) + (* Note: fails if there are choices! *) + fun exportf thi = + Drule.compose_single (Drule.forall_intr_list cfvs thi, + i, th) + in + (gthi0, exportf) + end; + +(* small example: +Goal "!! x. [| False; C x |] ==> P x"; +val th = topthm(); +val i = 1; +val (goalth, expf) = fix_alls i (topthm()); +*) + + +(* a nicer version of the above that leaves only a single subgoal (the +other subgoals are hidden hyps, that the exporter suffles about) +namely the subgoal that we were trying to solve. *) + +fun fix_alls i th = + let + val (gthi, exportf) = fix_alls' i th + val gthi' = Drule.rotate_prems 1 gthi + + val sgn = Thm.sign_of_thm th; + val ctermify = Thm.cterm_of sgn; + + val prems = tl (Thm.prems_of gthi) + val cprems = map ctermify prems; + val aprems = map Thm.assume cprems; + + val exportf' = + exportf o (Drule.implies_intr_list cprems) + in + (Drule.implies_elim_list gthi' aprems, exportf') + end; + +(* small example: +Goal "P x"; +val i = 1; +val th = topthm(); +val x = fix_alls (topthm()) 1; + +Goal "!! x. [| False; C x |] ==> P x"; +val th = topthm(); +val i = 1; +val (goalth, expf) = fix_alls' th i; + +val (premths, goalth2, expf2) = assume_prems 1 goalth; +val False_th = nth_elem (0,premths); +val anything = False_th RS (thm "FalseE"); +val th2 = anything RS goalth2; +val th1 = expf2 th2; +val final_th = flat (map expf th1); +*) + + +(* assume the premises of subgoal "i", this gives back a list of +assumed theorems that are the premices of subgoal i, it also gives +back a new goal thm and an exporter, the new goalthm is as the old +one, but without the premices, and the exporter will use a proof of +the new goalthm, possibly using the assumed premices, to shoe the +orginial goal. *) + +(* Note: Dealing with meta vars, need to meta-level-all them in the +shyps, which we can later instantiate with a specific value.... ? +think about this... maybe need to introduce some new fixed vars and +then remove them again at the end... like I do with rw_inst. *) +fun assume_prems i th = + let + val t = (prop_of th); + val gt = Logic.get_goal t i; + val _ = case Term.strip_all_vars gt of [] => () + | _ => raise ERROR_MESSAGE "assume_prems: goal has params" + val body = gt; + val prems = Logic.strip_imp_prems body; + val concl = Logic.strip_imp_concl body; + + val sgn = Thm.sign_of_thm th; + val ctermify = Thm.cterm_of sgn; + val cprems = map ctermify prems; + val aprems = map Thm.assume cprems; + val gthi = Thm.trivial (ctermify concl); + + fun explortf thi = + Drule.compose (Drule.implies_intr_list cprems thi, + i, th) + in + (aprems, gthi, explortf) + end; +(* small example: +Goal "False ==> b"; +val th = topthm(); +val i = 1; +val (prems, goalth, expf) = assume_prems i (topthm()); +val F = hd prems; +val FalseE = thm "FalseE"; +val anything = F RS FalseE; +val thi = anything RS goalth; +val res' = expf thi; +*) + + +(* Fixme: allow different order of subgoals *) +fun subgoal_thms th = + let + val t = (prop_of th); + + val prems = Logic.strip_imp_prems t; + + val sgn = Thm.sign_of_thm th; + val ctermify = Thm.cterm_of sgn; + + val aprems = map (Thm.trivial o ctermify) prems; + + fun explortf premths = + Drule.implies_elim_list th premths + in + (aprems, explortf) + end; +(* small example: +Goal "A & B"; +by (rtac conjI 1); +val th = topthm(); +val (subgoals, expf) = subgoal_thms (topthm()); +*) + +(* make all the premices of a theorem hidden, and provide an unhide +function, that will bring them back out at a later point. This is +useful if you want to get back these premices, after having used the +theorem with the premices hidden *) +fun hide_prems th = + let + val sgn = Thm.sign_of_thm th; + val ctermify = Thm.cterm_of sgn; + + val t = (prop_of th); + val prems = Logic.strip_imp_prems t; + val cprems = map ctermify prems; + val aprems = map Thm.trivial cprems; + + val unhidef = Drule.implies_intr_list cprems; + in + (Drule.implies_elim_list th aprems, unhidef) + end; + + + + +(* Fixme: allow different order of subgoals *) +fun fixed_subgoal_thms th = + let + val (subgoals, expf) = subgoal_thms th; + +(* fun export_sg (th, exp) = exp th; *) + fun export_sgs expfs ths = + expf (map2 (op |>) (ths, expfs)); + +(* expf (map export_sg (ths ~~ expfs)); *) + + + + in + apsnd export_sgs (Library.split_list (map (fix_alls 1) subgoals)) + end; + + +(* small example: +Goal "(!! x. ((C x) ==> (A x)))"; +val th = topthm(); +val i = 1; +val (subgoals, expf) = fixed_subgoal_thms (topthm()); +*) + +end; \ No newline at end of file diff -r c5c4884634b7 -r c7af682b9ee5 TFL/post.ML --- a/TFL/post.ML Thu Aug 19 12:35:45 2004 +0200 +++ b/TFL/post.ML Fri Aug 20 12:20:09 2004 +0200 @@ -195,6 +195,42 @@ error (mesg ^ "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); + +(* Derive the initial equations from the case-split rules to meet the +users specification of the recursive function. + Note: We don't do this if the wf conditions fail to be solved, as each +case may have a different wf condition. We could group the conditions +together and say that they must be true to solve the general case, +but that would hide from the user which sub-case they were related +to. Probably this is not important, and it would work fine, but, for now, I +prefer leaving more fine-grain control to the user. *) +local + fun get_related_thms i = + mapfilter ((fn (r,x) => if x = i then Some r else None)); + + fun solve_eq (th, [], i) = + raise ERROR_MESSAGE "derive_init_eqs: missing rules" + | solve_eq (th, [a], i) = [(a, i)] + | solve_eq (th, splitths as (_ :: _), i) = + [((standard o ObjectLogic.rulify_no_asm) + (CaseSplit.splitto splitths th), i)] + (* if there's an error, pretend nothing happened with this definition + We should probably print something out so that the user knows...? *) + handle ERROR_MESSAGE _ => map (fn x => (x,i)) splitths; +in +fun derive_init_eqs sgn rules eqs = + let + val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) + eqs + fun countlist l = + (rev o snd o (foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l) + in + flat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i)) + (countlist eqths)) + end; +end; + + (*--------------------------------------------------------------------------- * Defining a function with an associated termination relation. *---------------------------------------------------------------------------*) diff -r c5c4884634b7 -r c7af682b9ee5 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Aug 19 12:35:45 2004 +0200 +++ b/src/HOL/IsaMakefile Fri Aug 20 12:20:09 2004 +0200 @@ -80,7 +80,8 @@ $(SRC)/Provers/quasi.ML \ $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \ $(SRC)/Provers/trancl.ML \ - $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \ + $(SRC)/TFL/isand.ML $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML\ + $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \ $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \ @@ -96,7 +97,8 @@ Nat.thy NatArith.ML NatArith.thy \ Power.thy PreList.thy Product_Type.ML Product_Type.thy \ Refute.thy ROOT.ML \ - Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \ + Recdef.thy Reconstruction.thy Record.thy\ + Relation.ML Relation.thy Relation_Power.ML \ Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\ Set.ML Set.thy SetInterval.ML SetInterval.thy \ Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \ @@ -107,7 +109,7 @@ Tools/primrec_package.ML \ Tools/prop_logic.ML \ Tools/recdef_package.ML Tools/recfun_codegen.ML \ - Tools/record_package.ML \ + Tools/record_package.ML Tools/reconstruction.ML\ Tools/refute.ML Tools/refute_isar.ML \ Tools/rewrite_hol_proof.ML \ Tools/sat_solver.ML \ diff -r c5c4884634b7 -r c7af682b9ee5 src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Thu Aug 19 12:35:45 2004 +0200 +++ b/src/HOL/Recdef.thy Fri Aug 20 12:20:09 2004 +0200 @@ -8,6 +8,8 @@ theory Recdef imports Wellfounded_Relations Datatype files + ("../TFL/isand.ML") + ("../TFL/casesplit.ML") ("../TFL/utils.ML") ("../TFL/usyntax.ML") ("../TFL/dcterm.ML") @@ -43,6 +45,8 @@ lemma tfl_exE: "\x. P x ==> \x. P x --> Q ==> Q" by blast +use "../TFL/isand.ML" +use "../TFL/casesplit.ML" use "../TFL/utils.ML" use "../TFL/usyntax.ML" use "../TFL/dcterm.ML"