*To*: <stark at cs.stonybrook.edu>*Subject*: Re: [isabelle] A question on datatypes and functions*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Tue, 18 Oct 2016 10:14:25 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1bc0caf0-bffe-51a5-bee5-48e6a609a6fc@starkeffect.com>*References*: <1bc0caf0-bffe-51a5-bee5-48e6a609a6fc@starkeffect.com>

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

**Follow-Ups**:**Re: [isabelle] A question on datatypes and functions***From:*Eugene W. Stark

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

- Previous by Date: [isabelle] A question on datatypes and functions
- Next by Date: Re: [isabelle] A question on datatypes and functions
- Previous by Thread: [isabelle] A question on datatypes and functions
- 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