*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Knaster-Tarski Lemma*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Sat, 30 Nov 2013 11:26:23 -0200*In-reply-to*: <CAAPnxw2KDm6B16iD_r7JHrrahEK8e34wPbVgzz9-xCWovCcZEQ@mail.gmail.com>*References*: <CAAPnxw2KDm6B16iD_r7JHrrahEK8e34wPbVgzz9-xCWovCcZEQ@mail.gmail.com>*Sender*: alfio.martini at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Knaster-Tarski Lemma***From:*Tobias Nipkow

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

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

- Previous by Date: Re: [isabelle] Accessing slightly old versions of Isabelle
- Next by Date: Re: [isabelle] Knaster-Tarski Lemma
- Previous by Thread: [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