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.
>>
>>    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
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.