src/HOL/ex/Tarski.thy
 changeset 13585 db4005b40cc6 parent 13383 041d78bf9403 child 14569 78b75a9eec01
```     1.1 --- a/src/HOL/ex/Tarski.thy	Thu Sep 26 10:43:43 2002 +0200
1.2 +++ b/src/HOL/ex/Tarski.thy	Thu Sep 26 10:51:29 2002 +0200
1.3 @@ -1,12 +1,11 @@
1.4  (*  Title:      HOL/ex/Tarski.thy
1.5      ID:         \$Id\$
1.6      Author:     Florian Kammüller, Cambridge University Computer Laboratory
1.7 -    Copyright   1999  University of Cambridge
1.8  *)
1.9
1.10 -header {* The full theorem of Tarski *}
1.11 +header {* The Full Theorem of Tarski *}
1.12
1.13 -theory Tarski = Main:
1.14 +theory Tarski = Main + FuncSet:
1.15
1.16  text {*
1.17    Minimal version of lattice theory plus the full theorem of Tarski:
1.18 @@ -21,39 +20,31 @@
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 == \<forall>x\<in>A. \<forall>y\<in>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 -                       (\<forall>y \<in> po.<A>. P y --> (x,y): po.<r>)"
1.37 +  "least P po == @ x. x: pset po & P x &
1.38 +                       (\<forall>y \<in> pset po. P y --> (x,y): order po)"
1.39
1.40    greatest :: "['a => bool, 'a potype] => 'a"
1.41 -  "greatest P po == @ x. x: po.<A> & P x &
1.42 -                          (\<forall>y \<in> po.<A>. P y --> (y,x): po.<r>)"
1.43 +  "greatest P po == @ x. x: pset po & P x &
1.44 +                          (\<forall>y \<in> pset po. P y --> (y,x): order po)"
1.45
1.46    lub  :: "['a set, 'a potype] => 'a"
1.47 -  "lub S po == least (%x. \<forall>y\<in>S. (y,x): po.<r>) po"
1.48 +  "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
1.49
1.50    glb  :: "['a set, 'a potype] => 'a"
1.51 -  "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): po.<r>) po"
1.52 +  "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
1.53
1.54    isLub :: "['a set, 'a potype, 'a] => bool"
1.55 -  "isLub S po == %L. (L: po.<A> & (\<forall>y\<in>S. (y,L): po.<r>) &
1.56 -                     (\<forall>z\<in>po.<A>. (\<forall>y\<in>S. (y,z): po.<r>) --> (L,z): po.<r>))"
1.57 +  "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
1.58 +                   (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
1.59
1.60    isGlb :: "['a set, 'a potype, 'a] => bool"
1.61 -  "isGlb S po == %G. (G: po.<A> & (\<forall>y\<in>S. (G,y): po.<r>) &
1.62 -                     (\<forall>z \<in> po.<A>. (\<forall>y\<in>S. (z,y): po.<r>) --> (z,G): po.<r>))"
1.63 +  "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
1.64 +                 (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
1.65
1.66    "fix"    :: "[('a => 'a), 'a set] => 'a set"
1.67    "fix f A  == {x. x: A & f x = x}"
1.68 @@ -70,17 +61,17 @@
1.69    "Top po == greatest (%x. True) po"
1.70
1.71    PartialOrder :: "('a potype) set"
1.72 -  "PartialOrder == {P. refl (P.<A>) (P.<r>) & antisym (P.<r>) &
1.73 -                       trans (P.<r>)}"
1.74 +  "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) &
1.75 +                       trans (order P)}"
1.76
1.77    CompleteLattice :: "('a potype) set"
1.78    "CompleteLattice == {cl. cl: PartialOrder &
1.79 -                        (\<forall>S. S <= cl.<A> --> (\<exists>L. isLub S cl L)) &
1.80 -                        (\<forall>S. S <= cl.<A> --> (\<exists>G. isGlb S cl G))}"
1.81 +                        (\<forall>S. S <= pset cl --> (\<exists>L. isLub S cl L)) &
1.82 +                        (\<forall>S. S <= pset cl --> (\<exists>G. isGlb S cl G))}"
1.83
1.84    CLF :: "('a potype * ('a => 'a)) set"
1.85    "CLF == SIGMA cl: CompleteLattice.
1.86 -            {f. f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)}"
1.87 +            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}"
1.88
1.89    induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
1.90    "induced A r == {(a,b). a : A & b: A & (a,b): r}"
1.91 @@ -90,8 +81,8 @@
1.92    sublattice :: "('a potype * 'a set)set"
1.93    "sublattice ==
1.94        SIGMA cl: CompleteLattice.
1.95 -          {S. S <= cl.<A> &
1.96 -           (| pset = S, order = induced S (cl.<r>) |): CompleteLattice }"
1.97 +          {S. S <= pset cl &
1.98 +           (| pset = S, order = induced S (order cl) |): CompleteLattice }"
1.99
1.100  syntax
1.101    "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
1.102 @@ -101,15 +92,15 @@
1.103
1.104  constdefs
1.105    dual :: "'a potype => 'a potype"
1.106 -  "dual po == (| pset = po.<A>, order = converse (po.<r>) |)"
1.107 +  "dual po == (| pset = pset po, order = converse (order po) |)"
1.108
1.109  locale (open) PO =
1.110    fixes cl :: "'a potype"
1.111      and A  :: "'a set"
1.112      and r  :: "('a * 'a) set"
1.113    assumes cl_po:  "cl : PartialOrder"
1.114 -  defines A_def: "A == cl.<A>"
1.115 -     and  r_def: "r == cl.<r>"
1.116 +  defines A_def: "A == pset cl"
1.117 +     and  r_def: "r == order cl"
1.118
1.119  locale (open) CL = PO +
1.120    assumes cl_co:  "cl : CompleteLattice"
1.121 @@ -254,8 +245,8 @@
1.122  by (rule PO_imp_trans)
1.123
1.124  lemma CompleteLatticeI:
1.125 -     "[| po \<in> PartialOrder; (\<forall>S. S <= po.<A> --> (\<exists>L. isLub S po L));
1.126 -         (\<forall>S. S <= po.<A> --> (\<exists>G. isGlb S po G))|]
1.127 +     "[| po \<in> PartialOrder; (\<forall>S. S <= pset po --> (\<exists>L. isLub S po L));
1.128 +         (\<forall>S. S <= pset po --> (\<exists>G. isGlb S po G))|]
1.129        ==> po \<in> CompleteLattice"
1.130  apply (unfold CompleteLattice_def, blast)
1.131  done
1.132 @@ -268,19 +259,19 @@
1.133                   dualPO)
1.134  done
1.135
1.136 -lemma (in PO) dualA_iff: "(dual cl.<A>) = cl.<A>"
1.137 +lemma (in PO) dualA_iff: "pset (dual cl) = pset cl"
1.138  by (simp add: dual_def)
1.139
1.140 -lemma (in PO) dualr_iff: "((x, y) \<in> (dual cl.<r>)) = ((y, x) \<in> cl.<r>)"
1.141 +lemma (in PO) dualr_iff: "((x, y) \<in> (order(dual cl))) = ((y, x) \<in> order cl)"
1.142  by (simp add: dual_def)
1.143
1.144  lemma (in PO) monotone_dual:
1.145 -     "monotone f (cl.<A>) (cl.<r>) ==> monotone f (dual cl.<A>) (dual cl.<r>)"
1.146 -apply (simp add: monotone_def dualA_iff dualr_iff)
1.147 -done
1.148 +     "monotone f (pset cl) (order cl)
1.149 +     ==> monotone f (pset (dual cl)) (order(dual cl))"
1.150 +by (simp add: monotone_def dualA_iff dualr_iff)
1.151
1.152  lemma (in PO) interval_dual:
1.153 -     "[| x \<in> A; y \<in> A|] ==> interval r x y = interval (dual cl.<r>) y x"
1.154 +     "[| x \<in> A; y \<in> A|] ==> interval r x y = interval (order(dual cl)) y x"
1.155  apply (simp add: interval_def dualr_iff)
1.156  apply (fold r_def, fast)
1.157  done
1.158 @@ -416,7 +407,7 @@
1.159  *}
1.160
1.161  lemma (in CLF) [simp]:
1.162 -    "f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)"
1.163 +    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
1.164  apply (insert f_cl)
1.165  apply (simp add: CLF_def)
1.166  done
1.167 @@ -424,7 +415,7 @@
1.168  declare (in CLF) f_cl [simp]
1.169
1.170
1.171 -lemma (in CLF) f_in_funcset: "f \<in> A funcset A"
1.172 +lemma (in CLF) f_in_funcset: "f \<in> A -> A"
1.173  by (simp add: A_def)
1.174
1.175  lemma (in CLF) monotone_f: "monotone f A r"
1.176 @@ -460,7 +451,7 @@
1.177  apply (rule ballI)
1.178  apply (rule transE)
1.179  apply (rule CO_trans)
1.180 --- {* instantiates @{text "(x, ???z) \<in> cl.<r> to (x, f x)"}, *}
1.181 +-- {* instantiates @{text "(x, ???z) \<in> order cl to (x, f x)"}, *}
1.182  -- {* because of the def of @{text H} *}
1.183  apply fast
1.184  -- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *}
1.185 @@ -807,7 +798,7 @@
1.186  apply (simp add: intY1_def interval_def  intY1_elem)
1.187  done
1.188
1.189 -lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 funcset intY1"
1.190 +lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
1.191  apply (rule restrictI)
1.192  apply (erule intY1_f_closed)
1.193  done
```