--- 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
--- 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
--- 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