Re: [isabelle] pattern matching

Chris Capel wrote:
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.

??? Aren't x and y implicitly universally quantified over the _whole_ rule ?
That is (since they don't appear after the ==>, they are implicitly _existentially_ quantified where they appear).

BTW, you seem to be overloading 'n'.
Is there a better way to do this? Is there maybe a way to get the
second example to work?

What exactly happens when you try the second way?


Chris Capel

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