Re: [isabelle] Knaster-Tarski Lemma



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.