[isabelle] pattern matching

I'm trying to define an inductive set of type "token list set", where
"token" is just some datatype. Initially I had definitions along the
lines of this:

datatype token = C1 nat | C2 nat

inductive_set P where
base: "[C1 1, C2 2] : P" |
other: "ws @ [C1 x, C2 y] @ zs : P ==> ws @ [C1 x, C1 m, C2 n, C2 y] @ zs : P"

This is a clear, correct way of defining it. However, it's not at
*all* easy to work with when proving membership, whether forwards or
backwards, because of the need to break of the list one is unifying
with before applying the rule. So I tried changing it to this:

inductive_set P where
base: "[C1 1, C2 2] : P" |
other: "[| base : P; take 2 (drop n base) = [C1 x, C2 y] |] ==>
insert_list [C1 m, C2 n] base (n + 1) : P"

("insert_list x y n" puts x into y at n.) This definition, besides
being less clear, doesn't actually work, as "= [x, y]" doesn't perform
pattern matching. Instead, the equality asserts that (take a b) = [x,
y] for any x and y, which is obviously not true.

Is there a better way to do this? Is there maybe a way to get the
second example to work?

Chris Capel
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)

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