1.1 --- a/src/HOL/ex/Tarski.thy Tue Jul 27 22:32:22 1999 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,141 +0,0 @@
1.4 -(* Title: HOL/ex/Tarski
1.5 - ID: $Id$
1.6 - Author: Florian Kammueller, Cambridge University Computer Laboratory
1.7 - Copyright 1999 University of Cambridge
1.8 -
1.9 -Minimal version of lattice theory plus the full theorem of Tarski:
1.10 - The fixedpoints of a complete lattice themselves form a complete lattice.
1.11 -
1.12 -Illustrates first-class theories, using the Sigma representation of structures
1.13 -*)
1.14 -
1.15 -Tarski = Main +
1.16 -
1.17 -
1.18 -record 'a potype =
1.19 - pset :: "'a set"
1.20 - order :: "('a * 'a) set"
1.21 -
1.22 -syntax
1.23 - "@pset" :: "'a potype => 'a set" ("_ .<A>" [90] 90)
1.24 - "@order" :: "'a potype => ('a *'a)set" ("_ .<r>" [90] 90)
1.25 -
1.26 -translations
1.27 - "po.<A>" == "pset po"
1.28 - "po.<r>" == "order po"
1.29 -
1.30 -constdefs
1.31 - monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
1.32 - "monotone f A r == ! x: A. ! y: A. (x, y): r --> ((f x), (f y)) : r"
1.33 -
1.34 - least :: "['a => bool, 'a potype] => 'a"
1.35 - "least P po == @ x. x: po.<A> & P x &
1.36 - (! y: po.<A>. P y --> (x,y): po.<r>)"
1.37 -
1.38 - greatest :: "['a => bool, 'a potype] => 'a"
1.39 - "greatest P po == @ x. x: po.<A> & P x &
1.40 - (! y: po.<A>. P y --> (y,x): po.<r>)"
1.41 -
1.42 - lub :: "['a set, 'a potype] => 'a"
1.43 - "lub S po == least (%x. ! y: S. (y,x): po.<r>) po"
1.44 -
1.45 - glb :: "['a set, 'a potype] => 'a"
1.46 - "glb S po == greatest (%x. ! y: S. (x,y): po.<r>) po"
1.47 -
1.48 - islub :: "['a set, 'a potype, 'a] => bool"
1.49 - "islub S po == %L. (L: po.<A> & (! y: S. (y,L): po.<r>) &
1.50 - (! z:po.<A>. (! y: S. (y,z): po.<r>) --> (L,z): po.<r>))"
1.51 -
1.52 - isglb :: "['a set, 'a potype, 'a] => bool"
1.53 - "isglb S po == %G. (G: po.<A> & (! y: S. (G,y): po.<r>) &
1.54 - (! z: po.<A>. (! y: S. (z,y): po.<r>) --> (z,G): po.<r>))"
1.55 -
1.56 - fix :: "[('a => 'a), 'a set] => 'a set"
1.57 - "fix f A == {x. x: A & f x = x}"
1.58 -
1.59 - interval :: "[('a*'a) set,'a, 'a ] => 'a set"
1.60 - "interval r a b == {x. (a,x): r & (x,b): r}"
1.61 -
1.62 -
1.63 -constdefs
1.64 - Bot :: "'a potype => 'a"
1.65 - "Bot po == least (%x. True) po"
1.66 -
1.67 - Top :: "'a potype => 'a"
1.68 - "Top po == greatest (%x. True) po"
1.69 -
1.70 - PartialOrder :: "('a potype) set"
1.71 - "PartialOrder == {P. refl (P.<A>) (P.<r>) & antisym (P.<r>) &
1.72 - trans (P.<r>)}"
1.73 -
1.74 - CompleteLattice :: "('a potype) set"
1.75 - "CompleteLattice == {cl. cl: PartialOrder &
1.76 - (! S. S <= cl.<A> --> (? L. islub S cl L)) &
1.77 - (! S. S <= cl.<A> --> (? G. isglb S cl G))}"
1.78 -
1.79 - CLF :: "('a potype * ('a => 'a)) set"
1.80 - "CLF == SIGMA cl: CompleteLattice.
1.81 - {f. f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)}"
1.82 -
1.83 - induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
1.84 - "induced A r == {(a,b). a : A & b: A & (a,b): r}"
1.85 -
1.86 -
1.87 -
1.88 -
1.89 -constdefs
1.90 - sublattice :: "('a potype * 'a set)set"
1.91 - "sublattice ==
1.92 - SIGMA cl: CompleteLattice.
1.93 - {S. S <= cl.<A> &
1.94 - (| pset = S, order = induced S (cl.<r>) |): CompleteLattice }"
1.95 -
1.96 -syntax
1.97 - "@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
1.98 -
1.99 -translations
1.100 - "S <<= cl" == "S : sublattice ^^ {cl}"
1.101 -
1.102 -constdefs
1.103 - dual :: "'a potype => 'a potype"
1.104 - "dual po == (| pset = po.<A>, order = converse (po.<r>) |)"
1.105 -
1.106 -locale PO =
1.107 -fixes
1.108 - cl :: "'a potype"
1.109 - A :: "'a set"
1.110 - r :: "('a * 'a) set"
1.111 -assumes
1.112 - cl_po "cl : PartialOrder"
1.113 -defines
1.114 - A_def "A == cl.<A>"
1.115 - r_def "r == cl.<r>"
1.116 -
1.117 -locale CL = PO +
1.118 -fixes
1.119 -assumes
1.120 - cl_co "cl : CompleteLattice"
1.121 -
1.122 -locale CLF = CL +
1.123 -fixes
1.124 - f :: "'a => 'a"
1.125 - P :: "'a set"
1.126 -assumes
1.127 - f_cl "f : CLF ^^{cl}"
1.128 -defines
1.129 - P_def "P == fix f A"
1.130 -
1.131 -
1.132 -locale Tarski = CLF +
1.133 -fixes
1.134 - Y :: "'a set"
1.135 - intY1 :: "'a set"
1.136 - v :: "'a"
1.137 -assumes
1.138 - Y_ss "Y <= P"
1.139 -defines
1.140 - intY1_def "intY1 == interval r (lub Y cl) (Top cl)"
1.141 - v_def "v == glb {x. ((lam x: intY1. f x) x, x): induced intY1 r & x: intY1}
1.142 - (| pset=intY1, order=induced intY1 r|)"
1.143 -
1.144 -end