# HG changeset patch # User wenzelm # Date 1180610653 -7200 # Node ID ed3f6685ff90493e4296ddf69694c4d3724502fd # Parent 073a65f0bc408877ee99345c4ecc94ed0894c256 moved TFL files to canonical place; diff -r 073a65f0bc40 -r ed3f6685ff90 TFL/casesplit.ML --- a/TFL/casesplit.ML Thu May 31 13:18:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,337 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* 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 * typ -> int -> thm -> thm Seq.seq - - casesplit_name : - string -> int -> 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 list -> thm -> thm -*) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) - -(* logic-specific *) -signature CASE_SPLIT_DATA = -sig - val dest_Trueprop : term -> term - val mk_Trueprop : term -> term - val atomize : thm list - val rulify : thm list -end; - -structure CaseSplitData_HOL : CASE_SPLIT_DATA = -struct -val dest_Trueprop = HOLogic.dest_Trueprop; -val mk_Trueprop = HOLogic.mk_Trueprop; - -val atomize = thms "induct_atomize"; -val rulify = thms "induct_rulify"; -val rulify_fallback = thms "induct_rulify_fallback"; - -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 : theory -> typ -> thm - val cases_thm_of_induct_thm : thm -> thm - - (* case split tactics *) - val casesplit_free : - string * typ -> int -> thm -> thm Seq.seq - val casesplit_name : string -> int -> thm -> thm Seq.seq - - (* finding a free var to split *) - val find_term_split : - term * term -> (string * typ) option - val find_thm_split : - thm -> int -> thm -> (string * typ) option - val find_thms_split : - thm list -> int -> thm -> (string * typ) option - - (* try to recursively split conjectured thm to given list of thms *) - val splitto : thm list -> thm -> thm - - (* for use with the recdef package *) - val derive_init_eqs : - theory -> - (thm * int) list -> term list -> (thm * int) list -end; - -functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = -struct - -val rulify_goals = MetaSimplifier.rewrite_goals_rule Data.rulify; -val atomize_goals = MetaSimplifier.rewrite_goals_rule Data.atomize; - -(* 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 sgn; - val ty_str = case ty of - Type(ty_str, _) => ty_str - | TFree(s,_) => error ("Free type: " ^ s) - | TVar((s,i),_) => error ("Free variable: " ^ s) - val dt = case Symtab.lookup dtypestab ty_str - of SOME dt => dt - | NONE => error ("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 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, - Sign.typ_match sgn (Dty, ty) Vartab.empty) - | _ => error "not a valid case thm"; - val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T)) - (Vartab.dest type_insts); - val cPv = ctermify (Envir.subst_TVars type_insts Pv); - val cDv = ctermify (Envir.subst_TVars 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 (subgoalth, exp) = IsaND.fix_alls i th; - val subgoalth' = atomize_goals subgoalth; - val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); - val sgn = Thm.theory_of_thm th; - - val splitter_thm = mk_casesplit_goal_thm sgn fv gt; - val nsplits = Thm.nprems_of splitter_thm; - - val split_goal_th = splitter_thm RS subgoalth'; - val rulified_split_goal_th = rulify_goals split_goal_th; - in - IsaND.export_back exp rulified_split_goal_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 (subgoalth, exp) = IsaND.fix_alls i th; - val subgoalth' = atomize_goals subgoalth; - val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); - - val freets = Term.term_frees gt; - fun getter x = - let val (n,ty) = Term.dest_Free x in - (if vstr = n orelse vstr = Name.dest_skolem n - then SOME (n,ty) else NONE ) - handle Fail _ => NONE (* dest_skolem *) - end; - val (n,ty) = case Library.get_first getter freets - of SOME (n, ty) => (n, ty) - | _ => error ("no such variable " ^ vstr); - val sgn = Thm.theory_of_thm th; - - val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt; - val nsplits = Thm.nprems_of splitter_thm; - - val split_goal_th = splitter_thm RS subgoalth'; - - val rulified_split_goal_th = rulify_goals split_goal_th; - in - IsaND.export_back exp rulified_split_goal_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 (Free v, Var _) = NONE (* keep searching *) - | 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 split 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 split 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 _ = not (null splitths) orelse error "splitto: no given splitths"; - val sgn = Thm.theory_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 = - Thm.biresolution false [(false,split)] 1 th; - - fun split th = - (case find_thms_split splitths 1 th of - NONE => - (writeln "th:"; - Display.print_thm th; writeln "split ths:"; - Display.print_thms splitths; writeln "\n--"; - error "splitto: cannot find variable to split on") - | SOME v => - let - val gt = Data.dest_Trueprop (List.nth(Thm.prems_of th, 0)); - 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. *) -fun derive_init_eqs sgn rules eqs = - let - fun get_related_thms i = - List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE)); - fun add_eq (i, e) xs = - (e, (get_related_thms i rules), i) :: xs - fun solve_eq (th, [], i) = - error "derive_init_eqs: missing rules" - | solve_eq (th, [a], i) = (a, i) - | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i); - val eqths = - map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs; - in - [] - |> fold_index add_eq eqths - |> map solve_eq - |> rev - end; - -end; - - -structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL); diff -r 073a65f0bc40 -r ed3f6685ff90 TFL/dcterm.ML --- a/TFL/dcterm.ML Thu May 31 13:18:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,200 +0,0 @@ -(* Title: TFL/dcterm.ML - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge -*) - -(*--------------------------------------------------------------------------- - * Derived efficient cterm destructors. - *---------------------------------------------------------------------------*) - -signature DCTERM = -sig - val dest_comb: cterm -> cterm * cterm - val dest_abs: string option -> cterm -> cterm * cterm - val capply: cterm -> cterm -> cterm - val cabs: cterm -> cterm -> cterm - val mk_conj: cterm * cterm -> cterm - val mk_disj: cterm * cterm -> cterm - val mk_exists: cterm * cterm -> cterm - val dest_conj: cterm -> cterm * cterm - val dest_const: cterm -> {Name: string, Ty: typ} - val dest_disj: cterm -> cterm * cterm - val dest_eq: cterm -> cterm * cterm - val dest_exists: cterm -> cterm * cterm - val dest_forall: cterm -> cterm * cterm - val dest_imp: cterm -> cterm * cterm - val dest_let: cterm -> cterm * cterm - val dest_neg: cterm -> cterm - val dest_pair: cterm -> cterm * cterm - val dest_var: cterm -> {Name:string, Ty:typ} - val is_conj: cterm -> bool - val is_cons: cterm -> bool - val is_disj: cterm -> bool - val is_eq: cterm -> bool - val is_exists: cterm -> bool - val is_forall: cterm -> bool - val is_imp: cterm -> bool - val is_let: cterm -> bool - val is_neg: cterm -> bool - val is_pair: cterm -> bool - val list_mk_disj: cterm list -> cterm - val strip_abs: cterm -> cterm list * cterm - val strip_comb: cterm -> cterm * cterm list - val strip_disj: cterm -> cterm list - val strip_exists: cterm -> cterm list * cterm - val strip_forall: cterm -> cterm list * cterm - val strip_imp: cterm -> cterm list * cterm - val drop_prop: cterm -> cterm - val mk_prop: cterm -> cterm -end; - -structure Dcterm: DCTERM = -struct - -structure U = Utils; - -fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg}; - - -fun dest_comb t = Thm.dest_comb t - handle CTERM (msg, _) => raise ERR "dest_comb" msg; - -fun dest_abs a t = Thm.dest_abs a t - handle CTERM (msg, _) => raise ERR "dest_abs" msg; - -fun capply t u = Thm.capply t u - handle CTERM (msg, _) => raise ERR "capply" msg; - -fun cabs a t = Thm.cabs a t - handle CTERM (msg, _) => raise ERR "cabs" msg; - - -(*--------------------------------------------------------------------------- - * Some simple constructor functions. - *---------------------------------------------------------------------------*) - -val mk_hol_const = Thm.cterm_of HOL.thy o Const; - -fun mk_exists (r as (Bvar, Body)) = - let val ty = #T(rep_cterm Bvar) - val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT) - in capply c (uncurry cabs r) end; - - -local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) -in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2 -end; - -local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) -in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2 -end; - - -(*--------------------------------------------------------------------------- - * The primitives. - *---------------------------------------------------------------------------*) -fun dest_const ctm = - (case #t(rep_cterm ctm) - of Const(s,ty) => {Name = s, Ty = ty} - | _ => raise ERR "dest_const" "not a constant"); - -fun dest_var ctm = - (case #t(rep_cterm ctm) - of Var((s,i),ty) => {Name=s, Ty=ty} - | Free(s,ty) => {Name=s, Ty=ty} - | _ => raise ERR "dest_var" "not a variable"); - - -(*--------------------------------------------------------------------------- - * Derived destructor operations. - *---------------------------------------------------------------------------*) - -fun dest_monop expected tm = - let - fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected); - val (c, N) = dest_comb tm handle U.ERR _ => err (); - val name = #Name (dest_const c handle U.ERR _ => err ()); - in if name = expected then N else err () end; - -fun dest_binop expected tm = - let - fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected); - val (M, N) = dest_comb tm handle U.ERR _ => err () - in (dest_monop expected M, N) handle U.ERR _ => err () end; - -fun dest_binder expected tm = - dest_abs NONE (dest_monop expected tm) - handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected); - - -val dest_neg = dest_monop "not" -val dest_pair = dest_binop "Pair"; -val dest_eq = dest_binop "op =" -val dest_imp = dest_binop "op -->" -val dest_conj = dest_binop "op &" -val dest_disj = dest_binop "op |" -val dest_cons = dest_binop "Cons" -val dest_let = Library.swap o dest_binop "Let"; -val dest_select = dest_binder "Hilbert_Choice.Eps" -val dest_exists = dest_binder "Ex" -val dest_forall = dest_binder "All" - -(* Query routines *) - -val is_eq = can dest_eq -val is_imp = can dest_imp -val is_select = can dest_select -val is_forall = can dest_forall -val is_exists = can dest_exists -val is_neg = can dest_neg -val is_conj = can dest_conj -val is_disj = can dest_disj -val is_pair = can dest_pair -val is_let = can dest_let -val is_cons = can dest_cons - - -(*--------------------------------------------------------------------------- - * Iterated creation. - *---------------------------------------------------------------------------*) -val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm)); - -(*--------------------------------------------------------------------------- - * Iterated destruction. (To the "right" in a term.) - *---------------------------------------------------------------------------*) -fun strip break tm = - let fun dest (p as (ctm,accum)) = - let val (M,N) = break ctm - in dest (N, M::accum) - end handle U.ERR _ => p - in dest (tm,[]) - end; - -fun rev2swap (x,l) = (rev l, x); - -val strip_comb = strip (Library.swap o dest_comb) (* Goes to the "left" *) -val strip_imp = rev2swap o strip dest_imp -val strip_abs = rev2swap o strip (dest_abs NONE) -val strip_forall = rev2swap o strip dest_forall -val strip_exists = rev2swap o strip dest_exists - -val strip_disj = rev o (op::) o strip dest_disj - - -(*--------------------------------------------------------------------------- - * Going into and out of prop - *---------------------------------------------------------------------------*) - -fun mk_prop ctm = - let val {t, thy, ...} = Thm.rep_cterm ctm in - if can HOLogic.dest_Trueprop t then ctm - else Thm.cterm_of thy (HOLogic.mk_Trueprop t) - end - handle TYPE (msg, _, _) => raise ERR "mk_prop" msg - | TERM (msg, _) => raise ERR "mk_prop" msg; - -fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm; - - -end; diff -r 073a65f0bc40 -r ed3f6685ff90 TFL/post.ML --- a/TFL/post.ML Thu May 31 13:18:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,279 +0,0 @@ -(* Title: TFL/post.ML - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Second part of main module (postprocessing of TFL definitions). -*) - -signature TFL = -sig - val trace: bool ref - val quiet_mode: bool ref - val message: string -> unit - val tgoalw: theory -> thm list -> thm list -> thm list - val tgoal: theory -> thm list -> thm list - val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring -> - term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} - val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring -> - string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} - val defer_i: theory -> thm list -> xstring -> term list -> theory * thm - val defer: theory -> thm list -> xstring -> string list -> theory * thm -end; - -structure Tfl: TFL = -struct - -structure S = USyntax - - -(* messages *) - -val trace = Prim.trace - -val quiet_mode = ref false; -fun message s = if ! quiet_mode then () else writeln s; - - -(* misc *) - -(*--------------------------------------------------------------------------- - * Extract termination goals so that they can be put it into a goalstack, or - * have a tactic directly applied to them. - *--------------------------------------------------------------------------*) -fun termination_goals rules = - map (Type.freeze o HOLogic.dest_Trueprop) - (foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules); - -(*--------------------------------------------------------------------------- - * Finds the termination conditions in (highly massaged) definition and - * puts them into a goalstack. - *--------------------------------------------------------------------------*) -fun tgoalw thy defs rules = - case termination_goals rules of - [] => error "tgoalw: no termination conditions to prove" - | L => OldGoals.goalw_cterm defs - (Thm.cterm_of thy - (HOLogic.mk_Trueprop(USyntax.list_mk_conj L))); - -fun tgoal thy = tgoalw thy []; - -(*--------------------------------------------------------------------------- - * Three postprocessors are applied to the definition. It - * attempts to prove wellfoundedness of the given relation, simplifies the - * non-proved termination conditions, and finally attempts to prove the - * simplified termination conditions. - *--------------------------------------------------------------------------*) -fun std_postprocessor strict cs ss wfs = - Prim.postprocess strict - {wf_tac = REPEAT (ares_tac wfs 1), - terminator = asm_simp_tac ss 1 - THEN TRY (silent_arith_tac 1 ORELSE - fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1), - simplifier = Rules.simpl_conv ss []}; - - - -val concl = #2 o Rules.dest_thm; - -(*--------------------------------------------------------------------------- - * Postprocess a definition made by "define". This is a separate stage of - * processing from the definition stage. - *---------------------------------------------------------------------------*) -local -structure R = Rules -structure U = Utils - -(* The rest of these local definitions are for the tricky nested case *) -val solved = not o can S.dest_eq o #2 o S.strip_forall o concl - -fun id_thm th = - let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th)))); - in lhs aconv rhs end - handle U.ERR _ => false; - - -fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); -val P_imp_P_iff_True = prover "P --> (P= True)" RS mp; -val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; -fun mk_meta_eq r = case concl_of r of - Const("==",_)$_$_ => r - | _ $(Const("op =",_)$_$_) => r RS eq_reflection - | _ => r RS P_imp_P_eq_True - -(*Is this the best way to invoke the simplifier??*) -fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L)) - -fun join_assums th = - let val {thy,...} = rep_thm th - val tych = cterm_of thy - val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) - val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) - val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) - val cntxt = gen_union (op aconv) (cntxtl, cntxtr) - in - R.GEN_ALL - (R.DISCH_ALL - (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) - end - val gen_all = S.gen_all -in -fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} = - let - val _ = message "Proving induction theorem ..." - val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} - val _ = message "Postprocessing ..."; - val {rules, induction, nested_tcs} = - std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs} - in - case nested_tcs - of [] => {induction=induction, rules=rules,tcs=[]} - | L => let val dummy = message "Simplifying nested TCs ..." - val (solved,simplified,stubborn) = - fold_rev (fn th => fn (So,Si,St) => - if (id_thm th) then (So, Si, th::St) else - if (solved th) then (th::So, Si, St) - else (So, th::Si, St)) nested_tcs ([],[],[]) - val simplified' = map join_assums simplified - val dummy = (Prim.trace_thms "solved =" solved; - Prim.trace_thms "simplified' =" simplified') - val rewr = full_simplify (ss addsimps (solved @ simplified')); - val dummy = Prim.trace_thms "Simplifying the induction rule..." - [induction] - val induction' = rewr induction - val dummy = Prim.trace_thms "Simplifying the recursion rules..." - [rules] - val rules' = rewr rules - val _ = message "... Postprocessing finished"; - in - {induction = induction', - rules = rules', - tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) - (simplified@stubborn)} - end - end; - - -(*lcp: curry the predicate of the induction rule*) -fun curry_rule rl = - SplitRule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl; - -(*lcp: put a theorem into Isabelle form, using meta-level connectives*) -val meta_outer = - curry_rule o standard o - rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); - -(*Strip off the outer !P*) -val spec'= read_instantiate [("x","P::?'b=>bool")] spec; - -fun tracing true _ = () - | tracing false msg = writeln msg; - -fun simplify_defn strict thy cs ss congs wfs id pats def0 = - let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq - val {rules,rows,TCs,full_pats_TCs} = - Prim.post_definition congs (thy, (def,pats)) - val {lhs=f,rhs} = S.dest_eq (concl def) - val (_,[R,_]) = S.strip_comb rhs - val dummy = Prim.trace_thms "congs =" congs - (*the next step has caused simplifier looping in some cases*) - val {induction, rules, tcs} = - proof_stage strict cs ss wfs thy - {f = f, R = R, rules = rules, - full_pats_TCs = full_pats_TCs, - TCs = TCs} - val rules' = map (standard o ObjectLogic.rulify_no_asm) - (R.CONJUNCTS rules) - in {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')), - rules = ListPair.zip(rules', rows), - tcs = (termination_goals rules') @ tcs} - end - handle U.ERR {mesg,func,module} => - 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. --- Lucas Dixon, Aug 2004 *) -local - fun get_related_thms i = - List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE)); - - fun solve_eq (th, [], i) = - error "derive_init_eqs: missing rules" - | solve_eq (th, [a], i) = [(a, i)] - | solve_eq (th, splitths as (_ :: _), i) = - (writeln "Proving unsplit equation..."; - [((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 s => - (warning ("recdef (solve_eq): " ^ s); 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 (Library.foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l) - in - List.concat (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. - *---------------------------------------------------------------------------*) -fun define_i strict thy cs ss congs wfs fid R eqs = - let val {functional,pats} = Prim.mk_functional thy eqs - val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional - val {induct, rules, tcs} = - simplify_defn strict thy cs ss congs wfs fid pats def - val rules' = - if strict then derive_init_eqs thy rules eqs - else rules - in (thy, {rules = rules', induct = induct, tcs = tcs}) end; - -fun define strict thy cs ss congs wfs fid R seqs = - define_i strict thy cs ss congs wfs fid (Sign.read_term thy R) (map (Sign.read_term thy) seqs) - handle U.ERR {mesg,...} => error mesg; - - -(*--------------------------------------------------------------------------- - * - * Definitions with synthesized termination relation - * - *---------------------------------------------------------------------------*) - -fun func_of_cond_eqn tm = - #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm))))))); - -fun defer_i thy congs fid eqs = - let val {rules,R,theory,full_pats_TCs,SV,...} = - Prim.lazyR_def thy (Sign.base_name fid) congs eqs - val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules)); - val dummy = message "Proving induction theorem ..."; - val induction = Prim.mk_induction theory - {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} - in (theory, - (*return the conjoined induction rule and recursion equations, - with assumptions remaining to discharge*) - standard (induction RS (rules RS conjI))) - end - -fun defer thy congs fid seqs = - defer_i thy congs fid (map (Sign.read_term thy) seqs) - handle U.ERR {mesg,...} => error mesg; -end; - -end; diff -r 073a65f0bc40 -r ed3f6685ff90 TFL/rules.ML --- a/TFL/rules.ML Thu May 31 13:18:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,825 +0,0 @@ -(* Title: TFL/rules.ML - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Emulation of HOL inference rules for TFL -*) - -signature RULES = -sig - val dest_thm: thm -> term list * term - - (* Inference rules *) - val REFL: cterm -> thm - val ASSUME: cterm -> thm - val MP: thm -> thm -> thm - val MATCH_MP: thm -> thm -> thm - val CONJUNCT1: thm -> thm - val CONJUNCT2: thm -> thm - val CONJUNCTS: thm -> thm list - val DISCH: cterm -> thm -> thm - val UNDISCH: thm -> thm - val SPEC: cterm -> thm -> thm - val ISPEC: cterm -> thm -> thm - val ISPECL: cterm list -> thm -> thm - val GEN: cterm -> thm -> thm - val GENL: cterm list -> thm -> thm - val LIST_CONJ: thm list -> thm - - val SYM: thm -> thm - val DISCH_ALL: thm -> thm - val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm - val SPEC_ALL: thm -> thm - val GEN_ALL: thm -> thm - val IMP_TRANS: thm -> thm -> thm - val PROVE_HYP: thm -> thm -> thm - - val CHOOSE: cterm * thm -> thm -> thm - val EXISTS: cterm * cterm -> thm -> thm - val EXISTL: cterm list -> thm -> thm - val IT_EXISTS: (cterm*cterm) list -> thm -> thm - - val EVEN_ORS: thm list -> thm list - val DISJ_CASESL: thm -> thm list -> thm - - val list_beta_conv: cterm -> cterm list -> thm - val SUBS: thm list -> thm -> thm - val simpl_conv: simpset -> thm list -> cterm -> thm - - val rbeta: thm -> thm -(* For debugging my isabelle solver in the conditional rewriter *) - val term_ref: term list ref - val thm_ref: thm list ref - val ss_ref: simpset list ref - val tracing: bool ref - val CONTEXT_REWRITE_RULE: term * term list * thm * thm list - -> thm -> thm * term list - val RIGHT_ASSOC: thm -> thm - - val prove: bool -> cterm * tactic -> thm -end; - -structure Rules: RULES = -struct - -structure S = USyntax; -structure U = Utils; -structure D = Dcterm; - - -fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg}; - - -fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm)); -fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm)); - -fun dest_thm thm = - let val {prop,hyps,...} = Thm.rep_thm thm - in (map HOLogic.dest_Trueprop hyps, HOLogic.dest_Trueprop prop) end - handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop"; - - -(* Inference rules *) - -(*--------------------------------------------------------------------------- - * Equality (one step) - *---------------------------------------------------------------------------*) - -fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq - handle THM (msg, _, _) => raise RULES_ERR "REFL" msg; - -fun SYM thm = thm RS sym - handle THM (msg, _, _) => raise RULES_ERR "SYM" msg; - -fun ALPHA thm ctm1 = - let - val ctm2 = Thm.cprop_of thm; - val ctm2_eq = Thm.reflexive ctm2; - val ctm1_eq = Thm.reflexive ctm1; - in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end - handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg; - -fun rbeta th = - (case D.strip_comb (cconcl th) of - (_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r) - | _ => raise RULES_ERR "rbeta" ""); - - -(*---------------------------------------------------------------------------- - * Implication and the assumption list - * - * Assumptions get stuck on the meta-language assumption list. Implications - * are in the object language, so discharging an assumption "A" from theorem - * "B" results in something that looks like "A --> B". - *---------------------------------------------------------------------------*) - -fun ASSUME ctm = Thm.assume (D.mk_prop ctm); - - -(*--------------------------------------------------------------------------- - * Implication in TFL is -->. Meta-language implication (==>) is only used - * in the implementation of some of the inference rules below. - *---------------------------------------------------------------------------*) -fun MP th1 th2 = th2 RS (th1 RS mp) - handle THM (msg, _, _) => raise RULES_ERR "MP" msg; - -(*forces the first argument to be a proposition if necessary*) -fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI - handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg; - -fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm; - - -fun FILTER_DISCH_ALL P thm = - let fun check tm = P (#t (Thm.rep_cterm tm)) - in foldr (fn (tm,th) => if check tm then DISCH tm th else th) - thm (chyps thm) - end; - -(* freezeT expensive! *) -fun UNDISCH thm = - let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm)))) - in Thm.implies_elim (thm RS mp) (ASSUME tm) end - handle U.ERR _ => raise RULES_ERR "UNDISCH" "" - | THM _ => raise RULES_ERR "UNDISCH" ""; - -fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath; - -fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans) - handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg; - - -(*---------------------------------------------------------------------------- - * Conjunction - *---------------------------------------------------------------------------*) - -fun CONJUNCT1 thm = thm RS conjunct1 - handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg; - -fun CONJUNCT2 thm = thm RS conjunct2 - handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg; - -fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th]; - -fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list" - | LIST_CONJ [th] = th - | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst) - handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg; - - -(*---------------------------------------------------------------------------- - * Disjunction - *---------------------------------------------------------------------------*) -local val {prop,thy,...} = rep_thm disjI1 - val [P,Q] = term_vars prop - val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1 -in -fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1) - handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg; -end; - -local val {prop,thy,...} = rep_thm disjI2 - val [P,Q] = term_vars prop - val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2 -in -fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2) - handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg; -end; - - -(*---------------------------------------------------------------------------- - * - * A1 |- M1, ..., An |- Mn - * --------------------------------------------------- - * [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn] - * - *---------------------------------------------------------------------------*) - - -fun EVEN_ORS thms = - let fun blue ldisjs [] _ = [] - | blue ldisjs (th::rst) rdisjs = - let val tail = tl rdisjs - val rdisj_tl = D.list_mk_disj tail - in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl) - :: blue (ldisjs @ [cconcl th]) rst tail - end handle U.ERR _ => [fold_rev DISJ2 ldisjs th] - in blue [] thms (map cconcl thms) end; - - -(*---------------------------------------------------------------------------- - * - * A |- P \/ Q B,P |- R C,Q |- R - * --------------------------------------------------- - * A U B U C |- R - * - *---------------------------------------------------------------------------*) - -fun DISJ_CASES th1 th2 th3 = - let - val c = D.drop_prop (cconcl th1); - val (disj1, disj2) = D.dest_disj c; - val th2' = DISCH disj1 th2; - val th3' = DISCH disj2 th3; - in - th3' RS (th2' RS (th1 RS Thms.tfl_disjE)) - handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg - end; - - -(*----------------------------------------------------------------------------- - * - * |- A1 \/ ... \/ An [A1 |- M, ..., An |- M] - * --------------------------------------------------- - * |- M - * - * Note. The list of theorems may be all jumbled up, so we have to - * first organize it to align with the first argument (the disjunctive - * theorem). - *---------------------------------------------------------------------------*) - -fun organize eq = (* a bit slow - analogous to insertion sort *) - let fun extract a alist = - let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1" - | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t) - in ex ([],alist) - end - fun place [] [] = [] - | place (a::rst) alist = - let val (item,next) = extract a alist - in item::place rst next - end - | place _ _ = raise RULES_ERR "organize" "not a permutation.2" - in place - end; -(* freezeT expensive! *) -fun DISJ_CASESL disjth thl = - let val c = cconcl disjth - fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t - aconv term_of atm) - (#hyps(rep_thm th)) - val tml = D.strip_disj c - fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases" - | DL th [th1] = PROVE_HYP th th1 - | DL th [th1,th2] = DISJ_CASES th th1 th2 - | DL th (th1::rst) = - let val tm = #2(D.dest_disj(D.drop_prop(cconcl th))) - in DISJ_CASES th th1 (DL (ASSUME tm) rst) end - in DL (Thm.freezeT disjth) (organize eq tml thl) - end; - - -(*---------------------------------------------------------------------------- - * Universals - *---------------------------------------------------------------------------*) -local (* this is fragile *) - val {prop,thy,...} = rep_thm spec - val x = hd (tl (term_vars prop)) - val cTV = ctyp_of thy (type_of x) - val gspec = forall_intr (cterm_of thy x) spec -in -fun SPEC tm thm = - let val {thy,T,...} = rep_cterm tm - val gspec' = instantiate ([(cTV, ctyp_of thy T)], []) gspec - in - thm RS (forall_elim tm gspec') - end -end; - -fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm; - -val ISPEC = SPEC -val ISPECL = fold ISPEC; - -(* Not optimized! Too complicated. *) -local val {prop,thy,...} = rep_thm allI - val [P] = add_term_vars (prop, []) - fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty)) - fun ctm_theta s = map (fn (i, (_, tm2)) => - let val ctm2 = cterm_of s tm2 - in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2) - end) - fun certify s (ty_theta,tm_theta) = - (cty_theta s (Vartab.dest ty_theta), - ctm_theta s (Vartab.dest tm_theta)) -in -fun GEN v th = - let val gth = forall_intr v th - val {prop=Const("all",_)$Abs(x,ty,rst),thy,...} = rep_thm gth - val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *) - val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty); - val allI2 = instantiate (certify thy theta) allI - val thm = Thm.implies_elim allI2 gth - val {prop = tp $ (A $ Abs(_,_,M)),thy,...} = rep_thm thm - val prop' = tp $ (A $ Abs(x,ty,M)) - in ALPHA thm (cterm_of thy prop') - end -end; - -val GENL = fold_rev GEN; - -fun GEN_ALL thm = - let val {prop,thy,...} = rep_thm thm - val tycheck = cterm_of thy - val vlist = map tycheck (add_term_vars (prop, [])) - in GENL vlist thm - end; - - -fun MATCH_MP th1 th2 = - if (D.is_forall (D.drop_prop(cconcl th1))) - then MATCH_MP (th1 RS spec) th2 - else MP th1 th2; - - -(*---------------------------------------------------------------------------- - * Existentials - *---------------------------------------------------------------------------*) - - - -(*--------------------------------------------------------------------------- - * Existential elimination - * - * A1 |- ?x.t[x] , A2, "t[v]" |- t' - * ------------------------------------ (variable v occurs nowhere) - * A1 u A2 |- t' - * - *---------------------------------------------------------------------------*) - -fun CHOOSE (fvar, exth) fact = - let - val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth))) - val redex = D.capply lam fvar - val {thy, t = t$u,...} = Thm.rep_cterm redex - val residue = Thm.cterm_of thy (Term.betapply (t, u)) - in - GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm) - handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg - end; - -local val {prop,thy,...} = rep_thm exI - val [P,x] = term_vars prop -in -fun EXISTS (template,witness) thm = - let val {prop,thy,...} = rep_thm thm - val P' = cterm_of thy P - val x' = cterm_of thy x - val abstr = #2 (D.dest_comb template) - in - thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI) - handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg - end -end; - -(*---------------------------------------------------------------------------- - * - * A |- M - * ------------------- [v_1,...,v_n] - * A |- ?v1...v_n. M - * - *---------------------------------------------------------------------------*) - -fun EXISTL vlist th = - fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm) - vlist th; - - -(*---------------------------------------------------------------------------- - * - * A |- M[x_1,...,x_n] - * ---------------------------- [(x |-> y)_1,...,(x |-> y)_n] - * A |- ?y_1...y_n. M - * - *---------------------------------------------------------------------------*) -(* Could be improved, but needs "subst_free" for certified terms *) - -fun IT_EXISTS blist th = - let val {thy,...} = rep_thm th - val tych = cterm_of thy - val detype = #t o rep_cterm - val blist' = map (fn (x,y) => (detype x, detype y)) blist - fun ex v M = cterm_of thy (S.mk_exists{Bvar=v,Body = M}) - - in - fold_rev (fn (b as (r1,r2)) => fn thm => - EXISTS(ex r2 (subst_free [b] - (HOLogic.dest_Trueprop(#prop(rep_thm thm)))), tych r1) - thm) - blist' th - end; - -(*--------------------------------------------------------------------------- - * Faster version, that fails for some as yet unknown reason - * fun IT_EXISTS blist th = - * let val {thy,...} = rep_thm th - * val tych = cterm_of thy - * fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y) - * in - * fold (fn (b as (r1,r2), thm) => - * EXISTS(D.mk_exists(r2, tych(subst_free[detype b](#t(rep_cterm(cconcl thm))))), - * r1) thm) blist th - * end; - *---------------------------------------------------------------------------*) - -(*---------------------------------------------------------------------------- - * Rewriting - *---------------------------------------------------------------------------*) - -fun SUBS thl = - rewrite_rule (map (fn th => th RS eq_reflection handle THM _ => th) thl); - -val rew_conv = MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)); - -fun simpl_conv ss thl ctm = - rew_conv (ss addsimps thl) ctm RS meta_eq_to_obj_eq; - - -val RIGHT_ASSOC = rewrite_rule [Thms.disj_assoc]; - - - -(*--------------------------------------------------------------------------- - * TERMINATION CONDITION EXTRACTION - *---------------------------------------------------------------------------*) - - -(* Object language quantifier, i.e., "!" *) -fun Forall v M = S.mk_forall{Bvar=v, Body=M}; - - -(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *) -fun is_cong thm = - let val {prop, ...} = rep_thm thm - in case prop - of (Const("==>",_)$(Const("Trueprop",_)$ _) $ - (Const("==",_) $ (Const ("Wellfounded_Recursion.cut",_) $ f $ R $ a $ x) $ _)) => false - | _ => true - end; - - - -fun dest_equal(Const ("==",_) $ - (Const ("Trueprop",_) $ lhs) - $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs} - | dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs} - | dest_equal tm = S.dest_eq tm; - -fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm)); - -fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a - | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!"; - -val is_all = can (dest_all []); - -fun strip_all used fm = - if (is_all fm) - then let val ({Bvar, Body}, used') = dest_all used fm - val (bvs, core, used'') = strip_all used' Body - in ((Bvar::bvs), core, used'') - end - else ([], fm, used); - -fun break_all(Const("all",_) $ Abs (_,_,body)) = body - | break_all _ = raise RULES_ERR "break_all" "not a !!"; - -fun list_break_all(Const("all",_) $ Abs (s,ty,body)) = - let val (L,core) = list_break_all body - in ((s,ty)::L, core) - end - | list_break_all tm = ([],tm); - -(*--------------------------------------------------------------------------- - * Rename a term of the form - * - * !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn - * ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn. - * to one of - * - * !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn - * ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn. - * - * This prevents name problems in extraction, and helps the result to read - * better. There is a problem with varstructs, since they can introduce more - * than n variables, and some extra reasoning needs to be done. - *---------------------------------------------------------------------------*) - -fun get ([],_,L) = rev L - | get (ant::rst,n,L) = - case (list_break_all ant) - of ([],_) => get (rst, n+1,L) - | (vlist,body) => - let val eq = Logic.strip_imp_concl body - val (f,args) = S.strip_comb (get_lhs eq) - val (vstrl,_) = S.strip_abs f - val names = - Name.variant_list (add_term_names(body, [])) (map (#1 o dest_Free) vstrl) - in get (rst, n+1, (names,n)::L) end - handle TERM _ => get (rst, n+1, L) - | U.ERR _ => get (rst, n+1, L); - -(* Note: rename_params_rule counts from 1, not 0 *) -fun rename thm = - let val {prop,thy,...} = rep_thm thm - val tych = cterm_of thy - val ants = Logic.strip_imp_prems prop - val news = get (ants,1,[]) - in - fold rename_params_rule news thm - end; - - -(*--------------------------------------------------------------------------- - * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml) - *---------------------------------------------------------------------------*) - -fun list_beta_conv tm = - let fun rbeta th = Thm.transitive th (beta_conversion false (#2(D.dest_eq(cconcl th)))) - fun iter [] = Thm.reflexive tm - | iter (v::rst) = rbeta (combination(iter rst) (Thm.reflexive v)) - in iter end; - - -(*--------------------------------------------------------------------------- - * Trace information for the rewriter - *---------------------------------------------------------------------------*) -val term_ref = ref[] : term list ref -val ss_ref = ref [] : simpset list ref; -val thm_ref = ref [] : thm list ref; -val tracing = ref false; - -fun say s = if !tracing then writeln s else (); - -fun print_thms s L = - say (cat_lines (s :: map string_of_thm L)); - -fun print_cterms s L = - say (cat_lines (s :: map string_of_cterm L)); - - -(*--------------------------------------------------------------------------- - * General abstraction handlers, should probably go in USyntax. - *---------------------------------------------------------------------------*) -fun mk_aabs (vstr, body) = - S.mk_abs {Bvar = vstr, Body = body} - handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body}; - -fun list_mk_aabs (vstrl,tm) = - fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm; - -fun dest_aabs used tm = - let val ({Bvar,Body}, used') = S.dest_abs used tm - in (Bvar, Body, used') end - handle U.ERR _ => - let val {varstruct, body, used} = S.dest_pabs used tm - in (varstruct, body, used) end; - -fun strip_aabs used tm = - let val (vstr, body, used') = dest_aabs used tm - val (bvs, core, used'') = strip_aabs used' body - in (vstr::bvs, core, used'') end - handle U.ERR _ => ([], tm, used); - -fun dest_combn tm 0 = (tm,[]) - | dest_combn tm n = - let val {Rator,Rand} = S.dest_comb tm - val (f,rands) = dest_combn Rator (n-1) - in (f,Rand::rands) - end; - - - - -local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end - fun mk_fst tm = - let val ty as Type("*", [fty,sty]) = type_of tm - in Const ("fst", ty --> fty) $ tm end - fun mk_snd tm = - let val ty as Type("*", [fty,sty]) = type_of tm - in Const ("snd", ty --> sty) $ tm end -in -fun XFILL tych x vstruct = - let fun traverse p xocc L = - if (is_Free p) - then tych xocc::L - else let val (p1,p2) = dest_pair p - in traverse p1 (mk_fst xocc) (traverse p2 (mk_snd xocc) L) - end - in - traverse vstruct x [] -end end; - -(*--------------------------------------------------------------------------- - * Replace a free tuple (vstr) by a universally quantified variable (a). - * Note that the notion of "freeness" for a tuple is different than for a - * variable: if variables in the tuple also occur in any other place than - * an occurrences of the tuple, they aren't "free" (which is thus probably - * the wrong word to use). - *---------------------------------------------------------------------------*) - -fun VSTRUCT_ELIM tych a vstr th = - let val L = S.free_vars_lr vstr - val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr))) - val thm1 = implies_intr bind1 (SUBS [SYM(assume bind1)] th) - val thm2 = forall_intr_list (map tych L) thm1 - val thm3 = forall_elim_list (XFILL tych a vstr) thm2 - in refl RS - rewrite_rule [Thm.symmetric (surjective_pairing RS eq_reflection)] thm3 - end; - -fun PGEN tych a vstr th = - let val a1 = tych a - val vstr1 = tych vstr - in - forall_intr a1 - (if (is_Free vstr) - then cterm_instantiate [(vstr1,a1)] th - else VSTRUCT_ELIM tych a vstr th) - end; - - -(*--------------------------------------------------------------------------- - * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into - * - * (([x,y],N),vstr) - *---------------------------------------------------------------------------*) -fun dest_pbeta_redex used M n = - let val (f,args) = dest_combn M n - val dummy = dest_aabs used f - in (strip_aabs used f,args) - end; - -fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M; - -fun dest_impl tm = - let val ants = Logic.strip_imp_prems tm - val eq = Logic.strip_imp_concl tm - in (ants,get_lhs eq) - end; - -fun restricted t = isSome (S.find_term - (fn (Const("Wellfounded_Recursion.cut",_)) =>true | _ => false) - t) - -fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th = - let val globals = func::G - val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss - val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection]; - val tc_list = ref[]: term list ref - val dummy = term_ref := [] - val dummy = thm_ref := [] - val dummy = ss_ref := [] - val cut_lemma' = cut_lemma RS eq_reflection - fun prover used ss thm = - let fun cong_prover ss thm = - let val dummy = say "cong_prover:" - val cntxt = MetaSimplifier.prems_of_ss ss - val dummy = print_thms "cntxt:" cntxt - val dummy = say "cong rule:" - val dummy = say (string_of_thm thm) - val dummy = thm_ref := (thm :: !thm_ref) - val dummy = ss_ref := (ss :: !ss_ref) - (* Unquantified eliminate *) - fun uq_eliminate (thm,imp,thy) = - let val tych = cterm_of thy - val dummy = print_cterms "To eliminate:" [tych imp] - val ants = map tych (Logic.strip_imp_prems imp) - val eq = Logic.strip_imp_concl imp - val lhs = tych(get_lhs eq) - val ss' = MetaSimplifier.add_prems (map ASSUME ants) ss - val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs - handle U.ERR _ => Thm.reflexive lhs - val dummy = print_thms "proven:" [lhs_eq_lhs1] - val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 - val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq - in - lhs_eeq_lhs2 COMP thm - end - fun pq_eliminate (thm,thy,vlist,imp_body,lhs_eq) = - let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist) - val dummy = forall (op aconv) (ListPair.zip (vlist, args)) - orelse error "assertion failed in CONTEXT_REWRITE_RULE" - val imp_body1 = subst_free (ListPair.zip (args, vstrl)) - imp_body - val tych = cterm_of thy - val ants1 = map tych (Logic.strip_imp_prems imp_body1) - val eq1 = Logic.strip_imp_concl imp_body1 - val Q = get_lhs eq1 - val QeqQ1 = pbeta_reduce (tych Q) - val Q1 = #2(D.dest_eq(cconcl QeqQ1)) - val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss - val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1 - handle U.ERR _ => Thm.reflexive Q1 - val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2)) - val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl)) - val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection) - val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2 - val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ => - ((Q2eeqQ3 RS meta_eq_to_obj_eq) - RS ((thA RS meta_eq_to_obj_eq) RS trans)) - RS eq_reflection - val impth = implies_intr_list ants1 QeeqQ3 - val impth1 = impth RS meta_eq_to_obj_eq - (* Need to abstract *) - val ant_th = U.itlist2 (PGEN tych) args vstrl impth1 - in ant_th COMP thm - end - fun q_eliminate (thm,imp,thy) = - let val (vlist, imp_body, used') = strip_all used imp - val (ants,Q) = dest_impl imp_body - in if (pbeta_redex Q) (length vlist) - then pq_eliminate (thm,thy,vlist,imp_body,Q) - else - let val tych = cterm_of thy - val ants1 = map tych ants - val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss - val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm - (false,true,false) (prover used') ss' (tych Q) - handle U.ERR _ => Thm.reflexive (tych Q) - val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 - val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq - val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2 - in - ant_th COMP thm - end end - - fun eliminate thm = - case (rep_thm thm) - of {prop = (Const("==>",_) $ imp $ _), thy, ...} => - eliminate - (if not(is_all imp) - then uq_eliminate (thm,imp,thy) - else q_eliminate (thm,imp,thy)) - (* Assume that the leading constant is ==, *) - | _ => thm (* if it is not a ==> *) - in SOME(eliminate (rename thm)) end - handle U.ERR _ => NONE (* FIXME handle THM as well?? *) - - fun restrict_prover ss thm = - let val dummy = say "restrict_prover:" - val cntxt = rev(MetaSimplifier.prems_of_ss ss) - val dummy = print_thms "cntxt:" cntxt - val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _, - thy,...} = rep_thm thm - fun genl tm = let val vlist = subtract (op aconv) globals - (add_term_frees(tm,[])) - in fold_rev Forall vlist tm - end - (*-------------------------------------------------------------- - * This actually isn't quite right, since it will think that - * not-fully applied occs. of "f" in the context mean that the - * current call is nested. The real solution is to pass in a - * term "f v1..vn" which is a pattern that any full application - * of "f" will match. - *-------------------------------------------------------------*) - val func_name = #1(dest_Const func) - fun is_func (Const (name,_)) = (name = func_name) - | is_func _ = false - val rcontext = rev cntxt - val cncl = HOLogic.dest_Trueprop o Thm.prop_of - val antl = case rcontext of [] => [] - | _ => [S.list_mk_conj(map cncl rcontext)] - val TC = genl(S.list_mk_imp(antl, A)) - val dummy = print_cterms "func:" [cterm_of thy func] - val dummy = print_cterms "TC:" - [cterm_of thy (HOLogic.mk_Trueprop TC)] - val dummy = tc_list := (TC :: !tc_list) - val nestedp = isSome (S.find_term is_func TC) - val dummy = if nestedp then say "nested" else say "not_nested" - val dummy = term_ref := ([func,TC]@(!term_ref)) - val th' = if nestedp then raise RULES_ERR "solver" "nested function" - else let val cTC = cterm_of thy - (HOLogic.mk_Trueprop TC) - in case rcontext of - [] => SPEC_ALL(ASSUME cTC) - | _ => MP (SPEC_ALL (ASSUME cTC)) - (LIST_CONJ rcontext) - end - val th'' = th' RS thm - in SOME (th'') - end handle U.ERR _ => NONE (* FIXME handle THM as well?? *) - in - (if (is_cong thm) then cong_prover else restrict_prover) ss thm - end - val ctm = cprop_of th - val names = add_term_names (term_of ctm, []) - val th1 = MetaSimplifier.rewrite_cterm(false,true,false) - (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm - val th2 = equal_elim th1 th - in - (th2, List.filter (not o restricted) (!tc_list)) - end; - - -fun prove strict (ptm, tac) = - let - val {thy, t, ...} = Thm.rep_cterm ptm; - val ctxt = ProofContext.init thy |> Variable.auto_fixes t; - in - if strict then Goal.prove ctxt [] [] t (K tac) - else Goal.prove ctxt [] [] t (K tac) - handle ERROR msg => (warning msg; raise RULES_ERR "prove" msg) - end; - -end; diff -r 073a65f0bc40 -r ed3f6685ff90 TFL/tfl.ML --- a/TFL/tfl.ML Thu May 31 13:18:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1008 +0,0 @@ -(* Title: TFL/tfl.ML - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -First part of main module. -*) - -signature PRIM = -sig - val trace: bool ref - val trace_thms: string -> thm list -> unit - val trace_cterms: string -> cterm list -> unit - type pattern - val mk_functional: theory -> term list -> {functional: term, pats: pattern list} - val wfrec_definition0: theory -> string -> term -> term -> theory * thm - val post_definition: thm list -> theory * (thm * pattern list) -> - {rules: thm, - rows: int list, - TCs: term list list, - full_pats_TCs: (term * term list) list} - val wfrec_eqns: theory -> xstring -> thm list -> term list -> - {WFR: term, - SV: term list, - proto_def: term, - extracta: (thm * term list) list, - pats: pattern list} - val lazyR_def: theory -> xstring -> thm list -> term list -> - {theory: theory, - rules: thm, - R: term, - SV: term list, - full_pats_TCs: (term * term list) list, - patterns : pattern list} - val mk_induction: theory -> - {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm - val postprocess: bool -> {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} - -> theory -> {rules: thm, induction: thm, TCs: term list list} - -> {rules: thm, induction: thm, nested_tcs: thm list} -end; - -structure Prim: PRIM = -struct - -val trace = ref false; - -structure R = Rules; -structure S = USyntax; -structure U = Utils; - - -fun TFL_ERR func mesg = U.ERR {module = "Tfl", func = func, mesg = mesg}; - -val concl = #2 o R.dest_thm; -val hyp = #1 o R.dest_thm; - -val list_mk_type = U.end_itlist (curry (op -->)); - -fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1)); - -fun front_last [] = raise TFL_ERR "front_last" "empty list" - | front_last [x] = ([],x) - | front_last (h::t) = - let val (pref,x) = front_last t - in - (h::pref,x) - end; - - -(*--------------------------------------------------------------------------- - * The next function is common to pattern-match translation and - * proof of completeness of cases for the induction theorem. - * - * The curried function "gvvariant" returns a function to generate distinct - * variables that are guaranteed not to be in names. The names of - * the variables go u, v, ..., z, aa, ..., az, ... The returned - * function contains embedded refs! - *---------------------------------------------------------------------------*) -fun gvvariant names = - let val slist = ref names - val vname = ref "u" - fun new() = - if !vname mem_string (!slist) - then (vname := Symbol.bump_string (!vname); new()) - else (slist := !vname :: !slist; !vname) - in - fn ty => Free(new(), ty) - end; - - -(*--------------------------------------------------------------------------- - * Used in induction theorem production. This is the simple case of - * partitioning up pattern rows by the leading constructor. - *---------------------------------------------------------------------------*) -fun ipartition gv (constructors,rows) = - let fun pfail s = raise TFL_ERR "partition.part" s - fun part {constrs = [], rows = [], A} = rev A - | part {constrs = [], rows = _::_, A} = pfail"extra cases in defn" - | part {constrs = _::_, rows = [], A} = pfail"cases missing in defn" - | part {constrs = c::crst, rows, A} = - let val (c, T) = dest_Const c - val L = binder_types T - val (in_group, not_in_group) = - fold_rev (fn (row as (p::rst, rhs)) => - fn (in_group,not_in_group) => - let val (pc,args) = S.strip_comb p - in if (#1(dest_Const pc) = c) - then ((args@rst, rhs)::in_group, not_in_group) - else (in_group, row::not_in_group) - end) rows ([],[]) - val col_types = U.take type_of (length L, #1(hd in_group)) - in - part{constrs = crst, rows = not_in_group, - A = {constructor = c, - new_formals = map gv col_types, - group = in_group}::A} - end - in part{constrs = constructors, rows = rows, A = []} - end; - - - -(*--------------------------------------------------------------------------- - * Each pattern carries with it a tag (i,b) where - * i is the clause it came from and - * b=true indicates that clause was given by the user - * (or is an instantiation of a user supplied pattern) - * b=false --> i = ~1 - *---------------------------------------------------------------------------*) - -type pattern = term * (int * bool) - -fun pattern_map f (tm,x) = (f tm, x); - -fun pattern_subst theta = pattern_map (subst_free theta); - -val pat_of = fst; -fun row_of_pat x = fst (snd x); -fun given x = snd (snd x); - -(*--------------------------------------------------------------------------- - * Produce an instance of a constructor, plus genvars for its arguments. - *---------------------------------------------------------------------------*) -fun fresh_constr ty_match colty gv c = - let val (_,Ty) = dest_Const c - val L = binder_types Ty - and ty = body_type Ty - val ty_theta = ty_match ty colty - val c' = S.inst ty_theta c - val gvars = map (S.inst ty_theta o gv) L - in (c', gvars) - end; - - -(*--------------------------------------------------------------------------- - * Goes through a list of rows and picks out the ones beginning with a - * pattern with constructor = name. - *---------------------------------------------------------------------------*) -fun mk_group name rows = - fold_rev (fn (row as ((prfx, p::rst), rhs)) => - fn (in_group,not_in_group) => - let val (pc,args) = S.strip_comb p - in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false) - then (((prfx,args@rst), rhs)::in_group, not_in_group) - else (in_group, row::not_in_group) end) - rows ([],[]); - -(*--------------------------------------------------------------------------- - * Partition the rows. Not efficient: we should use hashing. - *---------------------------------------------------------------------------*) -fun partition _ _ (_,_,_,[]) = raise TFL_ERR "partition" "no rows" - | partition gv ty_match - (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) = -let val fresh = fresh_constr ty_match colty gv - fun part {constrs = [], rows, A} = rev A - | part {constrs = c::crst, rows, A} = - let val (c',gvars) = fresh c - val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows - val in_group' = - if (null in_group) (* Constructor not given *) - then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))] - else in_group - in - part{constrs = crst, - rows = not_in_group, - A = {constructor = c', - new_formals = gvars, - group = in_group'}::A} - end -in part{constrs=constructors, rows=rows, A=[]} -end; - -(*--------------------------------------------------------------------------- - * Misc. routines used in mk_case - *---------------------------------------------------------------------------*) - -fun mk_pat (c,l) = - let val L = length (binder_types (type_of c)) - fun build (prfx,tag,plist) = - let val args = Library.take (L,plist) - and plist' = Library.drop(L,plist) - in (prfx,tag,list_comb(c,args)::plist') end - in map build l end; - -fun v_to_prfx (prfx, v::pats) = (v::prfx,pats) - | v_to_prfx _ = raise TFL_ERR "mk_case" "v_to_prfx"; - -fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats) - | v_to_pats _ = raise TFL_ERR "mk_case" "v_to_pats"; - - -(*---------------------------------------------------------------------------- - * Translation of pattern terms into nested case expressions. - * - * This performs the translation and also builds the full set of patterns. - * Thus it supports the construction of induction theorems even when an - * incomplete set of patterns is given. - *---------------------------------------------------------------------------*) - -fun mk_case ty_info ty_match usednames range_ty = - let - fun mk_case_fail s = raise TFL_ERR "mk_case" s - val fresh_var = gvvariant usednames - val divide = partition fresh_var ty_match - fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row" - | expand constructors ty (row as ((prfx, p::rst), rhs)) = - if (is_Free p) - then let val fresh = fresh_constr ty_match ty fresh_var - fun expnd (c,gvs) = - let val capp = list_comb(c,gvs) - in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs) - end - in map expnd (map fresh constructors) end - else [row] - fun mk{rows=[],...} = mk_case_fail"no rows" - | mk{path=[], rows = ((prfx, []), (tm,tag))::_} = (* Done *) - ([(prfx,tag,[])], tm) - | mk{path=[], rows = _::_} = mk_case_fail"blunder" - | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} = - mk{path = path, - rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst} - | mk{path = u::rstp, rows as ((_, p::_), _)::_} = - let val (pat_rectangle,rights) = ListPair.unzip rows - val col0 = map(hd o #2) pat_rectangle - in - if (forall is_Free col0) - then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e) - (ListPair.zip (col0, rights)) - val pat_rectangle' = map v_to_prfx pat_rectangle - val (pref_patl,tm) = mk{path = rstp, - rows = ListPair.zip (pat_rectangle', - rights')} - in (map v_to_pats pref_patl, tm) - end - else - let val pty as Type (ty_name,_) = type_of p - in - case (ty_info ty_name) - of NONE => mk_case_fail("Not a known datatype: "^ty_name) - | SOME{case_const,constructors} => - let - val case_const_name = #1(dest_Const case_const) - val nrows = List.concat (map (expand constructors pty) rows) - val subproblems = divide(constructors, pty, range_ty, nrows) - val groups = map #group subproblems - and new_formals = map #new_formals subproblems - and constructors' = map #constructor subproblems - val news = map (fn (nf,rows) => {path = nf@rstp, rows=rows}) - (ListPair.zip (new_formals, groups)) - val rec_calls = map mk news - val (pat_rect,dtrees) = ListPair.unzip rec_calls - val case_functions = map S.list_mk_abs - (ListPair.zip (new_formals, dtrees)) - val types = map type_of (case_functions@[u]) @ [range_ty] - val case_const' = Const(case_const_name, list_mk_type types) - val tree = list_comb(case_const', case_functions@[u]) - val pat_rect1 = List.concat - (ListPair.map mk_pat (constructors', pat_rect)) - in (pat_rect1,tree) - end - end end - in mk - end; - - -(* Repeated variable occurrences in a pattern are not allowed. *) -fun FV_multiset tm = - case (S.dest_term tm) - of S.VAR{Name = c, Ty = T} => [Free(c, T)] - | S.CONST _ => [] - | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand - | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda"; - -fun no_repeat_vars thy pat = - let fun check [] = true - | check (v::rst) = - if member (op aconv) rst v then - raise TFL_ERR "no_repeat_vars" - (quote (#1 (dest_Free v)) ^ - " occurs repeatedly in the pattern " ^ - quote (string_of_cterm (Thry.typecheck thy pat))) - else check rst - in check (FV_multiset pat) - end; - -fun dest_atom (Free p) = p - | dest_atom (Const p) = p - | dest_atom _ = raise TFL_ERR "dest_atom" "function name not an identifier"; - -fun same_name (p,q) = #1(dest_atom p) = #1(dest_atom q); - -local fun mk_functional_err s = raise TFL_ERR "mk_functional" s - fun single [_$_] = - mk_functional_err "recdef does not allow currying" - | single [f] = f - | single fs = - (*multiple function names?*) - if length (distinct same_name fs) < length fs - then mk_functional_err - "The function being declared appears with multiple types" - else mk_functional_err - (Int.toString (length fs) ^ - " distinct function names being declared") -in -fun mk_functional thy clauses = - let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses - handle TERM _ => raise TFL_ERR "mk_functional" - "recursion equations must use the = relation") - val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L) - val atom = single (distinct (op aconv) funcs) - val (fname,ftype) = dest_atom atom - val dummy = map (no_repeat_vars thy) pats - val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats, - map (fn (t,i) => (t,(i,true))) (enumerate R)) - val names = foldr add_term_names [] R - val atype = type_of(hd pats) - and aname = Name.variant names "a" - val a = Free(aname,atype) - val ty_info = Thry.match_info thy - val ty_match = Thry.match_type thy - val range_ty = type_of (hd R) - val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty - {path=[a], rows=rows} - val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts - handle Match => mk_functional_err "error in pattern-match translation" - val patts2 = Library.sort (Library.int_ord o Library.pairself row_of_pat) patts1 - val finals = map row_of_pat patts2 - val originals = map (row_of_pat o #2) rows - val dummy = case (originals\\finals) - of [] => () - | L => mk_functional_err - ("The following clauses are redundant (covered by preceding clauses): " ^ - commas (map (fn i => Int.toString (i + 1)) L)) - in {functional = Abs(Sign.base_name fname, ftype, - abstract_over (atom, - absfree(aname,atype, case_tm))), - pats = patts2} -end end; - - -(*---------------------------------------------------------------------------- - * - * PRINCIPLES OF DEFINITION - * - *---------------------------------------------------------------------------*) - - -(*For Isabelle, the lhs of a definition must be a constant.*) -fun mk_const_def sign (c, Ty, rhs) = - singleton (ProofContext.infer_types (ProofContext.init sign)) - (Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs)); - -(*Make all TVars available for instantiation by adding a ? to the front*) -fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts) - | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort) - | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort); - -local val f_eq_wfrec_R_M = - #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY)))) - val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M - val (fname,_) = dest_Free f - val (wfrec,_) = S.strip_comb rhs -in -fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) = - let val def_name = if x<>fid then - raise TFL_ERR "wfrec_definition0" - ("Expected a definition of " ^ - quote fid ^ " but found one of " ^ - quote x) - else x ^ "_def" - val wfrec_R_M = map_types poly_tvars - (wfrec $ map_types poly_tvars R) - $ functional - val def_term = mk_const_def thy (x, Ty, wfrec_R_M) - val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy - in (thy', def) end; -end; - - - -(*--------------------------------------------------------------------------- - * This structure keeps track of congruence rules that aren't derived - * from a datatype definition. - *---------------------------------------------------------------------------*) -fun extraction_thms thy = - let val {case_rewrites,case_congs} = Thry.extract_info thy - in (case_rewrites, case_congs) - end; - - -(*--------------------------------------------------------------------------- - * Pair patterns with termination conditions. The full list of patterns for - * a definition is merged with the TCs arising from the user-given clauses. - * There can be fewer clauses than the full list, if the user omitted some - * cases. This routine is used to prepare input for mk_induction. - *---------------------------------------------------------------------------*) -fun merge full_pats TCs = -let fun insert (p,TCs) = - let fun insrt ((x as (h,[]))::rst) = - if (p aconv h) then (p,TCs)::rst else x::insrt rst - | insrt (x::rst) = x::insrt rst - | insrt[] = raise TFL_ERR "merge.insert" "pattern not found" - in insrt end - fun pass ([],ptcl_final) = ptcl_final - | pass (ptcs::tcl, ptcl) = pass(tcl, insert ptcs ptcl) -in - pass (TCs, map (fn p => (p,[])) full_pats) -end; - - -fun givens pats = map pat_of (List.filter given pats); - -fun post_definition meta_tflCongs (theory, (def, pats)) = - let val tych = Thry.typecheck theory - val f = #lhs(S.dest_eq(concl def)) - val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def - val pats' = List.filter given pats - val given_pats = map pat_of pats' - val rows = map row_of_pat pats' - val WFR = #ant(S.dest_imp(concl corollary)) - val R = #Rand(S.dest_comb WFR) - val corollary' = R.UNDISCH corollary (* put WF R on assums *) - val corollaries = map (fn pat => R.SPEC (tych pat) corollary') - given_pats - val (case_rewrites,context_congs) = extraction_thms theory - (*case_ss causes minimal simplification: bodies of case expressions are - not simplified. Otherwise large examples (Red-Black trees) are too - slow.*) - val case_ss = Simplifier.theory_context theory - (HOL_basic_ss addcongs - (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) theory addsimps case_rewrites) - val corollaries' = map (Simplifier.simplify case_ss) corollaries - val extract = R.CONTEXT_REWRITE_RULE - (f, [R], cut_apply, meta_tflCongs@context_congs) - val (rules, TCs) = ListPair.unzip (map extract corollaries') - val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules - val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR) - val rules1 = R.LIST_CONJ(map mk_cond_rule rules0) - in - {rules = rules1, - rows = rows, - full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)), - TCs = TCs} - end; - - -(*--------------------------------------------------------------------------- - * Perform the extraction without making the definition. Definition and - * extraction commute for the non-nested case. (Deferred recdefs) - * - * The purpose of wfrec_eqns is merely to instantiate the recursion theorem - * and extract termination conditions: no definition is made. - *---------------------------------------------------------------------------*) - -fun wfrec_eqns thy fid tflCongs eqns = - let val {lhs,rhs} = S.dest_eq (hd eqns) - val (f,args) = S.strip_comb lhs - val (fname,fty) = dest_atom f - val (SV,a) = front_last args (* SV = schematic variables *) - val g = list_comb(f,SV) - val h = Free(fname,type_of g) - val eqns1 = map (subst_free[(g,h)]) eqns - val {functional as Abs(x, Ty, _), pats} = mk_functional thy eqns1 - val given_pats = givens pats - (* val f = Free(x,Ty) *) - val Type("fun", [f_dty, f_rty]) = Ty - val dummy = if x<>fid then - raise TFL_ERR "wfrec_eqns" - ("Expected a definition of " ^ - quote fid ^ " but found one of " ^ - quote x) - else () - val (case_rewrites,context_congs) = extraction_thms thy - val tych = Thry.typecheck thy - val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY - val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0 - val R = Free (Name.variant (foldr add_term_names [] eqns) Rname, - Rtype) - val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0 - val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM) - val dummy = - if !trace then - writeln ("ORIGINAL PROTO_DEF: " ^ - Sign.string_of_term thy proto_def) - else () - val R1 = S.rand WFR - val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM) - val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats - val corollaries' = map (rewrite_rule case_rewrites) corollaries - fun extract X = R.CONTEXT_REWRITE_RULE - (f, R1::SV, cut_apply, tflCongs@context_congs) X - in {proto_def = proto_def, - SV=SV, - WFR=WFR, - pats=pats, - extracta = map extract corollaries'} - end; - - -(*--------------------------------------------------------------------------- - * Define the constant after extracting the termination conditions. The - * wellfounded relation used in the definition is computed by using the - * choice operator on the extracted conditions (plus the condition that - * such a relation must be wellfounded). - *---------------------------------------------------------------------------*) - -fun lazyR_def thy fid tflCongs eqns = - let val {proto_def,WFR,pats,extracta,SV} = - wfrec_eqns thy fid tflCongs eqns - val R1 = S.rand WFR - val f = #lhs(S.dest_eq proto_def) - val (extractants,TCl) = ListPair.unzip extracta - val dummy = if !trace - then (writeln "Extractants = "; - prths extractants; - ()) - else () - val TCs = foldr (gen_union (op aconv)) [] TCl - val full_rqt = WFR::TCs - val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt} - val R'abs = S.rand R' - val proto_def' = subst_free[(R1,R')] proto_def - val dummy = if !trace then writeln ("proto_def' = " ^ - Sign.string_of_term - thy proto_def') - else () - val {lhs,rhs} = S.dest_eq proto_def' - val (c,args) = S.strip_comb lhs - val (name,Ty) = dest_atom c - val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs)) - val ([def0], theory) = - thy - |> PureThy.add_defs_i false - [Thm.no_attributes (fid ^ "_def", defn)] - val def = Thm.freezeT def0; - val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def) - else () - (* val fconst = #lhs(S.dest_eq(concl def)) *) - val tych = Thry.typecheck theory - val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt - (*lcp: a lot of object-logic inference to remove*) - val baz = R.DISCH_ALL - (fold_rev R.DISCH full_rqt_prop - (R.LIST_CONJ extractants)) - val dum = if !trace then writeln ("baz = " ^ string_of_thm baz) - else () - val f_free = Free (fid, fastype_of f) (*'cos f is a Const*) - val SV' = map tych SV; - val SVrefls = map reflexive SV' - val def0 = (fold (fn x => fn th => R.rbeta(combination th x)) - SVrefls def) - RS meta_eq_to_obj_eq - val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0 - val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop) - val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon - theory Hilbert_Choice*) - thm "Hilbert_Choice.tfl_some" - handle ERROR msg => cat_error msg - "defer_recdef requires theory Main or at least Hilbert_Choice as parent" - val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th - in {theory = theory, R=R1, SV=SV, - rules = fold (U.C R.MP) (R.CONJUNCTS bar) def', - full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)), - patterns = pats} - end; - - - -(*---------------------------------------------------------------------------- - * - * INDUCTION THEOREM - * - *---------------------------------------------------------------------------*) - - -(*------------------------ Miscellaneous function -------------------------- - * - * [x_1,...,x_n] ?v_1...v_n. M[v_1,...,v_n] - * ----------------------------------------------------------- - * ( M[x_1,...,x_n], [(x_i,?v_1...v_n. M[v_1,...,v_n]), - * ... - * (x_j,?v_n. M[x_1,...,x_(n-1),v_n])] ) - * - * This function is totally ad hoc. Used in the production of the induction - * theorem. The nchotomy theorem can have clauses that look like - * - * ?v1..vn. z = C vn..v1 - * - * in which the order of quantification is not the order of occurrence of the - * quantified variables as arguments to C. Since we have no control over this - * aspect of the nchotomy theorem, we make the correspondence explicit by - * pairing the incoming new variable with the term it gets beta-reduced into. - *---------------------------------------------------------------------------*) - -fun alpha_ex_unroll (xlist, tm) = - let val (qvars,body) = S.strip_exists tm - val vlist = #2(S.strip_comb (S.rhs body)) - val plist = ListPair.zip (vlist, xlist) - val args = map (the o AList.lookup (op aconv) plist) qvars - handle Option => sys_error - "TFL fault [alpha_ex_unroll]: no correspondence" - fun build ex [] = [] - | build (_$rex) (v::rst) = - let val ex1 = Term.betapply(rex, v) - in ex1 :: build ex1 rst - end - val (nex::exl) = rev (tm::build tm args) - in - (nex, ListPair.zip (args, rev exl)) - end; - - - -(*---------------------------------------------------------------------------- - * - * PROVING COMPLETENESS OF PATTERNS - * - *---------------------------------------------------------------------------*) - -fun mk_case ty_info usednames thy = - let - val divide = ipartition (gvvariant usednames) - val tych = Thry.typecheck thy - fun tych_binding(x,y) = (tych x, tych y) - fun fail s = raise TFL_ERR "mk_case" s - fun mk{rows=[],...} = fail"no rows" - | mk{path=[], rows = [([], (thm, bindings))]} = - R.IT_EXISTS (map tych_binding bindings) thm - | mk{path = u::rstp, rows as (p::_, _)::_} = - let val (pat_rectangle,rights) = ListPair.unzip rows - val col0 = map hd pat_rectangle - val pat_rectangle' = map tl pat_rectangle - in - if (forall is_Free col0) (* column 0 is all variables *) - then let val rights' = map (fn ((thm,theta),v) => (thm,theta@[(u,v)])) - (ListPair.zip (rights, col0)) - in mk{path = rstp, rows = ListPair.zip (pat_rectangle', rights')} - end - else (* column 0 is all constructors *) - let val Type (ty_name,_) = type_of p - in - case (ty_info ty_name) - of NONE => fail("Not a known datatype: "^ty_name) - | SOME{constructors,nchotomy} => - let val thm' = R.ISPEC (tych u) nchotomy - val disjuncts = S.strip_disj (concl thm') - val subproblems = divide(constructors, rows) - val groups = map #group subproblems - and new_formals = map #new_formals subproblems - val existentials = ListPair.map alpha_ex_unroll - (new_formals, disjuncts) - val constraints = map #1 existentials - val vexl = map #2 existentials - fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b)) - val news = map (fn (nf,rows,c) => {path = nf@rstp, - rows = map (expnd c) rows}) - (U.zip3 new_formals groups constraints) - val recursive_thms = map mk news - val build_exists = Library.foldr - (fn((x,t), th) => - R.CHOOSE (tych x, R.ASSUME (tych t)) th) - val thms' = ListPair.map build_exists (vexl, recursive_thms) - val same_concls = R.EVEN_ORS thms' - in R.DISJ_CASESL thm' same_concls - end - end end - in mk - end; - - -fun complete_cases thy = - let val tych = Thry.typecheck thy - val ty_info = Thry.induct_info thy - in fn pats => - let val names = foldr add_term_names [] pats - val T = type_of (hd pats) - val aname = Name.variant names "a" - val vname = Name.variant (aname::names) "v" - val a = Free (aname, T) - val v = Free (vname, T) - val a_eq_v = HOLogic.mk_eq(a,v) - val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a) - (R.REFL (tych a)) - val th0 = R.ASSUME (tych a_eq_v) - val rows = map (fn x => ([x], (th0,[]))) pats - in - R.GEN (tych a) - (R.RIGHT_ASSOC - (R.CHOOSE(tych v, ex_th0) - (mk_case ty_info (vname::aname::names) - thy {path=[v], rows=rows}))) - end end; - - -(*--------------------------------------------------------------------------- - * Constructing induction hypotheses: one for each recursive call. - * - * Note. R will never occur as a variable in the ind_clause, because - * to do so, it would have to be from a nested definition, and we don't - * allow nested defns to have R variable. - * - * Note. When the context is empty, there can be no local variables. - *---------------------------------------------------------------------------*) -(* -local infix 5 ==> - fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} -in -fun build_ih f P (pat,TCs) = - let val globals = S.free_vars_lr pat - fun nested tm = isSome (S.find_term (curry (op aconv) f) tm) - fun dest_TC tm = - let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) - val (R,y,_) = S.dest_relation R_y_pat - val P_y = if (nested tm) then R_y_pat ==> P$y else P$y - in case cntxt - of [] => (P_y, (tm,[])) - | _ => let - val imp = S.list_mk_conj cntxt ==> P_y - val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals) - val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs - in (S.list_mk_forall(locals,imp), (tm,locals)) end - end - in case TCs - of [] => (S.list_mk_forall(globals, P$pat), []) - | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs) - val ind_clause = S.list_mk_conj ihs ==> P$pat - in (S.list_mk_forall(globals,ind_clause), TCs_locals) - end - end -end; -*) - -local infix 5 ==> - fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2} -in -fun build_ih f (P,SV) (pat,TCs) = - let val pat_vars = S.free_vars_lr pat - val globals = pat_vars@SV - fun nested tm = isSome (S.find_term (curry (op aconv) f) tm) - fun dest_TC tm = - let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm)) - val (R,y,_) = S.dest_relation R_y_pat - val P_y = if (nested tm) then R_y_pat ==> P$y else P$y - in case cntxt - of [] => (P_y, (tm,[])) - | _ => let - val imp = S.list_mk_conj cntxt ==> P_y - val lvs = subtract (op aconv) globals (S.free_vars_lr imp) - val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs - in (S.list_mk_forall(locals,imp), (tm,locals)) end - end - in case TCs - of [] => (S.list_mk_forall(pat_vars, P$pat), []) - | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs) - val ind_clause = S.list_mk_conj ihs ==> P$pat - in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals) - end - end -end; - -(*--------------------------------------------------------------------------- - * This function makes good on the promise made in "build_ih". - * - * Input is tm = "(!y. R y pat ==> P y) ==> P pat", - * TCs = TC_1[pat] ... TC_n[pat] - * thm = ih1 /\ ... /\ ih_n |- ih[pat] - *---------------------------------------------------------------------------*) -fun prove_case f thy (tm,TCs_locals,thm) = - let val tych = Thry.typecheck thy - val antc = tych(#ant(S.dest_imp tm)) - val thm' = R.SPEC_ALL thm - fun nested tm = isSome (S.find_term (curry (op aconv) f) tm) - fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC))))) - fun mk_ih ((TC,locals),th2,nested) = - R.GENL (map tych locals) - (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2 - else if S.is_imp (concl TC) then R.IMP_TRANS TC th2 - else R.MP th2 TC) - in - R.DISCH antc - (if S.is_imp(concl thm') (* recursive calls in this clause *) - then let val th1 = R.ASSUME antc - val TCs = map #1 TCs_locals - val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o - #2 o S.strip_forall) TCs - val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs)) - TCs_locals - val th2list = map (U.C R.SPEC th1 o tych) ylist - val nlist = map nested TCs - val triples = U.zip3 TClist th2list nlist - val Pylist = map mk_ih triples - in R.MP thm' (R.LIST_CONJ Pylist) end - else thm') - end; - - -(*--------------------------------------------------------------------------- - * - * x = (v1,...,vn) |- M[x] - * --------------------------------------------- - * ?v1 ... vn. x = (v1,...,vn) |- M[x] - * - *---------------------------------------------------------------------------*) -fun LEFT_ABS_VSTRUCT tych thm = - let fun CHOOSER v (tm,thm) = - let val ex_tm = S.mk_exists{Bvar=v,Body=tm} - in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm) - end - val [veq] = List.filter (can S.dest_eq) (#1 (R.dest_thm thm)) - val {lhs,rhs} = S.dest_eq veq - val L = S.free_vars_lr rhs - in #2 (fold_rev CHOOSER L (veq,thm)) end; - - -(*---------------------------------------------------------------------------- - * Input : f, R, and [(pat1,TCs1),..., (patn,TCsn)] - * - * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove - * recursion induction (Rinduct) by proving the antecedent of Sinduct from - * the antecedent of Rinduct. - *---------------------------------------------------------------------------*) -fun mk_induction thy {fconst, R, SV, pat_TCs_list} = -let val tych = Thry.typecheck thy - val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM) - val (pats,TCsl) = ListPair.unzip pat_TCs_list - val case_thm = complete_cases thy pats - val domain = (type_of o hd) pats - val Pname = Name.variant (foldr (Library.foldr add_term_names) - [] (pats::TCsl)) "P" - val P = Free(Pname, domain --> HOLogic.boolT) - val Sinduct = R.SPEC (tych P) Sinduction - val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct) - val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list - val (Rassums,TCl') = ListPair.unzip Rassums_TCl' - val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums)) - val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats - val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum) - val proved_cases = map (prove_case fconst thy) tasks - val v = Free (Name.variant (foldr add_term_names [] (map concl proved_cases)) - "v", - domain) - val vtyped = tych v - val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats - val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th') - (substs, proved_cases) - val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1 - val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases) - val dc = R.MP Sinduct dant - val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc))) - val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty) - val dc' = fold_rev (R.GEN o tych) vars - (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc) -in - R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc') -end -handle U.ERR _ => raise TFL_ERR "mk_induction" "failed derivation"; - - - - -(*--------------------------------------------------------------------------- - * - * POST PROCESSING - * - *---------------------------------------------------------------------------*) - - -fun simplify_induction thy hth ind = - let val tych = Thry.typecheck thy - val (asl,_) = R.dest_thm ind - val (_,tc_eq_tc') = R.dest_thm hth - val tc = S.lhs tc_eq_tc' - fun loop [] = ind - | loop (asm::rst) = - if (can (Thry.match_term thy asm) tc) - then R.UNDISCH - (R.MATCH_MP - (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind)) - hth) - else loop rst - in loop asl -end; - - -(*--------------------------------------------------------------------------- - * The termination condition is an antecedent to the rule, and an - * assumption to the theorem. - *---------------------------------------------------------------------------*) -fun elim_tc tcthm (rule,induction) = - (R.MP rule tcthm, R.PROVE_HYP tcthm induction) - - -fun trace_thms s L = - if !trace then writeln (cat_lines (s :: map string_of_thm L)) - else (); - -fun trace_cterms s L = - if !trace then writeln (cat_lines (s :: map string_of_cterm L)) - else ();; - - -fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} = -let val tych = Thry.typecheck theory - val prove = R.prove strict; - - (*--------------------------------------------------------------------- - * Attempt to eliminate WF condition. It's the only assumption of rules - *---------------------------------------------------------------------*) - val (rules1,induction1) = - let val thm = prove(tych(HOLogic.mk_Trueprop - (hd(#1(R.dest_thm rules)))), - wf_tac) - in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction) - end handle U.ERR _ => (rules,induction); - - (*---------------------------------------------------------------------- - * The termination condition (tc) is simplified to |- tc = tc' (there - * might not be a change!) and then 3 attempts are made: - * - * 1. if |- tc = T, then eliminate it with eqT; otherwise, - * 2. apply the terminator to tc'. If |- tc' = T then eliminate; else - * 3. replace tc by tc' in both the rules and the induction theorem. - *---------------------------------------------------------------------*) - - fun simplify_tc tc (r,ind) = - let val tc1 = tych tc - val _ = trace_cterms "TC before simplification: " [tc1] - val tc_eq = simplifier tc1 - val _ = trace_thms "result: " [tc_eq] - in - elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind) - handle U.ERR _ => - (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) - (prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))), - terminator))) - (r,ind) - handle U.ERR _ => - (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq), - simplify_induction theory tc_eq ind)) - end - - (*---------------------------------------------------------------------- - * Nested termination conditions are harder to get at, since they are - * left embedded in the body of the function (and in induction - * theorem hypotheses). Our "solution" is to simplify them, and try to - * prove termination, but leave the application of the resulting theorem - * to a higher level. So things go much as in "simplify_tc": the - * termination condition (tc) is simplified to |- tc = tc' (there might - * not be a change) and then 2 attempts are made: - * - * 1. if |- tc = T, then return |- tc; otherwise, - * 2. apply the terminator to tc'. If |- tc' = T then return |- tc; else - * 3. return |- tc = tc' - *---------------------------------------------------------------------*) - fun simplify_nested_tc tc = - let val tc_eq = simplifier (tych (#2 (S.strip_forall tc))) - in - R.GEN_ALL - (R.MATCH_MP Thms.eqT tc_eq - handle U.ERR _ => - (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) - (prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))), - terminator)) - handle U.ERR _ => tc_eq)) - end - - (*------------------------------------------------------------------- - * Attempt to simplify the termination conditions in each rule and - * in the induction theorem. - *-------------------------------------------------------------------*) - fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm - fun loop ([],extras,R,ind) = (rev R, ind, extras) - | loop ((r,ftcs)::rst, nthms, R, ind) = - let val tcs = #1(strip_imp (concl r)) - val extra_tcs = subtract (op aconv) tcs ftcs - val extra_tc_thms = map simplify_nested_tc extra_tcs - val (r1,ind1) = fold simplify_tc tcs (r,ind) - val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1 - in loop(rst, nthms@extra_tc_thms, r2::R, ind1) - end - val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs) - val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1) -in - {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras} -end; - - -end; diff -r 073a65f0bc40 -r ed3f6685ff90 TFL/thms.ML --- a/TFL/thms.ML Thu May 31 13:18:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -(* Title: TFL/thms.ML - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge -*) - -structure Thms = -struct - val WFREC_COROLLARY = thm "tfl_wfrec"; - val WF_INDUCTION_THM = thm "tfl_wf_induct"; - val CUT_DEF = thm "cut_def"; - val eqT = thm "tfl_eq_True"; - val rev_eq_mp = thm "tfl_rev_eq_mp"; - val simp_thm = thm "tfl_simp_thm"; - val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True"; - val imp_trans = thm "tfl_imp_trans"; - val disj_assoc = thm "tfl_disj_assoc"; - val tfl_disjE = thm "tfl_disjE"; - val choose_thm = thm "tfl_exE"; -end; diff -r 073a65f0bc40 -r ed3f6685ff90 TFL/thry.ML --- a/TFL/thry.ML Thu May 31 13:18:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,82 +0,0 @@ -(* Title: TFL/thry.ML - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge -*) - -signature THRY = -sig - val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list - val match_type: theory -> typ -> typ -> (typ * typ) list - val typecheck: theory -> term -> cterm - (*datatype facts of various flavours*) - val match_info: theory -> string -> {constructors: term list, case_const: term} option - val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option - val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list} -end; - -structure Thry: THRY = -struct - - -fun THRY_ERR func mesg = Utils.ERR {module = "Thry", func = func, mesg = mesg}; - - -(*--------------------------------------------------------------------------- - * Matching - *---------------------------------------------------------------------------*) - -local - -fun tybind (ixn, (S, T)) = (TVar (ixn, S), T); - -in - -fun match_term thry pat ob = - let - val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) (Vartab.empty, Vartab.empty); - fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t) - in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta)) - end; - -fun match_type thry pat ob = - map tybind (Vartab.dest (Sign.typ_match thry (pat, ob) Vartab.empty)); - -end; - - -(*--------------------------------------------------------------------------- - * Typing - *---------------------------------------------------------------------------*) - -fun typecheck thry t = - Thm.cterm_of thry t - handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg - | TERM (msg, _) => raise THRY_ERR "typecheck" msg; - - -(*--------------------------------------------------------------------------- - * Get information about datatypes - *---------------------------------------------------------------------------*) - -fun match_info thy dtco = - case (DatatypePackage.get_datatype thy dtco, - DatatypePackage.get_datatype_constrs thy dtco) of - (SOME { case_name, ... }, SOME constructors) => - SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors} - | _ => NONE; - -fun induct_info thy dtco = case DatatypePackage.get_datatype thy dtco of - NONE => NONE - | SOME {nchotomy, ...} => - SOME {nchotomy = nchotomy, - constructors = (map Const o the o DatatypePackage.get_datatype_constrs thy) dtco}; - -fun extract_info thy = - let val infos = (map snd o Symtab.dest o DatatypePackage.get_datatypes) thy - in {case_congs = map (mk_meta_eq o #case_cong) infos, - case_rewrites = List.concat (map (map mk_meta_eq o #case_rewrites) infos)} - end; - - -end; diff -r 073a65f0bc40 -r ed3f6685ff90 TFL/usyntax.ML --- a/TFL/usyntax.ML Thu May 31 13:18:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,409 +0,0 @@ -(* Title: TFL/usyntax.ML - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Emulation of HOL's abstract syntax functions. -*) - -signature USYNTAX = -sig - datatype lambda = VAR of {Name : string, Ty : typ} - | CONST of {Name : string, Ty : typ} - | COMB of {Rator: term, Rand : term} - | LAMB of {Bvar : term, Body : term} - - val alpha : typ - - (* Types *) - val type_vars : typ -> typ list - val type_varsl : typ list -> typ list - val mk_vartype : string -> typ - val is_vartype : typ -> bool - val strip_prod_type : typ -> typ list - - (* Terms *) - val free_vars_lr : term -> term list - val type_vars_in_term : term -> typ list - val dest_term : term -> lambda - - (* Prelogic *) - val inst : (typ*typ) list -> term -> term - - (* Construction routines *) - val mk_abs :{Bvar : term, Body : term} -> term - - val mk_imp :{ant : term, conseq : term} -> term - val mk_select :{Bvar : term, Body : term} -> term - val mk_forall :{Bvar : term, Body : term} -> term - val mk_exists :{Bvar : term, Body : term} -> term - val mk_conj :{conj1 : term, conj2 : term} -> term - val mk_disj :{disj1 : term, disj2 : term} -> term - val mk_pabs :{varstruct : term, body : term} -> term - - (* Destruction routines *) - val dest_const: term -> {Name : string, Ty : typ} - val dest_comb : term -> {Rator : term, Rand : term} - val dest_abs : string list -> term -> {Bvar : term, Body : term} * string list - val dest_eq : term -> {lhs : term, rhs : term} - val dest_imp : term -> {ant : term, conseq : term} - val dest_forall : term -> {Bvar : term, Body : term} - val dest_exists : term -> {Bvar : term, Body : term} - val dest_neg : term -> term - val dest_conj : term -> {conj1 : term, conj2 : term} - val dest_disj : term -> {disj1 : term, disj2 : term} - val dest_pair : term -> {fst : term, snd : term} - val dest_pabs : string list -> term -> {varstruct : term, body : term, used : string list} - - val lhs : term -> term - val rhs : term -> term - val rand : term -> term - - (* Query routines *) - val is_imp : term -> bool - val is_forall : term -> bool - val is_exists : term -> bool - val is_neg : term -> bool - val is_conj : term -> bool - val is_disj : term -> bool - val is_pair : term -> bool - val is_pabs : term -> bool - - (* Construction of a term from a list of Preterms *) - val list_mk_abs : (term list * term) -> term - val list_mk_imp : (term list * term) -> term - val list_mk_forall : (term list * term) -> term - val list_mk_conj : term list -> term - - (* Destructing a term to a list of Preterms *) - val strip_comb : term -> (term * term list) - val strip_abs : term -> (term list * term) - val strip_imp : term -> (term list * term) - val strip_forall : term -> (term list * term) - val strip_exists : term -> (term list * term) - val strip_disj : term -> term list - - (* Miscellaneous *) - val mk_vstruct : typ -> term list -> term - val gen_all : term -> term - val find_term : (term -> bool) -> term -> term option - val dest_relation : term -> term * term * term - val is_WFR : term -> bool - val ARB : typ -> term -end; - -structure USyntax: USYNTAX = -struct - -infix 4 ##; - -fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg}; - - -(*--------------------------------------------------------------------------- - * - * Types - * - *---------------------------------------------------------------------------*) -val mk_prim_vartype = TVar; -fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS); - -(* But internally, it's useful *) -fun dest_vtype (TVar x) = x - | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable"; - -val is_vartype = can dest_vtype; - -val type_vars = map mk_prim_vartype o typ_tvars -fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []); - -val alpha = mk_vartype "'a" -val beta = mk_vartype "'b" - -val strip_prod_type = HOLogic.prodT_factors; - - - -(*--------------------------------------------------------------------------- - * - * Terms - * - *---------------------------------------------------------------------------*) - -(* Free variables, in order of occurrence, from left to right in the - * syntax tree. *) -fun free_vars_lr tm = - let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end - fun add (t, frees) = case t of - Free _ => if (memb t frees) then frees else t::frees - | Abs (_,_,body) => add(body,frees) - | f$t => add(t, add(f, frees)) - | _ => frees - in rev(add(tm,[])) - end; - - - -val type_vars_in_term = map mk_prim_vartype o term_tvars; - - - -(* Prelogic *) -fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty) -fun inst theta = subst_vars (map dest_tybinding theta,[]) - - -(* Construction routines *) - -fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) - | mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) - | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable"; - - -fun mk_imp{ant,conseq} = - let val c = Const("op -->",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) - in list_comb(c,[ant,conseq]) - end; - -fun mk_select (r as {Bvar,Body}) = - let val ty = type_of Bvar - val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty) - in list_comb(c,[mk_abs r]) - end; - -fun mk_forall (r as {Bvar,Body}) = - let val ty = type_of Bvar - val c = Const("All",(ty --> HOLogic.boolT) --> HOLogic.boolT) - in list_comb(c,[mk_abs r]) - end; - -fun mk_exists (r as {Bvar,Body}) = - let val ty = type_of Bvar - val c = Const("Ex",(ty --> HOLogic.boolT) --> HOLogic.boolT) - in list_comb(c,[mk_abs r]) - end; - - -fun mk_conj{conj1,conj2} = - let val c = Const("op &",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) - in list_comb(c,[conj1,conj2]) - end; - -fun mk_disj{disj1,disj2} = - let val c = Const("op |",HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT) - in list_comb(c,[disj1,disj2]) - end; - -fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2); - -local -fun mk_uncurry(xt,yt,zt) = - Const("split",(xt --> yt --> zt) --> prod_ty xt yt --> zt) -fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} - | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair" -fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false -in -fun mk_pabs{varstruct,body} = - let fun mpa (varstruct, body) = - if is_var varstruct - then mk_abs {Bvar = varstruct, Body = body} - else let val {fst, snd} = dest_pair varstruct - in mk_uncurry (type_of fst, type_of snd, type_of body) $ - mpa (fst, mpa (snd, body)) - end - in mpa (varstruct, body) end - handle TYPE _ => raise USYN_ERR "mk_pabs" ""; -end; - -(* Destruction routines *) - -datatype lambda = VAR of {Name : string, Ty : typ} - | CONST of {Name : string, Ty : typ} - | COMB of {Rator: term, Rand : term} - | LAMB of {Bvar : term, Body : term}; - - -fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty} - | dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} - | dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} - | dest_term(M$N) = COMB{Rator=M,Rand=N} - | dest_term(Abs(s,ty,M)) = let val v = Free(s,ty) - in LAMB{Bvar = v, Body = Term.betapply (M,v)} - end - | dest_term(Bound _) = raise USYN_ERR "dest_term" "Bound"; - -fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} - | dest_const _ = raise USYN_ERR "dest_const" "not a constant"; - -fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} - | dest_comb _ = raise USYN_ERR "dest_comb" "not a comb"; - -fun dest_abs used (a as Abs(s, ty, M)) = - let - val s' = Name.variant used s; - val v = Free(s', ty); - in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used) - end - | dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction"; - -fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N} - | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality"; - -fun dest_imp(Const("op -->",_) $ M $ N) = {ant=M, conseq=N} - | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication"; - -fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a) - | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall"; - -fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a) - | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential"; - -fun dest_neg(Const("not",_) $ M) = M - | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation"; - -fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N} - | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction"; - -fun dest_disj(Const("op |",_) $ M $ N) = {disj1=M, disj2=N} - | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction"; - -fun mk_pair{fst,snd} = - let val ty1 = type_of fst - val ty2 = type_of snd - val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2) - in list_comb(c,[fst,snd]) - end; - -fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} - | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"; - - -local fun ucheck t = (if #Name(dest_const t) = "split" then t - else raise Match) -in -fun dest_pabs used tm = - let val ({Bvar,Body}, used') = dest_abs used tm - in {varstruct = Bvar, body = Body, used = used'} - end handle Utils.ERR _ => - let val {Rator,Rand} = dest_comb tm - val _ = ucheck Rator - val {varstruct = lv, body, used = used'} = dest_pabs used Rand - val {varstruct = rv, body, used = used''} = dest_pabs used' body - in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''} - end -end; - - -val lhs = #lhs o dest_eq -val rhs = #rhs o dest_eq -val rand = #Rand o dest_comb - - -(* Query routines *) -val is_imp = can dest_imp -val is_forall = can dest_forall -val is_exists = can dest_exists -val is_neg = can dest_neg -val is_conj = can dest_conj -val is_disj = can dest_disj -val is_pair = can dest_pair -val is_pabs = can (dest_pabs []) - - -(* Construction of a cterm from a list of Terms *) - -fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm; - -(* These others are almost never used *) -fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c; -fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t; -val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm}) - - -(* Need to reverse? *) -fun gen_all tm = list_mk_forall(term_frees tm, tm); - -(* Destructing a cterm to a list of Terms *) -fun strip_comb tm = - let fun dest(M$N, A) = dest(M, N::A) - | dest x = x - in dest(tm,[]) - end; - -fun strip_abs(tm as Abs _) = - let val ({Bvar,Body}, _) = dest_abs [] tm - val (bvs, core) = strip_abs Body - in (Bvar::bvs, core) - end - | strip_abs M = ([],M); - - -fun strip_imp fm = - if (is_imp fm) - then let val {ant,conseq} = dest_imp fm - val (was,wb) = strip_imp conseq - in ((ant::was), wb) - end - else ([],fm); - -fun strip_forall fm = - if (is_forall fm) - then let val {Bvar,Body} = dest_forall fm - val (bvs,core) = strip_forall Body - in ((Bvar::bvs), core) - end - else ([],fm); - - -fun strip_exists fm = - if (is_exists fm) - then let val {Bvar, Body} = dest_exists fm - val (bvs,core) = strip_exists Body - in (Bvar::bvs, core) - end - else ([],fm); - -fun strip_disj w = - if (is_disj w) - then let val {disj1,disj2} = dest_disj w - in (strip_disj disj1@strip_disj disj2) - end - else [w]; - - -(* Miscellaneous *) - -fun mk_vstruct ty V = - let fun follow_prod_type (Type("*",[ty1,ty2])) vs = - let val (ltm,vs1) = follow_prod_type ty1 vs - val (rtm,vs2) = follow_prod_type ty2 vs1 - in (mk_pair{fst=ltm, snd=rtm}, vs2) end - | follow_prod_type _ (v::vs) = (v,vs) - in #1 (follow_prod_type ty V) end; - - -(* Search a term for a sub-term satisfying the predicate p. *) -fun find_term p = - let fun find tm = - if (p tm) then SOME tm - else case tm of - Abs(_,_,body) => find body - | (t$u) => (case find t of NONE => find u | some => some) - | _ => NONE - in find - end; - -fun dest_relation tm = - if (type_of tm = HOLogic.boolT) - then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm - in (R,y,x) - end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure" - else raise USYN_ERR "dest_relation" "not a boolean term"; - -fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true - | is_WFR _ = false; - -fun ARB ty = mk_select{Bvar=Free("v",ty), - Body=Const("True",HOLogic.boolT)}; - -end; diff -r 073a65f0bc40 -r ed3f6685ff90 TFL/utils.ML --- a/TFL/utils.ML Thu May 31 13:18:52 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ -(* Title: TFL/utils.ML - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Basic utilities. -*) - -signature UTILS = -sig - exception ERR of {module: string, func: string, mesg: string} - val C: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c - val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a - val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c - val pluck: ('a -> bool) -> 'a list -> 'a * 'a list - val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list - val take: ('a -> 'b) -> int * 'a list -> 'b list -end; - -structure Utils: UTILS = -struct - -(*standard exception for TFL*) -exception ERR of {module: string, func: string, mesg: string}; - -fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg}; - - -fun C f x y = f y x - -fun end_itlist f [] = raise (UTILS_ERR "end_itlist" "list too short") - | end_itlist f [x] = x - | end_itlist f (x :: xs) = f x (end_itlist f xs); - -fun itlist2 f L1 L2 base_value = - let fun it ([],[]) = base_value - | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2)) - | it _ = raise UTILS_ERR "itlist2" "different length lists" - in it (L1,L2) - end; - -fun pluck p = - let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found" - | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A) - in fn L => remv(L,[]) - end; - -fun take f = - let fun grab(0,L) = [] - | grab(n, x::rst) = f x::grab(n-1,rst) - in grab - end; - -fun zip3 [][][] = [] - | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3 - | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths"; - - -end;