*To*: Richard Warburton <richard.warburton at gmail.com>*Subject*: Re: [isabelle] A Quantification Binding Question*From*: Mathieu Giorgino <giorgino at irit.fr>*Date*: Thu, 7 May 2009 13:37:18 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <749b5dd60905060746k1b5c2237w90b9d04db9250150@mail.gmail.com>*References*: <749b5dd60905060746k1b5c2237w90b9d04db9250150@mail.gmail.com>*Sender*: clej37 at gmail.com

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 > >

**References**:**[isabelle] A Quantification Binding Question***From:*Richard Warburton

- Previous by Date: Re: [isabelle] Extensions to the basic Isabelle/HOL theories
- Next by Date: Re: [isabelle] A Quantification Binding Question
- Previous by Thread: [isabelle] A Quantification Binding Question
- Next by Thread: Re: [isabelle] A Quantification Binding Question
- Cl-isabelle-users May 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list