Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] case_names for induction rule

Email Gateway (Mar 28 2024 at 07:33):

From: "\"Putti, Edoardo (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
I'm trying to set up the names of cases to use during a computation induction proof.
The reference manual says this can be done by using the case_names attribute,
unfortunately I'm not able to set it up correctly.

Here's my example. In the last lemma I set up induction, but the names declared
before the lemma are not picked up. Is there a way to debug this myself? Is there a command
to print all attributes for a constant?

theory Scratch
imports Main
begin

type_synonym flag = bool
abbreviation (input) "ShouldContinue ≡ True"
abbreviation (input) "ShouldCancel ≡ False"

datatype event = Continue | Stop | Cancel
type_synonym actions = "event list"

fun valid :: "flag ⇒ actions ⇒ bool" where
"valid f [] = True"
| "valid f (Continue # xs) ⟷ f = ShouldContinue ∧ valid ShouldContinue xs"
| "valid f (Stop # xs) ⟷ f = ShouldCancel ∧ valid ShouldCancel xs"
| "valid f (Cancel # xs) ⟷ valid ShouldCancel xs"

declare valid.induct [case_names A B C D]

lemma "valid ShouldContinue t ⟹ undefined"
proof(induction rule: valid.induct)
print_cases
end

Email Gateway (Mar 28 2024 at 08:56):

From: Thomas Sewell <tals4@cam.ac.uk>
You're close to the right syntax, but theorems aren't mutable.

Doing declare X[case_names ...] doesn't put the modified theorem anywhere, i.e. it doesn't do anything useful.

You could save the modified theorem with lemmas Y = X[case_names ...].

Alternatively, you can use it on the spot with apply (induct rule: X[case_names ...]).

Unfortunately, in this situation where the function package has generated an rule that isn't quite the one you want, there isn't a nice simple way to modify and replace it. You can save a variant, but users will tend to find the original thanks to its standard name.

Curiously, the function package parser seems to support naming each of the cases of the function, but this information doesn't seem to go anywhere.

Hope that helps,
Thomas.

Email Gateway (Mar 28 2024 at 09:27):

From: Tobias Nipkow <nipkow@in.tum.de>
Hi Thoams,

If the standard name is x.induct, I name my variant x_induct, which works well
for searches with "name:induct".

Tobias

smime.p7s

Last updated: Apr 29 2024 at 04:18 UTC