[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Stefan Berghofer]

Alexander Krauss wrote:
> In particular, Stefan discovered that replacing inductive set
> definitions by predicates was by no means as easy as everybody had
> expected. One good example is the small-step relation from Jinja and
> its various cousins. It had type "((expr * state) * (expr * state))
> set", and turning it into a 4-ary predicate (expr => state => expr =>
> state => bool) would cause problems with either version of the
> transitive closure operator. [Btw, the newer HOL/IMP/Small_Step.thy
> uses a binary predicate over pairs, which requires massaging the
> induction rule using [split_format (complete)]].

Hi all,

let me take the opportunity to advertise a useful feature of the induct
method that avoids such manual "massaging" of induction rules. For example,
the command

  proof(induct rule: small_step_induct)

in HOL/IMP/Types.thy can be replaced by

  proof(induct "(c,s)" "(c',s')" arbitrary: c s c' s' rule: small_step.induct)

which allows the standard induction rule small_step.induct to be used instead
of the small_step_induct rule produced using split_format, which is a bit of
a hack anyway. The above is a shorthand for

  proof(induct x=="(c,s)" y=="(c',s')" arbitrary: c s c' s' rule: small_step.induct)

Since revision b0aaec87751c (Jan 2010), the equational constraints arising from
such invocations of induct are solved automatically using injectivity / distinctness
rules for datatypes, so the rest of the proof script works as if the custom-made
induction rule had been applied.

Greetings,
Stefan