Email Gateway (Aug 18 2022 at 14:22): Email Gateway (Aug 18 2022 at 14:22):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Hello,
What is the best way to get Isabelle to automatically perform certain
case analysis steps within simplification?
e.g.
datatype gate = D | S | T1 | T2 | T3 | T4 | B1 | B2 | B3 | B4
fun reduce1_false2 :: "gate => bool => bool"
where
reduce1_false2_in_T1: "reduce1_false2 T1 g = g"
| reduce1_false2_in_T2: "reduce1_false2 T2 g = True"
| reduce1_false2_in_T3: "reduce1_false2 T3 g = ~ g"
| reduce1_false2_in_T4: "reduce1_false2 T4 g = True"
| reduce1_false2_in_B1: "reduce1_false2 B1 g = ~ g"
| reduce1_false2_in_B2: "reduce1_false2 B2 g = False"
| reduce1_false2_in_B3: "reduce1_false2 B3 g = g"
| reduce1_false2_in_B4: "reduce1_false2 B4 g = False"
| reduce1_false2_in_D: "reduce1_false2 D g = g"
| reduce1_false2_in_S: "reduce1_false2 S g = ~ g"
later when there is a goal of the form...
"P (reduce1_false2 gt g)"
I would like simp to automatically consider the cases for "gt".
suggestions?
thanks,
lucas
Email Gateway (Aug 18 2022 at 14:22):From: Tobias Nipkow <nipkow@in.tum.de>
You need to have a case-expression in your goal. If not, then you need
to prove your own splitting lemma first:
"P (reduce1_false2 gt g) = ((gt=T1 --> P g) & (gt=T2 --> P True) ...)"
Then you can go
apply(simp split: <split-lemma>)
Tobias
Lucas Dixon wrote:
Email Gateway (Aug 18 2022 at 14:23):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
Thanks; I found changing everything to using case-statementsm, as you
suggest, seemed to be the best approach (so far).
It would be nice to have some tools that let one derive case statements
from function definitions and visa-versa. Having the function definition
style of equations provides nice simp rules which don't expand the case
statements.
cheers,
lucas
Tobias Nipkow wrote:
Email Gateway (Aug 18 2022 at 14:23):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Thomas actually has made up a nice Isar attribute for that: it gives you (from a case statement) the standard simp rules you'd write in a function definition.
I'll see if we can dig this up and release it.
The other way would be to have the function package automatically prove the split rule instead.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 14:24):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
As Gerwin said, I wrote an Isar attribute to convert a "f x = case x of
..." definition into the standard simp rules for f.
There were some issues with variables of function type, which I've just
got around to addressing now. Here's a somewhat robust version.
The attached theory file should define an Isar attribute split_simps
which is used like so:
definition "f x a b = (case x of True => a | False => b)"
lemmas f_simps[simp] = f_def[split_rule bool.split]
The f_simps rule will be "f True a b = a && f False a b = b".
(We make this theory file available under a BSD license, feel free to
use it. The maintainers might consider adding it to the repository.)
Yours,
Thomas.
Gerwin Klein wrote:
SplitSimps.thy
Email Gateway (Aug 18 2022 at 14:24):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Allow me to send an immediate bugfix. I thought I was being clever by replacing HOL conjunction with Pure conjunction in the output of split_simps, but it appears that the simplifier doesn't know what to do with it.
Redefining conjunct_rules like this fixes it:
val conjunct_rules = foldr1 (fn (a, b) => [a, b] MRS conjI);
The reason for this is that theorem-modifying attributes don't seem to be able to emit a list of theorems, so I had to fold the theorems back into a single one. Perhaps the isabelle developers can think of a better way.
I attach the newest version.
Yours,
Thomas.
SplitSimps.thy
Last updated: Nov 21 2024 at 12:39 UTC