Re: [isabelle] A question on datatypes and functions
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.
>> 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.
> how about
> using assms by (cases a; cases b; simp)
This archive was generated by a fusion of
Pipermail (Mailman edition) and