[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)
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and