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