Re: [isabelle] On Recursion Induction



Dear Brian,

Thanks for your reply!

>Another standard idiom is to use "fix" to introduce a new free
>variable, which can then be used with "induct":

>theorem "\<forall>b. \<forall>e. valbool b e = valbool (NNF b) e"
>proof (rule allI)
 >fix b
>show "\<forall>e. valbool b e = valbool (NNF b) e"
 > by (induction b rule:NNF.induct) auto
>qed

That is the way I go about it when using Isar. So the question that
remains is: how to prove the theorem above (with all the (two)
quantifiers) using the procedural style (and without using induct_tac)?

All the Best!

On Tue, May 8, 2012 at 2:21 AM, Brian Huffman <huffman at in.tum.de> wrote:

> On Tue, May 8, 2012 at 7: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
>
> I was about to suggest the same thing.
>
> Another standard idiom is to use "fix" to introduce a new free
> variable, which can then be used with "induct":
>
> theorem "\<forall>b. \<forall>e. valbool b e = valbool (NNF b) e"
> proof (rule allI)
>  fix b
>  show "\<forall>e. valbool b e = valbool (NNF b) e"
>     by (induction b rule:NNF.induct) auto
> qed
>
> (Note that simply "proof", which applies a default intro rule, would
> also work in place of "proof (rule allI)".)
>
> - Brian
>



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