# 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.*