[isabelle] A question on datatypes and functions



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.

						- Gene Stark
theory Question
imports Main
begin

    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 \<Rightarrow> bool"
    where "I (V x) = True"
        | "I U = True"
        | "I (T tu) = (\<lambda>tu. fst tu \<and> 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 \<Rightarrow> '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"

    lemma
    assumes "\<not>is_T a" and "a \<noteq> U" and "b \<noteq> U"
    shows "F (T (a, b)) = (if I (F a) then T (a, F b) else T (F a, b))"
      sorry

end


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