Re: [isabelle] how is one supposed to get !!x. p(x) from p(?x)



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
>





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