Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Naming cases in the induction scheme of a func...

Email Gateway (Aug 19 2022 at 09:13):

From: Arthur Peters <amp@singingwizard.org>
I would like to provide names for clauses in a function and then have them
used in the induction rule.

For example, I have the following function:

fun t4 :: "nat => bool" where
four:
"t4 (Suc (Suc (Suc (Suc n)))) = t4 n" |
zero:
"t4 0 = True" |
default:
"t4 _ = False"

And I can reference the cases as 1, 2, 3_1, 3_2, 3_3. See the bottom for a
working proof in this form. However I would like to be able to do something
like the following with the names I gave used in the case names:

lemma
fixes n :: nat
shows "t4 n ==> ~ t4 (Suc n)"
proof (induction n rule: t4.induct)
case "default_1" then show "?case" by simp
next
case "default_2" then show "?case" by simp
next
case "zero" then show "?case" by simp
next
case "default_3" then show "?case" by simp
next
case "four"
from this show "?case" by simp
qed

I have read that this is possible for inductively defined sets, but it
found no description of how to do the same thing with functions.

As a side note, is it possible to combine all the trivial cases (the
defaults and zero) into one proof? All the proofs are identical so it would
be nice to be able to do more than one case at a time.

Thanks a lot.
-Arthur

Working proof:

lemma
fixes n :: nat
shows "t4 n ==> ~ t4 (Suc n)"
proof (induction n rule: t4.induct)
case "3_1" then show "?case" by simp
next
case "3_2" then show "?case" by simp
next
case "2" then show "?case" by simp
next
case "3_3" then show "?case" by simp
next
case "1"
from this show "?case" by simp
qed

Email Gateway (Aug 19 2022 at 09:13):

From: Lars Noschinski <noschinl@in.tum.de>
On 26.11.2012 00:07, Arthur Peters wrote:

I would like to provide names for clauses in a function and then have them
used in the induction rule.

For example, I have the following function:

fun t4 :: "nat => bool" where
four:
"t4 (Suc (Suc (Suc (Suc n)))) = t4 n" |
zero:
"t4 0 = True" |
default:
"t4 _ = False"

And I can reference the cases as 1, 2, 3_1, 3_2, 3_3. See the bottom for a
working proof in this form. However I would like to be able to do something
like the following with the names I gave used in the case names:
[...
I have read that this is possible for inductively defined sets, but it
found no description of how to do the same thing with functions.

The function package does not support this. However, you can use the
case_names attribute to annotate the generated induction lemma with the
case names:

lemma t4_induct = t4.induct[case_names four zero default]

gives you the induction rule you want.

As a side note, is it possible to combine all the trivial cases (the
defaults and zero) into one proof? All the proofs are identical so it would
be nice to be able to do more than one case at a time.

If the proof is trivial, you can just omit these cases and solve them in
the final step:

proof (induct rule: t4_induct)
case four ...
qed (auto ...)

If the proof is not trivial, but the same, you can do the following thing:

proof (induct rule: t4_induct)
have X: ... proof the theorem for the trivial cases ...
{ case default show ?case by (... X ...) }
{ case zero show ?case by (... X ...) }
next
case four ...
qed

-- Lars

Last updated: Nov 21 2024 at 12:39 UTC