Email Gateway (Aug 22 2022 at 14:17): Email Gateway (Aug 22 2022 at 14:17):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I have gotten a bit stuck on something, and would be grateful for any
advice from people who are more experienced at using the datatype and
function package.
My context is the following definitions (theory file attached),
which I have abstracted from a larger setting:
datatype (discs_sels) 'a "term" =
V 'a
| U
| T "'a term * 'a term"
| C "'a term * 'a term"
| L "'a term"
| L' "'a term"
| R "'a term"
| R' "'a term"
| A "'a term * 'a term * 'a term"
| A' "'a term * 'a term * 'a term"
primrec I :: "'a term ⇒ bool"
where "I (V x) = True"
| "I U = True"
| "I (T tu) = (λtu. fst tu ∧ snd tu) (map_prod I I tu)"
| "I (C tu) = False"
| "I (L t) = False"
| "I (L' t) = False"
| "I (R t) = False"
| "I (R' t) = False"
| "I (A tuv) = False"
| "I (A' tuv) = False"
fun F :: "'a term ⇒ 'a term"
where "F (T (T (a, b), c)) = A (a, b, c)"
| "F (T (U, b)) = L b"
| "F (T (a, U)) = R a"
| "F (T (a, b)) = (if I (F a) then T (a, F b) else T (F a, b))"
| "F a = a"
I would like to prove the following lemma, which (hopefully) says that
if we don't match the first three cases in the definition of F, then
F (T (a, b)) is governed by the fourth case.
lemma
assumes "¬is_T a" and "a ≠ U" and "b ≠ U"
shows "F (T (a, b)) = (if I (F a) then T (a, F b) else T (F a, b))"
sorry
I have not been successful at getting the system to prove this. The definition
of F expands into a substantial number of cases, and I don't know how to
guide the system through these cases, have it eliminate the ones that are
ruled out by the hypotheses, and verify the stated conclusion for the remaining
ones. I don't really want to type a long proof that involves the manual
enumeration of each of the cases in the expansion of F.
I have tried various reformulations of the definitions, but pretty much keep
getting stuck on the same thing. Hopefully someone on the list can give me
a hint as to how I could approach this. Thanks for any help you can offer.
- Gene Stark
Question.thy
Email Gateway (Aug 22 2022 at 14:17):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Gene,
how about
using assms by (cases a; cases b; simp)
Dmitriy
Email Gateway (Aug 22 2022 at 14:17):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Well then, that is another trick for my toolbox.
Thank you very much!
- Gene Stark
Last updated: Nov 21 2024 at 12:39 UTC