*To*: Chris Capel <pdf23ds at gmail.com>*Subject*: Re: [isabelle] pattern matching*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Mon, 09 Feb 2009 08:13:16 +1100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <737b61f30902070015w64ef9d75ma5eaaf1dec36144f@mail.gmail.com>*References*: <737b61f30902070015w64ef9d75ma5eaaf1dec36144f@mail.gmail.com>*User-agent*: Thunderbird 1.5.0.12 (X11/20070604)

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 ?

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? Jeremy

Chris Capel

**Follow-Ups**:**Re: [isabelle] pattern matching***From:*Chris Capel

**References**:**[isabelle] pattern matching***From:*Chris Capel

- Previous by Date: Re: [isabelle] pattern matching
- Next by Date: Re: [isabelle] pattern matching
- Previous by Thread: Re: [isabelle] pattern matching
- Next by Thread: Re: [isabelle] pattern matching
- Cl-isabelle-users February 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list