Re: [isabelle] A question on datatypes and functions
> On 18 Oct 2016, at 09:54, Eugene W. Stark <isabelle-users at starkeffect.com> wrote:
> 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.
> 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))"
> 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.
using assms by (cases a; cases b; simp)
This archive was generated by a fusion of
Pipermail (Mailman edition) and