Re: [isabelle] Knaster-Tarski Lemma



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!


On Sun, Dec 1, 2013 at 1:24 PM, Makarius <makarius at sketis.net> wrote:

> On Sat, 30 Nov 2013, Alfio Martini wrote:
>
>  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
>>
>
> 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




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