*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] On Recursion Induction*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Tue, 8 May 2012 16:40:40 -0300*Cc*: Brian Huffman <huffman.brian.c at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FA8AB8A.9000705@jaist.ac.jp>*References*: <CAAPnxw37MiOfcZv7xV2YR6UrhcA-_Vg2W6+k+ajdZA77L2RN8w@mail.gmail.com> <4FA8AB8A.9000705@jaist.ac.jp>*Sender*: alfio.martini at gmail.com

Dear Christian and Brian, Many thanks for your reply. Some remarks below: >(all methods with a "_tac" suffix are emulations for traditional tactics >(as used in apply-style proofs) and are considered "improper" by >isar-ref p. 173 I looked at section 9.2.3 in the reference manual and did not find "induct_tac" in the list of improper proof methods. But assuming it is, I think that the tutorial, for instance, Chapter 2, should be updated, shouldn´t it? >Moreover your statement >theorem "∀b. ∀e. valbool b e = valbool (NNF b) e" >is a bit strange since by-default all variables are (meta-)all-quantified >after a successful proof. With proper methods you can proof the >statement as follows: >theorem "valbool b e = valbool (NNF b) e" >by (induction b rule: NNF.induct) auto Good point. However, whenever I am playing (training) with Isabelle, I use toy problems like this. This means that I want Isabelle to check the proof I made by hand, so my level of abstraction is the set of rules of natural deduction. I usually play like this: first an exploratory proof using procedural style and auto and then a detailed step-by-step proof using the Isar language. I know that free variables become logical variables (in the sense of Prolog) and thus, operationally behave as if the were universally quantified and can be used more directly by the simplifier. But at the "playing level" I prefer to proceed like in a hand-made proof, first stripping off all the quantifiers and then applying induction. In this kind of exercise I can use this theorem further by applying rule allE and so on. So, I assume that this kind of approach can be only done with Isar and the fix command, as pointed out by Brian, which I usually do. >Your original version results in "ALL b e. valbool b e = valbool (NNF >b) e" (which is equivalent, but not so nice to use, since you cannot >directly instantiate it). I think I spoke about this above, but I would like to capture in a precise way (in a theorem) this equivalence. Informally we all know that they are. I often think about it. Do you know how to write (in Isabelle) this "equivalence"? All the Best! On Tue, May 8, 2012 at 2:13 AM, Christian Sternagel <c-sterna at jaist.ac.jp>wrote: > Dear Alfio, > > On 05/08/2012 01:03 PM, Alfio Martini wrote: > >> 1) In the proof of the theorem, below in the file (and in the image), I >> use >> recursion induction together >> with "induct_tac" (as taught in the tutorial) and everything works as >> expected. However, If I try to use >> >> apply (induction b rule: NNF.induct) as suggested by the new tutorial from >> Tobias >> Nipkow (e.g., section 2.3, page 15) , I get the following error message: >> >> ill-typed instantiation: b :; 'a. >> >> Why this is so? >> > "induct"/"induction" is not the same as "induct_tac" (all methods with a > "_tac" suffix are emulations for traditional tactics (as used in > apply-style proofs) and are considered "improper" by isar-ref p. 173. One > difference is that with traditional tactics case-analysis (case_tac) and > induction (induct_tac) is possible over meta-bound variables, for > "induct"/"induction" however, you need free variables (I guess in reality > the difference is more subtle, so please Isabelle-gurus, correct me). > Moreover your statement > > theorem "∀b. ∀e. valbool b e = valbool (NNF b) e" > > is a bit strange since by-default all variables are (meta-)all-quantified > after a successful proof. With proper methods you can proof the statement > as follows: > > theorem "valbool b e = valbool (NNF b) e" > by (induction b rule: NNF.induct) auto > > which is short for > > theorem "valbool b e = valbool (NNF b) e" > > apply (induction b rule: NNF.induct) > apply (auto) > done > > The resulting thm is "valbool ?b ?e = valbool (NNF ?b) ?e" (note the > question marks which mark schematic variables, i.e., variables that can be > instantiated arbitrarily according to their type). Your original version > results in "ALL b e. valbool b e = valbool (NNF b) e" (which is equivalent, > but not so nice to use, since you cannot directly instantiate it). > > hope this helps > > chris > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) Coordenador do Curso de Ciência da Computação Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil

**Follow-Ups**:**Re: [isabelle] On Recursion Induction***From:*Christian Sternagel

**Re: [isabelle] On Recursion Induction***From:*Lars Noschinski

**References**:**[isabelle] On Recursion Induction***From:*Alfio Martini

**Re: [isabelle] On Recursion Induction***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] On Recursion Induction
- Next by Date: Re: [isabelle] On Recursion Induction
- Previous by Thread: Re: [isabelle] On Recursion Induction
- Next by Thread: Re: [isabelle] On Recursion Induction
- Cl-isabelle-users May 2012 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