src/HOL/Import/HOLLight/HOLLight.thy
changeset 35416 d8d7d1b785af
parent 34974 18b41bba42b5
child 43786 fea3ed6951e3
     1.1 --- a/src/HOL/Import/HOLLight/HOLLight.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Import/HOLLight/HOLLight.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -95,8 +95,7 @@
     1.4  lemma EXCLUDED_MIDDLE: "ALL t::bool. t | ~ t"
     1.5    by (import hollight EXCLUDED_MIDDLE)
     1.6  
     1.7 -constdefs
     1.8 -  COND :: "bool => 'A => 'A => 'A" 
     1.9 +definition COND :: "bool => 'A => 'A => 'A" where 
    1.10    "COND ==
    1.11  %(t::bool) (t1::'A::type) t2::'A::type.
    1.12     SOME x::'A::type. (t = True --> x = t1) & (t = False --> x = t2)"
    1.13 @@ -173,15 +172,13 @@
    1.14  (b & P x True | ~ b & P y False)"
    1.15    by (import hollight th_cond)
    1.16  
    1.17 -constdefs
    1.18 -  LET_END :: "'A => 'A" 
    1.19 +definition LET_END :: "'A => 'A" where 
    1.20    "LET_END == %t::'A::type. t"
    1.21  
    1.22  lemma DEF_LET_END: "LET_END = (%t::'A::type. t)"
    1.23    by (import hollight DEF_LET_END)
    1.24  
    1.25 -constdefs
    1.26 -  GABS :: "('A => bool) => 'A" 
    1.27 +definition GABS :: "('A => bool) => 'A" where 
    1.28    "(op ==::(('A::type => bool) => 'A::type)
    1.29          => (('A::type => bool) => 'A::type) => prop)
    1.30   (GABS::('A::type => bool) => 'A::type)
    1.31 @@ -193,8 +190,7 @@
    1.32   (Eps::('A::type => bool) => 'A::type)"
    1.33    by (import hollight DEF_GABS)
    1.34  
    1.35 -constdefs
    1.36 -  GEQ :: "'A => 'A => bool" 
    1.37 +definition GEQ :: "'A => 'A => bool" where 
    1.38    "(op ==::('A::type => 'A::type => bool)
    1.39          => ('A::type => 'A::type => bool) => prop)
    1.40   (GEQ::'A::type => 'A::type => bool) (op =::'A::type => 'A::type => bool)"
    1.41 @@ -208,8 +204,7 @@
    1.42     x = Pair_Rep a b"
    1.43    by (import hollight PAIR_EXISTS_THM)
    1.44  
    1.45 -constdefs
    1.46 -  CURRY :: "('A * 'B => 'C) => 'A => 'B => 'C" 
    1.47 +definition CURRY :: "('A * 'B => 'C) => 'A => 'B => 'C" where 
    1.48    "CURRY ==
    1.49  %(u::'A::type * 'B::type => 'C::type) (ua::'A::type) ub::'B::type.
    1.50     u (ua, ub)"
    1.51 @@ -219,8 +214,7 @@
    1.52      u (ua, ub))"
    1.53    by (import hollight DEF_CURRY)
    1.54  
    1.55 -constdefs
    1.56 -  UNCURRY :: "('A => 'B => 'C) => 'A * 'B => 'C" 
    1.57 +definition UNCURRY :: "('A => 'B => 'C) => 'A * 'B => 'C" where 
    1.58    "UNCURRY ==
    1.59  %(u::'A::type => 'B::type => 'C::type) ua::'A::type * 'B::type.
    1.60     u (fst ua) (snd ua)"
    1.61 @@ -230,8 +224,7 @@
    1.62      u (fst ua) (snd ua))"
    1.63    by (import hollight DEF_UNCURRY)
    1.64  
    1.65 -constdefs
    1.66 -  PASSOC :: "(('A * 'B) * 'C => 'D) => 'A * 'B * 'C => 'D" 
    1.67 +definition PASSOC :: "(('A * 'B) * 'C => 'D) => 'A * 'B * 'C => 'D" where 
    1.68    "PASSOC ==
    1.69  %(u::('A::type * 'B::type) * 'C::type => 'D::type)
    1.70     ua::'A::type * 'B::type * 'C::type.
    1.71 @@ -291,8 +284,7 @@
    1.72     (m * n = NUMERAL_BIT1 0) = (m = NUMERAL_BIT1 0 & n = NUMERAL_BIT1 0)"
    1.73    by (import hollight MULT_EQ_1)
    1.74  
    1.75 -constdefs
    1.76 -  EXP :: "nat => nat => nat" 
    1.77 +definition EXP :: "nat => nat => nat" where 
    1.78    "EXP ==
    1.79  SOME EXP::nat => nat => nat.
    1.80     (ALL m::nat. EXP m 0 = NUMERAL_BIT1 0) &
    1.81 @@ -549,8 +541,7 @@
    1.82     (EX m::nat. P m & (ALL x::nat. P x --> <= x m))"
    1.83    by (import hollight num_MAX)
    1.84  
    1.85 -constdefs
    1.86 -  EVEN :: "nat => bool" 
    1.87 +definition EVEN :: "nat => bool" where 
    1.88    "EVEN ==
    1.89  SOME EVEN::nat => bool.
    1.90     EVEN 0 = True & (ALL n::nat. EVEN (Suc n) = (~ EVEN n))"
    1.91 @@ -560,8 +551,7 @@
    1.92      EVEN 0 = True & (ALL n::nat. EVEN (Suc n) = (~ EVEN n)))"
    1.93    by (import hollight DEF_EVEN)
    1.94  
    1.95 -constdefs
    1.96 -  ODD :: "nat => bool" 
    1.97 +definition ODD :: "nat => bool" where 
    1.98    "ODD ==
    1.99  SOME ODD::nat => bool. ODD 0 = False & (ALL n::nat. ODD (Suc n) = (~ ODD n))"
   1.100  
   1.101 @@ -641,8 +631,7 @@
   1.102  lemma SUC_SUB1: "ALL x::nat. Suc x - NUMERAL_BIT1 0 = x"
   1.103    by (import hollight SUC_SUB1)
   1.104  
   1.105 -constdefs
   1.106 -  FACT :: "nat => nat" 
   1.107 +definition FACT :: "nat => nat" where 
   1.108    "FACT ==
   1.109  SOME FACT::nat => nat.
   1.110     FACT 0 = NUMERAL_BIT1 0 & (ALL n::nat. FACT (Suc n) = Suc n * FACT n)"
   1.111 @@ -669,8 +658,7 @@
   1.112        COND (n = 0) (x = 0 & xa = 0) (m = x * n + xa & < xa n)"
   1.113    by (import hollight DIVMOD_EXIST_0)
   1.114  
   1.115 -constdefs
   1.116 -  DIV :: "nat => nat => nat" 
   1.117 +definition DIV :: "nat => nat => nat" where 
   1.118    "DIV ==
   1.119  SOME q::nat => nat => nat.
   1.120     EX r::nat => nat => nat.
   1.121 @@ -686,8 +674,7 @@
   1.122             (m = q m n * n + r m n & < (r m n) n))"
   1.123    by (import hollight DEF_DIV)
   1.124  
   1.125 -constdefs
   1.126 -  MOD :: "nat => nat => nat" 
   1.127 +definition MOD :: "nat => nat => nat" where 
   1.128    "MOD ==
   1.129  SOME r::nat => nat => nat.
   1.130     ALL (m::nat) n::nat.
   1.131 @@ -877,8 +864,7 @@
   1.132   n ~= 0 & (ALL (q::nat) r::nat. m = q * n + r & < r n --> P q r))"
   1.133    by (import hollight DIVMOD_ELIM_THM)
   1.134  
   1.135 -constdefs
   1.136 -  eqeq :: "'q_9910 => 'q_9909 => ('q_9910 => 'q_9909 => bool) => bool" 
   1.137 +definition eqeq :: "'q_9910 => 'q_9909 => ('q_9910 => 'q_9909 => bool) => bool" where 
   1.138    "eqeq ==
   1.139  %(u::'q_9910::type) (ua::'q_9909::type)
   1.140     ub::'q_9910::type => 'q_9909::type => bool. ub u ua"
   1.141 @@ -888,8 +874,7 @@
   1.142      ub::'q_9910::type => 'q_9909::type => bool. ub u ua)"
   1.143    by (import hollight DEF__equal__equal_)
   1.144  
   1.145 -constdefs
   1.146 -  mod_nat :: "nat => nat => nat => bool" 
   1.147 +definition mod_nat :: "nat => nat => nat => bool" where 
   1.148    "mod_nat ==
   1.149  %(u::nat) (ua::nat) ub::nat. EX (q1::nat) q2::nat. ua + u * q1 = ub + u * q2"
   1.150  
   1.151 @@ -898,8 +883,7 @@
   1.152      EX (q1::nat) q2::nat. ua + u * q1 = ub + u * q2)"
   1.153    by (import hollight DEF_mod_nat)
   1.154  
   1.155 -constdefs
   1.156 -  minimal :: "(nat => bool) => nat" 
   1.157 +definition minimal :: "(nat => bool) => nat" where 
   1.158    "minimal == %u::nat => bool. SOME n::nat. u n & (ALL m::nat. < m n --> ~ u m)"
   1.159  
   1.160  lemma DEF_minimal: "minimal =
   1.161 @@ -910,8 +894,7 @@
   1.162     Ex P = (P (minimal P) & (ALL x::nat. < x (minimal P) --> ~ P x))"
   1.163    by (import hollight MINIMAL)
   1.164  
   1.165 -constdefs
   1.166 -  WF :: "('A => 'A => bool) => bool" 
   1.167 +definition WF :: "('A => 'A => bool) => bool" where 
   1.168    "WF ==
   1.169  %u::'A::type => 'A::type => bool.
   1.170     ALL P::'A::type => bool.
   1.171 @@ -1605,8 +1588,7 @@
   1.172         ALL (xa::'A::type) y::'B::type. x (P xa y) = xa & Y (P xa y) = y)"
   1.173    by (import hollight INJ_INVERSE2)
   1.174  
   1.175 -constdefs
   1.176 -  NUMPAIR :: "nat => nat => nat" 
   1.177 +definition NUMPAIR :: "nat => nat => nat" where 
   1.178    "NUMPAIR ==
   1.179  %(u::nat) ua::nat.
   1.180     EXP (NUMERAL_BIT0 (NUMERAL_BIT1 0)) u *
   1.181 @@ -1626,8 +1608,7 @@
   1.182     (NUMPAIR x1 y1 = NUMPAIR x2 y2) = (x1 = x2 & y1 = y2)"
   1.183    by (import hollight NUMPAIR_INJ)
   1.184  
   1.185 -constdefs
   1.186 -  NUMFST :: "nat => nat" 
   1.187 +definition NUMFST :: "nat => nat" where 
   1.188    "NUMFST ==
   1.189  SOME X::nat => nat.
   1.190     EX Y::nat => nat.
   1.191 @@ -1639,8 +1620,7 @@
   1.192         ALL (x::nat) y::nat. X (NUMPAIR x y) = x & Y (NUMPAIR x y) = y)"
   1.193    by (import hollight DEF_NUMFST)
   1.194  
   1.195 -constdefs
   1.196 -  NUMSND :: "nat => nat" 
   1.197 +definition NUMSND :: "nat => nat" where 
   1.198    "NUMSND ==
   1.199  SOME Y::nat => nat.
   1.200     ALL (x::nat) y::nat. NUMFST (NUMPAIR x y) = x & Y (NUMPAIR x y) = y"
   1.201 @@ -1650,8 +1630,7 @@
   1.202      ALL (x::nat) y::nat. NUMFST (NUMPAIR x y) = x & Y (NUMPAIR x y) = y)"
   1.203    by (import hollight DEF_NUMSND)
   1.204  
   1.205 -constdefs
   1.206 -  NUMSUM :: "bool => nat => nat" 
   1.207 +definition NUMSUM :: "bool => nat => nat" where 
   1.208    "NUMSUM ==
   1.209  %(u::bool) ua::nat.
   1.210     COND u (Suc (NUMERAL_BIT0 (NUMERAL_BIT1 0) * ua))
   1.211 @@ -1667,8 +1646,7 @@
   1.212     (NUMSUM b1 x1 = NUMSUM b2 x2) = (b1 = b2 & x1 = x2)"
   1.213    by (import hollight NUMSUM_INJ)
   1.214  
   1.215 -constdefs
   1.216 -  NUMLEFT :: "nat => bool" 
   1.217 +definition NUMLEFT :: "nat => bool" where 
   1.218    "NUMLEFT ==
   1.219  SOME X::nat => bool.
   1.220     EX Y::nat => nat.
   1.221 @@ -1680,8 +1658,7 @@
   1.222         ALL (x::bool) y::nat. X (NUMSUM x y) = x & Y (NUMSUM x y) = y)"
   1.223    by (import hollight DEF_NUMLEFT)
   1.224  
   1.225 -constdefs
   1.226 -  NUMRIGHT :: "nat => nat" 
   1.227 +definition NUMRIGHT :: "nat => nat" where 
   1.228    "NUMRIGHT ==
   1.229  SOME Y::nat => nat.
   1.230     ALL (x::bool) y::nat. NUMLEFT (NUMSUM x y) = x & Y (NUMSUM x y) = y"
   1.231 @@ -1691,8 +1668,7 @@
   1.232      ALL (x::bool) y::nat. NUMLEFT (NUMSUM x y) = x & Y (NUMSUM x y) = y)"
   1.233    by (import hollight DEF_NUMRIGHT)
   1.234  
   1.235 -constdefs
   1.236 -  INJN :: "nat => nat => 'A => bool" 
   1.237 +definition INJN :: "nat => nat => 'A => bool" where 
   1.238    "INJN == %(u::nat) (n::nat) a::'A::type. n = u"
   1.239  
   1.240  lemma DEF_INJN: "INJN = (%(u::nat) (n::nat) a::'A::type. n = u)"
   1.241 @@ -1710,8 +1686,7 @@
   1.242             ((op =::nat => nat => bool) n1 n2)))"
   1.243    by (import hollight INJN_INJ)
   1.244  
   1.245 -constdefs
   1.246 -  INJA :: "'A => nat => 'A => bool" 
   1.247 +definition INJA :: "'A => nat => 'A => bool" where 
   1.248    "INJA == %(u::'A::type) (n::nat) b::'A::type. b = u"
   1.249  
   1.250  lemma DEF_INJA: "INJA = (%(u::'A::type) (n::nat) b::'A::type. b = u)"
   1.251 @@ -1720,8 +1695,7 @@
   1.252  lemma INJA_INJ: "ALL (a1::'A::type) a2::'A::type. (INJA a1 = INJA a2) = (a1 = a2)"
   1.253    by (import hollight INJA_INJ)
   1.254  
   1.255 -constdefs
   1.256 -  INJF :: "(nat => nat => 'A => bool) => nat => 'A => bool" 
   1.257 +definition INJF :: "(nat => nat => 'A => bool) => nat => 'A => bool" where 
   1.258    "INJF == %(u::nat => nat => 'A::type => bool) n::nat. u (NUMFST n) (NUMSND n)"
   1.259  
   1.260  lemma DEF_INJF: "INJF =
   1.261 @@ -1732,8 +1706,7 @@
   1.262     (INJF f1 = INJF f2) = (f1 = f2)"
   1.263    by (import hollight INJF_INJ)
   1.264  
   1.265 -constdefs
   1.266 -  INJP :: "(nat => 'A => bool) => (nat => 'A => bool) => nat => 'A => bool" 
   1.267 +definition INJP :: "(nat => 'A => bool) => (nat => 'A => bool) => nat => 'A => bool" where 
   1.268    "INJP ==
   1.269  %(u::nat => 'A::type => bool) (ua::nat => 'A::type => bool) (n::nat)
   1.270     a::'A::type. COND (NUMLEFT n) (u (NUMRIGHT n) a) (ua (NUMRIGHT n) a)"
   1.271 @@ -1748,8 +1721,7 @@
   1.272     (INJP f1 f2 = INJP f1' f2') = (f1 = f1' & f2 = f2')"
   1.273    by (import hollight INJP_INJ)
   1.274  
   1.275 -constdefs
   1.276 -  ZCONSTR :: "nat => 'A => (nat => nat => 'A => bool) => nat => 'A => bool" 
   1.277 +definition ZCONSTR :: "nat => 'A => (nat => nat => 'A => bool) => nat => 'A => bool" where 
   1.278    "ZCONSTR ==
   1.279  %(u::nat) (ua::'A::type) ub::nat => nat => 'A::type => bool.
   1.280     INJP (INJN (Suc u)) (INJP (INJA ua) (INJF ub))"
   1.281 @@ -1759,8 +1731,7 @@
   1.282      INJP (INJN (Suc u)) (INJP (INJA ua) (INJF ub)))"
   1.283    by (import hollight DEF_ZCONSTR)
   1.284  
   1.285 -constdefs
   1.286 -  ZBOT :: "nat => 'A => bool" 
   1.287 +definition ZBOT :: "nat => 'A => bool" where 
   1.288    "ZBOT == INJP (INJN 0) (SOME z::nat => 'A::type => bool. True)"
   1.289  
   1.290  lemma DEF_ZBOT: "ZBOT = INJP (INJN 0) (SOME z::nat => 'A::type => bool. True)"
   1.291 @@ -1770,8 +1741,7 @@
   1.292     ZCONSTR x xa xb ~= ZBOT"
   1.293    by (import hollight ZCONSTR_ZBOT)
   1.294  
   1.295 -constdefs
   1.296 -  ZRECSPACE :: "(nat => 'A => bool) => bool" 
   1.297 +definition ZRECSPACE :: "(nat => 'A => bool) => bool" where 
   1.298    "ZRECSPACE ==
   1.299  %a::nat => 'A::type => bool.
   1.300     ALL ZRECSPACE'::(nat => 'A::type => bool) => bool.
   1.301 @@ -1809,8 +1779,7 @@
   1.302    [where a="a :: 'A recspace" and r=r ,
   1.303     OF type_definition_recspace]
   1.304  
   1.305 -constdefs
   1.306 -  BOTTOM :: "'A recspace" 
   1.307 +definition BOTTOM :: "'A recspace" where 
   1.308    "(op ==::'A::type recspace => 'A::type recspace => prop)
   1.309   (BOTTOM::'A::type recspace)
   1.310   ((_mk_rec::(nat => 'A::type => bool) => 'A::type recspace)
   1.311 @@ -1822,8 +1791,7 @@
   1.312     (ZBOT::nat => 'A::type => bool))"
   1.313    by (import hollight DEF_BOTTOM)
   1.314  
   1.315 -constdefs
   1.316 -  CONSTR :: "nat => 'A => (nat => 'A recspace) => 'A recspace" 
   1.317 +definition CONSTR :: "nat => 'A => (nat => 'A recspace) => 'A recspace" where 
   1.318    "(op ==::(nat => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
   1.319          => (nat
   1.320              => 'A::type => (nat => 'A::type recspace) => 'A::type recspace)
   1.321 @@ -1900,8 +1868,7 @@
   1.322           f (CONSTR c i r) = Fn c i r (%n::nat. f (r n))"
   1.323    by (import hollight CONSTR_REC)
   1.324  
   1.325 -constdefs
   1.326 -  FCONS :: "'A => (nat => 'A) => nat => 'A" 
   1.327 +definition FCONS :: "'A => (nat => 'A) => nat => 'A" where 
   1.328    "FCONS ==
   1.329  SOME FCONS::'A::type => (nat => 'A::type) => nat => 'A::type.
   1.330     (ALL (a::'A::type) f::nat => 'A::type. FCONS a f 0 = a) &
   1.331 @@ -1917,8 +1884,7 @@
   1.332  lemma FCONS_UNDO: "ALL f::nat => 'A::type. f = FCONS (f 0) (f o Suc)"
   1.333    by (import hollight FCONS_UNDO)
   1.334  
   1.335 -constdefs
   1.336 -  FNIL :: "nat => 'A" 
   1.337 +definition FNIL :: "nat => 'A" where 
   1.338    "FNIL == %u::nat. SOME x::'A::type. True"
   1.339  
   1.340  lemma DEF_FNIL: "FNIL = (%u::nat. SOME x::'A::type. True)"
   1.341 @@ -1995,8 +1961,7 @@
   1.342    [where a="a :: 'A hollight.option" and r=r ,
   1.343     OF type_definition_option]
   1.344  
   1.345 -constdefs
   1.346 -  NONE :: "'A hollight.option" 
   1.347 +definition NONE :: "'A hollight.option" where 
   1.348    "(op ==::'A::type hollight.option => 'A::type hollight.option => prop)
   1.349   (NONE::'A::type hollight.option)
   1.350   ((_mk_option::'A::type recspace => 'A::type hollight.option)
   1.351 @@ -2093,8 +2058,7 @@
   1.352    [where a="a :: 'A hollight.list" and r=r ,
   1.353     OF type_definition_list]
   1.354  
   1.355 -constdefs
   1.356 -  NIL :: "'A hollight.list" 
   1.357 +definition NIL :: "'A hollight.list" where 
   1.358    "(op ==::'A::type hollight.list => 'A::type hollight.list => prop)
   1.359   (NIL::'A::type hollight.list)
   1.360   ((_mk_list::'A::type recspace => 'A::type hollight.list)
   1.361 @@ -2114,8 +2078,7 @@
   1.362       (%n::nat. BOTTOM::'A::type recspace)))"
   1.363    by (import hollight DEF_NIL)
   1.364  
   1.365 -constdefs
   1.366 -  CONS :: "'A => 'A hollight.list => 'A hollight.list" 
   1.367 +definition CONS :: "'A => 'A hollight.list => 'A hollight.list" where 
   1.368    "(op ==::('A::type => 'A::type hollight.list => 'A::type hollight.list)
   1.369          => ('A::type => 'A::type hollight.list => 'A::type hollight.list)
   1.370             => prop)
   1.371 @@ -2160,8 +2123,7 @@
   1.372     EX x::bool => 'A::type. x False = a & x True = b"
   1.373    by (import hollight bool_RECURSION)
   1.374  
   1.375 -constdefs
   1.376 -  ISO :: "('A => 'B) => ('B => 'A) => bool" 
   1.377 +definition ISO :: "('A => 'B) => ('B => 'A) => bool" where 
   1.378    "ISO ==
   1.379  %(u::'A::type => 'B::type) ua::'B::type => 'A::type.
   1.380     (ALL x::'B::type. u (ua x) = x) & (ALL y::'A::type. ua (u y) = y)"
   1.381 @@ -2244,15 +2206,13 @@
   1.382       (%n::nat. BOTTOM::bool recspace)))"
   1.383    by (import hollight DEF__10303)
   1.384  
   1.385 -constdefs
   1.386 -  two_1 :: "N_2" 
   1.387 +definition two_1 :: "N_2" where 
   1.388    "two_1 == _10302"
   1.389  
   1.390  lemma DEF_two_1: "two_1 = _10302"
   1.391    by (import hollight DEF_two_1)
   1.392  
   1.393 -constdefs
   1.394 -  two_2 :: "N_2" 
   1.395 +definition two_2 :: "N_2" where 
   1.396    "two_2 == _10303"
   1.397  
   1.398  lemma DEF_two_2: "two_2 = _10303"
   1.399 @@ -2337,22 +2297,19 @@
   1.400       (%n::nat. BOTTOM::bool recspace)))"
   1.401    by (import hollight DEF__10328)
   1.402  
   1.403 -constdefs
   1.404 -  three_1 :: "N_3" 
   1.405 +definition three_1 :: "N_3" where 
   1.406    "three_1 == _10326"
   1.407  
   1.408  lemma DEF_three_1: "three_1 = _10326"
   1.409    by (import hollight DEF_three_1)
   1.410  
   1.411 -constdefs
   1.412 -  three_2 :: "N_3" 
   1.413 +definition three_2 :: "N_3" where 
   1.414    "three_2 == _10327"
   1.415  
   1.416  lemma DEF_three_2: "three_2 = _10327"
   1.417    by (import hollight DEF_three_2)
   1.418  
   1.419 -constdefs
   1.420 -  three_3 :: "N_3" 
   1.421 +definition three_3 :: "N_3" where 
   1.422    "three_3 == _10328"
   1.423  
   1.424  lemma DEF_three_3: "three_3 = _10328"
   1.425 @@ -2365,8 +2322,7 @@
   1.426     All P"
   1.427    by (import hollight list_INDUCT)
   1.428  
   1.429 -constdefs
   1.430 -  HD :: "'A hollight.list => 'A" 
   1.431 +definition HD :: "'A hollight.list => 'A" where 
   1.432    "HD ==
   1.433  SOME HD::'A::type hollight.list => 'A::type.
   1.434     ALL (t::'A::type hollight.list) h::'A::type. HD (CONS h t) = h"
   1.435 @@ -2376,8 +2332,7 @@
   1.436      ALL (t::'A::type hollight.list) h::'A::type. HD (CONS h t) = h)"
   1.437    by (import hollight DEF_HD)
   1.438  
   1.439 -constdefs
   1.440 -  TL :: "'A hollight.list => 'A hollight.list" 
   1.441 +definition TL :: "'A hollight.list => 'A hollight.list" where 
   1.442    "TL ==
   1.443  SOME TL::'A::type hollight.list => 'A::type hollight.list.
   1.444     ALL (h::'A::type) t::'A::type hollight.list. TL (CONS h t) = t"
   1.445 @@ -2387,8 +2342,7 @@
   1.446      ALL (h::'A::type) t::'A::type hollight.list. TL (CONS h t) = t)"
   1.447    by (import hollight DEF_TL)
   1.448  
   1.449 -constdefs
   1.450 -  APPEND :: "'A hollight.list => 'A hollight.list => 'A hollight.list" 
   1.451 +definition APPEND :: "'A hollight.list => 'A hollight.list => 'A hollight.list" where 
   1.452    "APPEND ==
   1.453  SOME APPEND::'A::type hollight.list
   1.454               => 'A::type hollight.list => 'A::type hollight.list.
   1.455 @@ -2405,8 +2359,7 @@
   1.456          APPEND (CONS h t) l = CONS h (APPEND t l)))"
   1.457    by (import hollight DEF_APPEND)
   1.458  
   1.459 -constdefs
   1.460 -  REVERSE :: "'A hollight.list => 'A hollight.list" 
   1.461 +definition REVERSE :: "'A hollight.list => 'A hollight.list" where 
   1.462    "REVERSE ==
   1.463  SOME REVERSE::'A::type hollight.list => 'A::type hollight.list.
   1.464     REVERSE NIL = NIL &
   1.465 @@ -2420,8 +2373,7 @@
   1.466          REVERSE (CONS x l) = APPEND (REVERSE l) (CONS x NIL)))"
   1.467    by (import hollight DEF_REVERSE)
   1.468  
   1.469 -constdefs
   1.470 -  LENGTH :: "'A hollight.list => nat" 
   1.471 +definition LENGTH :: "'A hollight.list => nat" where 
   1.472    "LENGTH ==
   1.473  SOME LENGTH::'A::type hollight.list => nat.
   1.474     LENGTH NIL = 0 &
   1.475 @@ -2435,8 +2387,7 @@
   1.476          LENGTH (CONS h t) = Suc (LENGTH t)))"
   1.477    by (import hollight DEF_LENGTH)
   1.478  
   1.479 -constdefs
   1.480 -  MAP :: "('A => 'B) => 'A hollight.list => 'B hollight.list" 
   1.481 +definition MAP :: "('A => 'B) => 'A hollight.list => 'B hollight.list" where 
   1.482    "MAP ==
   1.483  SOME MAP::('A::type => 'B::type)
   1.484            => 'A::type hollight.list => 'B::type hollight.list.
   1.485 @@ -2452,8 +2403,7 @@
   1.486          MAP f (CONS h t) = CONS (f h) (MAP f t)))"
   1.487    by (import hollight DEF_MAP)
   1.488  
   1.489 -constdefs
   1.490 -  LAST :: "'A hollight.list => 'A" 
   1.491 +definition LAST :: "'A hollight.list => 'A" where 
   1.492    "LAST ==
   1.493  SOME LAST::'A::type hollight.list => 'A::type.
   1.494     ALL (h::'A::type) t::'A::type hollight.list.
   1.495 @@ -2465,8 +2415,7 @@
   1.496         LAST (CONS h t) = COND (t = NIL) h (LAST t))"
   1.497    by (import hollight DEF_LAST)
   1.498  
   1.499 -constdefs
   1.500 -  REPLICATE :: "nat => 'q_16860 => 'q_16860 hollight.list" 
   1.501 +definition REPLICATE :: "nat => 'q_16860 => 'q_16860 hollight.list" where 
   1.502    "REPLICATE ==
   1.503  SOME REPLICATE::nat => 'q_16860::type => 'q_16860::type hollight.list.
   1.504     (ALL x::'q_16860::type. REPLICATE 0 x = NIL) &
   1.505 @@ -2480,8 +2429,7 @@
   1.506          REPLICATE (Suc n) x = CONS x (REPLICATE n x)))"
   1.507    by (import hollight DEF_REPLICATE)
   1.508  
   1.509 -constdefs
   1.510 -  NULL :: "'q_16875 hollight.list => bool" 
   1.511 +definition NULL :: "'q_16875 hollight.list => bool" where 
   1.512    "NULL ==
   1.513  SOME NULL::'q_16875::type hollight.list => bool.
   1.514     NULL NIL = True &
   1.515 @@ -2495,8 +2443,7 @@
   1.516          NULL (CONS h t) = False))"
   1.517    by (import hollight DEF_NULL)
   1.518  
   1.519 -constdefs
   1.520 -  ALL_list :: "('q_16895 => bool) => 'q_16895 hollight.list => bool" 
   1.521 +definition ALL_list :: "('q_16895 => bool) => 'q_16895 hollight.list => bool" where 
   1.522    "ALL_list ==
   1.523  SOME u::('q_16895::type => bool) => 'q_16895::type hollight.list => bool.
   1.524     (ALL P::'q_16895::type => bool. u P NIL = True) &
   1.525 @@ -2527,9 +2474,8 @@
   1.526          t::'q_16916::type hollight.list. u P (CONS h t) = (P h | u P t)))"
   1.527    by (import hollight DEF_EX)
   1.528  
   1.529 -constdefs
   1.530 -  ITLIST :: "('q_16939 => 'q_16938 => 'q_16938)
   1.531 -=> 'q_16939 hollight.list => 'q_16938 => 'q_16938" 
   1.532 +definition ITLIST :: "('q_16939 => 'q_16938 => 'q_16938)
   1.533 +=> 'q_16939 hollight.list => 'q_16938 => 'q_16938" where 
   1.534    "ITLIST ==
   1.535  SOME ITLIST::('q_16939::type => 'q_16938::type => 'q_16938::type)
   1.536               => 'q_16939::type hollight.list
   1.537 @@ -2553,8 +2499,7 @@
   1.538          ITLIST f (CONS h t) b = f h (ITLIST f t b)))"
   1.539    by (import hollight DEF_ITLIST)
   1.540  
   1.541 -constdefs
   1.542 -  MEM :: "'q_16964 => 'q_16964 hollight.list => bool" 
   1.543 +definition MEM :: "'q_16964 => 'q_16964 hollight.list => bool" where 
   1.544    "MEM ==
   1.545  SOME MEM::'q_16964::type => 'q_16964::type hollight.list => bool.
   1.546     (ALL x::'q_16964::type. MEM x NIL = False) &
   1.547 @@ -2570,9 +2515,8 @@
   1.548          MEM x (CONS h t) = (x = h | MEM x t)))"
   1.549    by (import hollight DEF_MEM)
   1.550  
   1.551 -constdefs
   1.552 -  ALL2 :: "('q_16997 => 'q_17004 => bool)
   1.553 -=> 'q_16997 hollight.list => 'q_17004 hollight.list => bool" 
   1.554 +definition ALL2 :: "('q_16997 => 'q_17004 => bool)
   1.555 +=> 'q_16997 hollight.list => 'q_17004 hollight.list => bool" where 
   1.556    "ALL2 ==
   1.557  SOME ALL2::('q_16997::type => 'q_17004::type => bool)
   1.558             => 'q_16997::type hollight.list
   1.559 @@ -2604,10 +2548,9 @@
   1.560  ALL2 P (CONS h1 t1) (CONS h2 t2) = (P h1 h2 & ALL2 P t1 t2)"
   1.561    by (import hollight ALL2)
   1.562  
   1.563 -constdefs
   1.564 -  MAP2 :: "('q_17089 => 'q_17096 => 'q_17086)
   1.565 +definition MAP2 :: "('q_17089 => 'q_17096 => 'q_17086)
   1.566  => 'q_17089 hollight.list
   1.567 -   => 'q_17096 hollight.list => 'q_17086 hollight.list" 
   1.568 +   => 'q_17096 hollight.list => 'q_17086 hollight.list" where 
   1.569    "MAP2 ==
   1.570  SOME MAP2::('q_17089::type => 'q_17096::type => 'q_17086::type)
   1.571             => 'q_17089::type hollight.list
   1.572 @@ -2639,8 +2582,7 @@
   1.573  CONS (f h1 h2) (MAP2 f t1 t2)"
   1.574    by (import hollight MAP2)
   1.575  
   1.576 -constdefs
   1.577 -  EL :: "nat => 'q_17157 hollight.list => 'q_17157" 
   1.578 +definition EL :: "nat => 'q_17157 hollight.list => 'q_17157" where 
   1.579    "EL ==
   1.580  SOME EL::nat => 'q_17157::type hollight.list => 'q_17157::type.
   1.581     (ALL l::'q_17157::type hollight.list. EL 0 l = HD l) &
   1.582 @@ -2654,8 +2596,7 @@
   1.583          EL (Suc n) l = EL n (TL l)))"
   1.584    by (import hollight DEF_EL)
   1.585  
   1.586 -constdefs
   1.587 -  FILTER :: "('q_17182 => bool) => 'q_17182 hollight.list => 'q_17182 hollight.list" 
   1.588 +definition FILTER :: "('q_17182 => bool) => 'q_17182 hollight.list => 'q_17182 hollight.list" where 
   1.589    "FILTER ==
   1.590  SOME FILTER::('q_17182::type => bool)
   1.591               => 'q_17182::type hollight.list
   1.592 @@ -2676,8 +2617,7 @@
   1.593          COND (P h) (CONS h (FILTER P t)) (FILTER P t)))"
   1.594    by (import hollight DEF_FILTER)
   1.595  
   1.596 -constdefs
   1.597 -  ASSOC :: "'q_17211 => ('q_17211 * 'q_17205) hollight.list => 'q_17205" 
   1.598 +definition ASSOC :: "'q_17211 => ('q_17211 * 'q_17205) hollight.list => 'q_17205" where 
   1.599    "ASSOC ==
   1.600  SOME ASSOC::'q_17211::type
   1.601              => ('q_17211::type * 'q_17205::type) hollight.list
   1.602 @@ -2695,9 +2635,8 @@
   1.603         ASSOC a (CONS h t) = COND (fst h = a) (snd h) (ASSOC a t))"
   1.604    by (import hollight DEF_ASSOC)
   1.605  
   1.606 -constdefs
   1.607 -  ITLIST2 :: "('q_17235 => 'q_17243 => 'q_17233 => 'q_17233)
   1.608 -=> 'q_17235 hollight.list => 'q_17243 hollight.list => 'q_17233 => 'q_17233" 
   1.609 +definition ITLIST2 :: "('q_17235 => 'q_17243 => 'q_17233 => 'q_17233)
   1.610 +=> 'q_17235 hollight.list => 'q_17243 hollight.list => 'q_17233 => 'q_17233" where 
   1.611    "ITLIST2 ==
   1.612  SOME ITLIST2::('q_17235::type
   1.613                 => 'q_17243::type => 'q_17233::type => 'q_17233::type)
   1.614 @@ -3041,8 +2980,7 @@
   1.615  ALL2 Q l l'"
   1.616    by (import hollight MONO_ALL2)
   1.617  
   1.618 -constdefs
   1.619 -  dist :: "nat * nat => nat" 
   1.620 +definition dist :: "nat * nat => nat" where 
   1.621    "dist == %u::nat * nat. fst u - snd u + (snd u - fst u)"
   1.622  
   1.623  lemma DEF_dist: "dist = (%u::nat * nat. fst u - snd u + (snd u - fst u))"
   1.624 @@ -3133,8 +3071,7 @@
   1.625     (EX (x::nat) N::nat. ALL i::nat. <= N i --> <= (P i) (Q i + x))"
   1.626    by (import hollight BOUNDS_IGNORE)
   1.627  
   1.628 -constdefs
   1.629 -  is_nadd :: "(nat => nat) => bool" 
   1.630 +definition is_nadd :: "(nat => nat) => bool" where 
   1.631    "is_nadd ==
   1.632  %u::nat => nat.
   1.633     EX B::nat.
   1.634 @@ -3211,8 +3148,7 @@
   1.635            (A * n + B)"
   1.636    by (import hollight NADD_ALTMUL)
   1.637  
   1.638 -constdefs
   1.639 -  nadd_eq :: "nadd => nadd => bool" 
   1.640 +definition nadd_eq :: "nadd => nadd => bool" where 
   1.641    "nadd_eq ==
   1.642  %(u::nadd) ua::nadd.
   1.643     EX B::nat. ALL n::nat. <= (dist (dest_nadd u n, dest_nadd ua n)) B"
   1.644 @@ -3231,8 +3167,7 @@
   1.645  lemma NADD_EQ_TRANS: "ALL (x::nadd) (y::nadd) z::nadd. nadd_eq x y & nadd_eq y z --> nadd_eq x z"
   1.646    by (import hollight NADD_EQ_TRANS)
   1.647  
   1.648 -constdefs
   1.649 -  nadd_of_num :: "nat => nadd" 
   1.650 +definition nadd_of_num :: "nat => nadd" where 
   1.651    "nadd_of_num == %u::nat. mk_nadd (op * u)"
   1.652  
   1.653  lemma DEF_nadd_of_num: "nadd_of_num = (%u::nat. mk_nadd (op * u))"
   1.654 @@ -3247,8 +3182,7 @@
   1.655  lemma NADD_OF_NUM_EQ: "ALL (m::nat) n::nat. nadd_eq (nadd_of_num m) (nadd_of_num n) = (m = n)"
   1.656    by (import hollight NADD_OF_NUM_EQ)
   1.657  
   1.658 -constdefs
   1.659 -  nadd_le :: "nadd => nadd => bool" 
   1.660 +definition nadd_le :: "nadd => nadd => bool" where 
   1.661    "nadd_le ==
   1.662  %(u::nadd) ua::nadd.
   1.663     EX B::nat. ALL n::nat. <= (dest_nadd u n) (dest_nadd ua n + B)"
   1.664 @@ -3289,8 +3223,7 @@
   1.665  lemma NADD_OF_NUM_LE: "ALL (m::nat) n::nat. nadd_le (nadd_of_num m) (nadd_of_num n) = <= m n"
   1.666    by (import hollight NADD_OF_NUM_LE)
   1.667  
   1.668 -constdefs
   1.669 -  nadd_add :: "nadd => nadd => nadd" 
   1.670 +definition nadd_add :: "nadd => nadd => nadd" where 
   1.671    "nadd_add ==
   1.672  %(u::nadd) ua::nadd. mk_nadd (%n::nat. dest_nadd u n + dest_nadd ua n)"
   1.673  
   1.674 @@ -3332,8 +3265,7 @@
   1.675      (nadd_of_num (x + xa))"
   1.676    by (import hollight NADD_OF_NUM_ADD)
   1.677  
   1.678 -constdefs
   1.679 -  nadd_mul :: "nadd => nadd => nadd" 
   1.680 +definition nadd_mul :: "nadd => nadd => nadd" where 
   1.681    "nadd_mul ==
   1.682  %(u::nadd) ua::nadd. mk_nadd (%n::nat. dest_nadd u (dest_nadd ua n))"
   1.683  
   1.684 @@ -3438,8 +3370,7 @@
   1.685     (EX (A::nat) N::nat. ALL n::nat. <= N n --> <= n (A * dest_nadd x n))"
   1.686    by (import hollight NADD_LBOUND)
   1.687  
   1.688 -constdefs
   1.689 -  nadd_rinv :: "nadd => nat => nat" 
   1.690 +definition nadd_rinv :: "nadd => nat => nat" where 
   1.691    "nadd_rinv == %(u::nadd) n::nat. DIV (n * n) (dest_nadd u n)"
   1.692  
   1.693  lemma DEF_nadd_rinv: "nadd_rinv = (%(u::nadd) n::nat. DIV (n * n) (dest_nadd u n))"
   1.694 @@ -3528,8 +3459,7 @@
   1.695            <= (dist (m * nadd_rinv x n, n * nadd_rinv x m)) (B * (m + n)))"
   1.696    by (import hollight NADD_MUL_LINV_LEMMA8)
   1.697  
   1.698 -constdefs
   1.699 -  nadd_inv :: "nadd => nadd" 
   1.700 +definition nadd_inv :: "nadd => nadd" where 
   1.701    "nadd_inv ==
   1.702  %u::nadd.
   1.703     COND (nadd_eq u (nadd_of_num 0)) (nadd_of_num 0) (mk_nadd (nadd_rinv u))"
   1.704 @@ -3570,15 +3500,13 @@
   1.705    [where a="a :: hreal" and r=r ,
   1.706     OF type_definition_hreal]
   1.707  
   1.708 -constdefs
   1.709 -  hreal_of_num :: "nat => hreal" 
   1.710 +definition hreal_of_num :: "nat => hreal" where 
   1.711    "hreal_of_num == %m::nat. mk_hreal (nadd_eq (nadd_of_num m))"
   1.712  
   1.713  lemma DEF_hreal_of_num: "hreal_of_num = (%m::nat. mk_hreal (nadd_eq (nadd_of_num m)))"
   1.714    by (import hollight DEF_hreal_of_num)
   1.715  
   1.716 -constdefs
   1.717 -  hreal_add :: "hreal => hreal => hreal" 
   1.718 +definition hreal_add :: "hreal => hreal => hreal" where 
   1.719    "hreal_add ==
   1.720  %(x::hreal) y::hreal.
   1.721     mk_hreal
   1.722 @@ -3594,8 +3522,7 @@
   1.723              nadd_eq (nadd_add xa ya) u & dest_hreal x xa & dest_hreal y ya))"
   1.724    by (import hollight DEF_hreal_add)
   1.725  
   1.726 -constdefs
   1.727 -  hreal_mul :: "hreal => hreal => hreal" 
   1.728 +definition hreal_mul :: "hreal => hreal => hreal" where 
   1.729    "hreal_mul ==
   1.730  %(x::hreal) y::hreal.
   1.731     mk_hreal
   1.732 @@ -3611,8 +3538,7 @@
   1.733              nadd_eq (nadd_mul xa ya) u & dest_hreal x xa & dest_hreal y ya))"
   1.734    by (import hollight DEF_hreal_mul)
   1.735  
   1.736 -constdefs
   1.737 -  hreal_le :: "hreal => hreal => bool" 
   1.738 +definition hreal_le :: "hreal => hreal => bool" where 
   1.739    "hreal_le ==
   1.740  %(x::hreal) y::hreal.
   1.741     SOME u::bool.
   1.742 @@ -3626,8 +3552,7 @@
   1.743            nadd_le xa ya = u & dest_hreal x xa & dest_hreal y ya)"
   1.744    by (import hollight DEF_hreal_le)
   1.745  
   1.746 -constdefs
   1.747 -  hreal_inv :: "hreal => hreal" 
   1.748 +definition hreal_inv :: "hreal => hreal" where 
   1.749    "hreal_inv ==
   1.750  %x::hreal.
   1.751     mk_hreal
   1.752 @@ -3685,22 +3610,19 @@
   1.753     hreal_le a b --> hreal_le (hreal_mul a c) (hreal_mul b c)"
   1.754    by (import hollight HREAL_LE_MUL_RCANCEL_IMP)
   1.755  
   1.756 -constdefs
   1.757 -  treal_of_num :: "nat => hreal * hreal" 
   1.758 +definition treal_of_num :: "nat => hreal * hreal" where 
   1.759    "treal_of_num == %u::nat. (hreal_of_num u, hreal_of_num 0)"
   1.760  
   1.761  lemma DEF_treal_of_num: "treal_of_num = (%u::nat. (hreal_of_num u, hreal_of_num 0))"
   1.762    by (import hollight DEF_treal_of_num)
   1.763  
   1.764 -constdefs
   1.765 -  treal_neg :: "hreal * hreal => hreal * hreal" 
   1.766 +definition treal_neg :: "hreal * hreal => hreal * hreal" where 
   1.767    "treal_neg == %u::hreal * hreal. (snd u, fst u)"
   1.768  
   1.769  lemma DEF_treal_neg: "treal_neg = (%u::hreal * hreal. (snd u, fst u))"
   1.770    by (import hollight DEF_treal_neg)
   1.771  
   1.772 -constdefs
   1.773 -  treal_add :: "hreal * hreal => hreal * hreal => hreal * hreal" 
   1.774 +definition treal_add :: "hreal * hreal => hreal * hreal => hreal * hreal" where 
   1.775    "treal_add ==
   1.776  %(u::hreal * hreal) ua::hreal * hreal.
   1.777     (hreal_add (fst u) (fst ua), hreal_add (snd u) (snd ua))"
   1.778 @@ -3710,8 +3632,7 @@
   1.779      (hreal_add (fst u) (fst ua), hreal_add (snd u) (snd ua)))"
   1.780    by (import hollight DEF_treal_add)
   1.781  
   1.782 -constdefs
   1.783 -  treal_mul :: "hreal * hreal => hreal * hreal => hreal * hreal" 
   1.784 +definition treal_mul :: "hreal * hreal => hreal * hreal => hreal * hreal" where 
   1.785    "treal_mul ==
   1.786  %(u::hreal * hreal) ua::hreal * hreal.
   1.787     (hreal_add (hreal_mul (fst u) (fst ua)) (hreal_mul (snd u) (snd ua)),
   1.788 @@ -3723,8 +3644,7 @@
   1.789       hreal_add (hreal_mul (fst u) (snd ua)) (hreal_mul (snd u) (fst ua))))"
   1.790    by (import hollight DEF_treal_mul)
   1.791  
   1.792 -constdefs
   1.793 -  treal_le :: "hreal * hreal => hreal * hreal => bool" 
   1.794 +definition treal_le :: "hreal * hreal => hreal * hreal => bool" where 
   1.795    "treal_le ==
   1.796  %(u::hreal * hreal) ua::hreal * hreal.
   1.797     hreal_le (hreal_add (fst u) (snd ua)) (hreal_add (fst ua) (snd u))"
   1.798 @@ -3734,8 +3654,7 @@
   1.799      hreal_le (hreal_add (fst u) (snd ua)) (hreal_add (fst ua) (snd u)))"
   1.800    by (import hollight DEF_treal_le)
   1.801  
   1.802 -constdefs
   1.803 -  treal_inv :: "hreal * hreal => hreal * hreal" 
   1.804 +definition treal_inv :: "hreal * hreal => hreal * hreal" where 
   1.805    "treal_inv ==
   1.806  %u::hreal * hreal.
   1.807     COND (fst u = snd u) (hreal_of_num 0, hreal_of_num 0)
   1.808 @@ -3755,8 +3674,7 @@
   1.809          hreal_inv (SOME d::hreal. snd u = hreal_add (fst u) d))))"
   1.810    by (import hollight DEF_treal_inv)
   1.811  
   1.812 -constdefs
   1.813 -  treal_eq :: "hreal * hreal => hreal * hreal => bool" 
   1.814 +definition treal_eq :: "hreal * hreal => hreal * hreal => bool" where 
   1.815    "treal_eq ==
   1.816  %(u::hreal * hreal) ua::hreal * hreal.
   1.817     hreal_add (fst u) (snd ua) = hreal_add (fst ua) (snd u)"
   1.818 @@ -3916,15 +3834,13 @@
   1.819    [where a="a :: hollight.real" and r=r ,
   1.820     OF type_definition_real]
   1.821  
   1.822 -constdefs
   1.823 -  real_of_num :: "nat => hollight.real" 
   1.824 +definition real_of_num :: "nat => hollight.real" where 
   1.825    "real_of_num == %m::nat. mk_real (treal_eq (treal_of_num m))"
   1.826  
   1.827  lemma DEF_real_of_num: "real_of_num = (%m::nat. mk_real (treal_eq (treal_of_num m)))"
   1.828    by (import hollight DEF_real_of_num)
   1.829  
   1.830 -constdefs
   1.831 -  real_neg :: "hollight.real => hollight.real" 
   1.832 +definition real_neg :: "hollight.real => hollight.real" where 
   1.833    "real_neg ==
   1.834  %x1::hollight.real.
   1.835     mk_real
   1.836 @@ -3940,8 +3856,7 @@
   1.837              treal_eq (treal_neg x1a) u & dest_real x1 x1a))"
   1.838    by (import hollight DEF_real_neg)
   1.839  
   1.840 -constdefs
   1.841 -  real_add :: "hollight.real => hollight.real => hollight.real" 
   1.842 +definition real_add :: "hollight.real => hollight.real => hollight.real" where 
   1.843    "real_add ==
   1.844  %(x1::hollight.real) y1::hollight.real.
   1.845     mk_real
   1.846 @@ -3959,8 +3874,7 @@
   1.847              dest_real x1 x1a & dest_real y1 y1a))"
   1.848    by (import hollight DEF_real_add)
   1.849  
   1.850 -constdefs
   1.851 -  real_mul :: "hollight.real => hollight.real => hollight.real" 
   1.852 +definition real_mul :: "hollight.real => hollight.real => hollight.real" where 
   1.853    "real_mul ==
   1.854  %(x1::hollight.real) y1::hollight.real.
   1.855     mk_real
   1.856 @@ -3978,8 +3892,7 @@
   1.857              dest_real x1 x1a & dest_real y1 y1a))"
   1.858    by (import hollight DEF_real_mul)
   1.859  
   1.860 -constdefs
   1.861 -  real_le :: "hollight.real => hollight.real => bool" 
   1.862 +definition real_le :: "hollight.real => hollight.real => bool" where 
   1.863    "real_le ==
   1.864  %(x1::hollight.real) y1::hollight.real.
   1.865     SOME u::bool.
   1.866 @@ -3993,8 +3906,7 @@
   1.867            treal_le x1a y1a = u & dest_real x1 x1a & dest_real y1 y1a)"
   1.868    by (import hollight DEF_real_le)
   1.869  
   1.870 -constdefs
   1.871 -  real_inv :: "hollight.real => hollight.real" 
   1.872 +definition real_inv :: "hollight.real => hollight.real" where 
   1.873    "real_inv ==
   1.874  %x::hollight.real.
   1.875     mk_real
   1.876 @@ -4008,15 +3920,13 @@
   1.877           EX xa::hreal * hreal. treal_eq (treal_inv xa) u & dest_real x xa))"
   1.878    by (import hollight DEF_real_inv)
   1.879  
   1.880 -constdefs
   1.881 -  real_sub :: "hollight.real => hollight.real => hollight.real" 
   1.882 +definition real_sub :: "hollight.real => hollight.real => hollight.real" where 
   1.883    "real_sub == %(u::hollight.real) ua::hollight.real. real_add u (real_neg ua)"
   1.884  
   1.885  lemma DEF_real_sub: "real_sub = (%(u::hollight.real) ua::hollight.real. real_add u (real_neg ua))"
   1.886    by (import hollight DEF_real_sub)
   1.887  
   1.888 -constdefs
   1.889 -  real_lt :: "hollight.real => hollight.real => bool" 
   1.890 +definition real_lt :: "hollight.real => hollight.real => bool" where 
   1.891    "real_lt == %(u::hollight.real) ua::hollight.real. ~ real_le ua u"
   1.892  
   1.893  lemma DEF_real_lt: "real_lt = (%(u::hollight.real) ua::hollight.real. ~ real_le ua u)"
   1.894 @@ -4040,8 +3950,7 @@
   1.895  lemma DEF_real_gt: "hollight.real_gt = (%(u::hollight.real) ua::hollight.real. real_lt ua u)"
   1.896    by (import hollight DEF_real_gt)
   1.897  
   1.898 -constdefs
   1.899 -  real_abs :: "hollight.real => hollight.real" 
   1.900 +definition real_abs :: "hollight.real => hollight.real" where 
   1.901    "real_abs ==
   1.902  %u::hollight.real. COND (real_le (real_of_num 0) u) u (real_neg u)"
   1.903  
   1.904 @@ -4049,8 +3958,7 @@
   1.905  (%u::hollight.real. COND (real_le (real_of_num 0) u) u (real_neg u))"
   1.906    by (import hollight DEF_real_abs)
   1.907  
   1.908 -constdefs
   1.909 -  real_pow :: "hollight.real => nat => hollight.real" 
   1.910 +definition real_pow :: "hollight.real => nat => hollight.real" where 
   1.911    "real_pow ==
   1.912  SOME real_pow::hollight.real => nat => hollight.real.
   1.913     (ALL x::hollight.real. real_pow x 0 = real_of_num (NUMERAL_BIT1 0)) &
   1.914 @@ -4064,22 +3972,19 @@
   1.915          real_pow x (Suc n) = real_mul x (real_pow x n)))"
   1.916    by (import hollight DEF_real_pow)
   1.917  
   1.918 -constdefs
   1.919 -  real_div :: "hollight.real => hollight.real => hollight.real" 
   1.920 +definition real_div :: "hollight.real => hollight.real => hollight.real" where 
   1.921    "real_div == %(u::hollight.real) ua::hollight.real. real_mul u (real_inv ua)"
   1.922  
   1.923  lemma DEF_real_div: "real_div = (%(u::hollight.real) ua::hollight.real. real_mul u (real_inv ua))"
   1.924    by (import hollight DEF_real_div)
   1.925  
   1.926 -constdefs
   1.927 -  real_max :: "hollight.real => hollight.real => hollight.real" 
   1.928 +definition real_max :: "hollight.real => hollight.real => hollight.real" where 
   1.929    "real_max == %(u::hollight.real) ua::hollight.real. COND (real_le u ua) ua u"
   1.930  
   1.931  lemma DEF_real_max: "real_max = (%(u::hollight.real) ua::hollight.real. COND (real_le u ua) ua u)"
   1.932    by (import hollight DEF_real_max)
   1.933  
   1.934 -constdefs
   1.935 -  real_min :: "hollight.real => hollight.real => hollight.real" 
   1.936 +definition real_min :: "hollight.real => hollight.real => hollight.real" where 
   1.937    "real_min == %(u::hollight.real) ua::hollight.real. COND (real_le u ua) u ua"
   1.938  
   1.939  lemma DEF_real_min: "real_min = (%(u::hollight.real) ua::hollight.real. COND (real_le u ua) u ua)"
   1.940 @@ -5212,8 +5117,7 @@
   1.941  (ALL x::hollight.real. All (P x))"
   1.942    by (import hollight REAL_WLOG_LT)
   1.943  
   1.944 -constdefs
   1.945 -  mod_real :: "hollight.real => hollight.real => hollight.real => bool" 
   1.946 +definition mod_real :: "hollight.real => hollight.real => hollight.real => bool" where 
   1.947    "mod_real ==
   1.948  %(u::hollight.real) (ua::hollight.real) ub::hollight.real.
   1.949     EX q::hollight.real. real_sub ua ub = real_mul q u"
   1.950 @@ -5223,8 +5127,7 @@
   1.951      EX q::hollight.real. real_sub ua ub = real_mul q u)"
   1.952    by (import hollight DEF_mod_real)
   1.953  
   1.954 -constdefs
   1.955 -  DECIMAL :: "nat => nat => hollight.real" 
   1.956 +definition DECIMAL :: "nat => nat => hollight.real" where 
   1.957    "DECIMAL == %(u::nat) ua::nat. real_div (real_of_num u) (real_of_num ua)"
   1.958  
   1.959  lemma DEF_DECIMAL: "DECIMAL = (%(u::nat) ua::nat. real_div (real_of_num u) (real_of_num ua))"
   1.960 @@ -5267,8 +5170,7 @@
   1.961  (real_mul x1 y2 = real_mul x2 y1)"
   1.962    by (import hollight RAT_LEMMA5)
   1.963  
   1.964 -constdefs
   1.965 -  is_int :: "hollight.real => bool" 
   1.966 +definition is_int :: "hollight.real => bool" where 
   1.967    "is_int ==
   1.968  %u::hollight.real.
   1.969     EX n::nat. u = real_of_num n | u = real_neg (real_of_num n)"
   1.970 @@ -5297,8 +5199,7 @@
   1.971        dest_int x = real_of_num n | dest_int x = real_neg (real_of_num n)"
   1.972    by (import hollight dest_int_rep)
   1.973  
   1.974 -constdefs
   1.975 -  int_le :: "hollight.int => hollight.int => bool" 
   1.976 +definition int_le :: "hollight.int => hollight.int => bool" where 
   1.977    "int_le ==
   1.978  %(u::hollight.int) ua::hollight.int. real_le (dest_int u) (dest_int ua)"
   1.979  
   1.980 @@ -5306,8 +5207,7 @@
   1.981  (%(u::hollight.int) ua::hollight.int. real_le (dest_int u) (dest_int ua))"
   1.982    by (import hollight DEF_int_le)
   1.983  
   1.984 -constdefs
   1.985 -  int_lt :: "hollight.int => hollight.int => bool" 
   1.986 +definition int_lt :: "hollight.int => hollight.int => bool" where 
   1.987    "int_lt ==
   1.988  %(u::hollight.int) ua::hollight.int. real_lt (dest_int u) (dest_int ua)"
   1.989  
   1.990 @@ -5315,8 +5215,7 @@
   1.991  (%(u::hollight.int) ua::hollight.int. real_lt (dest_int u) (dest_int ua))"
   1.992    by (import hollight DEF_int_lt)
   1.993  
   1.994 -constdefs
   1.995 -  int_ge :: "hollight.int => hollight.int => bool" 
   1.996 +definition int_ge :: "hollight.int => hollight.int => bool" where 
   1.997    "int_ge ==
   1.998  %(u::hollight.int) ua::hollight.int.
   1.999     hollight.real_ge (dest_int u) (dest_int ua)"
  1.1000 @@ -5326,8 +5225,7 @@
  1.1001      hollight.real_ge (dest_int u) (dest_int ua))"
  1.1002    by (import hollight DEF_int_ge)
  1.1003  
  1.1004 -constdefs
  1.1005 -  int_gt :: "hollight.int => hollight.int => bool" 
  1.1006 +definition int_gt :: "hollight.int => hollight.int => bool" where 
  1.1007    "int_gt ==
  1.1008  %(u::hollight.int) ua::hollight.int.
  1.1009     hollight.real_gt (dest_int u) (dest_int ua)"
  1.1010 @@ -5337,8 +5235,7 @@
  1.1011      hollight.real_gt (dest_int u) (dest_int ua))"
  1.1012    by (import hollight DEF_int_gt)
  1.1013  
  1.1014 -constdefs
  1.1015 -  int_of_num :: "nat => hollight.int" 
  1.1016 +definition int_of_num :: "nat => hollight.int" where 
  1.1017    "int_of_num == %u::nat. mk_int (real_of_num u)"
  1.1018  
  1.1019  lemma DEF_int_of_num: "int_of_num = (%u::nat. mk_int (real_of_num u))"
  1.1020 @@ -5347,8 +5244,7 @@
  1.1021  lemma int_of_num_th: "ALL x::nat. dest_int (int_of_num x) = real_of_num x"
  1.1022    by (import hollight int_of_num_th)
  1.1023  
  1.1024 -constdefs
  1.1025 -  int_neg :: "hollight.int => hollight.int" 
  1.1026 +definition int_neg :: "hollight.int => hollight.int" where 
  1.1027    "int_neg == %u::hollight.int. mk_int (real_neg (dest_int u))"
  1.1028  
  1.1029  lemma DEF_int_neg: "int_neg = (%u::hollight.int. mk_int (real_neg (dest_int u)))"
  1.1030 @@ -5357,8 +5253,7 @@
  1.1031  lemma int_neg_th: "ALL x::hollight.int. dest_int (int_neg x) = real_neg (dest_int x)"
  1.1032    by (import hollight int_neg_th)
  1.1033  
  1.1034 -constdefs
  1.1035 -  int_add :: "hollight.int => hollight.int => hollight.int" 
  1.1036 +definition int_add :: "hollight.int => hollight.int => hollight.int" where 
  1.1037    "int_add ==
  1.1038  %(u::hollight.int) ua::hollight.int.
  1.1039     mk_int (real_add (dest_int u) (dest_int ua))"
  1.1040 @@ -5372,8 +5267,7 @@
  1.1041     dest_int (int_add x xa) = real_add (dest_int x) (dest_int xa)"
  1.1042    by (import hollight int_add_th)
  1.1043  
  1.1044 -constdefs
  1.1045 -  int_sub :: "hollight.int => hollight.int => hollight.int" 
  1.1046 +definition int_sub :: "hollight.int => hollight.int => hollight.int" where 
  1.1047    "int_sub ==
  1.1048  %(u::hollight.int) ua::hollight.int.
  1.1049     mk_int (real_sub (dest_int u) (dest_int ua))"
  1.1050 @@ -5387,8 +5281,7 @@
  1.1051     dest_int (int_sub x xa) = real_sub (dest_int x) (dest_int xa)"
  1.1052    by (import hollight int_sub_th)
  1.1053  
  1.1054 -constdefs
  1.1055 -  int_mul :: "hollight.int => hollight.int => hollight.int" 
  1.1056 +definition int_mul :: "hollight.int => hollight.int => hollight.int" where 
  1.1057    "int_mul ==
  1.1058  %(u::hollight.int) ua::hollight.int.
  1.1059     mk_int (real_mul (dest_int u) (dest_int ua))"
  1.1060 @@ -5402,8 +5295,7 @@
  1.1061     dest_int (int_mul x y) = real_mul (dest_int x) (dest_int y)"
  1.1062    by (import hollight int_mul_th)
  1.1063  
  1.1064 -constdefs
  1.1065 -  int_abs :: "hollight.int => hollight.int" 
  1.1066 +definition int_abs :: "hollight.int => hollight.int" where 
  1.1067    "int_abs == %u::hollight.int. mk_int (real_abs (dest_int u))"
  1.1068  
  1.1069  lemma DEF_int_abs: "int_abs = (%u::hollight.int. mk_int (real_abs (dest_int u)))"
  1.1070 @@ -5412,8 +5304,7 @@
  1.1071  lemma int_abs_th: "ALL x::hollight.int. dest_int (int_abs x) = real_abs (dest_int x)"
  1.1072    by (import hollight int_abs_th)
  1.1073  
  1.1074 -constdefs
  1.1075 -  int_max :: "hollight.int => hollight.int => hollight.int" 
  1.1076 +definition int_max :: "hollight.int => hollight.int => hollight.int" where 
  1.1077    "int_max ==
  1.1078  %(u::hollight.int) ua::hollight.int.
  1.1079     mk_int (real_max (dest_int u) (dest_int ua))"
  1.1080 @@ -5427,8 +5318,7 @@
  1.1081     dest_int (int_max x y) = real_max (dest_int x) (dest_int y)"
  1.1082    by (import hollight int_max_th)
  1.1083  
  1.1084 -constdefs
  1.1085 -  int_min :: "hollight.int => hollight.int => hollight.int" 
  1.1086 +definition int_min :: "hollight.int => hollight.int => hollight.int" where 
  1.1087    "int_min ==
  1.1088  %(u::hollight.int) ua::hollight.int.
  1.1089     mk_int (real_min (dest_int u) (dest_int ua))"
  1.1090 @@ -5442,8 +5332,7 @@
  1.1091     dest_int (int_min x y) = real_min (dest_int x) (dest_int y)"
  1.1092    by (import hollight int_min_th)
  1.1093  
  1.1094 -constdefs
  1.1095 -  int_pow :: "hollight.int => nat => hollight.int" 
  1.1096 +definition int_pow :: "hollight.int => nat => hollight.int" where 
  1.1097    "int_pow == %(u::hollight.int) ua::nat. mk_int (real_pow (dest_int u) ua)"
  1.1098  
  1.1099  lemma DEF_int_pow: "int_pow = (%(u::hollight.int) ua::nat. mk_int (real_pow (dest_int u) ua))"
  1.1100 @@ -5496,8 +5385,7 @@
  1.1101     d ~= int_of_num 0 --> (EX c::hollight.int. int_lt x (int_mul c d))"
  1.1102    by (import hollight INT_ARCH)
  1.1103  
  1.1104 -constdefs
  1.1105 -  mod_int :: "hollight.int => hollight.int => hollight.int => bool" 
  1.1106 +definition mod_int :: "hollight.int => hollight.int => hollight.int => bool" where 
  1.1107    "mod_int ==
  1.1108  %(u::hollight.int) (ua::hollight.int) ub::hollight.int.
  1.1109     EX q::hollight.int. int_sub ua ub = int_mul q u"
  1.1110 @@ -5507,8 +5395,7 @@
  1.1111      EX q::hollight.int. int_sub ua ub = int_mul q u)"
  1.1112    by (import hollight DEF_mod_int)
  1.1113  
  1.1114 -constdefs
  1.1115 -  IN :: "'A => ('A => bool) => bool" 
  1.1116 +definition IN :: "'A => ('A => bool) => bool" where 
  1.1117    "IN == %(u::'A::type) ua::'A::type => bool. ua u"
  1.1118  
  1.1119  lemma DEF_IN: "IN = (%(u::'A::type) ua::'A::type => bool. ua u)"
  1.1120 @@ -5518,15 +5405,13 @@
  1.1121     (x = xa) = (ALL xb::'A::type. IN xb x = IN xb xa)"
  1.1122    by (import hollight EXTENSION)
  1.1123  
  1.1124 -constdefs
  1.1125 -  GSPEC :: "('A => bool) => 'A => bool" 
  1.1126 +definition GSPEC :: "('A => bool) => 'A => bool" where 
  1.1127    "GSPEC == %u::'A::type => bool. u"
  1.1128  
  1.1129  lemma DEF_GSPEC: "GSPEC = (%u::'A::type => bool. u)"
  1.1130    by (import hollight DEF_GSPEC)
  1.1131  
  1.1132 -constdefs
  1.1133 -  SETSPEC :: "'q_37056 => bool => 'q_37056 => bool" 
  1.1134 +definition SETSPEC :: "'q_37056 => bool => 'q_37056 => bool" where 
  1.1135    "SETSPEC == %(u::'q_37056::type) (ua::bool) ub::'q_37056::type. ua & u = ub"
  1.1136  
  1.1137  lemma DEF_SETSPEC: "SETSPEC = (%(u::'q_37056::type) (ua::bool) ub::'q_37056::type. ua & u = ub)"
  1.1138 @@ -5548,15 +5433,13 @@
  1.1139  (ALL (p::'q_37194::type => bool) x::'q_37194::type. IN x p = p x)"
  1.1140    by (import hollight IN_ELIM_THM)
  1.1141  
  1.1142 -constdefs
  1.1143 -  EMPTY :: "'A => bool" 
  1.1144 +definition EMPTY :: "'A => bool" where 
  1.1145    "EMPTY == %x::'A::type. False"
  1.1146  
  1.1147  lemma DEF_EMPTY: "EMPTY = (%x::'A::type. False)"
  1.1148    by (import hollight DEF_EMPTY)
  1.1149  
  1.1150 -constdefs
  1.1151 -  INSERT :: "'A => ('A => bool) => 'A => bool" 
  1.1152 +definition INSERT :: "'A => ('A => bool) => 'A => bool" where 
  1.1153    "INSERT == %(u::'A::type) (ua::'A::type => bool) y::'A::type. IN y ua | y = u"
  1.1154  
  1.1155  lemma DEF_INSERT: "INSERT =
  1.1156 @@ -5585,8 +5468,7 @@
  1.1157      GSPEC (%ub::'A::type. EX x::'A::type. SETSPEC ub (IN x u | IN x ua) x))"
  1.1158    by (import hollight DEF_UNION)
  1.1159  
  1.1160 -constdefs
  1.1161 -  UNIONS :: "(('A => bool) => bool) => 'A => bool" 
  1.1162 +definition UNIONS :: "(('A => bool) => bool) => 'A => bool" where 
  1.1163    "UNIONS ==
  1.1164  %u::('A::type => bool) => bool.
  1.1165     GSPEC
  1.1166 @@ -5615,8 +5497,7 @@
  1.1167      GSPEC (%ub::'A::type. EX x::'A::type. SETSPEC ub (IN x u & IN x ua) x))"
  1.1168    by (import hollight DEF_INTER)
  1.1169  
  1.1170 -constdefs
  1.1171 -  INTERS :: "(('A => bool) => bool) => 'A => bool" 
  1.1172 +definition INTERS :: "(('A => bool) => bool) => 'A => bool" where 
  1.1173    "INTERS ==
  1.1174  %u::('A::type => bool) => bool.
  1.1175     GSPEC
  1.1176 @@ -5632,8 +5513,7 @@
  1.1177              SETSPEC ua (ALL ua::'A::type => bool. IN ua u --> IN x ua) x))"
  1.1178    by (import hollight DEF_INTERS)
  1.1179  
  1.1180 -constdefs
  1.1181 -  DIFF :: "('A => bool) => ('A => bool) => 'A => bool" 
  1.1182 +definition DIFF :: "('A => bool) => ('A => bool) => 'A => bool" where 
  1.1183    "DIFF ==
  1.1184  %(u::'A::type => bool) ua::'A::type => bool.
  1.1185     GSPEC (%ub::'A::type. EX x::'A::type. SETSPEC ub (IN x u & ~ IN x ua) x)"
  1.1186 @@ -5648,8 +5528,7 @@
  1.1187  GSPEC (%u::'A::type. EX y::'A::type. SETSPEC u (IN y s | y = x) y)"
  1.1188    by (import hollight INSERT)
  1.1189  
  1.1190 -constdefs
  1.1191 -  DELETE :: "('A => bool) => 'A => 'A => bool" 
  1.1192 +definition DELETE :: "('A => bool) => 'A => 'A => bool" where 
  1.1193    "DELETE ==
  1.1194  %(u::'A::type => bool) ua::'A::type.
  1.1195     GSPEC (%ub::'A::type. EX y::'A::type. SETSPEC ub (IN y u & y ~= ua) y)"
  1.1196 @@ -5659,8 +5538,7 @@
  1.1197      GSPEC (%ub::'A::type. EX y::'A::type. SETSPEC ub (IN y u & y ~= ua) y))"
  1.1198    by (import hollight DEF_DELETE)
  1.1199  
  1.1200 -constdefs
  1.1201 -  SUBSET :: "('A => bool) => ('A => bool) => bool" 
  1.1202 +definition SUBSET :: "('A => bool) => ('A => bool) => bool" where 
  1.1203    "SUBSET ==
  1.1204  %(u::'A::type => bool) ua::'A::type => bool.
  1.1205     ALL x::'A::type. IN x u --> IN x ua"
  1.1206 @@ -5670,8 +5548,7 @@
  1.1207      ALL x::'A::type. IN x u --> IN x ua)"
  1.1208    by (import hollight DEF_SUBSET)
  1.1209  
  1.1210 -constdefs
  1.1211 -  PSUBSET :: "('A => bool) => ('A => bool) => bool" 
  1.1212 +definition PSUBSET :: "('A => bool) => ('A => bool) => bool" where 
  1.1213    "PSUBSET ==
  1.1214  %(u::'A::type => bool) ua::'A::type => bool. SUBSET u ua & u ~= ua"
  1.1215  
  1.1216 @@ -5679,8 +5556,7 @@
  1.1217  (%(u::'A::type => bool) ua::'A::type => bool. SUBSET u ua & u ~= ua)"
  1.1218    by (import hollight DEF_PSUBSET)
  1.1219  
  1.1220 -constdefs
  1.1221 -  DISJOINT :: "('A => bool) => ('A => bool) => bool" 
  1.1222 +definition DISJOINT :: "('A => bool) => ('A => bool) => bool" where 
  1.1223    "DISJOINT ==
  1.1224  %(u::'A::type => bool) ua::'A::type => bool. hollight.INTER u ua = EMPTY"
  1.1225  
  1.1226 @@ -5688,15 +5564,13 @@
  1.1227  (%(u::'A::type => bool) ua::'A::type => bool. hollight.INTER u ua = EMPTY)"
  1.1228    by (import hollight DEF_DISJOINT)
  1.1229  
  1.1230 -constdefs
  1.1231 -  SING :: "('A => bool) => bool" 
  1.1232 +definition SING :: "('A => bool) => bool" where 
  1.1233    "SING == %u::'A::type => bool. EX x::'A::type. u = INSERT x EMPTY"
  1.1234  
  1.1235  lemma DEF_SING: "SING = (%u::'A::type => bool. EX x::'A::type. u = INSERT x EMPTY)"
  1.1236    by (import hollight DEF_SING)
  1.1237  
  1.1238 -constdefs
  1.1239 -  FINITE :: "('A => bool) => bool" 
  1.1240 +definition FINITE :: "('A => bool) => bool" where 
  1.1241    "FINITE ==
  1.1242  %a::'A::type => bool.
  1.1243     ALL FINITE'::('A::type => bool) => bool.
  1.1244 @@ -5718,15 +5592,13 @@
  1.1245         FINITE' a)"
  1.1246    by (import hollight DEF_FINITE)
  1.1247  
  1.1248 -constdefs
  1.1249 -  INFINITE :: "('A => bool) => bool" 
  1.1250 +definition INFINITE :: "('A => bool) => bool" where 
  1.1251    "INFINITE == %u::'A::type => bool. ~ FINITE u"
  1.1252  
  1.1253  lemma DEF_INFINITE: "INFINITE = (%u::'A::type => bool. ~ FINITE u)"
  1.1254    by (import hollight DEF_INFINITE)
  1.1255  
  1.1256 -constdefs
  1.1257 -  IMAGE :: "('A => 'B) => ('A => bool) => 'B => bool" 
  1.1258 +definition IMAGE :: "('A => 'B) => ('A => bool) => 'B => bool" where 
  1.1259    "IMAGE ==
  1.1260  %(u::'A::type => 'B::type) ua::'A::type => bool.
  1.1261     GSPEC
  1.1262 @@ -5740,8 +5612,7 @@
  1.1263           EX y::'B::type. SETSPEC ub (EX x::'A::type. IN x ua & y = u x) y))"
  1.1264    by (import hollight DEF_IMAGE)
  1.1265  
  1.1266 -constdefs
  1.1267 -  INJ :: "('A => 'B) => ('A => bool) => ('B => bool) => bool" 
  1.1268 +definition INJ :: "('A => 'B) => ('A => bool) => ('B => bool) => bool" where 
  1.1269    "INJ ==
  1.1270  %(u::'A::type => 'B::type) (ua::'A::type => bool) ub::'B::type => bool.
  1.1271     (ALL x::'A::type. IN x ua --> IN (u x) ub) &
  1.1272 @@ -5754,8 +5625,7 @@
  1.1273          IN x ua & IN y ua & u x = u y --> x = y))"
  1.1274    by (import hollight DEF_INJ)
  1.1275  
  1.1276 -constdefs
  1.1277 -  SURJ :: "('A => 'B) => ('A => bool) => ('B => bool) => bool" 
  1.1278 +definition SURJ :: "('A => 'B) => ('A => bool) => ('B => bool) => bool" where 
  1.1279    "SURJ ==
  1.1280  %(u::'A::type => 'B::type) (ua::'A::type => bool) ub::'B::type => bool.
  1.1281     (ALL x::'A::type. IN x ua --> IN (u x) ub) &
  1.1282 @@ -5767,8 +5637,7 @@
  1.1283      (ALL x::'B::type. IN x ub --> (EX y::'A::type. IN y ua & u y = x)))"
  1.1284    by (import hollight DEF_SURJ)
  1.1285  
  1.1286 -constdefs
  1.1287 -  BIJ :: "('A => 'B) => ('A => bool) => ('B => bool) => bool" 
  1.1288 +definition BIJ :: "('A => 'B) => ('A => bool) => ('B => bool) => bool" where 
  1.1289    "BIJ ==
  1.1290  %(u::'A::type => 'B::type) (ua::'A::type => bool) ub::'B::type => bool.
  1.1291     INJ u ua ub & SURJ u ua ub"
  1.1292 @@ -5778,22 +5647,19 @@
  1.1293      INJ u ua ub & SURJ u ua ub)"
  1.1294    by (import hollight DEF_BIJ)
  1.1295  
  1.1296 -constdefs
  1.1297 -  CHOICE :: "('A => bool) => 'A" 
  1.1298 +definition CHOICE :: "('A => bool) => 'A" where 
  1.1299    "CHOICE == %u::'A::type => bool. SOME x::'A::type. IN x u"
  1.1300  
  1.1301  lemma DEF_CHOICE: "CHOICE = (%u::'A::type => bool. SOME x::'A::type. IN x u)"
  1.1302    by (import hollight DEF_CHOICE)
  1.1303  
  1.1304 -constdefs
  1.1305 -  REST :: "('A => bool) => 'A => bool" 
  1.1306 +definition REST :: "('A => bool) => 'A => bool" where 
  1.1307    "REST == %u::'A::type => bool. DELETE u (CHOICE u)"
  1.1308  
  1.1309  lemma DEF_REST: "REST = (%u::'A::type => bool. DELETE u (CHOICE u))"
  1.1310    by (import hollight DEF_REST)
  1.1311  
  1.1312 -constdefs
  1.1313 -  CARD_GE :: "('q_37693 => bool) => ('q_37690 => bool) => bool" 
  1.1314 +definition CARD_GE :: "('q_37693 => bool) => ('q_37690 => bool) => bool" where 
  1.1315    "CARD_GE ==
  1.1316  %(u::'q_37693::type => bool) ua::'q_37690::type => bool.
  1.1317     EX f::'q_37693::type => 'q_37690::type.
  1.1318 @@ -5807,8 +5673,7 @@
  1.1319            IN y ua --> (EX x::'q_37693::type. IN x u & y = f x))"
  1.1320    by (import hollight DEF_CARD_GE)
  1.1321  
  1.1322 -constdefs
  1.1323 -  CARD_LE :: "('q_37702 => bool) => ('q_37701 => bool) => bool" 
  1.1324 +definition CARD_LE :: "('q_37702 => bool) => ('q_37701 => bool) => bool" where 
  1.1325    "CARD_LE ==
  1.1326  %(u::'q_37702::type => bool) ua::'q_37701::type => bool. CARD_GE ua u"
  1.1327  
  1.1328 @@ -5816,8 +5681,7 @@
  1.1329  (%(u::'q_37702::type => bool) ua::'q_37701::type => bool. CARD_GE ua u)"
  1.1330    by (import hollight DEF_CARD_LE)
  1.1331  
  1.1332 -constdefs
  1.1333 -  CARD_EQ :: "('q_37712 => bool) => ('q_37713 => bool) => bool" 
  1.1334 +definition CARD_EQ :: "('q_37712 => bool) => ('q_37713 => bool) => bool" where 
  1.1335    "CARD_EQ ==
  1.1336  %(u::'q_37712::type => bool) ua::'q_37713::type => bool.
  1.1337     CARD_LE u ua & CARD_LE ua u"
  1.1338 @@ -5827,8 +5691,7 @@
  1.1339      CARD_LE u ua & CARD_LE ua u)"
  1.1340    by (import hollight DEF_CARD_EQ)
  1.1341  
  1.1342 -constdefs
  1.1343 -  CARD_GT :: "('q_37727 => bool) => ('q_37728 => bool) => bool" 
  1.1344 +definition CARD_GT :: "('q_37727 => bool) => ('q_37728 => bool) => bool" where 
  1.1345    "CARD_GT ==
  1.1346  %(u::'q_37727::type => bool) ua::'q_37728::type => bool.
  1.1347     CARD_GE u ua & ~ CARD_GE ua u"
  1.1348 @@ -5838,8 +5701,7 @@
  1.1349      CARD_GE u ua & ~ CARD_GE ua u)"
  1.1350    by (import hollight DEF_CARD_GT)
  1.1351  
  1.1352 -constdefs
  1.1353 -  CARD_LT :: "('q_37743 => bool) => ('q_37744 => bool) => bool" 
  1.1354 +definition CARD_LT :: "('q_37743 => bool) => ('q_37744 => bool) => bool" where 
  1.1355    "CARD_LT ==
  1.1356  %(u::'q_37743::type => bool) ua::'q_37744::type => bool.
  1.1357     CARD_LE u ua & ~ CARD_LE ua u"
  1.1358 @@ -5849,8 +5711,7 @@
  1.1359      CARD_LE u ua & ~ CARD_LE ua u)"
  1.1360    by (import hollight DEF_CARD_LT)
  1.1361  
  1.1362 -constdefs
  1.1363 -  COUNTABLE :: "('q_37757 => bool) => bool" 
  1.1364 +definition COUNTABLE :: "('q_37757 => bool) => bool" where 
  1.1365    "(op ==::(('q_37757::type => bool) => bool)
  1.1366          => (('q_37757::type => bool) => bool) => prop)
  1.1367   (COUNTABLE::('q_37757::type => bool) => bool)
  1.1368 @@ -6470,9 +6331,8 @@
  1.1369     FINITE s --> FINITE (DIFF s t)"
  1.1370    by (import hollight FINITE_DIFF)
  1.1371  
  1.1372 -constdefs
  1.1373 -  FINREC :: "('q_41824 => 'q_41823 => 'q_41823)
  1.1374 -=> 'q_41823 => ('q_41824 => bool) => 'q_41823 => nat => bool" 
  1.1375 +definition FINREC :: "('q_41824 => 'q_41823 => 'q_41823)
  1.1376 +=> 'q_41823 => ('q_41824 => bool) => 'q_41823 => nat => bool" where 
  1.1377    "FINREC ==
  1.1378  SOME FINREC::('q_41824::type => 'q_41823::type => 'q_41823::type)
  1.1379               => 'q_41823::type
  1.1380 @@ -6558,9 +6418,8 @@
  1.1381             FINITE s --> g (INSERT x s) = COND (IN x s) (g s) (f x (g s))))"
  1.1382    by (import hollight SET_RECURSION_LEMMA)
  1.1383  
  1.1384 -constdefs
  1.1385 -  ITSET :: "('q_42525 => 'q_42524 => 'q_42524)
  1.1386 -=> ('q_42525 => bool) => 'q_42524 => 'q_42524" 
  1.1387 +definition ITSET :: "('q_42525 => 'q_42524 => 'q_42524)
  1.1388 +=> ('q_42525 => bool) => 'q_42524 => 'q_42524" where 
  1.1389    "ITSET ==
  1.1390  %(u::'q_42525::type => 'q_42524::type => 'q_42524::type)
  1.1391     (ua::'q_42525::type => bool) ub::'q_42524::type.
  1.1392 @@ -6630,8 +6489,7 @@
  1.1393            EX x::'A::type. SETSPEC u (IN x s & (P::'A::type => bool) x) x))"
  1.1394    by (import hollight FINITE_RESTRICT)
  1.1395  
  1.1396 -constdefs
  1.1397 -  CARD :: "('q_42918 => bool) => nat" 
  1.1398 +definition CARD :: "('q_42918 => bool) => nat" where 
  1.1399    "CARD == %u::'q_42918::type => bool. ITSET (%x::'q_42918::type. Suc) u 0"
  1.1400  
  1.1401  lemma DEF_CARD: "CARD = (%u::'q_42918::type => bool. ITSET (%x::'q_42918::type. Suc) u 0)"
  1.1402 @@ -6674,8 +6532,7 @@
  1.1403     CARD s + CARD t = CARD u"
  1.1404    by (import hollight CARD_UNION_EQ)
  1.1405  
  1.1406 -constdefs
  1.1407 -  HAS_SIZE :: "('q_43199 => bool) => nat => bool" 
  1.1408 +definition HAS_SIZE :: "('q_43199 => bool) => nat => bool" where 
  1.1409    "HAS_SIZE == %(u::'q_43199::type => bool) ua::nat. FINITE u & CARD u = ua"
  1.1410  
  1.1411  lemma DEF_HAS_SIZE: "HAS_SIZE = (%(u::'q_43199::type => bool) ua::nat. FINITE u & CARD u = ua)"
  1.1412 @@ -6944,8 +6801,7 @@
  1.1413         (ALL xa::'A::type. IN xa x --> (EX! m::nat. < m n & f m = xa)))"
  1.1414    by (import hollight HAS_SIZE_INDEX)
  1.1415  
  1.1416 -constdefs
  1.1417 -  set_of_list :: "'q_45968 hollight.list => 'q_45968 => bool" 
  1.1418 +definition set_of_list :: "'q_45968 hollight.list => 'q_45968 => bool" where 
  1.1419    "set_of_list ==
  1.1420  SOME set_of_list::'q_45968::type hollight.list => 'q_45968::type => bool.
  1.1421     set_of_list NIL = EMPTY &
  1.1422 @@ -6959,8 +6815,7 @@
  1.1423          set_of_list (CONS h t) = INSERT h (set_of_list t)))"
  1.1424    by (import hollight DEF_set_of_list)
  1.1425  
  1.1426 -constdefs
  1.1427 -  list_of_set :: "('q_45986 => bool) => 'q_45986 hollight.list" 
  1.1428 +definition list_of_set :: "('q_45986 => bool) => 'q_45986 hollight.list" where 
  1.1429    "list_of_set ==
  1.1430  %u::'q_45986::type => bool.
  1.1431     SOME l::'q_45986::type hollight.list.
  1.1432 @@ -6999,8 +6854,7 @@
  1.1433     hollight.UNION (set_of_list x) (set_of_list xa)"
  1.1434    by (import hollight SET_OF_LIST_APPEND)
  1.1435  
  1.1436 -constdefs
  1.1437 -  pairwise :: "('q_46198 => 'q_46198 => bool) => ('q_46198 => bool) => bool" 
  1.1438 +definition pairwise :: "('q_46198 => 'q_46198 => bool) => ('q_46198 => bool) => bool" where 
  1.1439    "pairwise ==
  1.1440  %(u::'q_46198::type => 'q_46198::type => bool) ua::'q_46198::type => bool.
  1.1441     ALL (x::'q_46198::type) y::'q_46198::type.
  1.1442 @@ -7012,8 +6866,7 @@
  1.1443         IN x ua & IN y ua & x ~= y --> u x y)"
  1.1444    by (import hollight DEF_pairwise)
  1.1445  
  1.1446 -constdefs
  1.1447 -  PAIRWISE :: "('q_46220 => 'q_46220 => bool) => 'q_46220 hollight.list => bool" 
  1.1448 +definition PAIRWISE :: "('q_46220 => 'q_46220 => bool) => 'q_46220 hollight.list => bool" where 
  1.1449    "PAIRWISE ==
  1.1450  SOME PAIRWISE::('q_46220::type => 'q_46220::type => bool)
  1.1451                 => 'q_46220::type hollight.list => bool.
  1.1452 @@ -7075,8 +6928,7 @@
  1.1453         (EMPTY::'A::type => bool))))"
  1.1454    by (import hollight FINITE_IMAGE_IMAGE)
  1.1455  
  1.1456 -constdefs
  1.1457 -  dimindex :: "('A => bool) => nat" 
  1.1458 +definition dimindex :: "('A => bool) => nat" where 
  1.1459    "(op ==::(('A::type => bool) => nat) => (('A::type => bool) => nat) => prop)
  1.1460   (dimindex::('A::type => bool) => nat)
  1.1461   (%u::'A::type => bool.
  1.1462 @@ -7125,8 +6977,7 @@
  1.1463     dimindex s = dimindex t"
  1.1464    by (import hollight DIMINDEX_FINITE_IMAGE)
  1.1465  
  1.1466 -constdefs
  1.1467 -  finite_index :: "nat => 'A" 
  1.1468 +definition finite_index :: "nat => 'A" where 
  1.1469    "(op ==::(nat => 'A::type) => (nat => 'A::type) => prop)
  1.1470   (finite_index::nat => 'A::type)
  1.1471   ((Eps::((nat => 'A::type) => bool) => nat => 'A::type)
  1.1472 @@ -7287,8 +7138,7 @@
  1.1473                        xa))))))"
  1.1474    by (import hollight CART_EQ)
  1.1475  
  1.1476 -constdefs
  1.1477 -  lambda :: "(nat => 'A) => ('A, 'B) cart" 
  1.1478 +definition lambda :: "(nat => 'A) => ('A, 'B) cart" where 
  1.1479    "(op ==::((nat => 'A::type) => ('A::type, 'B::type) cart)
  1.1480          => ((nat => 'A::type) => ('A::type, 'B::type) cart) => prop)
  1.1481   (lambda::(nat => 'A::type) => ('A::type, 'B::type) cart)
  1.1482 @@ -7388,8 +7238,7 @@
  1.1483    [where a="a :: ('A, 'B) finite_sum" and r=r ,
  1.1484     OF type_definition_finite_sum]
  1.1485  
  1.1486 -constdefs
  1.1487 -  pastecart :: "('A, 'M) cart => ('A, 'N) cart => ('A, ('M, 'N) finite_sum) cart" 
  1.1488 +definition pastecart :: "('A, 'M) cart => ('A, 'N) cart => ('A, ('M, 'N) finite_sum) cart" where 
  1.1489    "(op ==::(('A::type, 'M::type) cart
  1.1490           => ('A::type, 'N::type) cart
  1.1491              => ('A::type, ('M::type, 'N::type) finite_sum) cart)
  1.1492 @@ -7439,8 +7288,7 @@
  1.1493                   (hollight.UNIV::'M::type => bool))))))"
  1.1494    by (import hollight DEF_pastecart)
  1.1495  
  1.1496 -constdefs
  1.1497 -  fstcart :: "('A, ('M, 'N) finite_sum) cart => ('A, 'M) cart" 
  1.1498 +definition fstcart :: "('A, ('M, 'N) finite_sum) cart => ('A, 'M) cart" where 
  1.1499    "fstcart ==
  1.1500  %u::('A::type, ('M::type, 'N::type) finite_sum) cart. lambda ($ u)"
  1.1501  
  1.1502 @@ -7448,8 +7296,7 @@
  1.1503  (%u::('A::type, ('M::type, 'N::type) finite_sum) cart. lambda ($ u))"
  1.1504    by (import hollight DEF_fstcart)
  1.1505  
  1.1506 -constdefs
  1.1507 -  sndcart :: "('A, ('M, 'N) finite_sum) cart => ('A, 'N) cart" 
  1.1508 +definition sndcart :: "('A, ('M, 'N) finite_sum) cart => ('A, 'N) cart" where 
  1.1509    "(op ==::(('A::type, ('M::type, 'N::type) finite_sum) cart
  1.1510           => ('A::type, 'N::type) cart)
  1.1511          => (('A::type, ('M::type, 'N::type) finite_sum) cart
  1.1512 @@ -7616,8 +7463,7 @@
  1.1513     (EX xb::'q_48070::type => 'q_48091::type. x = xb o xa)"
  1.1514    by (import hollight FUNCTION_FACTORS_LEFT)
  1.1515  
  1.1516 -constdefs
  1.1517 -  dotdot :: "nat => nat => nat => bool" 
  1.1518 +definition dotdot :: "nat => nat => nat => bool" where 
  1.1519    "dotdot ==
  1.1520  %(u::nat) ua::nat.
  1.1521     GSPEC (%ub::nat. EX x::nat. SETSPEC ub (<= u x & <= x ua) x)"
  1.1522 @@ -7718,8 +7564,7 @@
  1.1523     SUBSET (dotdot m n) (dotdot p q) = (< n m | <= p m & <= n q)"
  1.1524    by (import hollight SUBSET_NUMSEG)
  1.1525  
  1.1526 -constdefs
  1.1527 -  neutral :: "('q_48985 => 'q_48985 => 'q_48985) => 'q_48985" 
  1.1528 +definition neutral :: "('q_48985 => 'q_48985 => 'q_48985) => 'q_48985" where 
  1.1529    "neutral ==
  1.1530  %u::'q_48985::type => 'q_48985::type => 'q_48985::type.
  1.1531     SOME x::'q_48985::type. ALL y::'q_48985::type. u x y = y & u y x = y"
  1.1532 @@ -7729,8 +7574,7 @@
  1.1533      SOME x::'q_48985::type. ALL y::'q_48985::type. u x y = y & u y x = y)"
  1.1534    by (import hollight DEF_neutral)
  1.1535  
  1.1536 -constdefs
  1.1537 -  monoidal :: "('A => 'A => 'A) => bool" 
  1.1538 +definition monoidal :: "('A => 'A => 'A) => bool" where 
  1.1539    "monoidal ==
  1.1540  %u::'A::type => 'A::type => 'A::type.
  1.1541     (ALL (x::'A::type) y::'A::type. u x y = u y x) &
  1.1542 @@ -7746,8 +7590,7 @@
  1.1543      (ALL x::'A::type. u (neutral u) x = x))"
  1.1544    by (import hollight DEF_monoidal)
  1.1545  
  1.1546 -constdefs
  1.1547 -  support :: "('B => 'B => 'B) => ('A => 'B) => ('A => bool) => 'A => bool" 
  1.1548 +definition support :: "('B => 'B => 'B) => ('A => 'B) => ('A => bool) => 'A => bool" where 
  1.1549    "support ==
  1.1550  %(u::'B::type => 'B::type => 'B::type) (ua::'A::type => 'B::type)
  1.1551     ub::'A::type => bool.
  1.1552 @@ -7763,9 +7606,8 @@
  1.1553           EX x::'A::type. SETSPEC uc (IN x ub & ua x ~= neutral u) x))"
  1.1554    by (import hollight DEF_support)
  1.1555  
  1.1556 -constdefs
  1.1557 -  iterate :: "('q_49090 => 'q_49090 => 'q_49090)
  1.1558 -=> ('A => bool) => ('A => 'q_49090) => 'q_49090" 
  1.1559 +definition iterate :: "('q_49090 => 'q_49090 => 'q_49090)
  1.1560 +=> ('A => bool) => ('A => 'q_49090) => 'q_49090" where 
  1.1561    "iterate ==
  1.1562  %(u::'q_49090::type => 'q_49090::type => 'q_49090::type)
  1.1563     (ua::'A::type => bool) ub::'A::type => 'q_49090::type.
  1.1564 @@ -8017,8 +7859,7 @@
  1.1565         iterate u_4247 s f = iterate u_4247 t g)"
  1.1566    by (import hollight ITERATE_EQ_GENERAL)
  1.1567  
  1.1568 -constdefs
  1.1569 -  nsum :: "('q_51017 => bool) => ('q_51017 => nat) => nat" 
  1.1570 +definition nsum :: "('q_51017 => bool) => ('q_51017 => nat) => nat" where 
  1.1571    "(op ==::(('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  1.1572          => (('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  1.1573             => prop)
  1.1574 @@ -8965,9 +8806,8 @@
  1.1575     hollight.sum x xb = hollight.sum xa xc"
  1.1576    by (import hollight SUM_EQ_GENERAL)
  1.1577  
  1.1578 -constdefs
  1.1579 -  CASEWISE :: "(('q_57926 => 'q_57930) * ('q_57931 => 'q_57926 => 'q_57890)) hollight.list
  1.1580 -=> 'q_57931 => 'q_57930 => 'q_57890" 
  1.1581 +definition CASEWISE :: "(('q_57926 => 'q_57930) * ('q_57931 => 'q_57926 => 'q_57890)) hollight.list
  1.1582 +=> 'q_57931 => 'q_57930 => 'q_57890" where 
  1.1583    "CASEWISE ==
  1.1584  SOME CASEWISE::(('q_57926::type => 'q_57930::type) *
  1.1585                  ('q_57931::type
  1.1586 @@ -9084,11 +8924,10 @@
  1.1587      x"
  1.1588    by (import hollight CASEWISE_WORKS)
  1.1589  
  1.1590 -constdefs
  1.1591 -  admissible :: "('q_58228 => 'q_58221 => bool)
  1.1592 +definition admissible :: "('q_58228 => 'q_58221 => bool)
  1.1593  => (('q_58228 => 'q_58224) => 'q_58234 => bool)
  1.1594     => ('q_58234 => 'q_58221)
  1.1595 -      => (('q_58228 => 'q_58224) => 'q_58234 => 'q_58229) => bool" 
  1.1596 +      => (('q_58228 => 'q_58224) => 'q_58234 => 'q_58229) => bool" where 
  1.1597    "admissible ==
  1.1598  %(u::'q_58228::type => 'q_58221::type => bool)
  1.1599     (ua::('q_58228::type => 'q_58224::type) => 'q_58234::type => bool)
  1.1600 @@ -9114,10 +8953,9 @@
  1.1601         uc f a = uc g a)"
  1.1602    by (import hollight DEF_admissible)
  1.1603  
  1.1604 -constdefs
  1.1605 -  tailadmissible :: "('A => 'A => bool)
  1.1606 +definition tailadmissible :: "('A => 'A => bool)
  1.1607  => (('A => 'B) => 'P => bool)
  1.1608 -   => ('P => 'A) => (('A => 'B) => 'P => 'B) => bool" 
  1.1609 +   => ('P => 'A) => (('A => 'B) => 'P => 'B) => bool" where 
  1.1610    "tailadmissible ==
  1.1611  %(u::'A::type => 'A::type => bool)
  1.1612     (ua::('A::type => 'B::type) => 'P::type => bool)
  1.1613 @@ -9151,11 +8989,10 @@
  1.1614             ua f a --> uc f a = COND (P f a) (f (G f a)) (H f a)))"
  1.1615    by (import hollight DEF_tailadmissible)
  1.1616  
  1.1617 -constdefs
  1.1618 -  superadmissible :: "('q_58378 => 'q_58378 => bool)
  1.1619 +definition superadmissible :: "('q_58378 => 'q_58378 => bool)
  1.1620  => (('q_58378 => 'q_58380) => 'q_58386 => bool)
  1.1621     => ('q_58386 => 'q_58378)
  1.1622 -      => (('q_58378 => 'q_58380) => 'q_58386 => 'q_58380) => bool" 
  1.1623 +      => (('q_58378 => 'q_58380) => 'q_58386 => 'q_58380) => bool" where 
  1.1624    "superadmissible ==
  1.1625  %(u::'q_58378::type => 'q_58378::type => bool)
  1.1626     (ua::('q_58378::type => 'q_58380::type) => 'q_58386::type => bool)