*To*: traytel at inf.ethz.ch*Subject*: Re: [isabelle] A question on datatypes and functions*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Tue, 18 Oct 2016 06:06:52 -0400*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <2512BFB4-D049-403C-994D-E045A4E18BC5@inf.ethz.ch>*References*: <1bc0caf0-bffe-51a5-bee5-48e6a609a6fc@starkeffect.com> <2512BFB4-D049-403C-994D-E045A4E18BC5@inf.ethz.ch>*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

Well then, that is another trick for my toolbox. Thank you very much! - Gene Stark On 10/18/2016 04:14 AM, Dmitriy Traytel wrote: > Hi Gene, > >> 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. >> >> 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. > > how about > > using assms by (cases a; cases b; simp) > > Dmitriy > >

**References**:**[isabelle] A question on datatypes and functions***From:*Eugene W. Stark

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

- Previous by Date: Re: [isabelle] A question on datatypes and functions
- Next by Date: Re: [isabelle] Transfer: types in skeleton are too specific
- Previous by Thread: Re: [isabelle] A question on datatypes and functions
- Next by Thread: [isabelle] 2 new AFP entries
- 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