[isabelle] Explanation of induction rules for inductive predicates?


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"

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"

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.