Email Gateway (Aug 22 2022 at 13:10): Email Gateway (Aug 22 2022 at 13:10):From: Lars Hupel <hupel@in.tum.de>
Dear list,
it appears that in a "for" clause for inductive definitions, I can only
list the parameters in their respective order. That is, I can't state
that the second parameter of a definition remains unchanged. Is this
intentional? It means that now I have to either reshuffle all uses of my
definition or prove a custom induction rule.
Cheers
Lars
Email Gateway (Aug 22 2022 at 13:10):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
This is indeed a limitation of inductive. The canonical way around it is to define the
constant with the order of arguments as required by inductive and simultaneously an
abbreviation which does the reshuffling. This looks as follows:
inductive test' :: "'a ⇒ nat ⇒ bool"
and test :: "nat ⇒ 'a ⇒ bool"
for b
where
"test a b ≡ test' b a"
| "test 0 b"
| "test n b ⟹ test (Suc n) b"
thm test'.induct
Hope this helps,
Andreas
Last updated: Apr 16 2024 at 20:15 UTC