# HG changeset patch # User krauss # Date 1184613763 -7200 # Node ID 2040846d1bbef34c6cb7b197a6a005c6407ae872 # Parent cfe8d4bf749a32fa9e3b7a3942617bad52649d73 some interface cleanup diff -r cfe8d4bf749a -r 2040846d1bbe src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Mon Jul 16 21:17:12 2007 +0200 +++ b/src/HOL/Tools/function_package/context_tree.ML Mon Jul 16 21:22:43 2007 +0200 @@ -9,19 +9,19 @@ signature FUNDEF_CTXTREE = sig + type depgraph type ctx_tree (* FIXME: This interface is a mess and needs to be cleaned up! *) val cong_deps : thm -> int IntGraph.T val add_congs : thm list - val mk_tree: (thm * FundefCommon.depgraph) list -> - (string * typ) -> term -> Proof.context -> term -> FundefCommon.ctx_tree + val mk_tree: (thm * depgraph) list -> + (string * typ) -> term -> Proof.context -> term -> ctx_tree - val inst_tree: theory -> term -> term -> FundefCommon.ctx_tree - -> FundefCommon.ctx_tree + val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree - val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list + val add_context_varnames : ctx_tree -> string list -> string list val export_term : (string * typ) list * term list -> term -> term val export_thm : theory -> (string * typ) list * term list -> thm -> thm @@ -33,9 +33,9 @@ (((string * typ) list * thm list) * thm) list -> (((string * typ) list * thm list) * thm) list * 'b -> (((string * typ) list * thm list) * thm) list * 'b) - -> FundefCommon.ctx_tree -> 'b -> 'b + -> ctx_tree -> 'b -> 'b - val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list + val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> ctx_tree -> thm * (thm * thm) list end structure FundefCtxTree : FUNDEF_CTXTREE = @@ -44,6 +44,13 @@ open FundefCommon open FundefLib +type depgraph = int IntGraph.T + +datatype ctx_tree + = Leaf of term + | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list) + | RCall of (term * ctx_tree) + (* Maps "Trueprop A = B" to "A" *) val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop @@ -160,7 +167,7 @@ fun import_thm thy (fixes, athms) = fold (forall_elim o cterm_of thy o Free) fixes - #> fold implies_elim_swp athms + #> fold (flip implies_elim) athms fun assume_in_ctxt thy (fixes, athms) prop = let diff -r cfe8d4bf749a -r 2040846d1bbe src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jul 16 21:17:12 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Jul 16 21:22:43 2007 +0200 @@ -26,14 +26,6 @@ val rel_name = suffix "_rel" val dom_name = suffix "_dom" -type depgraph = int IntGraph.T - -datatype ctx_tree - = Leaf of term - | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list) - | RCall of (term * ctx_tree) - - datatype fundef_result = FundefResult of @@ -58,6 +50,7 @@ { defname : string, + (* contains no logical entities: invariant under morphisms *) add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory, fs : term list, @@ -73,7 +66,7 @@ val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi val name = Morphism.name phi in - FundefCtxData { add_simps = add_simps (* contains no logical entities *), + FundefCtxData { add_simps = add_simps, fs = map term fs, R = term R, psimps = fact psimps, pinducts = fact pinducts, termination = thm termination, defname = name defname } @@ -154,7 +147,6 @@ FundefData.map (fold (fn f => NetRules.insert (f, data)) fs) #> store_termination_rule termination - (* Configuration management *) datatype fundef_opt = Sequential @@ -186,6 +178,10 @@ fun target_of (FundefConfig {target, ...}) = target +val default_config = FundefConfig { sequential=false, default="%x. arbitrary", + target=NONE, domintros=false, tailrec=false } + + (* Common operations on equations *) fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b) @@ -248,7 +244,7 @@ val _ = null rvs orelse error (input_error ("Variable" ^ plural " " "s " rvs ^ commas_quote rvs ^ " occur" ^ plural "s" "" rvs ^ " on right hand side only:")) - val _ = forall (FundefLib.forall_aterms (fn Free (n, _) => not (n mem fnames) | _ => true)) gs + val _ = forall (not o Term.exists_subterm (fn Free (n, _) => n mem fnames | _ => false)) gs orelse error (input_error "Recursive Calls not allowed in premises") in fqgar @@ -265,14 +261,23 @@ type fixes = ((string * typ) * mixfix) list type 'a spec = ((bstring * Attrib.src list) * 'a list) list -type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec -> (term list * (thm list -> thm spec)) +type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec + -> (term list * (thm list -> thm spec) * (thm list -> thm list list)) + +val fname_of = fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o snd o dest_all_all fun empty_preproc check _ _ ctxt fixes spec = let val (nas,tss) = split_list spec val _ = check ctxt fixes (flat tss) + val ts = flat tss + val fnames = map (fst o fst) fixes + val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) ts + + fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) + |> map (map snd) in - (flat tss, curry op ~~ nas o Library.unflat tss) + (ts, curry op ~~ nas o Library.unflat tss, sort) end structure Preprocessor = GenericDataFun @@ -313,44 +318,11 @@ val flags_statements = statements_ow >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow)) - - fun basic_apply_flags ((config, fixes), (flags, statements)) = ((config, fixes), statements) in fun fundef_parser default_cfg = (config_parser default_cfg -- P.fixes --| P.$$$ "where" -- flags_statements) - end - - - -val default_config = FundefConfig { sequential=false, default="%x. arbitrary", - target=NONE, domintros=false, tailrec=false } - - end end -(* Common Abbreviations *) - -structure FundefAbbrev = -struct - -fun implies_elim_swp x y = implies_elim y x - -(* HOL abbreviations *) -val boolT = HOLogic.boolT -val mk_prod = HOLogic.mk_prod -val mk_eq = HOLogic.mk_eq -val eq_const = HOLogic.eq_const -val Trueprop = HOLogic.mk_Trueprop -val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT - -fun free_to_var (Free (v,T)) = Var ((v,0),T) - | free_to_var _ = raise Match - -fun var_to_free (Var ((v,_),T)) = Free (v,T) - | var_to_free _ = raise Match - - -end diff -r cfe8d4bf749a -r 2040846d1bbe src/HOL/Tools/function_package/fundef_core.ML --- a/src/HOL/Tools/function_package/fundef_core.ML Mon Jul 16 21:17:12 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_core.ML Mon Jul 16 21:22:43 2007 +0200 @@ -24,10 +24,11 @@ structure FundefCore : FUNDEF_CORE = struct +val boolT = HOLogic.boolT +val mk_eq = HOLogic.mk_eq open FundefLib open FundefCommon -open FundefAbbrev datatype globals = Globals of { @@ -85,7 +86,7 @@ qglr : ((string * typ) list * term list * term * term), cdata : clause_context, - tree: ctx_tree, + tree: FundefCtxTree.ctx_tree, lGI: thm, RCs: rec_call_info list } @@ -125,8 +126,8 @@ let val shift = incr_boundvars (length qs') in - (implies $ Trueprop (eq_const domT $ shift lhs $ lhs') - $ Trueprop (eq_const ranT $ shift rhs $ rhs')) + (implies $ HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs') + $ HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs') |> curry abstract_over fvar @@ -140,12 +141,12 @@ fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = let fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = - Trueprop Pbool - |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs))) + HOLogic.mk_Trueprop Pbool + |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs))) |> fold_rev (curry Logic.mk_implies) gs |> fold_rev mk_forall_rename (map fst oqs ~~ qs) in - Trueprop Pbool + HOLogic.mk_Trueprop Pbool |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) |> mk_forall_rename ("x", x) |> mk_forall_rename ("P", Pbool) @@ -168,7 +169,7 @@ val cqs = map (cterm_of thy) qs val ags = map (assume o cterm_of thy) gs - val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) + val case_hyp = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) in ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } @@ -203,18 +204,18 @@ val lGI = GIntro_thm |> forall_elim (cert f) |> fold forall_elim cqs - |> fold implies_elim_swp ags + |> fold (flip implies_elim) ags fun mk_call_info (rcfix, rcassm, rcarg) RI = let val llRI = RI |> fold forall_elim cqs |> fold (forall_elim o cert o Free) rcfix - |> fold implies_elim_swp ags - |> fold implies_elim_swp rcassm + |> fold (flip implies_elim) ags + |> fold (flip implies_elim) rcassm val h_assum = - Trueprop (G $ rcarg $ (h $ rcarg)) + HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |> fold_rev (mk_forall o Free) rcfix |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] @@ -263,16 +264,16 @@ val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj - val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj))) + val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) in if j < i then let val compat = lookup_compat_thm j i cts in compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) - |> fold implies_elim_swp agsj - |> fold implies_elim_swp agsi - |> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) + |> fold (flip implies_elim) agsj + |> fold (flip implies_elim) agsi + |> flip implies_elim ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) end else let @@ -280,9 +281,9 @@ in compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) - |> fold implies_elim_swp agsi - |> fold implies_elim_swp agsj - |> implies_elim_swp (assume lhsi_eq_lhsj) + |> fold (flip implies_elim) agsi + |> fold (flip implies_elim) agsj + |> flip implies_elim (assume lhsi_eq_lhsj) |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) end end @@ -330,11 +331,11 @@ val RLj_import = RLj |> fold forall_elim cqsj' - |> fold implies_elim_swp agsj' - |> fold implies_elim_swp Ghsj' + |> fold (flip implies_elim) agsj' + |> fold (flip implies_elim) Ghsj' - val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h)))) - val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) + val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) + val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) in (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) |> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) @@ -364,7 +365,7 @@ val existence = fold (curry op COMP o prep_RC) RCs lGI val P = cterm_of thy (mk_eq (y, rhsC)) - val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y))) + val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas @@ -372,8 +373,8 @@ |> forall_elim (cterm_of thy lhs) |> forall_elim (cterm_of thy y) |> forall_elim P - |> implies_elim_swp G_lhs_y - |> fold implies_elim_swp unique_clauses + |> flip implies_elim G_lhs_y + |> fold (flip implies_elim) unique_clauses |> implies_intr (cprop_of G_lhs_y) |> forall_intr (cterm_of thy y) @@ -409,8 +410,8 @@ (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (R $ Bound 0 $ x) - $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ + implies $ HOLogic.mk_Trueprop (R $ Bound 0 $ x) + $ HOLogic.mk_Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))) |> cterm_of thy @@ -430,7 +431,7 @@ |> forall_elim_vars 0 |> fold (curry op COMP) ex1s |> implies_intr (ihyp) - |> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x))) + |> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |> forall_intr (cterm_of thy x) |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it) @@ -453,11 +454,11 @@ fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = let fun mk_h_assm (rcfix, rcassm, rcarg) = - Trueprop (Gvar $ rcarg $ (fvar $ rcarg)) + HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg)) |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |> fold_rev (mk_forall o Free) rcfix in - Trueprop (Gvar $ lhs $ rhs) + HOLogic.mk_Trueprop (Gvar $ lhs $ rhs) |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |> fold_rev (curry Logic.mk_implies) gs |> fold_rev mk_forall (fvar :: qs) @@ -494,7 +495,7 @@ val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)])) fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = - Trueprop (Rvar $ rcarg $ lhs) + HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs) |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |> fold_rev (curry Logic.mk_implies) gs |> fold_rev (mk_forall o Free) rcfix @@ -551,8 +552,8 @@ fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = let - val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) - val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *) + val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) + val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) in ((assume z_smaller) RS ((assume lhs_acc) RS acc_downward)) |> (fn it => it COMP graph_is_function) @@ -580,23 +581,23 @@ val Globals {domT, x, z, a, P, D, ...} = globals val acc_R = mk_acc domT R - val x_D = assume (cterm_of thy (Trueprop (D $ x))) - val a_D = cterm_of thy (Trueprop (D $ a)) + val x_D = assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) + val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) - val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x))) + val D_subset = cterm_of thy (mk_forall x (implies $ HOLogic.mk_Trueprop (D $ x) $ HOLogic.mk_Trueprop (acc_R $ x))) val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) mk_forall x - (mk_forall z (Logic.mk_implies (Trueprop (D $ x), - Logic.mk_implies (Trueprop (R $ z $ x), - Trueprop (D $ z))))) + (mk_forall z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), + Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), + HOLogic.mk_Trueprop (D $ z))))) |> cterm_of thy (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (R $ Bound 0 $ x) - $ Trueprop (P $ Bound 0)) + implies $ HOLogic.mk_Trueprop (R $ Bound 0 $ x) + $ HOLogic.mk_Trueprop (P $ Bound 0)) |> cterm_of thy val aihyp = assume ihyp @@ -612,26 +613,26 @@ fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih |> forall_elim (cterm_of thy rcarg) - |> implies_elim_swp llRI + |> flip implies_elim llRI |> fold_rev (implies_intr o cprop_of) CCas |> fold_rev (forall_intr o cterm_of thy o Free) RIvs val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) - val step = Trueprop (P $ lhs) + val step = HOLogic.mk_Trueprop (P $ lhs) |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |> fold_rev (curry Logic.mk_implies) gs - |> curry Logic.mk_implies (Trueprop (D $ lhs)) + |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |> cterm_of thy val P_lhs = assume step |> fold forall_elim cqs - |> implies_elim_swp lhs_D - |> fold implies_elim_swp ags - |> fold implies_elim_swp P_recs + |> flip implies_elim lhs_D + |> fold (flip implies_elim) ags + |> fold (flip implies_elim) P_recs - val res = cterm_of thy (Trueprop (P $ x)) + val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) |> Simplifier.rewrite replace_x_ss |> symmetric (* P lhs == P x *) |> (fn eql => equal_elim eql P_lhs) (* "P x" *) @@ -687,7 +688,7 @@ let val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...}, qglr = (oqs, _, _, _), ...} = clause - val goal = Trueprop (mk_acc domT R $ lhs) + val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |> fold_rev (curry Logic.mk_implies) gs |> cterm_of thy in @@ -719,7 +720,7 @@ let val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub) - val hyp = Trueprop (R' $ arg $ lhs) + val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |> fold_rev (curry Logic.mk_implies o prop_of) used |> FundefCtxTree.export_term (fixes, map prop_of assumes) |> fold_rev (curry Logic.mk_implies o prop_of) ags @@ -728,13 +729,13 @@ val thm = assume hyp |> fold forall_elim cqs - |> fold implies_elim_swp ags + |> fold (flip implies_elim) ags |> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *) - |> fold implies_elim_swp used + |> fold (flip implies_elim) used val acc = thm COMP ih_case - val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg))) + val z_eq_arg = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (z, arg))) val arg_eq_z = (assume z_eq_arg) RS sym @@ -742,8 +743,8 @@ |> implies_intr (cprop_of case_hyp) |> implies_intr z_eq_arg - val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg)))) - val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) + val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg)))) + val x_eq_lhs = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) val ethm = (z_acc OF [z_eq_arg, x_eq_lhs]) |> FundefCtxTree.export_thm thy (fixes, @@ -767,20 +768,20 @@ val R' = Free ("R", fastype_of R) - val Rrel = Free ("R", mk_relT (domT, domT)) - val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel + val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) + val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel - val wfR' = cterm_of thy (Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) + val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const ("Wellfounded_Recursion.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *) (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) val ihyp = all domT $ Abs ("z", domT, - implies $ Trueprop (R' $ Bound 0 $ x) - $ Trueprop (acc_R $ Bound 0)) + implies $ HOLogic.mk_Trueprop (R' $ Bound 0 $ x) + $ HOLogic.mk_Trueprop (acc_R $ Bound 0)) |> cterm_of thy val ihyp_a = assume ihyp |> forall_elim_vars 0 - val R_z_x = cterm_of thy (Trueprop (R $ z $ x)) + val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[]) in @@ -842,14 +843,15 @@ val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *) val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *) + fun simp_default_tac ss = asm_full_simp_tac (ss addsimps [default_thm, Let_def]) in Goal.prove ctxt [] [] trsimp (fn _ => rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 - THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1)) + THEN (SIMPSET' simp_default_tac 1) THEN (etac not_acc_down 1) - THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 1) + THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' simp_default_tac)) 1) |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end in diff -r cfe8d4bf749a -r 2040846d1bbe src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jul 16 21:17:12 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jul 16 21:22:43 2007 +0200 @@ -249,13 +249,21 @@ |> tap (check_defs ctxt fixes) (* Standard checks *) |> tap (map (check_pats ctxt)) (* More checks for sequential mode *) |> curry op ~~ flags' - |> add_catchall fixes (* Completion: still disabled *) + |> add_catchall fixes (* Completion *) |> FundefSplit.split_some_equations ctxt fun restore_spec thms = nas ~~ Library.take (length nas, Library.unflat spliteqs thms) + + val spliteqs' = flat (Library.take (length nas, spliteqs)) + val fnames = map (fst o fst) fixes + val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' + + fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) + |> map (map snd) + in - (flat spliteqs, restore_spec) + (flat spliteqs, restore_spec, sort) end else FundefCommon.empty_preproc check_defs config flags ctxt fixes spec diff -r cfe8d4bf749a -r 2040846d1bbe src/HOL/Tools/function_package/fundef_lib.ML --- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jul 16 21:17:12 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jul 16 21:22:43 2007 +0200 @@ -73,8 +73,6 @@ (ctx, [], t) -fun implies_elim_swp a b = implies_elim b a - fun map3 _ [] [] [] = [] | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs | map3 _ _ _ _ = raise Library.UnequalLengths; diff -r cfe8d4bf749a -r 2040846d1bbe src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Mon Jul 16 21:17:12 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Jul 16 21:22:43 2007 +0200 @@ -44,20 +44,20 @@ fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" -fun add_simps fixes post sort label moreatts simps lthy = +fun add_simps fnames post sort label moreatts simps lthy = let - val fnames = map (fst o fst) fixes + val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts + val spec = post simps + |> map (apfst (apsnd (append atts))) val (saved_spec_simps, lthy) = - fold_map note_theorem (post simps) lthy + fold_map note_theorem spec lthy + val saved_simps = flat (map snd saved_spec_simps) - val simps_by_f = sort saved_simps fun add_for_f fname simps = - note_theorem - ((NameSpace.qualified fname label, Attrib.internal (K Simplifier.simp_add) :: moreatts), - simps) #> snd + note_theorem ((NameSpace.qualified fname label, []), simps) #> snd in (saved_simps, fold2 add_for_f fnames simps_by_f lthy) @@ -68,8 +68,9 @@ val FundefResult {fs, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = cont (Goal.close_result proof) + val fnames = map (fst o fst) fixes val qualify = NameSpace.qualified defname - val addsmps = add_simps fixes post sort_cont + val addsmps = add_simps fnames post sort_cont val (((psimps', pinducts'), (_, [termination'])), lthy) = lthy @@ -107,11 +108,11 @@ fun gen_add_fundef prep fixspec eqnss config flags lthy = let val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy - val (eqs, post) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec + val (eqs, post, sort_cont) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec val defname = mk_defname fixes - val ((goalstate, cont, sort_cont), lthy) = + val ((goalstate, cont), lthy) = FundefMutual.prepare_fundef_mutual config defname fixes eqs lthy val afterqed = fundef_afterqed config fixes post defname cont sort_cont @@ -190,6 +191,7 @@ DatatypeHooks.add case_cong_hook #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy) + (* ad-hoc method to convert elimination-style goals to existential statements *) fun insert_int_goal thy subg st = diff -r cfe8d4bf749a -r 2040846d1bbe src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Mon Jul 16 21:17:12 2007 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Mon Jul 16 21:22:43 2007 +0200 @@ -16,7 +16,6 @@ -> local_theory -> ((thm (* goalstate *) * (thm -> FundefCommon.fundef_result) (* proof continuation *) - * (thm list -> thm list list) (* sorting continuation *) ) * local_theory) end @@ -332,19 +331,6 @@ trsimps=mtrsimps} end -(* puts an object in the "right bucket" *) -fun store_grouped P x [] = [] - | store_grouped P x ((l, xs)::bs) = - if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs) - -fun sort_by_function (Mutual {fqgars, ...}) names xs = - fold_rev (store_grouped (op = o apfst fst)) (* fill *) - (map name_of_fqgar (Library.take (length xs, fqgars)) ~~ xs) (* the name-thm pairs *) - (map (rpair []) names) (* in the empty buckets labeled with names *) - - |> map (snd #> map snd) (* and remove the labels afterwards *) - - fun prepare_fundef_mutual config defname fixes eqss lthy = let val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) @@ -356,9 +342,8 @@ val (mutual', lthy'') = define_projections fixes mutual fsum lthy' val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' - val sort_cont = sort_by_function mutual' (map (fst o fst) fixes) in - ((goalstate, mutual_cont, sort_cont), lthy'') + ((goalstate, mutual_cont), lthy'') end