--- a/src/HOL/Tools/Function/function.ML Wed Nov 13 20:14:24 2024 +0100
+++ b/src/HOL/Tools/Function/function.ML Wed Nov 13 23:11:06 2024 +0100
@@ -75,7 +75,11 @@
val fixes = map (apfst (apfst Binding.name_of)) fixes0
val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0
val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
-
+ val props0 = map snd spec0
+ val vars0 = map Term.strip_all_vars props0
+ val input_eqns =
+ map (fn (ps,prop) => Term.subst_bounds (rev (map Free ps), Term.strip_all_body prop))
+ (vars0 ~~ props0)
val fnames = map (fst o fst) fixes0
val defname = Binding.conglomerate fnames;
@@ -122,7 +126,7 @@
{ add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', totality=NONE,
fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
- pelims=pelims',elims=NONE}
+ pelims=pelims', elims=NONE, input_eqns = input_eqns}
val _ =
Proof_Display.print_consts do_print (Position.thread_data ()) lthy2
@@ -180,7 +184,7 @@
| NONE => error "Not a function"))
val { termination, fs, R, add_simps, case_names, psimps,
- pinducts, defname, fnames, cases, dom, pelims, ...} = info
+ pinducts, defname, fnames, cases, dom, pelims, input_eqns, ...} = info
val domT = domain_type (fastype_of R)
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
fun afterqed [[raw_totality]] lthy1 =
@@ -204,7 +208,7 @@
let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps,
case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
simps=SOME simps, inducts=SOME inducts, termination=termination, totality=SOME totality,
- cases=cases, pelims=pelims, elims=SOME elims}
+ cases=cases, pelims=pelims, elims=SOME elims, input_eqns = input_eqns}
|> transform_function_data (Morphism.binding_morphism "" prep_binding)
in
(info',
--- a/src/HOL/Tools/Function/function_common.ML Wed Nov 13 20:14:24 2024 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Wed Nov 13 23:11:06 2024 +0100
@@ -25,7 +25,8 @@
totality : thm option,
cases : thm list,
pelims: thm list list,
- elims: thm list list option}
+ elims: thm list list option,
+ input_eqns: term list}
val profile : bool Unsynchronized.ref
val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
val mk_acc : typ -> term -> term
@@ -99,10 +100,11 @@
totality : thm option,
cases : thm list,
pelims : thm list list,
- elims : thm list list option}
+ elims : thm list list option,
+ input_eqns: term list}
fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
- simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
+ simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims, input_eqns} : info) =
let
val term = Morphism.term phi
val thm = Morphism.thm phi
@@ -114,7 +116,8 @@
inducts = Option.map fact inducts, termination = thm termination,
totality = Option.map thm totality, defname = Morphism.binding phi defname,
is_partial = is_partial, cases = fact cases,
- pelims = map fact pelims, elims = Option.map (map fact) elims }
+ pelims = map fact pelims, elims = Option.map (map fact) elims,
+ input_eqns = map term input_eqns }
end