Re: [isabelle] inductive + for



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


On 15/04/16 16:27, Lars Hupel wrote:
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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.