*To*: Richard Warburton <richard.warburton at gmail.com>*Subject*: Re: [isabelle] A Quantification Binding Question*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 7 May 2009 11:02:36 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <749b5dd60905060746k1b5c2237w90b9d04db9250150@mail.gmail.com>*References*: <749b5dd60905060746k1b5c2237w90b9d04db9250150@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

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, - Brian On Wed, May 6, 2009 at 7:46 AM, Richard Warburton < richard.warburton at gmail.com> wrote: > 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] A Quantification Binding Question
- Next by Date: Re: [isabelle] Extensions to the basic Isabelle/HOL theories
- Previous by Thread: Re: [isabelle] A Quantification Binding Question
- Next by Thread: [isabelle] Extensions to the basic Isabelle/HOL theories
- 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