Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Knaster-Tarski Lemma

view this post on Zulip Email Gateway (Aug 19 2022 at 12:46):

From: Alfio Martini <alfio.martini@acm.org>
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)
Knaster_Tarski.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 12:46):

From: Alfio Martini <alfio.martini@acm.org>
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!

view this post on Zulip Email Gateway (Aug 19 2022 at 12:47):

From: Tobias Nipkow <nipkow@in.tum.de>
Am 30/11/2013 14:26, schrieb Alfio Martini:

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.

It is hidden (no_notation) in Main.
You can get it back by importing Library/Lattice_Syntax.

Tobias

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

view this post on Zulip Email Gateway (Aug 19 2022 at 12:47):

From: Peter Lammich <lammich@in.tum.de>
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.

view this post on Zulip Email Gateway (Aug 19 2022 at 12:47):

From: Alfio Martini <alfio.martini@acm.org>
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!

view this post on Zulip Email Gateway (Aug 19 2022 at 13:09):

From: Makarius <makarius@sketis.net>
A fully authentic version of the example is
$ISABELLE_HOME/src/HOL/Isar_Examples/Knaster_Tarski.thy

The "printed" versions in papers and slides that appeared over the years
occasionally vary in some requirements of notation, or even some implicit
rule declarations for lattice theory.

Note that this example was the first non-trivial Isar proof in history.
The Isar proof before it was for "A --> A", the one after it the
Hahn-Banach Theorem formalized by Gertrud Bauer on 40 pages.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 13:11):

From: Alfio Martini <alfio.martini@acm.org>
Thanks Makarius. If only I had remembered to take a look at this folder
from the start, I would have
saved myself a couple of hours (to put it mildly)...

Best!

view this post on Zulip Email Gateway (Aug 19 2022 at 13:11):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Alfio,

This squared syntax is a special »feature« of Lattices.thy and
Complete_Lattice.thy. There has been some discussion whether it should
be removed there, but this never evolved into some kind of action.

Hope this helps,
Florian
signature.asc

Last updated: Apr 26 2024 at 04:17 UTC