*To*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Subject*: Re: [isabelle] pattern matching*From*: Chris Capel <pdf23ds at gmail.com>*Date*: Sun, 8 Feb 2009 15:42:47 -0600*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <498F4AEC.2000407@rsise.anu.edu.au>*References*: <737b61f30902070015w64ef9d75ma5eaaf1dec36144f@mail.gmail.com> <498F4AEC.2000407@rsise.anu.edu.au>

On Sun, Feb 8, 2009 at 15:13, Jeremy Dawson <jeremy at rsise.anu.edu.au> wrote: > Chris Capel wrote: >> 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). I *believe* so, but I'm not sure. I didn't mean to imply otherwise. My point was that unification doesn't instantiate them. > BTW, you seem to be overloading 'n'. Oops. My actual theory does not do this. :) >> 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? Well, with some more testing I've seen that this will work (i.e. it's correct), but the problem is I have to manually instantiate x and y, whereas ideally they would be instantiated by unification. That was the same problem with the first formulation--manual instantiation of stuff that you would wish wasn't necessary. However, maybe, as per Tobias, I need to learn to do structured proofs. 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)

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

**Re: [isabelle] pattern matching***From:*Jeremy Dawson

- Previous by Date: Re: [isabelle] pattern matching
- Next by Date: [isabelle] Primrec
- Previous by Thread: Re: [isabelle] pattern matching
- Next by Thread: [isabelle] Primrec
- 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