Re: [isabelle] On Recursion Induction



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




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