Re: [isabelle] resend question about structured induction



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.