*To*: Juan Antonio Navarro Pérez <juannavarroperez at gmail.com>*Subject*: Re: [isabelle] Simplification of unique elements*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 8 Dec 2009 14:30:49 -0800*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <6e8674ca0912080804g2b6d71a0k4e7acf90a4736742@mail.gmail.com>*References*: <6e8674ca0912080804g2b6d71a0k4e7acf90a4736742@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

2009/12/8 Juan Antonio Navarro Pérez <juannavarroperez at gmail.com>: > Suppose I have some unary predicate P, and I have proved that it has a > unique satisfying solution. That is, I prove the theorem: > > theorem unique [simp]: "[| P a; P b |] ==> a = b" > > It seems that, even after declaring the rule as a simplification, the > rule is not always applied by Isabelle. As an example, the following > proof attempt fails. > > theorem foo: "[| P a; P b |] ==> f a = f b" > apply (simp) Hi Juan, When you declare "unique" as a simp rule, Isabelle's simplifier immediately notices that it would cause looping in its original form. Instead, it uses this rule for simplification: "[| P a; P b |] ==> (a = b) == True" (I determined this by doing "simp add: unique" with "Trace Simplifier" enabled.) This modified form won't loop, but it is not sufficient to prove your theorem "foo". One possibility is to use "unique" with auto, as a dest rule: theorem foo: "[| P a; P b |] ==> f a = f b" by (auto dest: unique) The effect of "dest: unique" is that when auto finds "P a" and "P b" in the assumptions, it will remove "P a" and replace it by "a = b". Another possibility is to do some trickery with Isabelle's definite-choice operator. This method works using only ordinary simp rules, but you will need to prove existence as well as uniqueness, and it also requires the definition of an extra constant. lemma exists: "EX x. P x" sorry lemma exists1: "EX! x. P x" using exists unique by (rule ex_ex1I) definition "theP = (THE x. P x)" lemma P_iff: "P a = (a = theP)" unfolding theP_def apply safe apply (rule the1_equality [symmetric]) apply (rule exists1) apply assumption apply (rule theI') apply (rule exists1) done Unlike "unique", lemma "P_iff" is a well-behaved simp rule. theorem foo: "[| P a; P b |] ==> f a = f b" by (simp add: P_iff) Hope this helps, - Brian

**References**:**[isabelle] Simplification of unique elements***From:*Juan Antonio Navarro Pérez

- Previous by Date: [isabelle] Simplification of unique elements
- Next by Date: Re: [isabelle] Fwd: Re: Unicode tokens
- Previous by Thread: [isabelle] Simplification of unique elements
- Next by Thread: Re: [isabelle] Fwd: Re: Unicode tokens
- Cl-isabelle-users December 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