Email Gateway (Aug 22 2022 at 11:08): Email Gateway (Aug 22 2022 at 11:08):From: Lars Hupel <hupel@in.tum.de>
Dear list,
assume I have a bunch of theorems which together look like a function
specification. For example:
size3 (?x3.0 # ?x2.0) = Numeral1 + size3 ?x2.0
size3 [] = 0
I want to derive an induction schema from those, i.e.:
(!!x3 x2. ?P x2 ==> ?P (x3 # x2)) ==> ?P [] ==> ?P ?a0.0
I know about the 'induction_schema' tactic which is able to prove that one
for me, but I need to come up with it in the first place. The way I could
do it is, of course, to define an auxiliary function using the theorems I
have as defining equations and then ask the function package to tell me
the induction schema it came up with. However, that is a lot of machinery.
I'm looking for a simpler solution here.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:08):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Lars,
I do not know of any other way than defining an auxiliary function. From a quick look at
the sources of the function package, I guess that it is not easy to disentangle the
derivation of the inductive predicate from the construction of the function. (You
essentially want the functionality implemented in
function_core.ML/mk_partial_induct_rule.) The reason is that the function package first
proves a partial induction rule and then (after the termination proof) removes the domain
preconditions. Obviously, the partial induction rule is shown by induction on the domain
predicate. But if you don't do the construction, then there is also no domain predicate.
Cheers,
Andreas
Email Gateway (Aug 22 2022 at 11:08):From: Lars Hupel <hupel@in.tum.de>
Dear Andreas,
I do not know of any other way than defining an auxiliary function.
I've spent the better part of the afternoon doing just that, and it turns
out it's even uglier than I anticipated. I'm not going to go into the
details of what makes the process hairy.
The bottom line is this: When I throw my theorems at the equivalent of
"fun", I get the finished induction rule, but I can't use it, because the
internal construction updates the theory and I would need to return an
updated theory as well. However, if I inspect the result I get, set up a
new goal from it and prove it again, I get the rule that I wanted.
Anyway, thanks for the explanation why the function package doesn't expose
that functionality. I guess I just have to live with my horrific code now.
Cheers
Lars
Last updated: Apr 26 2024 at 20:16 UTC