*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] resend question about structured induction*From*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Sun, 15 May 2011 20:25:17 -0400*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BANLkTinP5wX32KM5aoJ_i-0Yxb1wZ5+1xg@mail.gmail.com>*References*: <BANLkTikEtQznF3ogM0QY6KUNhnz0gTL8gw@mail.gmail.com> <BANLkTinP5wX32KM5aoJ_i-0Yxb1wZ5+1xg@mail.gmail.com>*Sender*: rpollack0 at gmail.com

Thanks Brian, You understood the question as I meant it. I consider it a weakness that the fact `C (Suc n)` is not in scope where it logically should be. Of the two solutions you suggest, the one I first discovered is illogical, and the second one you point out is less comfortable for the user because the assumption isn't checked by Isabelle at the point it is introduced. Due to the profusion of renamed variables under the "case" it is easy to misstate such assumptions. Best, Randy -- On Sun, May 15, 2011 at 7:03 PM, Brian Huffman <brianh at cs.pdx.edu> wrote: > 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 > >

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

**Re: [isabelle] resend question about structured induction***From:*Brian Huffman

- Previous by Date: Re: [isabelle] resend question about structured induction
- Next by Date: [isabelle] Question concerning HOAS
- Previous by Thread: Re: [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