*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] resend question about structured induction*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sun, 15 May 2011 16:03:41 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BANLkTikEtQznF3ogM0QY6KUNhnz0gTL8gw@mail.gmail.com>*References*: <BANLkTikEtQznF3ogM0QY6KUNhnz0gTL8gw@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

On Sun, May 15, 2011 at 3:25 PM, Randy Pollack <rpollack at inf.ed.ac.uk> wrote: > lemma > assumes h:"inductiveR x" and j:"P x" > shows "Q1 x" and "Q2 x" > using h proof (induct) > (case ...) case 1 have "P x0" by fact show "Q1 x0" ... > case 2 have "P x0" by fact show "Q2 x0" ... > > I want to eliminate the duplication in the last two lines. I think I understand your problem now. Did you mean to say, "using h j proof (induct)" above? Here is another example adapted from HOL/Induct/Common_Patterns.thy; I've added the extra assumption "C n" which is added to the inductive hypothesis. At the point of "case (Suc n)", you might like to be able to use the assumption "C (Suc n)" to derive some other facts, and use those in both subcases 1 and 2. The problem is that the "case" command does not assume "C (Suc n)" for you until you get all the way down to the subcases. lemma fixes n :: nat assumes "C n" shows "A n ==> P n" and "B n ==> Q n" using `C n` proof (induct n) case 0 { case 1 note `A 0` show "P 0" sorry next case 2 note `B 0` show "Q 0" sorry } next case (Suc n) note `A n ==> C n ==> P n` and `B n ==> C n ==> Q n` (*** `C (Suc n)` has not been assumed yet at this point ***) { case 1 note `A (Suc n)` and `C (Suc n)` show "P (Suc n)" sorry next case 2 note `B (Suc n)` and `C (Suc n)` show "Q (Suc n)" sorry } qed I can think of two solutions, one of which you already discovered: > In fact, playing with examples shows that > > lemma > assumes h:"inductiveR x" and j:"P x" > shows "Q1 x" and "Q2 x" > using h proof (induct) > (case ...x0...) (** the fact "P x0" is not known here **) > case 1 have j:"P x0" by fact > show "Q1 x0" proof (... j ...) > case 2 show "Q2 x0" proof (... j ...) (** why is j in scope here? **) > > works. I don't understand the scoping of facts in this example. By omitting the "next" between subcases 1 and 2, Isabelle doesn't reset the proof context, so "j" is still in scope. This technique wouldn't work for my example above though, since when you use two "case" commands without using "next" in between, you get a proof context that is essentially the union of the two cases. Here the second subcase fails because too many assumptions are in scope. lemma fixes n :: nat assumes "C n" shows "A n ==> P n" and "B n ==> Q n" using `C n` proof (induct n) case (Suc n) case 1 note `A (Suc n)` and `C (Suc n)` show "P (Suc n)" sorry case 2 note `C (Suc n)` and `C (Suc n)` show "Q (Suc n)" (*** error because assumption `A (Suc n)` is still in scope ***) Solution 2: If the "case" command doesn't make the necessary assumptions early enough for you, you can always "assume" them yourself, like this: lemma fixes n :: nat assumes "C n" shows "A n ==> P n" and "B n ==> Q n" using `C n` proof (induct n) case 0 { case 1 note `A 0` show "P 0" sorry next case 2 note `B 0` show "Q 0" sorry } next case (Suc n) assume foo: "C (Suc n)" from foo have bar: ... { case 1 note `A (Suc n)` show "P (Suc n)" using bar sorry next case 2 note `B (Suc n)` show "Q (Suc n)" using bar sorry } qed The validity of this might make a bit more sense if you remember that the "case" command is essentially syntactic sugar for a bunch of "fix" and "assume" commands. Whenever you do a "show" command, Isar only requires that the assumptions in scope are a subset of the ones in the goal you are trying to solve. Hope this helps, - Brian

**Follow-Ups**:**Re: [isabelle] resend question about structured induction***From:*Randy Pollack

**References**:**[isabelle] resend question about structured induction***From:*Randy Pollack

- Previous by Date: [isabelle] resend question about structured induction
- Next by Date: Re: [isabelle] resend question about structured induction
- Previous by Thread: [isabelle] resend question about structured induction
- Next by Thread: Re: [isabelle] resend question about structured induction
- Cl-isabelle-users May 2011 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