src/HOL/Metis_Examples/Tarski.thy

--- a/src/HOL/Metis_Examples/Tarski.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -20,59 +20,56 @@
   pset  :: "'a set"
   order :: "('a * 'a) set"
 
-constdefs
-  monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
+definition monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool" where
   "monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r"
 
-  least :: "['a => bool, 'a potype] => 'a"
+definition least :: "['a => bool, 'a potype] => 'a" where
   "least P po == @ x. x: pset po & P x &
                        (\<forall>y \<in> pset po. P y --> (x,y): order po)"
 
-  greatest :: "['a => bool, 'a potype] => 'a"
+definition greatest :: "['a => bool, 'a potype] => 'a" where
   "greatest P po == @ x. x: pset po & P x &
                           (\<forall>y \<in> pset po. P y --> (y,x): order po)"
 
-  lub  :: "['a set, 'a potype] => 'a"
+definition lub  :: "['a set, 'a potype] => 'a" where
   "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
 
-  glb  :: "['a set, 'a potype] => 'a"
+definition glb  :: "['a set, 'a potype] => 'a" where
   "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
 
-  isLub :: "['a set, 'a potype, 'a] => bool"
+definition isLub :: "['a set, 'a potype, 'a] => bool" where
   "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
                    (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
 
-  isGlb :: "['a set, 'a potype, 'a] => bool"
+definition isGlb :: "['a set, 'a potype, 'a] => bool" where
   "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
                  (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
 
-  "fix"    :: "[('a => 'a), 'a set] => 'a set"
+definition "fix"    :: "[('a => 'a), 'a set] => 'a set" where
   "fix f A  == {x. x: A & f x = x}"
 
-  interval :: "[('a*'a) set,'a, 'a ] => 'a set"
+definition interval :: "[('a*'a) set,'a, 'a ] => 'a set" where
   "interval r a b == {x. (a,x): r & (x,b): r}"
 
-constdefs
-  Bot :: "'a potype => 'a"
+definition Bot :: "'a potype => 'a" where
   "Bot po == least (%x. True) po"
 
-  Top :: "'a potype => 'a"
+definition Top :: "'a potype => 'a" where
   "Top po == greatest (%x. True) po"
 
-  PartialOrder :: "('a potype) set"
+definition PartialOrder :: "('a potype) set" where
   "PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) &
                        trans (order P)}"
 
-  CompleteLattice :: "('a potype) set"
+definition CompleteLattice :: "('a potype) set" where
   "CompleteLattice == {cl. cl: PartialOrder &
                         (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) &
                         (\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
 
-  induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
+definition induced :: "['a set, ('a * 'a) set] => ('a *'a)set" where
   "induced A r == {(a,b). a : A & b: A & (a,b): r}"
 
-constdefs
-  sublattice :: "('a potype * 'a set)set"
+definition sublattice :: "('a potype * 'a set)set" where
   "sublattice ==
       SIGMA cl: CompleteLattice.
           {S. S \<subseteq> pset cl &
@@ -82,8 +79,7 @@
   sublattice_syntax :: "['a set, 'a potype] => bool" ("_ <<= _" [51, 50] 50)
   where "S <<= cl \<equiv> S : sublattice `` {cl}"
 
-constdefs
-  dual :: "'a potype => 'a potype"
+definition dual :: "'a potype => 'a potype" where
   "dual po == (| pset = pset po, order = converse (order po) |)"
 
 locale PO =