Re: [isabelle] pattern matching



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)





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