src/HOL/ex/Tarski.thy
author wenzelm
Tue Jul 27 22:34:11 1999 +0200 (1999-07-27)
changeset 7112 b142788d79e8
child 10797 028d22926a41
permissions -rw-r--r--
back again, supposedly with correct perms;
wenzelm@7112
     1
(*  Title:      HOL/ex/Tarski
wenzelm@7112
     2
    ID:         $Id$
wenzelm@7112
     3
    Author:     Florian Kammueller, Cambridge University Computer Laboratory
wenzelm@7112
     4
    Copyright   1999  University of Cambridge
wenzelm@7112
     5
wenzelm@7112
     6
Minimal version of lattice theory plus the full theorem of Tarski:
wenzelm@7112
     7
   The fixedpoints of a complete lattice themselves form a complete lattice.
wenzelm@7112
     8
wenzelm@7112
     9
Illustrates first-class theories, using the Sigma representation of structures
wenzelm@7112
    10
*)
wenzelm@7112
    11
wenzelm@7112
    12
Tarski = Main + 
wenzelm@7112
    13
wenzelm@7112
    14
wenzelm@7112
    15
record 'a potype = 
wenzelm@7112
    16
  pset  :: "'a set"
wenzelm@7112
    17
  order :: "('a * 'a) set"
wenzelm@7112
    18
wenzelm@7112
    19
syntax
wenzelm@7112
    20
  "@pset" :: "'a potype => 'a set"             ("_ .<A>"  [90] 90)
wenzelm@7112
    21
  "@order" :: "'a potype => ('a *'a)set"       ("_ .<r>"  [90] 90) 
wenzelm@7112
    22
wenzelm@7112
    23
translations
wenzelm@7112
    24
  "po.<A>" == "pset po"
wenzelm@7112
    25
  "po.<r>" == "order po"
wenzelm@7112
    26
wenzelm@7112
    27
constdefs
wenzelm@7112
    28
  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
wenzelm@7112
    29
    "monotone f A r == ! x: A. ! y: A. (x, y): r --> ((f x), (f y)) : r"
wenzelm@7112
    30
wenzelm@7112
    31
  least :: "['a => bool, 'a potype] => 'a"
wenzelm@7112
    32
   "least P po == @ x. x: po.<A> & P x &
wenzelm@7112
    33
                       (! y: po.<A>. P y --> (x,y): po.<r>)"
wenzelm@7112
    34
wenzelm@7112
    35
  greatest :: "['a => bool, 'a potype] => 'a"
wenzelm@7112
    36
   "greatest P po == @ x. x: po.<A> & P x &
wenzelm@7112
    37
                          (! y: po.<A>. P y --> (y,x): po.<r>)"
wenzelm@7112
    38
wenzelm@7112
    39
  lub  :: "['a set, 'a potype] => 'a"
wenzelm@7112
    40
   "lub S po == least (%x. ! y: S. (y,x): po.<r>) po"
wenzelm@7112
    41
wenzelm@7112
    42
  glb  :: "['a set, 'a potype] => 'a"
wenzelm@7112
    43
   "glb S po == greatest (%x. ! y: S. (x,y): po.<r>) po"
wenzelm@7112
    44
wenzelm@7112
    45
  islub :: "['a set, 'a potype, 'a] => bool"
wenzelm@7112
    46
   "islub S po == %L. (L: po.<A> & (! y: S. (y,L): po.<r>) &
wenzelm@7112
    47
                      (! z:po.<A>. (! y: S. (y,z): po.<r>) --> (L,z): po.<r>))"
wenzelm@7112
    48
wenzelm@7112
    49
  isglb :: "['a set, 'a potype, 'a] => bool"
wenzelm@7112
    50
   "isglb S po == %G. (G: po.<A> & (! y: S. (G,y): po.<r>) &
wenzelm@7112
    51
                     (! z: po.<A>. (! y: S. (z,y): po.<r>) --> (z,G): po.<r>))"
wenzelm@7112
    52
wenzelm@7112
    53
  fix    :: "[('a => 'a), 'a set] => 'a set"
wenzelm@7112
    54
   "fix f A  == {x. x: A & f x = x}"
wenzelm@7112
    55
wenzelm@7112
    56
  interval :: "[('a*'a) set,'a, 'a ] => 'a set"
wenzelm@7112
    57
   "interval r a b == {x. (a,x): r & (x,b): r}"
wenzelm@7112
    58
wenzelm@7112
    59
wenzelm@7112
    60
constdefs
wenzelm@7112
    61
  Bot :: "'a potype => 'a"
wenzelm@7112
    62
   "Bot po == least (%x. True) po"
