Re: [isabelle] A Quantification Binding Question



 Hi Richard,

I think that instead of
lemma Res_Split2: "ALL x. (f d = g d ) & res f d x = res g d x --> f = g"

What you really meant to say was
lemma Res_Split2: "(ALL x. (f d = g d ) & res f d x = res g d x) --> f = g"

Note the placement of the parentheses here; you really only want the
quantifier to range over the left side of the implication, not the whole
subgoal.

The parsing situation with quantification vs. implication is a little
confusing in Isabelle, because there are object-logic and meta-logic
versions of each. Here's a summary of how all the combinations are parsed:

"ALL x. P x --> Q x" is parsed as "ALL x. (P x --> Q x)"
"ALL x. P x ==> Q x" is parsed as "(ALL x. P x) ==> Q x"
"!!x. P x ==> Q x" is parsed as "!!x. (P x ==> Q x)"

Hope this helps,
- Brian

On Wed, May 6, 2009 at 7:46 AM, Richard Warburton <
richard.warburton at gmail.com> wrote:

> Hi,
>
> I have a simple definition for restricting functions:
>
> definition res :: "('a ~=> 'b) => 'a => 'a ~=> 'b" where
> "res f v x = (if (x=v) then None else (f x))"
>
> About which I've proved a lemma that allows me to seperate some pieces
> of information about the function:
>
> lemma Res_Split: "ALL x. (f d = g d ) & res f d x = res g d x --> f x = g
> x"
>  apply (simp only: res_def)
>  apply(split split_if)
>  apply (simp)
> done
>
> However, I really want to prove an equivalence between the functions f and
> g:
>
> lemma Res_Split2: "ALL x. (f d = g d ) & res f d x = res g d x --> f = g"
>
> The problem I keep running into when doing this is that I try to use
> extensionality of the functions f and g, I get a new binding scope
> (and thus a different x).  For example if I take the above lemma and
> 'apply (simp only: expand_fun_eq)' then it leaves with the following
> proof state:
>
> ALL x. f d = g d & res f d x = res g d x --> (ALL x. f x = g x)
>
> Apologies if I've missed something trivial here, but I can't see if
> there's a trick that can be used to reduce this state to Res_Split.
> Any help on the matter would be most appreciated.
>
> regards,
>
>  Richard Warburton
>
>




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