[isabelle] A Quantification Binding Question


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)

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.


  Richard Warburton

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