# HG changeset patch
# User wenzelm
# Date 933107607 -7200
# Node ID 25a4e864be9c98613211be2e7a0624a81aa0f936
# Parent  6c943cedc613d0fb348444d2a15b7ae82af7dbfd
*** empty log message ***

diff -r 6c943cedc613 -r 25a4e864be9c src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Tue Jul 27 22:32:22 1999 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(*  Title:      HOL/ex/Tarski
-    ID:         $Id$
-    Author:     Florian Kammueller, Cambridge University Computer Laboratory
-    Copyright   1999  University of Cambridge
-
-Minimal version of lattice theory plus the full theorem of Tarski:
-   The fixedpoints of a complete lattice themselves form a complete lattice.
-
-Illustrates first-class theories, using the Sigma representation of structures
-*)
-
-Tarski = Main + 
-
-
-record 'a potype = 
-  pset  :: "'a set"
-  order :: "('a * 'a) set"
-
-syntax
-  "@pset" :: "'a potype => 'a set"             ("_ .<A>"  [90] 90)
-  "@order" :: "'a potype => ('a *'a)set"       ("_ .<r>"  [90] 90) 
-
-translations
-  "po.<A>" == "pset po"
-  "po.<r>" == "order po"
-
-constdefs
-  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
-    "monotone f A r == ! x: A. ! y: A. (x, y): r --> ((f x), (f y)) : r"
-
-  least :: "['a => bool, 'a potype] => 'a"
-   "least P po == @ x. x: po.<A> & P x &
-                       (! y: po.<A>. P y --> (x,y): po.<r>)"
-
-  greatest :: "['a => bool, 'a potype] => 'a"
-   "greatest P po == @ x. x: po.<A> & P x &
-                          (! y: po.<A>. P y --> (y,x): po.<r>)"
-
-  lub  :: "['a set, 'a potype] => 'a"
-   "lub S po == least (%x. ! y: S. (y,x): po.<r>) po"
-
-  glb  :: "['a set, 'a potype] => 'a"
-   "glb S po == greatest (%x. ! y: S. (x,y): po.<r>) po"
-
-  islub :: "['a set, 'a potype, 'a] => bool"
-   "islub S po == %L. (L: po.<A> & (! y: S. (y,L): po.<r>) &
-                      (! z:po.<A>. (! y: S. (y,z): po.<r>) --> (L,z): po.<r>))"
-
-  isglb :: "['a set, 'a potype, 'a] => bool"
-   "isglb S po == %G. (G: po.<A> & (! y: S. (G,y): po.<r>) &
-                     (! z: po.<A>. (! y: S. (z,y): po.<r>) --> (z,G): po.<r>))"
-
-  fix    :: "[('a => 'a), 'a set] => 'a set"
-   "fix f A  == {x. x: A & f x = x}"
-
-  interval :: "[('a*'a) set,'a, 'a ] => 'a set"
-   "interval r a b == {x. (a,x): r & (x,b): r}"
-
-
-constdefs
-  Bot :: "'a potype => 'a"
-   "Bot po == least (%x. True) po"
-
-  Top :: "'a potype => 'a"
-   "Top po == greatest (%x. True) po"
-
-  PartialOrder :: "('a potype) set"
-   "PartialOrder == {P. refl (P.<A>) (P.<r>) & antisym (P.<r>) &
-		        trans (P.<r>)}"
-
-  CompleteLattice :: "('a potype) set"
-   "CompleteLattice == {cl. cl: PartialOrder & 
-			(! S. S <= cl.<A> --> (? L. islub S cl L)) &
-			(! S. S <= cl.<A> --> (? G. isglb S cl G))}"
-
-  CLF :: "('a potype * ('a => 'a)) set"
-   "CLF == SIGMA cl: CompleteLattice.
-             {f. f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)}"
-  
-  induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
-   "induced A r == {(a,b). a : A & b: A & (a,b): r}"
-
-
-
-
-constdefs
-  sublattice :: "('a potype * 'a set)set"
-   "sublattice == 
-      SIGMA cl: CompleteLattice.
-          {S. S <= cl.<A> &
-	   (| pset = S, order = induced S (cl.<r>) |): CompleteLattice }"
-
-syntax
-  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
-
-translations
-  "S <<= cl" == "S : sublattice ^^ {cl}"
-
-constdefs
-  dual :: "'a potype => 'a potype"
-   "dual po == (| pset = po.<A>, order = converse (po.<r>) |)"
-
-locale PO = 
-fixes 
-  cl :: "'a potype"
-  A  :: "'a set"
-  r  :: "('a * 'a) set"
-assumes 
-  cl_po  "cl : PartialOrder"
-defines
-  A_def "A == cl.<A>"
-  r_def "r == cl.<r>"
-
-locale CL = PO +
-fixes 
-assumes 
-  cl_co  "cl : CompleteLattice"
-
-locale CLF = CL +
-fixes
-  f :: "'a => 'a"
-  P :: "'a set"
-assumes 
-  f_cl "f : CLF ^^{cl}"
-defines
-  P_def "P == fix f A"
-
-
-locale Tarski = CLF + 
-fixes
-  Y :: "'a set"
-  intY1 :: "'a set"
-  v     :: "'a"
-assumes
-  Y_ss "Y <= P"
-defines
-  intY1_def "intY1 == interval r (lub Y cl) (Top cl)"
-  v_def "v == glb {x. ((lam x: intY1. f x) x, x): induced intY1 r & x: intY1}
-	          (| pset=intY1, order=induced intY1 r|)"
-
-end