# [isabelle] Knaster-Tarski Lemma

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

Attachment: Knaster_Tarski.thy
Description: Binary data

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