*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Knaster-Tarski Lemma*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 30 Nov 2013 17:44:41 +0100*In-reply-to*: <CAAPnxw1gW58j-yTK+gjmHmJavvtemZpKTfo3M1GBCSaVMj7qrw@mail.gmail.com>*References*: <CAAPnxw2KDm6B16iD_r7JHrrahEK8e34wPbVgzz9-xCWovCcZEQ@mail.gmail.com> <CAAPnxw1gW58j-yTK+gjmHmJavvtemZpKTfo3M1GBCSaVMj7qrw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:24.0) Gecko/20100101 Thunderbird/24.1.1

Am 30/11/2013 14:26, schrieb Alfio Martini: > Dear Users, > > I solved the problem using the notation facility. But I am not sure what > this was necessary since > this syntax seems to be available in the theory Complete_Lattice. It does > not seem to be exported > though. It is hidden (no_notation) in Main. You can get it back by importing Library/Lattice_Syntax. Tobias > notation > less_eq (infix "⊑" 50) and > Inf ("⨅_" [900] 900) > > lemma Knaster_Tarski: > fixes f::"'a::complete_lattice ⇒ 'a" > assumes mono:"⋀ x y. x ⊑ y ⟹ f x ⊑ f y" > shows "f( ⨅ {x. f(x) ≤ x}) = ⨅ {x. f(x) ≤ x}" (is "f ?k = ?k") > proof - > have "f ?k ≤ ?k" (is " _ ≤ Inf ?P") > proof (rule Inf_greatest) > fix x0 assume "x0 ∈ ?P" > then have "?k ⊑ x0" by (rule Inf_lower) > from this and mono have "f(?k) ⊑ f(x0)" by simp > from `x0 ∈ ?P` have "f(x0) ⊑ x0" by simp > from `f(?k) ⊑ f(x0)` and this show "f(?k) ⊑ x0" by simp > qed > also have "?k ⊑ f(?k)" > proof (rule Inf_lower) > from mono and `f(?k) ≤ ?k` have "f(f ?k) ⊑ f(?k)" by simp > then show "f ?k ∈ ?P" by simp > qed > finally show "f ?k = ?k" by this > qed > > Best! > > > On Fri, Nov 29, 2013 at 9:21 PM, Alfio Martini <alfio.martini at acm.org>wrote: > >> Dear Isabelle Users, >> >> I typed a slightly different version of Makarius´s proof of Knaster-Tarski >> lemma >> according to his Orsay´s slides. Everything works fine but I >> have to use "Inf" instead of "\<Sqinter>" or "INF". Otherwise I get the >> error message "inner lexical error. Failed to parse proposition". >> Probably something related to a wrong use of this type class. >> >> lemma Knaster_Tarski: >> fixes f::"'a::complete_lattice⇒ 'a" >> assumes mono:"⋀ x y. x ≤ y ⟹ f x ≤ f y" >> shows "f( Inf {x. f(x) ≤ x}) = Inf {x. f(x) ≤ x}" (is "f ?k = ?k") >> proof - >> have "f ?k ≤ ?k" (is " _ ≤ Inf ?P") >> proof (rule Inf_greatest) >> fix x0 assume "x0 ∈ ?P" >> then have "?k ≤ x0" by (rule Inf_lower) >> from this and mono have "f(?k) ≤ f(x0)" by simp >> from `x0 ∈ ?P` have "f(x0) ≤ x0" by simp >> from `f(?k) ≤ f(x0)` and this show "f(?k) ≤ x0" by simp >> qed >> also have "?k ≤ f(?k)" >> proof (rule Inf_lower) >> from mono and `f(?k) ≤ ?k` have "f(f ?k) ≤ f(?k)" by simp >> then show "f ?k ∈ ?P" by simp >> qed >> finally show "f ?k = ?k" by this >> qed >> >> >> Thanks for any help on this (thy file attached) >> >> -- >> Alfio Ricardo Martini >> PhD in Computer Science (TU Berlin) >> www.inf.pucrs.br/alfio >> Lattes: http://lattes.cnpq.br/4016080665372277 >> Associate Professor at Faculty of Informatics (PUCRS) >> Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática >> 90619-900 -Porto Alegre - RS - Brasil >> > > >

**References**:**[isabelle] Knaster-Tarski Lemma***From:*Alfio Martini

**Re: [isabelle] Knaster-Tarski Lemma***From:*Alfio Martini

- Previous by Date: Re: [isabelle] Knaster-Tarski Lemma
- Next by Date: Re: [isabelle] Knaster-Tarski Lemma
- Previous by Thread: Re: [isabelle] Knaster-Tarski Lemma
- Next by Thread: Re: [isabelle] Knaster-Tarski Lemma
- Cl-isabelle-users November 2013 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