Re: [isabelle] structured induction



On Sun, May 15, 2011 at 2:56 PM, Randy Pollack <rpollack at inf.ed.ac.uk> wrote:
> In the following example (taken from
> ~~/src/HOL/Induct/Common_Patterns.thy) there is apparently unnecessary
> duplication.
>
> lemma
>  fixes n :: nat
>  shows "P n" and "Q n"
> proof (induct n)
>  case 0 case 1
>  show "P 0" sorry
> next
>  case 0 case 2
>  show "Q 0" sorry
> next
>  case (Suc n) case 1
>  note hyps = `P n` `Q n`              (**** this line ... ****)
>  show "P (Suc n)" sorry
> next
>  case (Suc n) case 2
>  note hyps = `P n` `Q n`              (**** ... duplicated ***)
>  show "Q (Suc n)" sorry
> qed

Hi Randy,

It is the "next" command that removes the local definition of "hyps"
from scope. Maybe you could try something like this:

lemma
 fixes n :: nat
 shows "P n" and "Q n"
proof (induct n)
  case 0
    case 1
    show "P 0" sorry
    case 2
    show "Q 0" sorry
next
  case (Suc n)
    note hyps = `P n` `Q n`
    case 1
    show "P (Suc n)" using hyps sorry
    case 2
    show "Q (Suc n)" using hyps sorry
qed

>
> I want to know how to avoid this duplication.  Even more, I have the
> common example
>
> lemma
> assumes h:"inductiveR x"
> and

It looks like the rest of your question was cut off. Could you resend it?

- Brian





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