Re: [isabelle] resend question about structured induction



On Sun, 15 May 2011, Randy Pollack 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

I want to know how to avoid this duplication.

First of all, the boundaries of nested cases are determined by the "induct" method. Further refinement of this behaviour is on the TODO list for several years, but that method has accumulated so many features already, that it takes a long time to clear it out again.

Given the current behaviour there are still many ways how to express the proof. The "Common_Patterns" are just some examples to explain the main ideas. E.g. the above duplication of "P n" and "Q n" as propositions can be avoided by using the fact names produced by each case, i.e. "Suc", "Suc.hyps", "Suc.prems". You can also project from there using syntax such as "Suc(2)" although such numbers make proofs a bit hard to read and maintain.


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.

This is another example why it is a bad idea to invent new Isar indentation rules on the spot. The indentation that is hard-wired into Proof General is quite precise approximation of important semantic aspects of the language. In particular, the 'case' command merely augments the context monotonically, without introducing any block structure on its own. So no change of indentation here.

I've also made a mistake many years ago in calling it 'case' in the first place, which sounds too much like a rigid structure in corellation with the goal state, which it isn't.


To understand Isar block structure in general, you can always use { ... } explicitly, but in practice it is usually suppressed due to the following implicit principles -- using ( ... ) for the true internal parantheses that do not have concrete syntax:

  (1) a proof body opens an extra pair of spare parentheses like this:

       (
       have A
       (
         proof method
           body
         qed method
       )
       )

  (2) concrete user commands are defined as follows:

        {    == ((
        }    == ))
        next == )(

      More precisely

        next == ) note nothing (

      which explains why you cannot push results over that boundary.


	Makarius





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