Email Gateway (Aug 18 2022 at 13:28): Email Gateway (Aug 18 2022 at 13:28):From: Mathieu Giorgino <giorgino@irit.fr>
Hi,
Written in this way, your lemma is equivalent to:
"(f d = g d ) & res f d x = res g d x --> f = g"
and so your assumptions are in fact :
f x = g x & f d = g d
Some ways to write it correctly are:
lemma Res_Split2: "ALL x. (f d = g d) & res f d x = res g d x ==> f = g"
lemma Res_Split2: "(f d = g d) & (ALL x. res f d x = res g d x) --> f = g"
lemma Res_Split2: "(f d = g d) & res f d = res g d --> f = g"
apply (clarsimp simp add:expand_fun_eq res_def)
apply (case_tac "x=d")
by simp_all
Regards,
Mathieu Giorgino
Email Gateway (Aug 18 2022 at 13:33):From: Richard Warburton <richard.warburton@gmail.com>
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
Email Gateway (Aug 18 2022 at 13:35):From: Brian Huffman <brianh@cs.pdx.edu>
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,
Last updated: May 03 2024 at 04:19 UTC