# HG changeset patch # User krauss # Date 1149530052 -7200 # Node ID ebc3b67fbd2ca81a0a7a56610aa0bc9c0199f70f # Parent 45897b49fdd2980e3e05211706fac03b18e3d16f HOL/Tools/fundef_package: Cleanup diff -r 45897b49fdd2 -r ebc3b67fbd2c src/HOL/Tools/function_package/fundef_prep.ML --- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 05 19:09:40 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 05 19:54:12 2006 +0200 @@ -9,12 +9,8 @@ signature FUNDEF_PREP = sig - val prepare_fundef_curried : thm list -> term list -> theory - -> FundefCommon.curry_info option * xstring * (FundefCommon.prep_result * theory) - - val prepare_fundef_new : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list - -> FundefCommon.prep_result * theory - + val prepare_fundef : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list + -> FundefCommon.prep_result * theory end @@ -302,25 +298,7 @@ * Defines the function, the graph and the termination relation, synthesizes completeness * and comatibility conditions and returns everything. *) -fun prepare_fundef congs eqs defname thy = - let - val (names, thy) = setup_context (analyze_eqs eqs) defname congs thy - val Names {G, R, glrs, trees, ...} = names - - val {G_intros, vRiss, R_intross, complete, compat} = extract_conditions thy names trees congs - - val (G_intro_thms, (thy, _)) = inductive_def G_intros (thy, G) - val (R_intro_thmss, (thy, _)) = fold_burrow inductive_def R_intross (thy, R) - - val n = length glrs - val clauses = map3 (mk_clause_info thy names) ((1 upto n) ~~ glrs) (G_intro_thms ~~ trees) (map2 (curry op ~~) vRiss R_intro_thmss) - in - (Prep {names = names, complete=complete, compat=compat, clauses = clauses}, - thy) - end - - -fun prepare_fundef_new thy congs defname f glrs used = +fun prepare_fundef thy congs defname f glrs used = let val (names, thy) = setup_context (f, glrs, used) defname congs thy val Names {G, R, glrs, trees, ...} = names @@ -340,49 +318,4 @@ - - - - -fun prepare_fundef_curried congs eqs thy = - let - val lhs1 = hd eqs - |> dest_implies_list |> snd - |> HOLogic.dest_Trueprop - |> HOLogic.dest_eq |> fst - - val (f, args) = strip_comb lhs1 - val Const(fname, fT) = f - val fxname = Sign.extern_const thy fname - in - if (length args < 2) - then (NONE, fxname, (prepare_fundef congs eqs fxname thy)) - else - let - val (caTs, uaTs) = chop (length args) (binder_types fT) - val newtype = foldr1 HOLogic.mk_prodT caTs --> (uaTs ---> body_type fT) - val gxname = fxname ^ "_tupled" - - val thy = Sign.add_consts_i [(gxname, newtype, NoSyn)] thy - val gc = Const (Sign.intern_const thy gxname, newtype) - - val vars = map2 (fn i => fn T => Free ("x"^(string_of_int i), T)) - (1 upto (length caTs)) caTs - - val f_lambda = fold_rev lambda vars (gc $ foldr1 HOLogic.mk_prod vars) - - val def = Logic.mk_equals (fold (curry ((op $) o Library.swap)) vars f, - gc $ foldr1 HOLogic.mk_prod vars) - - val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", def), [])] thy - - val g_to_f_ss = HOL_basic_ss addsimps [symmetric f_def] - val eqs_tupled = map (Pattern.rewrite_term thy [(f, f_lambda)] []) eqs - in - (SOME (Curry {curry_ss = g_to_f_ss, argTs = caTs}), fxname, prepare_fundef congs eqs_tupled fxname thy) - end - end - - - end \ No newline at end of file diff -r 45897b49fdd2 -r ebc3b67fbd2c src/HOL/Tools/function_package/fundef_proof.ML --- a/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 05 19:09:40 2006 +0200 +++ b/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 05 19:54:12 2006 +0200 @@ -12,9 +12,6 @@ val mk_partial_rules : theory -> thm list -> FundefCommon.prep_result -> thm -> thm list -> FundefCommon.fundef_result - - val mk_partial_rules_curried : theory -> thm list -> FundefCommon.curry_info option -> FundefCommon.prep_result - -> thm -> thm list -> FundefCommon.fundef_result end @@ -541,39 +538,6 @@ end -fun curry_induct_rule thy argTs induct = - let - val vnums = (1 upto (length argTs)) - val avars = map2 (fn T => fn i => Var (("a",i), T)) argTs vnums - val atup = foldr1 HOLogic.mk_prod avars - val Q = Var (("P",1),argTs ---> HOLogic.boolT) - val P = tupled_lambda atup (list_comb (Q, avars)) - in - induct |> freezeT - |> instantiate' [] [SOME (cterm_of thy atup), SOME (cterm_of thy P)] - |> zero_var_indexes - |> full_simplify (HOL_basic_ss addsimps [split_apply]) - |> varifyT - end - - - -fun mk_partial_rules_curried thy congs NONE data complete_thm compat_thms = - mk_partial_rules thy congs data complete_thm compat_thms - | mk_partial_rules_curried thy congs (SOME (Curry {curry_ss, argTs})) data complete_thm compat_thms = - let - val FundefResult {f, G, R, compatibility, completeness, psimps, subset_pinduct,simple_pinduct,total_intro,dom_intros} = - mk_partial_rules thy congs data complete_thm compat_thms - val cpsimps = map (simplify curry_ss) psimps - val cpinduct = full_simplify curry_ss simple_pinduct - |> curry_induct_rule thy argTs - val cdom_intros = map (full_simplify curry_ss) dom_intros - val ctotal_intro = full_simplify curry_ss total_intro - in - FundefResult {f=f, G=G, R=R, compatibility=compat_thms, completeness=complete_thm, - psimps=cpsimps, subset_pinduct=subset_pinduct, simple_pinduct=cpinduct, total_intro=ctotal_intro, dom_intros=cdom_intros} - end - end diff -r 45897b49fdd2 -r ebc3b67fbd2c src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Mon Jun 05 19:09:40 2006 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Mon Jun 05 19:54:12 2006 +0200 @@ -129,7 +129,7 @@ val global_glrs = flat qglrss val used = fold (fn (qs, _, _, _) => fold (curry op ins_string o fst o dest_Free) qs) global_glrs [] in - (mutual, name, FundefPrep.prepare_fundef_new thy congs name (Const sum_const) global_glrs used) + (mutual, name, FundefPrep.prepare_fundef thy congs name (Const sum_const) global_glrs used) end