Re: [isabelle] Explanation of induction rules for inductive predicates?

Am 23/01/2013 00:39, schrieb James Cooper:
> Hello,
> I'm new to the Isabelle system, so this might be a bit simplistic, but I've
> looked through the tutorials and references and can't really find an
> explanation. It's possible I'm just missing something, so if anyone can
> explain what that is I'd be very grateful.
> Basically, I'm trying to build a little interpreter, but the interpreter
> and typechecker need to use "inductive" rather than e.g. "primrec" or
> "function" because they do not provably terminate. That's fine, but the
> proof rules for "inductive_rule.induct" don't seem to work straight for me.
> (I'm on the Isabelle jEdit IDE for Mac, if it makes a difference.)
> For instance, my typechecking predicate looks like
> inductive typecheck :: "type env => expr => type => bool"
> where chkNum: "typecheck env (NumExpr n) NumType"
>     | chkStr: "typecheck env (StrExpr s) StringType"
>     | chkVar: "lookup env v = Some t ==> typecheck
>     | chkLength: "typecheck env a StringType ==> typecheck env (LengthExpr
> a) NumType"
> etc.
> where there's exactly one case for each expression type in the second
> argument. So I want to prove a little set of inversion lemmas,
> lemma num_const_invert: "typecheck env (NumExpr n) t ==> t = NumType"
> etc.

A couple of solutions.

1. Use the nice inductive_cases command defined just for that purpose, eg

inductive_cases xyz: "typecheck env (NumExpr n) t"

which produces what you want, but in "elimination form". This is ideal for proof
automation and you should add "[elim!]" after "xyz" to tell auto and friends
about it and they will apply it automatically to assumptions of the proof state.
(No "!" if the repeated application could loop).

2. Don't use induction but cases and instantiate the rule explicitly:

apply (cases env "NumExpr n" t rule: typecheck.cases)

3. You can prove it in Isar by hand (see 4.4.5 Rule inversion in my Programming
and Proving tutorial)

4. apply(erule typecheck.cases)

I don't think this is adequately documented.


> Since the typechecking rules are syntax-directed, this seems like it should
> be simple: induct on the typechecking rules, have the chkNum case trivially
> and watch every other case produce e.g. "StringExpr s = NumExpr n" as an
> assumption and proof by contradiction. Instead, the expression argument
> gets wiped out and "apply (induction rule: type check.induct)" produces
>  1. /\ env n. NumType = NumType
>  2. /\ env s. StringType = NumType
>  3. /\ env v t1. lookup env v = Some t1 ==> t1 = NumType
>  4. /\ env a. typecheck env a StrType  ==> StringType = NumType ==> NumType
> = NumType
> ...
> which is obviously insoluble. As best I can tell it's inducting over a
> *generic* term "typecheck env expr t", and the knowledge that expr is
> really NumExpr n has been lost; as a result it's trying to prove that
> typecheck *always* produces a NumType, with predictably strange results.
> Any idea what's going on here? Am I doing something wrong? What's the
> *right* way to define a nonterminating function of this kind and prove
> things over it?
> James Cooper

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.