Re: [isabelle] A question on datatypes and functions



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.