*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] A question on datatypes and functions*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Tue, 18 Oct 2016 03:54:47 -0400*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

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

theory Question imports Main begin 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 \<Rightarrow> bool" where "I (V x) = True" | "I U = True" | "I (T tu) = (\<lambda>tu. fst tu \<and> 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 \<Rightarrow> '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" lemma assumes "\<not>is_T a" and "a \<noteq> U" and "b \<noteq> U" shows "F (T (a, b)) = (if I (F a) then T (a, F b) else T (F a, b))" sorry end

**Follow-Ups**:**Re: [isabelle] A question on datatypes and functions***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Exception Chr raised while processing "fun" (Isabelle 2016)
- Next by Date: Re: [isabelle] A question on datatypes and functions
- Previous by Thread: Re: [isabelle] Transfer: types in skeleton are too specific
- Next by Thread: Re: [isabelle] A question on datatypes and functions
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list