# HG changeset patch
# User nipkow
# Date 1731535858 -3600
# Node ID 29e60ca6ec01809d5ca8c382e357eb41064348dc
# Parent  07c802837a8cf04ee088c4049d8d4679134671c8
added field input_eqns to record the list of equations (the specification)
given to the function command.

diff -r 07c802837a8c -r 29e60ca6ec01 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Nov 08 22:52:29 2024 +0100
+++ b/src/HOL/Tools/Function/function.ML	Wed Nov 13 23:10:58 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',
diff -r 07c802837a8c -r 29e60ca6ec01 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Nov 08 22:52:29 2024 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Wed Nov 13 23:10:58 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