*To*: Peter Lammich <lammich at in.tum.de>, Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Knaster-Tarski Lemma*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Sat, 30 Nov 2013 15:42:39 -0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <1385830513.2487.37.camel@lapbroy33>*References*: <CAAPnxw2KDm6B16iD_r7JHrrahEK8e34wPbVgzz9-xCWovCcZEQ@mail.gmail.com> <CAAPnxw1gW58j-yTK+gjmHmJavvtemZpKTfo3M1GBCSaVMj7qrw@mail.gmail.com> <1385830513.2487.37.camel@lapbroy33>*Sender*: alfio.martini at gmail.com

Thanks Peter and Tobias, However, even after importing Lattice_Syntax it is still necessary to provide the following declaration notation less_eq (infix "⊑" 50) Its is hidden (via no_notation) at the end of Complete_Lattice and not available in Lattice_Syntax.thy Best! On Sat, Nov 30, 2013 at 2:55 PM, Peter Lammich <lammich at in.tum.de> wrote: > The syntax is explicitly hidden at the end of Complete_Lattice.thy. > However, there is a theory "~~/src/HOL/Library/Lattice_Syntax". > Importing this theory gives you all the fancy lattice syntax. > > -- > Peter > > On Sa, 2013-11-30 at 11:26 -0200, Alfio Martini wrote: > > 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. > > > > 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 > > > > > > > > > > > > -- 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

**Re: [isabelle] Knaster-Tarski Lemma***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Knaster-Tarski Lemma
- Next by Date: Re: [isabelle] Isabelle2013-2-RC2 available for testing
- Previous 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