Email Gateway (Aug 18 2022 at 14:04): Email Gateway (Aug 18 2022 at 14:04):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear all,
I was trying to produce a "fun" definition that given a list produces
a couple of lists (the following definition of "gener" is just a
simplified version where my question already arises).
fun gener :: "'a list => (nat list * 'a list)"
where
gener_Cons: "gener (a # b # l) =
(if a = b then (0 # fst (gener (b # l)), snd (gener (b # l)))
else (fst (gener l), snd (gener l)))"
|gener_Nil: "gener a = ([], a)"
Somehow, the induction rule associated to the previous definition:
thm gener.induct
has the following aspect:
\<And> a b l. [| a = b ==> ?P (b # l); a = b ==> ?P (b # l); a
\<noteq> b ==> ?P l; a \<noteq> b ==> ?P l |] ==> ?P (a # b # l);
?P []; \<And>v. ?P [v] |]
==> ?P ?a0.0
where both cases "a = b" and "a \<noteq> b" appear twice, which does
not pose any limitation but may result a bit annoying when trying to
number hypothesis.
May somebody know a way to avoid this behaviour?
Thanks in advance,
Jesus
Email Gateway (Aug 18 2022 at 14:05):From: Alexander Krauss <krauss@in.tum.de>
Hi Jesus,
I think you mean that you would prefer to have the case distinction a
= b vs a ~= b built into the induction rule, instead of having to do
it yourself each time you apply it. The function package never does
such things automatically, in order to have a predictable berhaviour.
If you know what rule you would like to see, you can also state it
yourself and use the "induct_scheme" method to derive it, usually
almost automatically. See ch. 5 of my thesis for details
(http://www4.in.tum.de/~krauss/diss/krauss_phd.pdf).
Cheers,
Alex
Last updated: Nov 21 2024 at 12:39 UTC