*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Explanation of induction rules for inductive predicates?*From*: James Cooper <not.fenimore at gmail.com>*Date*: Tue, 22 Jan 2013 18:39:15 -0500

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. 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

**Follow-Ups**:**Re: [isabelle] Explanation of induction rules for inductive predicates?***From:*Andreas Lochbihler

**Re: [isabelle] Explanation of induction rules for inductive predicates?***From:*Tobias Nipkow

- Previous by Date: [isabelle] Inria research positions
- Next by Date: Re: [isabelle] Explanation of induction rules for inductive predicates?
- Previous by Thread: [isabelle] Inria research positions
- Next by Thread: Re: [isabelle] Explanation of induction rules for inductive predicates?
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list