# HG changeset patch # User wenzelm # Date 1180610332 -7200 # Node ID 073a65f0bc408877ee99345c4ecc94ed0894c256 # Parent ddc5800b699f672423d859d15687bf61449467df moved TFL files to canonical place; diff -r ddc5800b699f -r 073a65f0bc40 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu May 31 13:18:42 2007 +0200 +++ b/src/HOL/IsaMakefile Thu May 31 13:18:52 2007 +0200 @@ -81,10 +81,10 @@ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \ $(SRC)/Provers/trancl.ML $(SRC)/Pure/General/int.ML \ - $(SRC)/Pure/General/rat.ML $(SRC)/TFL/casesplit.ML \ - $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \ - $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ - $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML ATP_Linkup.thy \ + $(SRC)/Pure/General/rat.ML Tools/TFL/casesplit.ML \ + Tools/TFL/dcterm.ML Tools/TFL/post.ML Tools/TFL/rules.ML \ + Tools/TFL/tfl.ML Tools/TFL/thms.ML Tools/TFL/thry.ML \ + Tools/TFL/usyntax.ML Tools/TFL/utils.ML ATP_Linkup.thy \ Accessible_Part.thy Code_Generator.thy Datatype.thy Divides.thy \ Equiv_Relations.thy Extraction.thy Finite_Set.thy FixedPoint.thy \ Fun.thy FunDef.thy HOL.thy Hilbert_Choice.thy Inductive.thy \ diff -r ddc5800b699f -r 073a65f0bc40 src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Thu May 31 13:18:42 2007 +0200 +++ b/src/HOL/Recdef.thy Thu May 31 13:18:52 2007 +0200 @@ -8,15 +8,15 @@ theory Recdef imports Wellfounded_Relations FunDef uses - ("../TFL/casesplit.ML") - ("../TFL/utils.ML") - ("../TFL/usyntax.ML") - ("../TFL/dcterm.ML") - ("../TFL/thms.ML") - ("../TFL/rules.ML") - ("../TFL/thry.ML") - ("../TFL/tfl.ML") - ("../TFL/post.ML") + ("Tools/TFL/casesplit.ML") + ("Tools/TFL/utils.ML") + ("Tools/TFL/usyntax.ML") + ("Tools/TFL/dcterm.ML") + ("Tools/TFL/thms.ML") + ("Tools/TFL/rules.ML") + ("Tools/TFL/thry.ML") + ("Tools/TFL/tfl.ML") + ("Tools/TFL/post.ML") ("Tools/recdef_package.ML") begin @@ -44,15 +44,15 @@ lemma tfl_exE: "\x. P x ==> \x. P x --> Q ==> Q" by blast -use "../TFL/casesplit.ML" -use "../TFL/utils.ML" -use "../TFL/usyntax.ML" -use "../TFL/dcterm.ML" -use "../TFL/thms.ML" -use "../TFL/rules.ML" -use "../TFL/thry.ML" -use "../TFL/tfl.ML" -use "../TFL/post.ML" +use "Tools/TFL/casesplit.ML" +use "Tools/TFL/utils.ML" +use "Tools/TFL/usyntax.ML" +use "Tools/TFL/dcterm.ML" +use "Tools/TFL/thms.ML" +use "Tools/TFL/rules.ML" +use "Tools/TFL/thry.ML" +use "Tools/TFL/tfl.ML" +use "Tools/TFL/post.ML" use "Tools/recdef_package.ML" setup RecdefPackage.setup @@ -63,7 +63,7 @@ same_fst_def less_Suc_eq [THEN iffD2] -lemmas [recdef_cong] = +lemmas [recdef_cong] = if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong lemmas [recdef_wf] = diff -r ddc5800b699f -r 073a65f0bc40 src/HOL/Tools/TFL/casesplit.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/TFL/casesplit.ML Thu May 31 13:18:52 2007 +0200 @@ -0,0 +1,331 @@ +(* Title: HOL/Tools/TFL/casesplit.ML + ID: $Id$ + Author: Lucas Dixon, University of Edinburgh + +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 ddc5800b699f -r 073a65f0bc40 src/HOL/Tools/TFL/dcterm.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/TFL/dcterm.ML Thu May 31 13:18:52 2007 +0200 @@ -0,0 +1,200 @@ +(* Title: HOL/Tools/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 ddc5800b699f -r 073a65f0bc40 src/HOL/Tools/TFL/post.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/TFL/post.ML Thu May 31 13:18:52 2007 +0200 @@ -0,0 +1,279 @@ +(* Title: HOL/Tools/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 ddc5800b699f -r 073a65f0bc40 src/HOL/Tools/TFL/rules.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/TFL/rules.ML Thu May 31 13:18:52 2007 +0200 @@ -0,0 +1,825 @@ +(* Title: HOL/Tools/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 ddc5800b699f -r 073a65f0bc40 src/HOL/Tools/TFL/tfl.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/TFL/tfl.ML Thu May 31 13:18:52 2007 +0200 @@ -0,0 +1,1008 @@ +(* Title: HOL/Tools/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 ddc5800b699f -r 073a65f0bc40 src/HOL/Tools/TFL/thms.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/TFL/thms.ML Thu May 31 13:18:52 2007 +0200 @@ -0,0 +1,20 @@ +(* Title: HOL/Tools/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 ddc5800b699f -r 073a65f0bc40 src/HOL/Tools/TFL/thry.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/TFL/thry.ML Thu May 31 13:18:52 2007 +0200 @@ -0,0 +1,82 @@ +(* Title: HOL/Tools/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 ddc5800b699f -r 073a65f0bc40 src/HOL/Tools/TFL/usyntax.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/TFL/usyntax.ML Thu May 31 13:18:52 2007 +0200 @@ -0,0 +1,409 @@ +(* Title: HOL/Tools/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 ddc5800b699f -r 073a65f0bc40 src/HOL/Tools/TFL/utils.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/TFL/utils.ML Thu May 31 13:18:52 2007 +0200 @@ -0,0 +1,59 @@ +(* Title: HOL/Tools/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;