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