*To*: Alfio Martini <alfio.martini at acm.org>*Subject*: Re: [isabelle] Knaster-Tarski Lemma*From*: Peter Lammich <lammich at in.tum.de>*Date*: Sat, 30 Nov 2013 17:55:13 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAAPnxw1gW58j-yTK+gjmHmJavvtemZpKTfo3M1GBCSaVMj7qrw@mail.gmail.com>*References*: <CAAPnxw2KDm6B16iD_r7JHrrahEK8e34wPbVgzz9-xCWovCcZEQ@mail.gmail.com> <CAAPnxw1gW58j-yTK+gjmHmJavvtemZpKTfo3M1GBCSaVMj7qrw@mail.gmail.com>

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

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

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