Re: [isabelle] Knaster-Tarski Lemma



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.