Re: [isabelle] A Quantification Binding Question



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

2009/5/6 Richard Warburton <richard.warburton at 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
>
>




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