Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] structured induction

view this post on Zulip Email Gateway (Aug 18 2022 at 11:45):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
Consider the following example:

lemma valid_fitch:
fixes G :: "(par * tp) list"
assumes h:"valid G"
shows "\<exists> a A. G \<parallel>- a : A"
using h
proof (induct G rule: list.induct) -- "explicit induction rule"
case Nil
...

This induction behaves as exected, i.e. induction over the list G (I
was explicit about the induction rule to use).

However consider the following:

lemma valid_fitch:
fixes G :: "(par * tp) list"
assumes h:"valid G"
shows "\<exists> a A. G \<parallel>- a : A"
using h
proof (induct G) -- "let Isar decide which induction rule"
case Nil

*** Unknown case: "Nil"
*** At command "case".

Isar did induction over the judgement "valid G" instead of over the
list G. This seems unintended.

Am I missing something about the syntax? (BTW, this example is in
nominal Isabelle, but I guess that doesn't play any role in the
situation.)

Thanks,
Randy

view this post on Zulip Email Gateway (Aug 18 2022 at 11:45):

From: Clemens Ballarin <ballarin@in.tum.de>
By "using h" the fact "valid G" is chained into the proof and the
induct method uses the first chained fact to choose the induction
rule. (The Isar Ref manual contains useful table detailing what
induct and cases do in which situations.)

Clemens

view this post on Zulip Email Gateway (Aug 18 2022 at 12:20):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
I love Isar structured induction. Here are two questions.

Consider:

lemma
assumes h:"R M" --"R is an inductively defined relation"
shows "P M = {}" "Q M" --"P and Q are any properties"
using h proof (induct)
case (constr1 X) --"constr1 is a single argument constructor of R"
show ?case

The last line will fail:

*** Unbound schematic variable: ?case

The ProofGeneral drop down for cases shows something about
"subcases: 1 2" How do I get ?case to work in this setting?

Question 2: Please give pointers to some examples of well-founded
induction over a measure function in Isabelle 2008. I know of
Makarius' note "Structured Induction Proofs ...", but I still can't
get things to work in the structured way (as opposed to using the
object language to give an explicit induction predicate ...).

Thanks
Randy

view this post on Zulip Email Gateway (Aug 18 2022 at 12:20):

From: Makarius <makarius@sketis.net>
On Tue, 5 Aug 2008, Randy Pollack wrote:

lemma
assumes h:"R M" --"R is an inductively defined relation"
shows "P M = {}" "Q M" --"P and Q are any properties"
using h proof (induct)
case (constr1 X) --"constr1 is a single argument constructor of R"
show ?case

The last line will fail:

*** Unbound schematic variable: ?case

The ProofGeneral drop down for cases shows something about
"subcases: 1 2" How do I get ?case to work in this setting?

You first need to enter the particular sub cases before the ?case binding
show up. See the end of src/HOL/Induct/Common_Patterns.thy for examples
for induction with multiple goals.

Please give pointers to some examples of well-founded induction over a
measure function in Isabelle 2008. I know of Makarius' note "Structured
Induction Proofs ...", but I still can't get things to work in the
structured way (as opposed to using the object language to give an
explicit induction predicate ...).

Maybe you did not use the proper rule, which is wf_induct_rule as opposed
to the old wf_induct (the correct rule is already declared as canonical
induction scheme for wf r facts). Here is an example pattern involving
both an extra parameter x and premise "A x a", apart from the induction
argument a:

lemma
fixes a :: 'a
and r :: "('a * 'a) set"
and x :: 'b
assumes "wf r"
and "A x a"
shows "B x a"
using assms
proof (induct a arbitrary: x)
case (less a)
note prem = A x a
-- {* cf. @{thm less.prems} *}
note hyp = !!x y. (y, a) : r ==> A x y ==> B x y
-- {* cf. @{thm less.hyps} *}
show ?case sorry
qed

The example from the "Structured Induction Proofs ..." paper is in
src/HOL/Isar_examples/Puzzle.thy (it uses the less_induct rule).

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 17:41):

From: Randy Pollack <rpollack@inf.ed.ac.uk>
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. Even more, I have the
common example

lemma
assumes h:"inductiveR x"
and

view this post on Zulip Email Gateway (Aug 18 2022 at 17:41):

From: Brian Huffman <brianh@cs.pdx.edu>
On Sun, May 15, 2011 at 2:56 PM, Randy Pollack <rpollack@inf.ed.ac.uk> 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

Hi Randy,

It is the "next" command that removes the local definition of "hyps"
from scope. Maybe you could try something like this:

lemma
fixes n :: nat
shows "P n" and "Q n"
proof (induct n)
case 0
case 1
show "P 0" sorry
case 2
show "Q 0" sorry
next
case (Suc n)
note hyps = P n Q n
case 1
show "P (Suc n)" using hyps sorry
case 2
show "Q (Suc n)" using hyps sorry
qed

I want to know how to avoid this duplication.  Even more, I have the
common example

lemma
assumes h:"inductiveR x"
and

It looks like the rest of your question was cut off. Could you resend it?

Last updated: May 01 2024 at 20:18 UTC