Re: [isabelle] Case distinction with Recursion Induction



Dear Brian,

That was really a great hint. Exactly what I wanted! I was not aware
of this "lemmas" command. I will look into into in more detail.

All the Best!

On Tue, May 15, 2012 at 3:32 AM, Brian Huffman <huffman at in.tum.de> wrote:

> On Tue, May 15, 2012 at 8:12 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> > The names of the cases for recursive functions are 1, 2, ....
> > The reason is that fun may modify the input equations to disambiguate
> them. Thus
> > one equation may become two or more and one would need some clever
> naming scheme
> > to deal with that situation in inductions.
>
> Hi Alfio,
>
> Note that if you don't like the default case names, you can rename
> them using the "case_names" attribute on the induction rule. You can
> use the "lemmas" command to save the updated rule for reuse. For
> example:
>
> fun fib :: "nat => nat" where
>  "fib 0 = 0" | "fib (Suc 0) = 1" | "fib n = fib (n - 1) + fib (n - 2)"
>
> lemmas fib_induct = fib.induct [case_names 0 Suc_0 Suc_Suc]
>
> lemma "fib n \<le> fib (Suc n)"
> proof (induct n rule: fib_induct)
>  case 0 show ?case by simp
> next
>  case Suc_0 show ?case by simp
> next
>  case (Suc_Suc k) thus ?case by simp
> qed
>
> - Brian
>
> > Am 14/05/2012 22:50, schrieb Alfio Martini:
> >> Dear Isabelle Users,
> >>
> >> I was playing a bit with  proofs with recursion induction in Isar and
> after
> >> a while, it
> >> became all too boring to type those long formulas so that I looked for
> some
> >> ways of improving this
> >> situation.
> >>
> >> Pattern-matching with  meta-variables as unknowns was a huge
> improvement.
> >> But
> >> I tried also pattern matching via case distinction and did not succeed.
> >> Firstly, I thought case distinction
> >> was only possible with structural induction. But in the new tutorial
> >> (Programming and
> >> Proving) one sees that proofs  using rule induction can be done via case
> >> distinction
> >> with respect to the name (labels) of the rules.
> >>
> >> Unfortunately, I did not succeed using this trick (of using a label) for
> >> recursion induction.
> >> Am I missing something very basic here?
> >>
> >> Best!
> >>
> >
>



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