*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] how is one supposed to get !!x. p(x) from p(?x)*From*: Andrei Borac <zerosum42 at gmail.com>*Date*: Wed, 12 May 2010 11:57:10 -0700*In-reply-to*: <AANLkTilsRoXLMbBlypQKFn1gw_aHM1F6Vzltt5OLS75x@mail.gmail.com>*References*: <AANLkTilsRoXLMbBlypQKFn1gw_aHM1F6Vzltt5OLS75x@mail.gmail.com>

Ok, second attempt; I have found a more accurate way to represent the problem. Sorry that the title is incorrect (it's p(some x) from !!x. p(x)). Anyways, here is what is actually not working: consts f :: "nat list => nat => nat option" consts g :: "nat list => nat => nat option" lemma False apply(subgoal_tac " !!context param value. [| !!param_any. f context param_any = Some value ==> (case (g context param_any) of None => 0 | Some value_some => value_some) = value; g context param = None; f context param = Some value |] ==> value = 0") defer Resulting in the first subgoal: !!context param value. [| !!param_any. f context param_any = Some value ==> (case g context param_any of None => 0 | Some value_some => value_some) = value; g context param = None; f context param = Some value |] ==> value = 0 where all variables are green. Now it seems like setting "param_any" to "param" should work. We know that "f" produced something and that the case of "g" is None, so we should get value = 0, as required. However, clarsimp will not do it (and I can't seem to be able to split the option in my apply-style proof). What will work (or why can't it work ...)? -Andrei On Wed, May 12, 2010 at 12:54 AM, Andrei Borac <zerosum42 at gmail.com> wrote: > Ok, so I have a kind of "two-dimensional" induction that I'm trying to > do. Here is a stripped-down example that illustrates the difficulty: > > consts p :: "nat => nat => bool" > > lemma base: "(p 0 y)" > sorry (* lemma base: p 0 ?y *) > > lemma meta: "(p row col) ==> (p (row + 1) any_col)" > sorry (* lemma meta: p ?row ?col ==> p (?row + 1) ?any_col *) > > lemma half: "(!!col. (p row col)) ==> (p (row + 1) any_col)" > sorry (* lemma half: (!!col. p ?row col) ==> p (?row + 1) ?any_col *) > > lemma desired: "(p row col)" > > The base cases and inductive steps are simply "provided" using "sorry" > to keep the example simple. meta and half are basically the same thing > except in meta "col" is a meta-whatsitcalled or maybe > schematic-whatsitcalled. Now, after 3 hours of trial and error, I have > succeeded in providing the desired lemma: > > lemma helper: "!!row. (!!col. p row col) ==> p (Suc row) col" > apply(drule half[where any_col=col]) > apply(simp) > done (* lemma helper: (!!col. p ?row col) ==> p (Suc ?row) ?col *) > > lemma desired: "(p row col)" > apply(induct row arbitrary: col) > apply(simp add: base) > apply(simp add: helper) > done (* lemma desired: p ?row ?col *) > > So, how is this kind of thing -supposed- to be done? Is there a way to > apply something in the main proof to get this done without a helper > lemma? I was thinking the obvious thing is change it to subgoal_tac, > but so far all my attempts have been unsuccessful. Plus, it seems like > there should be an even better way. > > Thanks, > -Andrei >

**Follow-Ups**:**Re: [isabelle] how is one supposed to get !!x. p(x) from p(?x)***From:*Tobias Nipkow

**References**:**[isabelle] how is one supposed to get !!x. p(x) from p(?x)***From:*Andrei Borac

- Previous by Date: Re: [isabelle] Dependent types and existence of n-dimensional space.
- Next by Date: Re: [isabelle] Dependent types and existence of n-dimensional space.
- Previous by Thread: [isabelle] how is one supposed to get !!x. p(x) from p(?x)
- Next by Thread: Re: [isabelle] how is one supposed to get !!x. p(x) from p(?x)
- Cl-isabelle-users May 2010 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