David Wang (Dec 07 2023 at 00:49): David Wang (Dec 07 2023 at 00:49):Hello,
I have the following statement:
(case bfold b t of
Bc True ⇒ bdefs c1 t |
Bc False ⇒ bdefs c2 t |
_ ⇒ merge (bdefs c1 t) (bdefs c2 t)
) |`(- (lvars c1 ∪ lvars c2))
I have show shown that each of the cases simplifies to:
t |` (-(lvars c1 ∪ lvars c2))
How do I show that the original statement must simplify to the same statement?
Yong Kiam (Dec 07 2023 at 00:52):does using the split theorem for your datatype work? it should be named something like foo.split
David Wang (Dec 07 2023 at 01:04):Yong Kiam said:
does using the split theorem for your datatype work? it should be named something like
foo.split
case (If b c1 c2)
...
hence 1: "bdefs c1 t |` (-(lvars c1 ∪ lvars c2))
= t |` (-(lvars c1 ∪ lvars c2))" by auto
...
hence 2: "bdefs c2 t |` (-(lvars c1 ∪ lvars c2))
= t |` (-(lvars c1 ∪ lvars c2))" by auto
have 3: "merge (bdefs c1 t) (bdefs c2 t) |` (-(lvars c1 ∪ lvars c2))
= t |` (-(lvars c1 ∪ lvars c2))"
using 1 2 merge_restrict by blast
...
also have "... = (case (bfold b t) of
(Bc True) ⇒ bdefs c1 t |
(Bc False) ⇒ bdefs c2 t |
_ ⇒ merge (bdefs c1 t) (bdefs c2 t)
) |` (-(lvars c1 ∪ lvars c2))" by simp
also have "... = t |` (-(lvars c1 ∪ lvars c2))"
using 1 2 3
by (auto split: bexp.split)
(* or using 1 2 3 bexp.split sledgehammer *)
Surprisingly not.
Yong Kiam (Dec 07 2023 at 01:06):do you mean the above auto split: bexp.split line doesn't work?
David Wang (Dec 07 2023 at 01:07):Yong Kiam said:
do you mean the above
auto split: bexp.splitline doesn't work?
This worked in the end:
(auto split: bexp.split bool.split)
Thank you.
Last updated: Apr 28 2024 at 12:28 UTC