[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
bulwahn at in.tum.de
Fri Aug 19 11:00:11 CEST 2011
Stefan Berghofer wrote:
> 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.
In most cases, the advertised feature of the induct method does the job
to avoid manual massaging of the induction rule, as you outlined in your
mail. But in certain cases, the features of the induct method do not
supersede the massaging, e.g. with split_format.
Consider the following example:
inductive R :: "('a * 'b) => ('a * 'b) => bool"
"R x y ==> R y z ==> R x z"
lemma "R (a, b) (c, d) ==> True"
proof (induct "(a, b)" "(c, d)" rule: R.induct)
lemmas R_induct = R.induct[split_format (complete)]
"R (a, b) (c, d) ==> True"
proof (induct rule: R_induct)
In the first case, you obtain a free variable y of pair type, and
usually it requires to obtain y's components within the proof step,
there is no possibility to get this splitting with the induct method
right now. Using split_format enables this splitting, as you can see in
the second example. This drawback actually stopped us integrating the
method for doing "more automatic" rule inductions, which we discussed
offline last Christmas.
More information about the isabelle-dev