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