Re: [isabelle] Knaster-Tarski Lemma



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






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