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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
