Re: [isabelle] pattern matching

Your second definition looks correct to me. But it is probably not much
easier to use than the first. I would stick to the first definition and
write structured proofs where you rearrange the list into the required
form (one simp step will do that) before apply the rule.


Chris Capel schrieb:
> 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

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