Re: [isabelle] resend question about structured induction



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





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