Re: [isabelle] A Quantification Binding Question
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
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,
On Wed, May 6, 2009 at 7:46 AM, Richard Warburton <
richard.warburton at gmail.com> wrote:
> 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
> apply (simp only: res_def)
> apply(split split_if)
> apply (simp)
> However, I really want to prove an equivalence between the functions f and
> 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.
> Richard Warburton
This archive was generated by a fusion of
Pipermail (Mailman edition) and