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

[Lukas Bulwahn]

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.
>
Hi Stefan,


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"
where
   "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)
oops

lemmas R_induct = R.induct[split_format (complete)]

lemma
   "R (a, b) (c, d) ==> True"
proof (induct rule: R_induct)
oops


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.


Lukas