wenzelm@7112
    63
wenzelm@7112
    64
  Top :: "'a potype => 'a"
wenzelm@7112
    65
   "Top po == greatest (%x. True) po"
wenzelm@7112
    66
wenzelm@7112
    67
  PartialOrder :: "('a potype) set"
wenzelm@7112
    68
   "PartialOrder == {P. refl (P.<A>) (P.<r>) & antisym (P.<r>) &
wenzelm@7112
    69
		        trans (P.<r>)}"
wenzelm@7112
    70
wenzelm@7112
    71
  CompleteLattice :: "('a potype) set"
wenzelm@7112
    72
   "CompleteLattice == {cl. cl: PartialOrder & 
wenzelm@7112
    73
			(! S. S <= cl.<A> --> (? L. islub S cl L)) &
wenzelm@7112
    74
			(! S. S <= cl.<A> --> (? G. isglb S cl G))}"
wenzelm@7112
    75
wenzelm@7112
    76
  CLF :: "('a potype * ('a => 'a)) set"
wenzelm@7112
    77
   "CLF == SIGMA cl: CompleteLattice.
wenzelm@7112
    78
             {f. f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)}"
wenzelm@7112
    79
  
wenzelm@7112
    80
  induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
wenzelm@7112
    81
   "induced A r == {(a,b). a : A & b: A & (a,b): r}"
wenzelm@7112
    82
wenzelm@7112
    83
wenzelm@7112
    84
wenzelm@7112
    85
wenzelm@7112
    86
constdefs
wenzelm@7112
    87
  sublattice :: "('a potype * 'a set)set"
wenzelm@7112
    88
   "sublattice == 
wenzelm@7112
    89
      SIGMA cl: CompleteLattice.
wenzelm@7112
    90
          {S. S <= cl.<A> &
wenzelm@7112
    91
	   (| pset = S, order = induced S (cl.<r>) |): CompleteLattice }"
wenzelm@7112
    92
wenzelm@7112
    93
syntax
wenzelm@7112
    94
  "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
wenzelm@7112
    95
wenzelm@7112
    96
translations
wenzelm@7112
    97
  "S <<= cl" == "S : sublattice ^^ {cl}"
wenzelm@7112
    98
wenzelm@7112
    99
constdefs
wenzelm@7112
   100
  dual :: "'a potype => 'a potype"
wenzelm@7112
   101
   "dual po == (| pset = po.<A>, order = converse (po.<r>) |)"
wenzelm@7112
   102
wenzelm@7112
   103
locale PO = 
wenzelm@7112
   104
fixes 
wenzelm@7112
   105
  cl :: "'a potype"
wenzelm@7112
   106
  A  :: "'a set"
wenzelm@7112
   107
  r  :: "('a * 'a) set"
wenzelm@7112
   108
assumes 
wenzelm@7112
   109
  cl_po  "cl : PartialOrder"
wenzelm@7112
   110
defines
wenzelm@7112
   111
  A_def "A == cl.<A>"
wenzelm@7112
   112
  r_def "r == cl.<r>"
wenzelm@7112
   113
wenzelm@7112
   114
locale CL = PO +
wenzelm@7112
   115
fixes 
wenzelm@7112
   116
assumes 
wenzelm@7112
   117
  cl_co  "cl : CompleteLattice"
wenzelm@7112
   118
wenzelm@7112
   119
locale CLF = CL +
wenzelm@7112
   120
fixes
wenzelm@7112
   121
  f :: "'a => 'a"
wenzelm@7112
   122
  P :: "'a set"
wenzelm@7112
   123
assumes 
wenzelm@7112
   124
  f_cl "f : CLF ^^{cl}"
wenzelm@7112
   125
defines
wenzelm@7112
   126
  P_def "P == fix f A"
wenzelm@7112
   127
wenzelm@7112
   128
wenzelm@7112
   129
locale Tarski = CLF + 
wenzelm@7112
   130
fixes
wenzelm@7112
   131
  Y :: "'a set"
wenzelm@7112
   132
  intY1 :: "'a set"
wenzelm@7112
   133
  v     :: "'a"
wenzelm@7112
   134
assumes
wenzelm@7112
   135
  Y_ss "Y <= P"
wenzelm@7112
   136
defines
wenzelm@7112
   137
  intY1_def "intY1 == interval r (lub Y cl) (Top cl)"
wenzelm@7112
   138
  v_def "v == glb {x. ((lam x: intY1. f x) x, x): induced intY1 r & x: intY1}
wenzelm@7112
   139
	          (| pset=intY1, order=induced intY1 r|)"
wenzelm@7112
   140
wenzelm@7112
   141
end