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