src/HOL/Import/HOL/HOL4Base.thy
changeset 35416 d8d7d1b785af
parent 30971 7fbebf75b3ef
child 37600 18f69eb29e66
     1.1 --- a/src/HOL/Import/HOL/HOL4Base.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/Import/HOL/HOL4Base.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -4,22 +4,19 @@
     1.4  
     1.5  ;setup_theory bool
     1.6  
     1.7 -constdefs
     1.8 -  ARB :: "'a" 
     1.9 +definition ARB :: "'a" where 
    1.10    "ARB == SOME x::'a::type. True"
    1.11  
    1.12  lemma ARB_DEF: "ARB = (SOME x::'a::type. True)"
    1.13    by (import bool ARB_DEF)
    1.14  
    1.15 -constdefs
    1.16 -  IN :: "'a => ('a => bool) => bool" 
    1.17 +definition IN :: "'a => ('a => bool) => bool" where 
    1.18    "IN == %(x::'a::type) f::'a::type => bool. f x"
    1.19  
    1.20  lemma IN_DEF: "IN = (%(x::'a::type) f::'a::type => bool. f x)"
    1.21    by (import bool IN_DEF)
    1.22  
    1.23 -constdefs
    1.24 -  RES_FORALL :: "('a => bool) => ('a => bool) => bool" 
    1.25 +definition RES_FORALL :: "('a => bool) => ('a => bool) => bool" where 
    1.26    "RES_FORALL ==
    1.27  %(p::'a::type => bool) m::'a::type => bool. ALL x::'a::type. IN x p --> m x"
    1.28  
    1.29 @@ -28,8 +25,7 @@
    1.30      ALL x::'a::type. IN x p --> m x)"
    1.31    by (import bool RES_FORALL_DEF)
    1.32  
    1.33 -constdefs
    1.34 -  RES_EXISTS :: "('a => bool) => ('a => bool) => bool" 
    1.35 +definition RES_EXISTS :: "('a => bool) => ('a => bool) => bool" where 
    1.36    "RES_EXISTS ==
    1.37  %(p::'a::type => bool) m::'a::type => bool. EX x::'a::type. IN x p & m x"
    1.38  
    1.39 @@ -37,8 +33,7 @@
    1.40  (%(p::'a::type => bool) m::'a::type => bool. EX x::'a::type. IN x p & m x)"
    1.41    by (import bool RES_EXISTS_DEF)
    1.42  
    1.43 -constdefs
    1.44 -  RES_EXISTS_UNIQUE :: "('a => bool) => ('a => bool) => bool" 
    1.45 +definition RES_EXISTS_UNIQUE :: "('a => bool) => ('a => bool) => bool" where 
    1.46    "RES_EXISTS_UNIQUE ==
    1.47  %(p::'a::type => bool) m::'a::type => bool.
    1.48     RES_EXISTS p m &
    1.49 @@ -52,8 +47,7 @@
    1.50       (%x::'a::type. RES_FORALL p (%y::'a::type. m x & m y --> x = y)))"
    1.51    by (import bool RES_EXISTS_UNIQUE_DEF)
    1.52  
    1.53 -constdefs
    1.54 -  RES_SELECT :: "('a => bool) => ('a => bool) => 'a" 
    1.55 +definition RES_SELECT :: "('a => bool) => ('a => bool) => 'a" where 
    1.56    "RES_SELECT ==
    1.57  %(p::'a::type => bool) m::'a::type => bool. SOME x::'a::type. IN x p & m x"
    1.58  
    1.59 @@ -264,15 +258,13 @@
    1.60  
    1.61  ;setup_theory combin
    1.62  
    1.63 -constdefs
    1.64 -  K :: "'a => 'b => 'a" 
    1.65 +definition K :: "'a => 'b => 'a" where 
    1.66    "K == %(x::'a::type) y::'b::type. x"
    1.67  
    1.68  lemma K_DEF: "K = (%(x::'a::type) y::'b::type. x)"
    1.69    by (import combin K_DEF)
    1.70  
    1.71 -constdefs
    1.72 -  S :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" 
    1.73 +definition S :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" where 
    1.74    "S ==
    1.75  %(f::'a::type => 'b::type => 'c::type) (g::'a::type => 'b::type)
    1.76     x::'a::type. f x (g x)"
    1.77 @@ -282,8 +274,7 @@
    1.78      x::'a::type. f x (g x))"
    1.79    by (import combin S_DEF)
    1.80  
    1.81 -constdefs
    1.82 -  I :: "'a => 'a" 
    1.83 +definition I :: "'a => 'a" where 
    1.84    "(op ==::('a::type => 'a::type) => ('a::type => 'a::type) => prop)
    1.85   (I::'a::type => 'a::type)
    1.86   ((S::('a::type => ('a::type => 'a::type) => 'a::type)
    1.87 @@ -299,16 +290,14 @@
    1.88     (K::'a::type => 'a::type => 'a::type))"
    1.89    by (import combin I_DEF)
    1.90  
    1.91 -constdefs
    1.92 -  C :: "('a => 'b => 'c) => 'b => 'a => 'c" 
    1.93 +definition C :: "('a => 'b => 'c) => 'b => 'a => 'c" where 
    1.94    "C == %(f::'a::type => 'b::type => 'c::type) (x::'b::type) y::'a::type. f y x"
    1.95  
    1.96  lemma C_DEF: "C =
    1.97  (%(f::'a::type => 'b::type => 'c::type) (x::'b::type) y::'a::type. f y x)"
    1.98    by (import combin C_DEF)
    1.99  
   1.100 -constdefs
   1.101 -  W :: "('a => 'a => 'b) => 'a => 'b" 
   1.102 +definition W :: "('a => 'a => 'b) => 'a => 'b" where 
   1.103    "W == %(f::'a::type => 'a::type => 'b::type) x::'a::type. f x x"
   1.104  
   1.105  lemma W_DEF: "W = (%(f::'a::type => 'a::type => 'b::type) x::'a::type. f x x)"
   1.106 @@ -582,8 +571,7 @@
   1.107  
   1.108  ;setup_theory relation
   1.109  
   1.110 -constdefs
   1.111 -  TC :: "('a => 'a => bool) => 'a => 'a => bool" 
   1.112 +definition TC :: "('a => 'a => bool) => 'a => 'a => bool" where 
   1.113    "TC ==
   1.114  %(R::'a::type => 'a::type => bool) (a::'a::type) b::'a::type.
   1.115     ALL P::'a::type => 'a::type => bool.
   1.116 @@ -601,8 +589,7 @@
   1.117         P a b)"
   1.118    by (import relation TC_DEF)
   1.119  
   1.120 -constdefs
   1.121 -  RTC :: "('a => 'a => bool) => 'a => 'a => bool" 
   1.122 +definition RTC :: "('a => 'a => bool) => 'a => 'a => bool" where 
   1.123    "RTC ==
   1.124  %(R::'a::type => 'a::type => bool) (a::'a::type) b::'a::type.
   1.125     ALL P::'a::type => 'a::type => bool.
   1.126 @@ -644,8 +631,7 @@
   1.127     (ALL (x::'a::type) (y::'a::type) z::'a::type. R x y & R y z --> R x z)"
   1.128    by (import relation transitive_def)
   1.129  
   1.130 -constdefs
   1.131 -  pred_reflexive :: "('a => 'a => bool) => bool" 
   1.132 +definition pred_reflexive :: "('a => 'a => bool) => bool" where 
   1.133    "pred_reflexive == %R::'a::type => 'a::type => bool. ALL x::'a::type. R x x"
   1.134  
   1.135  lemma reflexive_def: "ALL R::'a::type => 'a::type => bool.
   1.136 @@ -788,8 +774,7 @@
   1.137     (ALL (x::'a::type) y::'a::type. RTC R x y --> RTC Q x y)"
   1.138    by (import relation RTC_MONOTONE)
   1.139  
   1.140 -constdefs
   1.141 -  WF :: "('a => 'a => bool) => bool" 
   1.142 +definition WF :: "('a => 'a => bool) => bool" where 
   1.143    "WF ==
   1.144  %R::'a::type => 'a::type => bool.
   1.145     ALL B::'a::type => bool.
   1.146 @@ -814,8 +799,7 @@
   1.147     WF x --> x xa xb --> xa ~= xb"
   1.148    by (import relation WF_NOT_REFL)
   1.149  
   1.150 -constdefs
   1.151 -  EMPTY_REL :: "'a => 'a => bool" 
   1.152 +definition EMPTY_REL :: "'a => 'a => bool" where 
   1.153    "EMPTY_REL == %(x::'a::type) y::'a::type. False"
   1.154  
   1.155  lemma EMPTY_REL_DEF: "ALL (x::'a::type) y::'a::type. EMPTY_REL x y = False"
   1.156 @@ -847,8 +831,7 @@
   1.157     WF R --> WF (relation.inv_image R f)"
   1.158    by (import relation WF_inv_image)
   1.159  
   1.160 -constdefs
   1.161 -  RESTRICT :: "('a => 'b) => ('a => 'a => bool) => 'a => 'a => 'b" 
   1.162 +definition RESTRICT :: "('a => 'b) => ('a => 'a => bool) => 'a => 'a => 'b" where 
   1.163    "RESTRICT ==
   1.164  %(f::'a::type => 'b::type) (R::'a::type => 'a::type => bool) (x::'a::type)
   1.165     y::'a::type. if R y x then f y else ARB"
   1.166 @@ -891,8 +874,7 @@
   1.167     the_fun R M x = Eps (approx R M x)"
   1.168    by (import relation the_fun_def)
   1.169  
   1.170 -constdefs
   1.171 -  WFREC :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'b" 
   1.172 +definition WFREC :: "('a => 'a => bool) => (('a => 'b) => 'a => 'b) => 'a => 'b" where 
   1.173    "WFREC ==
   1.174  %(R::'a::type => 'a::type => bool)
   1.175     (M::('a::type => 'b::type) => 'a::type => 'b::type) x::'a::type.
   1.176 @@ -1052,8 +1034,7 @@
   1.177     split xb x = split f' xa"
   1.178    by (import pair pair_case_cong)
   1.179  
   1.180 -constdefs
   1.181 -  LEX :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" 
   1.182 +definition LEX :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" where 
   1.183    "LEX ==
   1.184  %(R1::'a::type => 'a::type => bool) (R2::'b::type => 'b::type => bool)
   1.185     (s::'a::type, t::'b::type) (u::'a::type, v::'b::type).
   1.186 @@ -1069,8 +1050,7 @@
   1.187     WF x & WF xa --> WF (LEX x xa)"
   1.188    by (import pair WF_LEX)
   1.189  
   1.190 -constdefs
   1.191 -  RPROD :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" 
   1.192 +definition RPROD :: "('a => 'a => bool) => ('b => 'b => bool) => 'a * 'b => 'a * 'b => bool" where 
   1.193    "RPROD ==
   1.194  %(R1::'a::type => 'a::type => bool) (R2::'b::type => 'b::type => bool)
   1.195     (s::'a::type, t::'b::type) (u::'a::type, v::'b::type). R1 s u & R2 t v"
   1.196 @@ -1113,8 +1093,7 @@
   1.197  lemma NOT_LESS_EQ: "ALL (m::nat) n::nat. m = n --> ~ m < n"
   1.198    by (import prim_rec NOT_LESS_EQ)
   1.199  
   1.200 -constdefs
   1.201 -  SIMP_REC_REL :: "(nat => 'a) => 'a => ('a => 'a) => nat => bool" 
   1.202 +definition SIMP_REC_REL :: "(nat => 'a) => 'a => ('a => 'a) => nat => bool" where 
   1.203    "(op ==::((nat => 'a::type)
   1.204           => 'a::type => ('a::type => 'a::type) => nat => bool)
   1.205          => ((nat => 'a::type)
   1.206 @@ -1187,8 +1166,7 @@
   1.207     (ALL m::nat. SIMP_REC x f (Suc m) = f (SIMP_REC x f m))"
   1.208    by (import prim_rec SIMP_REC_THM)
   1.209  
   1.210 -constdefs
   1.211 -  PRE :: "nat => nat" 
   1.212 +definition PRE :: "nat => nat" where 
   1.213    "PRE == %m::nat. if m = 0 then 0 else SOME n::nat. m = Suc n"
   1.214  
   1.215  lemma PRE_DEF: "ALL m::nat. PRE m = (if m = 0 then 0 else SOME n::nat. m = Suc n)"
   1.216 @@ -1197,8 +1175,7 @@
   1.217  lemma PRE: "PRE 0 = 0 & (ALL m::nat. PRE (Suc m) = m)"
   1.218    by (import prim_rec PRE)
   1.219  
   1.220 -constdefs
   1.221 -  PRIM_REC_FUN :: "'a => ('a => nat => 'a) => nat => nat => 'a" 
   1.222 +definition PRIM_REC_FUN :: "'a => ('a => nat => 'a) => nat => nat => 'a" where 
   1.223    "PRIM_REC_FUN ==
   1.224  %(x::'a::type) f::'a::type => nat => 'a::type.
   1.225     SIMP_REC (%n::nat. x) (%(fun::nat => 'a::type) n::nat. f (fun (PRE n)) n)"
   1.226 @@ -1214,8 +1191,7 @@
   1.227         PRIM_REC_FUN x f (Suc m) n = f (PRIM_REC_FUN x f m (PRE n)) n)"
   1.228    by (import prim_rec PRIM_REC_EQN)
   1.229  
   1.230 -constdefs
   1.231 -  PRIM_REC :: "'a => ('a => nat => 'a) => nat => 'a" 
   1.232 +definition PRIM_REC :: "'a => ('a => nat => 'a) => nat => 'a" where 
   1.233    "PRIM_REC ==
   1.234  %(x::'a::type) (f::'a::type => nat => 'a::type) m::nat.
   1.235     PRIM_REC_FUN x f m (PRE m)"
   1.236 @@ -1286,8 +1262,7 @@
   1.237  
   1.238  ;setup_theory arithmetic
   1.239  
   1.240 -constdefs
   1.241 -  nat_elim__magic :: "nat => nat" 
   1.242 +definition nat_elim__magic :: "nat => nat" where 
   1.243    "nat_elim__magic == %n::nat. n"
   1.244  
   1.245  lemma nat_elim__magic: "ALL n::nat. nat_elim__magic n = n"
   1.246 @@ -1746,22 +1721,19 @@
   1.247  
   1.248  ;setup_theory hrat
   1.249  
   1.250 -constdefs
   1.251 -  trat_1 :: "nat * nat" 
   1.252 +definition trat_1 :: "nat * nat" where 
   1.253    "trat_1 == (0, 0)"
   1.254  
   1.255  lemma trat_1: "trat_1 = (0, 0)"
   1.256    by (import hrat trat_1)
   1.257  
   1.258 -constdefs
   1.259 -  trat_inv :: "nat * nat => nat * nat" 
   1.260 +definition trat_inv :: "nat * nat => nat * nat" where 
   1.261    "trat_inv == %(x::nat, y::nat). (y, x)"
   1.262  
   1.263  lemma trat_inv: "ALL (x::nat) y::nat. trat_inv (x, y) = (y, x)"
   1.264    by (import hrat trat_inv)
   1.265  
   1.266 -constdefs
   1.267 -  trat_add :: "nat * nat => nat * nat => nat * nat" 
   1.268 +definition trat_add :: "nat * nat => nat * nat => nat * nat" where 
   1.269    "trat_add ==
   1.270  %(x::nat, y::nat) (x'::nat, y'::nat).
   1.271     (PRE (Suc x * Suc y' + Suc x' * Suc y), PRE (Suc y * Suc y'))"
   1.272 @@ -1771,8 +1743,7 @@
   1.273     (PRE (Suc x * Suc y' + Suc x' * Suc y), PRE (Suc y * Suc y'))"
   1.274    by (import hrat trat_add)
   1.275  
   1.276 -constdefs
   1.277 -  trat_mul :: "nat * nat => nat * nat => nat * nat" 
   1.278 +definition trat_mul :: "nat * nat => nat * nat => nat * nat" where 
   1.279    "trat_mul ==
   1.280  %(x::nat, y::nat) (x'::nat, y'::nat).
   1.281     (PRE (Suc x * Suc x'), PRE (Suc y * Suc y'))"
   1.282 @@ -1788,8 +1759,7 @@
   1.283  (ALL n::nat. trat_sucint (Suc n) = trat_add (trat_sucint n) trat_1)"
   1.284    by (import hrat trat_sucint)
   1.285  
   1.286 -constdefs
   1.287 -  trat_eq :: "nat * nat => nat * nat => bool" 
   1.288 +definition trat_eq :: "nat * nat => nat * nat => bool" where 
   1.289    "trat_eq ==
   1.290  %(x::nat, y::nat) (x'::nat, y'::nat). Suc x * Suc y' = Suc x' * Suc y"
   1.291  
   1.292 @@ -1901,23 +1871,20 @@
   1.293      (EX x::nat * nat. r = trat_eq x) = (dest_hrat (mk_hrat r) = r))"
   1.294    by (import hrat hrat_tybij)
   1.295  
   1.296 -constdefs
   1.297 -  hrat_1 :: "hrat" 
   1.298 +definition hrat_1 :: "hrat" where 
   1.299    "hrat_1 == mk_hrat (trat_eq trat_1)"
   1.300  
   1.301  lemma hrat_1: "hrat_1 = mk_hrat (trat_eq trat_1)"
   1.302    by (import hrat hrat_1)
   1.303  
   1.304 -constdefs
   1.305 -  hrat_inv :: "hrat => hrat" 
   1.306 +definition hrat_inv :: "hrat => hrat" where 
   1.307    "hrat_inv == %T1::hrat. mk_hrat (trat_eq (trat_inv (Eps (dest_hrat T1))))"
   1.308  
   1.309  lemma hrat_inv: "ALL T1::hrat.
   1.310     hrat_inv T1 = mk_hrat (trat_eq (trat_inv (Eps (dest_hrat T1))))"
   1.311    by (import hrat hrat_inv)
   1.312  
   1.313 -constdefs
   1.314 -  hrat_add :: "hrat => hrat => hrat" 
   1.315 +definition hrat_add :: "hrat => hrat => hrat" where 
   1.316    "hrat_add ==
   1.317  %(T1::hrat) T2::hrat.
   1.318     mk_hrat (trat_eq (trat_add (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
   1.319 @@ -1927,8 +1894,7 @@
   1.320     mk_hrat (trat_eq (trat_add (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
   1.321    by (import hrat hrat_add)
   1.322  
   1.323 -constdefs
   1.324 -  hrat_mul :: "hrat => hrat => hrat" 
   1.325 +definition hrat_mul :: "hrat => hrat => hrat" where 
   1.326    "hrat_mul ==
   1.327  %(T1::hrat) T2::hrat.
   1.328     mk_hrat (trat_eq (trat_mul (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
   1.329 @@ -1938,8 +1904,7 @@
   1.330     mk_hrat (trat_eq (trat_mul (Eps (dest_hrat T1)) (Eps (dest_hrat T2))))"
   1.331    by (import hrat hrat_mul)
   1.332  
   1.333 -constdefs
   1.334 -  hrat_sucint :: "nat => hrat" 
   1.335 +definition hrat_sucint :: "nat => hrat" where 
   1.336    "hrat_sucint == %T1::nat. mk_hrat (trat_eq (trat_sucint T1))"
   1.337  
   1.338  lemma hrat_sucint: "ALL T1::nat. hrat_sucint T1 = mk_hrat (trat_eq (trat_sucint T1))"
   1.339 @@ -1987,8 +1952,7 @@
   1.340  
   1.341  ;setup_theory hreal
   1.342  
   1.343 -constdefs
   1.344 -  hrat_lt :: "hrat => hrat => bool" 
   1.345 +definition hrat_lt :: "hrat => hrat => bool" where 
   1.346    "hrat_lt == %(x::hrat) y::hrat. EX d::hrat. y = hrat_add x d"
   1.347  
   1.348  lemma hrat_lt: "ALL (x::hrat) y::hrat. hrat_lt x y = (EX d::hrat. y = hrat_add x d)"
   1.349 @@ -2096,8 +2060,7 @@
   1.350     hrat_lt x y --> (EX xa::hrat. hrat_lt x xa & hrat_lt xa y)"
   1.351    by (import hreal HRAT_MEAN)
   1.352  
   1.353 -constdefs
   1.354 -  isacut :: "(hrat => bool) => bool" 
   1.355 +definition isacut :: "(hrat => bool) => bool" where 
   1.356    "isacut ==
   1.357  %C::hrat => bool.
   1.358     Ex C &
   1.359 @@ -2113,8 +2076,7 @@
   1.360      (ALL x::hrat. C x --> (EX y::hrat. C y & hrat_lt x y)))"
   1.361    by (import hreal isacut)
   1.362  
   1.363 -constdefs
   1.364 -  cut_of_hrat :: "hrat => hrat => bool" 
   1.365 +definition cut_of_hrat :: "hrat => hrat => bool" where 
   1.366    "cut_of_hrat == %(x::hrat) y::hrat. hrat_lt y x"
   1.367  
   1.368  lemma cut_of_hrat: "ALL x::hrat. cut_of_hrat x = (%y::hrat. hrat_lt y x)"
   1.369 @@ -2173,15 +2135,13 @@
   1.370     (EX x::hrat. hreal.cut X x & ~ hreal.cut X (hrat_mul u x))"
   1.371    by (import hreal CUT_NEARTOP_MUL)
   1.372  
   1.373 -constdefs
   1.374 -  hreal_1 :: "hreal" 
   1.375 +definition hreal_1 :: "hreal" where 
   1.376    "hreal_1 == hreal (cut_of_hrat hrat_1)"
   1.377  
   1.378  lemma hreal_1: "hreal_1 = hreal (cut_of_hrat hrat_1)"
   1.379    by (import hreal hreal_1)
   1.380  
   1.381 -constdefs
   1.382 -  hreal_add :: "hreal => hreal => hreal" 
   1.383 +definition hreal_add :: "hreal => hreal => hreal" where 
   1.384    "hreal_add ==
   1.385  %(X::hreal) Y::hreal.
   1.386     hreal
   1.387 @@ -2197,8 +2157,7 @@
   1.388             w = hrat_add x y & hreal.cut X x & hreal.cut Y y)"
   1.389    by (import hreal hreal_add)
   1.390  
   1.391 -constdefs
   1.392 -  hreal_mul :: "hreal => hreal => hreal" 
   1.393 +definition hreal_mul :: "hreal => hreal => hreal" where 
   1.394    "hreal_mul ==
   1.395  %(X::hreal) Y::hreal.
   1.396     hreal
   1.397 @@ -2214,8 +2173,7 @@
   1.398             w = hrat_mul x y & hreal.cut X x & hreal.cut Y y)"
   1.399    by (import hreal hreal_mul)
   1.400  
   1.401 -constdefs
   1.402 -  hreal_inv :: "hreal => hreal" 
   1.403 +definition hreal_inv :: "hreal => hreal" where 
   1.404    "hreal_inv ==
   1.405  %X::hreal.
   1.406     hreal
   1.407 @@ -2233,8 +2191,7 @@
   1.408             (ALL x::hrat. hreal.cut X x --> hrat_lt (hrat_mul w x) d))"
   1.409    by (import hreal hreal_inv)
   1.410  
   1.411 -constdefs
   1.412 -  hreal_sup :: "(hreal => bool) => hreal" 
   1.413 +definition hreal_sup :: "(hreal => bool) => hreal" where 
   1.414    "hreal_sup ==
   1.415  %P::hreal => bool. hreal (%w::hrat. EX X::hreal. P X & hreal.cut X w)"
   1.416  
   1.417 @@ -2242,8 +2199,7 @@
   1.418     hreal_sup P = hreal (%w::hrat. EX X::hreal. P X & hreal.cut X w)"
   1.419    by (import hreal hreal_sup)
   1.420  
   1.421 -constdefs
   1.422 -  hreal_lt :: "hreal => hreal => bool" 
   1.423 +definition hreal_lt :: "hreal => hreal => bool" where 
   1.424    "hreal_lt ==
   1.425  %(X::hreal) Y::hreal.
   1.426     X ~= Y & (ALL x::hrat. hreal.cut X x --> hreal.cut Y x)"
   1.427 @@ -2301,8 +2257,7 @@
   1.428  lemma HREAL_NOZERO: "ALL (X::hreal) Y::hreal. hreal_add X Y ~= X"
   1.429    by (import hreal HREAL_NOZERO)
   1.430  
   1.431 -constdefs
   1.432 -  hreal_sub :: "hreal => hreal => hreal" 
   1.433 +definition hreal_sub :: "hreal => hreal => hreal" where 
   1.434    "hreal_sub ==
   1.435  %(Y::hreal) X::hreal.
   1.436     hreal
   1.437 @@ -2358,15 +2313,13 @@
   1.438  (ALL x::nat. Suc (NUMERAL_BIT2 x) = NUMERAL_BIT1 (Suc x))"
   1.439    by (import numeral numeral_suc)
   1.440  
   1.441 -constdefs
   1.442 -  iZ :: "nat => nat" 
   1.443 +definition iZ :: "nat => nat" where 
   1.444    "iZ == %x::nat. x"
   1.445  
   1.446  lemma iZ: "ALL x::nat. iZ x = x"
   1.447    by (import numeral iZ)
   1.448  
   1.449 -constdefs
   1.450 -  iiSUC :: "nat => nat" 
   1.451 +definition iiSUC :: "nat => nat" where 
   1.452    "iiSUC == %n::nat. Suc (Suc n)"
   1.453  
   1.454  lemma iiSUC: "ALL n::nat. iiSUC n = Suc (Suc n)"
   1.455 @@ -2699,8 +2652,7 @@
   1.456      iBIT_cases (NUMERAL_BIT2 n) zf bf1 bf2 = bf2 n)"
   1.457    by (import numeral iBIT_cases)
   1.458  
   1.459 -constdefs
   1.460 -  iDUB :: "nat => nat" 
   1.461 +definition iDUB :: "nat => nat" where 
   1.462    "iDUB == %x::nat. x + x"
   1.463  
   1.464  lemma iDUB: "ALL x::nat. iDUB x = x + x"
   1.465 @@ -2771,8 +2723,7 @@
   1.466     NUMERAL_BIT2 x * xa = iDUB (iZ (x * xa + xa))"
   1.467    by (import numeral numeral_mult)
   1.468  
   1.469 -constdefs
   1.470 -  iSQR :: "nat => nat" 
   1.471 +definition iSQR :: "nat => nat" where 
   1.472    "iSQR == %x::nat. x * x"
   1.473  
   1.474  lemma iSQR: "ALL x::nat. iSQR x = x * x"
   1.475 @@ -2809,8 +2760,7 @@
   1.476         ALL (xa::'A::type) y::'B::type. x (P xa y) = xa & Y (P xa y) = y)"
   1.477    by (import ind_type INJ_INVERSE2)
   1.478  
   1.479 -constdefs
   1.480 -  NUMPAIR :: "nat => nat => nat" 
   1.481 +definition NUMPAIR :: "nat => nat => nat" where 
   1.482    "NUMPAIR == %(x::nat) y::nat. 2 ^ x * (2 * y + 1)"
   1.483  
   1.484  lemma NUMPAIR: "ALL (x::nat) y::nat. NUMPAIR x y = 2 ^ x * (2 * y + 1)"
   1.485 @@ -2831,8 +2781,7 @@
   1.486  specification (NUMFST NUMSND) NUMPAIR_DEST: "ALL (x::nat) y::nat. NUMFST (NUMPAIR x y) = x & NUMSND (NUMPAIR x y) = y"
   1.487    by (import ind_type NUMPAIR_DEST)
   1.488  
   1.489 -constdefs
   1.490 -  NUMSUM :: "bool => nat => nat" 
   1.491 +definition NUMSUM :: "bool => nat => nat" where 
   1.492    "NUMSUM == %(b::bool) x::nat. if b then Suc (2 * x) else 2 * x"
   1.493  
   1.494  lemma NUMSUM: "ALL (b::bool) x::nat. NUMSUM b x = (if b then Suc (2 * x) else 2 * x)"
   1.495 @@ -2849,8 +2798,7 @@
   1.496  specification (NUMLEFT NUMRIGHT) NUMSUM_DEST: "ALL (x::bool) y::nat. NUMLEFT (NUMSUM x y) = x & NUMRIGHT (NUMSUM x y) = y"
   1.497    by (import ind_type NUMSUM_DEST)
   1.498  
   1.499 -constdefs
   1.500 -  INJN :: "nat => nat => 'a => bool" 
   1.501 +definition INJN :: "nat => nat => 'a => bool" where 
   1.502    "INJN == %(m::nat) (n::nat) a::'a::type. n = m"
   1.503  
   1.504  lemma INJN: "ALL m::nat. INJN m = (%(n::nat) a::'a::type. n = m)"
   1.505 @@ -2859,8 +2807,7 @@
   1.506  lemma INJN_INJ: "ALL (n1::nat) n2::nat. (INJN n1 = INJN n2) = (n1 = n2)"
   1.507    by (import ind_type INJN_INJ)
   1.508  
   1.509 -constdefs
   1.510 -  INJA :: "'a => nat => 'a => bool" 
   1.511 +definition INJA :: "'a => nat => 'a => bool" where 
   1.512    "INJA == %(a::'a::type) (n::nat) b::'a::type. b = a"
   1.513  
   1.514  lemma INJA: "ALL a::'a::type. INJA a = (%(n::nat) b::'a::type. b = a)"
   1.515 @@ -2869,8 +2816,7 @@
   1.516  lemma INJA_INJ: "ALL (a1::'a::type) a2::'a::type. (INJA a1 = INJA a2) = (a1 = a2)"
   1.517    by (import ind_type INJA_INJ)
   1.518  
   1.519 -constdefs
   1.520 -  INJF :: "(nat => nat => 'a => bool) => nat => 'a => bool" 
   1.521 +definition INJF :: "(nat => nat => 'a => bool) => nat => 'a => bool" where 
   1.522    "INJF == %(f::nat => nat => 'a::type => bool) n::nat. f (NUMFST n) (NUMSND n)"
   1.523  
   1.524  lemma INJF: "ALL f::nat => nat => 'a::type => bool.
   1.525 @@ -2881,8 +2827,7 @@
   1.526     (INJF f1 = INJF f2) = (f1 = f2)"
   1.527    by (import ind_type INJF_INJ)
   1.528  
   1.529 -constdefs
   1.530 -  INJP :: "(nat => 'a => bool) => (nat => 'a => bool) => nat => 'a => bool" 
   1.531 +definition INJP :: "(nat => 'a => bool) => (nat => 'a => bool) => nat => 'a => bool" where 
   1.532    "INJP ==
   1.533  %(f1::nat => 'a::type => bool) (f2::nat => 'a::type => bool) (n::nat)
   1.534     a::'a::type. if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a"
   1.535 @@ -2898,8 +2843,7 @@
   1.536     (INJP f1 f2 = INJP f1' f2') = (f1 = f1' & f2 = f2')"
   1.537    by (import ind_type INJP_INJ)
   1.538  
   1.539 -constdefs
   1.540 -  ZCONSTR :: "nat => 'a => (nat => nat => 'a => bool) => nat => 'a => bool" 
   1.541 +definition ZCONSTR :: "nat => 'a => (nat => nat => 'a => bool) => nat => 'a => bool" where 
   1.542    "ZCONSTR ==
   1.543  %(c::nat) (i::'a::type) r::nat => nat => 'a::type => bool.
   1.544     INJP (INJN (Suc c)) (INJP (INJA i) (INJF r))"
   1.545 @@ -2908,8 +2852,7 @@
   1.546     ZCONSTR c i r = INJP (INJN (Suc c)) (INJP (INJA i) (INJF r))"
   1.547    by (import ind_type ZCONSTR)
   1.548  
   1.549 -constdefs
   1.550 -  ZBOT :: "nat => 'a => bool" 
   1.551 +definition ZBOT :: "nat => 'a => bool" where 
   1.552    "ZBOT == INJP (INJN 0) (SOME z::nat => 'a::type => bool. True)"
   1.553  
   1.554  lemma ZBOT: "ZBOT = INJP (INJN 0) (SOME z::nat => 'a::type => bool. True)"
   1.555 @@ -2919,8 +2862,7 @@
   1.556     ZCONSTR x xa xb ~= ZBOT"
   1.557    by (import ind_type ZCONSTR_ZBOT)
   1.558  
   1.559 -constdefs
   1.560 -  ZRECSPACE :: "(nat => 'a => bool) => bool" 
   1.561 +definition ZRECSPACE :: "(nat => 'a => bool) => bool" where 
   1.562    "ZRECSPACE ==
   1.563  %a0::nat => 'a::type => bool.
   1.564     ALL ZRECSPACE'::(nat => 'a::type => bool) => bool.
   1.565 @@ -2993,15 +2935,13 @@
   1.566  (ALL r::nat => 'a::type => bool. ZRECSPACE r = (dest_rec (mk_rec r) = r))"
   1.567    by (import ind_type recspace_repfns)
   1.568  
   1.569 -constdefs
   1.570 -  BOTTOM :: "'a recspace" 
   1.571 +definition BOTTOM :: "'a recspace" where 
   1.572    "BOTTOM == mk_rec ZBOT"
   1.573  
   1.574  lemma BOTTOM: "BOTTOM = mk_rec ZBOT"
   1.575    by (import ind_type BOTTOM)
   1.576  
   1.577 -constdefs
   1.578 -  CONSTR :: "nat => 'a => (nat => 'a recspace) => 'a recspace" 
   1.579 +definition CONSTR :: "nat => 'a => (nat => 'a recspace) => 'a recspace" where 
   1.580    "CONSTR ==
   1.581  %(c::nat) (i::'a::type) r::nat => 'a::type recspace.
   1.582     mk_rec (ZCONSTR c i (%n::nat. dest_rec (r n)))"
   1.583 @@ -3049,15 +2989,13 @@
   1.584  (ALL (a::'a::type) (f::nat => 'a::type) n::nat. FCONS a f (Suc n) = f n)"
   1.585    by (import ind_type FCONS)
   1.586  
   1.587 -constdefs
   1.588 -  FNIL :: "nat => 'a" 
   1.589 +definition FNIL :: "nat => 'a" where 
   1.590    "FNIL == %n::nat. SOME x::'a::type. True"
   1.591  
   1.592  lemma FNIL: "ALL n::nat. FNIL n = (SOME x::'a::type. True)"
   1.593    by (import ind_type FNIL)
   1.594  
   1.595 -constdefs
   1.596 -  ISO :: "('a => 'b) => ('b => 'a) => bool" 
   1.597 +definition ISO :: "('a => 'b) => ('b => 'a) => bool" where 
   1.598    "ISO ==
   1.599  %(f::'a::type => 'b::type) g::'b::type => 'a::type.
   1.600     (ALL x::'b::type. f (g x) = x) & (ALL y::'a::type. g (f y) = y)"
   1.601 @@ -3434,8 +3372,7 @@
   1.602     (EX x::'a::type. IN x s & (ALL y::'a::type. IN y s --> M x <= M y))"
   1.603    by (import pred_set SET_MINIMUM)
   1.604  
   1.605 -constdefs
   1.606 -  EMPTY :: "'a => bool" 
   1.607 +definition EMPTY :: "'a => bool" where 
   1.608    "EMPTY == %x::'a::type. False"
   1.609  
   1.610  lemma EMPTY_DEF: "EMPTY = (%x::'a::type. False)"
   1.611 @@ -3468,8 +3405,7 @@
   1.612  lemma EQ_UNIV: "(ALL x::'a::type. IN x (s::'a::type => bool)) = (s = pred_set.UNIV)"
   1.613    by (import pred_set EQ_UNIV)
   1.614  
   1.615 -constdefs
   1.616 -  SUBSET :: "('a => bool) => ('a => bool) => bool" 
   1.617 +definition SUBSET :: "('a => bool) => ('a => bool) => bool" where 
   1.618    "SUBSET ==
   1.619  %(s::'a::type => bool) t::'a::type => bool.
   1.620     ALL x::'a::type. IN x s --> IN x t"
   1.621 @@ -3501,8 +3437,7 @@
   1.622  lemma UNIV_SUBSET: "ALL x::'a::type => bool. SUBSET pred_set.UNIV x = (x = pred_set.UNIV)"
   1.623    by (import pred_set UNIV_SUBSET)
   1.624  
   1.625 -constdefs
   1.626 -  PSUBSET :: "('a => bool) => ('a => bool) => bool" 
   1.627 +definition PSUBSET :: "('a => bool) => ('a => bool) => bool" where 
   1.628    "PSUBSET == %(s::'a::type => bool) t::'a::type => bool. SUBSET s t & s ~= t"
   1.629  
   1.630  lemma PSUBSET_DEF: "ALL (s::'a::type => bool) t::'a::type => bool.
   1.631 @@ -3640,8 +3575,7 @@
   1.632     pred_set.INTER (pred_set.UNION x xa) (pred_set.UNION x xb)"
   1.633    by (import pred_set INTER_OVER_UNION)
   1.634  
   1.635 -constdefs
   1.636 -  DISJOINT :: "('a => bool) => ('a => bool) => bool" 
   1.637 +definition DISJOINT :: "('a => bool) => ('a => bool) => bool" where 
   1.638    "DISJOINT ==
   1.639  %(s::'a::type => bool) t::'a::type => bool. pred_set.INTER s t = EMPTY"
   1.640  
   1.641 @@ -3672,8 +3606,7 @@
   1.642     DISJOINT u (pred_set.UNION s t) = (DISJOINT s u & DISJOINT t u)"
   1.643    by (import pred_set DISJOINT_UNION_BOTH)
   1.644  
   1.645 -constdefs
   1.646 -  DIFF :: "('a => bool) => ('a => bool) => 'a => bool" 
   1.647 +definition DIFF :: "('a => bool) => ('a => bool) => 'a => bool" where 
   1.648    "DIFF ==
   1.649  %(s::'a::type => bool) t::'a::type => bool.
   1.650     GSPEC (%x::'a::type. (x, IN x s & ~ IN x t))"
   1.651 @@ -3702,8 +3635,7 @@
   1.652  lemma DIFF_EQ_EMPTY: "ALL x::'a::type => bool. DIFF x x = EMPTY"
   1.653    by (import pred_set DIFF_EQ_EMPTY)
   1.654  
   1.655 -constdefs
   1.656 -  INSERT :: "'a => ('a => bool) => 'a => bool" 
   1.657 +definition INSERT :: "'a => ('a => bool) => 'a => bool" where 
   1.658    "INSERT ==
   1.659  %(x::'a::type) s::'a::type => bool.
   1.660     GSPEC (%y::'a::type. (y, y = x | IN y s))"
   1.661 @@ -3778,8 +3710,7 @@
   1.662     DIFF (INSERT x s) t = (if IN x t then DIFF s t else INSERT x (DIFF s t))"
   1.663    by (import pred_set INSERT_DIFF)
   1.664  
   1.665 -constdefs
   1.666 -  DELETE :: "('a => bool) => 'a => 'a => bool" 
   1.667 +definition DELETE :: "('a => bool) => 'a => 'a => bool" where 
   1.668    "DELETE == %(s::'a::type => bool) x::'a::type. DIFF s (INSERT x EMPTY)"
   1.669  
   1.670  lemma DELETE_DEF: "ALL (s::'a::type => bool) x::'a::type. DELETE s x = DIFF s (INSERT x EMPTY)"
   1.671 @@ -3852,8 +3783,7 @@
   1.672  specification (CHOICE) CHOICE_DEF: "ALL x::'a::type => bool. x ~= EMPTY --> IN (CHOICE x) x"
   1.673    by (import pred_set CHOICE_DEF)
   1.674  
   1.675 -constdefs
   1.676 -  REST :: "('a => bool) => 'a => bool" 
   1.677 +definition REST :: "('a => bool) => 'a => bool" where 
   1.678    "REST == %s::'a::type => bool. DELETE s (CHOICE s)"
   1.679  
   1.680  lemma REST_DEF: "ALL s::'a::type => bool. REST s = DELETE s (CHOICE s)"
   1.681 @@ -3871,8 +3801,7 @@
   1.682  lemma REST_PSUBSET: "ALL x::'a::type => bool. x ~= EMPTY --> PSUBSET (REST x) x"
   1.683    by (import pred_set REST_PSUBSET)
   1.684  
   1.685 -constdefs
   1.686 -  SING :: "('a => bool) => bool" 
   1.687 +definition SING :: "('a => bool) => bool" where 
   1.688    "SING == %s::'a::type => bool. EX x::'a::type. s = INSERT x EMPTY"
   1.689  
   1.690  lemma SING_DEF: "ALL s::'a::type => bool. SING s = (EX x::'a::type. s = INSERT x EMPTY)"
   1.691 @@ -3917,8 +3846,7 @@
   1.692  lemma SING_IFF_EMPTY_REST: "ALL x::'a::type => bool. SING x = (x ~= EMPTY & REST x = EMPTY)"
   1.693    by (import pred_set SING_IFF_EMPTY_REST)
   1.694  
   1.695 -constdefs
   1.696 -  IMAGE :: "('a => 'b) => ('a => bool) => 'b => bool" 
   1.697 +definition IMAGE :: "('a => 'b) => ('a => bool) => 'b => bool" where 
   1.698    "IMAGE ==
   1.699  %(f::'a::type => 'b::type) s::'a::type => bool.
   1.700     GSPEC (%x::'a::type. (f x, IN x s))"
   1.701 @@ -3971,8 +3899,7 @@
   1.702      (pred_set.INTER (IMAGE f s) (IMAGE f t))"
   1.703    by (import pred_set IMAGE_INTER)
   1.704  
   1.705 -constdefs
   1.706 -  INJ :: "('a => 'b) => ('a => bool) => ('b => bool) => bool" 
   1.707 +definition INJ :: "('a => 'b) => ('a => bool) => ('b => bool) => bool" where 
   1.708    "INJ ==
   1.709  %(f::'a::type => 'b::type) (s::'a::type => bool) t::'b::type => bool.
   1.710     (ALL x::'a::type. IN x s --> IN (f x) t) &
   1.711 @@ -3998,8 +3925,7 @@
   1.712     (ALL xa::'a::type => bool. INJ x xa EMPTY = (xa = EMPTY))"
   1.713    by (import pred_set INJ_EMPTY)
   1.714  
   1.715 -constdefs
   1.716 -  SURJ :: "('a => 'b) => ('a => bool) => ('b => bool) => bool" 
   1.717 +definition SURJ :: "('a => 'b) => ('a => bool) => ('b => bool) => bool" where 
   1.718    "SURJ ==
   1.719  %(f::'a::type => 'b::type) (s::'a::type => bool) t::'b::type => bool.
   1.720     (ALL x::'a::type. IN x s --> IN (f x) t) &
   1.721 @@ -4028,8 +3954,7 @@
   1.722     SURJ x xa xb = (IMAGE x xa = xb)"
   1.723    by (import pred_set IMAGE_SURJ)
   1.724  
   1.725 -constdefs
   1.726 -  BIJ :: "('a => 'b) => ('a => bool) => ('b => bool) => bool" 
   1.727 +definition BIJ :: "('a => 'b) => ('a => bool) => ('b => bool) => bool" where 
   1.728    "BIJ ==
   1.729  %(f::'a::type => 'b::type) (s::'a::type => bool) t::'b::type => bool.
   1.730     INJ f s t & SURJ f s t"
   1.731 @@ -4065,8 +3990,7 @@
   1.732     SURJ f s t --> (ALL x::'b::type. IN x t --> f (RINV f s x) = x)"
   1.733    by (import pred_set RINV_DEF)
   1.734  
   1.735 -constdefs
   1.736 -  FINITE :: "('a => bool) => bool" 
   1.737 +definition FINITE :: "('a => bool) => bool" where 
   1.738    "FINITE ==
   1.739  %s::'a::type => bool.
   1.740     ALL P::('a::type => bool) => bool.
   1.741 @@ -4219,8 +4143,7 @@
   1.742     (ALL x::'a::type => bool. FINITE x --> P x)"
   1.743    by (import pred_set FINITE_COMPLETE_INDUCTION)
   1.744  
   1.745 -constdefs
   1.746 -  INFINITE :: "('a => bool) => bool" 
   1.747 +definition INFINITE :: "('a => bool) => bool" where 
   1.748    "INFINITE == %s::'a::type => bool. ~ FINITE s"
   1.749  
   1.750  lemma INFINITE_DEF: "ALL s::'a::type => bool. INFINITE s = (~ FINITE s)"
   1.751 @@ -4320,8 +4243,7 @@
   1.752                                  (f n)))))))))"
   1.753    by (import pred_set FINITE_WEAK_ENUMERATE)
   1.754  
   1.755 -constdefs
   1.756 -  BIGUNION :: "(('a => bool) => bool) => 'a => bool" 
   1.757 +definition BIGUNION :: "(('a => bool) => bool) => 'a => bool" where 
   1.758    "BIGUNION ==
   1.759  %P::('a::type => bool) => bool.
   1.760     GSPEC (%x::'a::type. (x, EX p::'a::type => bool. IN p P & IN x p))"
   1.761 @@ -4367,8 +4289,7 @@
   1.762     FINITE (BIGUNION x)"
   1.763    by (import pred_set FINITE_BIGUNION)
   1.764  
   1.765 -constdefs
   1.766 -  BIGINTER :: "(('a => bool) => bool) => 'a => bool" 
   1.767 +definition BIGINTER :: "(('a => bool) => bool) => 'a => bool" where 
   1.768    "BIGINTER ==
   1.769  %B::('a::type => bool) => bool.
   1.770     GSPEC (%x::'a::type. (x, ALL P::'a::type => bool. IN P B --> IN x P))"
   1.771 @@ -4406,8 +4327,7 @@
   1.772     DISJOINT x (BIGINTER xb) & DISJOINT (BIGINTER xb) x"
   1.773    by (import pred_set DISJOINT_BIGINTER)
   1.774  
   1.775 -constdefs
   1.776 -  CROSS :: "('a => bool) => ('b => bool) => 'a * 'b => bool" 
   1.777 +definition CROSS :: "('a => bool) => ('b => bool) => 'a * 'b => bool" where 
   1.778    "CROSS ==
   1.779  %(P::'a::type => bool) Q::'b::type => bool.
   1.780     GSPEC (%p::'a::type * 'b::type. (p, IN (fst p) P & IN (snd p) Q))"
   1.781 @@ -4460,8 +4380,7 @@
   1.782     FINITE (CROSS P Q) = (P = EMPTY | Q = EMPTY | FINITE P & FINITE Q)"
   1.783    by (import pred_set FINITE_CROSS_EQ)
   1.784  
   1.785 -constdefs
   1.786 -  COMPL :: "('a => bool) => 'a => bool" 
   1.787 +definition COMPL :: "('a => bool) => 'a => bool" where 
   1.788    "COMPL == DIFF pred_set.UNIV"
   1.789  
   1.790  lemma COMPL_DEF: "ALL P::'a::type => bool. COMPL P = DIFF pred_set.UNIV P"
   1.791 @@ -4513,8 +4432,7 @@
   1.792  lemma CARD_COUNT: "ALL n::nat. CARD (count n) = n"
   1.793    by (import pred_set CARD_COUNT)
   1.794  
   1.795 -constdefs
   1.796 -  ITSET_tupled :: "('a => 'b => 'b) => ('a => bool) * 'b => 'b" 
   1.797 +definition ITSET_tupled :: "('a => 'b => 'b) => ('a => bool) * 'b => 'b" where 
   1.798    "ITSET_tupled ==
   1.799  %f::'a::type => 'b::type => 'b::type.
   1.800     WFREC
   1.801 @@ -4546,8 +4464,7 @@
   1.802          else ARB)"
   1.803    by (import pred_set ITSET_tupled_primitive_def)
   1.804  
   1.805 -constdefs
   1.806 -  ITSET :: "('a => 'b => 'b) => ('a => bool) => 'b => 'b" 
   1.807 +definition ITSET :: "('a => 'b => 'b) => ('a => bool) => 'b => 'b" where 
   1.808    "ITSET ==
   1.809  %(f::'a::type => 'b::type => 'b::type) (x::'a::type => bool) x1::'b::type.
   1.810     ITSET_tupled f (x, x1)"
   1.811 @@ -4578,8 +4495,7 @@
   1.812  
   1.813  ;setup_theory operator
   1.814  
   1.815 -constdefs
   1.816 -  ASSOC :: "('a => 'a => 'a) => bool" 
   1.817 +definition ASSOC :: "('a => 'a => 'a) => bool" where 
   1.818    "ASSOC ==
   1.819  %f::'a::type => 'a::type => 'a::type.
   1.820     ALL (x::'a::type) (y::'a::type) z::'a::type. f x (f y z) = f (f x y) z"
   1.821 @@ -4589,8 +4505,7 @@
   1.822     (ALL (x::'a::type) (y::'a::type) z::'a::type. f x (f y z) = f (f x y) z)"
   1.823    by (import operator ASSOC_DEF)
   1.824  
   1.825 -constdefs
   1.826 -  COMM :: "('a => 'a => 'b) => bool" 
   1.827 +definition COMM :: "('a => 'a => 'b) => bool" where 
   1.828    "COMM ==
   1.829  %f::'a::type => 'a::type => 'b::type.
   1.830     ALL (x::'a::type) y::'a::type. f x y = f y x"
   1.831 @@ -4599,8 +4514,7 @@
   1.832     COMM f = (ALL (x::'a::type) y::'a::type. f x y = f y x)"
   1.833    by (import operator COMM_DEF)
   1.834  
   1.835 -constdefs
   1.836 -  FCOMM :: "('a => 'b => 'a) => ('c => 'a => 'a) => bool" 
   1.837 +definition FCOMM :: "('a => 'b => 'a) => ('c => 'a => 'a) => bool" where 
   1.838    "FCOMM ==
   1.839  %(f::'a::type => 'b::type => 'a::type) g::'c::type => 'a::type => 'a::type.
   1.840     ALL (x::'c::type) (y::'a::type) z::'b::type. g x (f y z) = f (g x y) z"
   1.841 @@ -4611,8 +4525,7 @@
   1.842     (ALL (x::'c::type) (y::'a::type) z::'b::type. g x (f y z) = f (g x y) z)"
   1.843    by (import operator FCOMM_DEF)
   1.844  
   1.845 -constdefs
   1.846 -  RIGHT_ID :: "('a => 'b => 'a) => 'b => bool" 
   1.847 +definition RIGHT_ID :: "('a => 'b => 'a) => 'b => bool" where 
   1.848    "RIGHT_ID ==
   1.849  %(f::'a::type => 'b::type => 'a::type) e::'b::type.
   1.850     ALL x::'a::type. f x e = x"
   1.851 @@ -4621,8 +4534,7 @@
   1.852     RIGHT_ID f e = (ALL x::'a::type. f x e = x)"
   1.853    by (import operator RIGHT_ID_DEF)
   1.854  
   1.855 -constdefs
   1.856 -  LEFT_ID :: "('a => 'b => 'b) => 'a => bool" 
   1.857 +definition LEFT_ID :: "('a => 'b => 'b) => 'a => bool" where 
   1.858    "LEFT_ID ==
   1.859  %(f::'a::type => 'b::type => 'b::type) e::'a::type.
   1.860     ALL x::'b::type. f e x = x"
   1.861 @@ -4631,8 +4543,7 @@
   1.862     LEFT_ID f e = (ALL x::'b::type. f e x = x)"
   1.863    by (import operator LEFT_ID_DEF)
   1.864  
   1.865 -constdefs
   1.866 -  MONOID :: "('a => 'a => 'a) => 'a => bool" 
   1.867 +definition MONOID :: "('a => 'a => 'a) => 'a => bool" where 
   1.868    "MONOID ==
   1.869  %(f::'a::type => 'a::type => 'a::type) e::'a::type.
   1.870     ASSOC f & RIGHT_ID f e & LEFT_ID f e"
   1.871 @@ -4690,15 +4601,13 @@
   1.872  lemma IS_EL_DEF: "ALL (x::'a::type) l::'a::type list. x mem l = list_exists (op = x) l"
   1.873    by (import rich_list IS_EL_DEF)
   1.874  
   1.875 -constdefs
   1.876 -  AND_EL :: "bool list => bool" 
   1.877 +definition AND_EL :: "bool list => bool" where 
   1.878    "AND_EL == list_all I"
   1.879  
   1.880  lemma AND_EL_DEF: "AND_EL = list_all I"
   1.881    by (import rich_list AND_EL_DEF)
   1.882  
   1.883 -constdefs
   1.884 -  OR_EL :: "bool list => bool" 
   1.885 +definition OR_EL :: "bool list => bool" where 
   1.886    "OR_EL == list_exists I"
   1.887  
   1.888  lemma OR_EL_DEF: "OR_EL = list_exists I"
   1.889 @@ -4816,16 +4725,14 @@
   1.890      (if P x then ([], x # l) else (x # fst (SPLITP P l), snd (SPLITP P l))))"
   1.891    by (import rich_list SPLITP)
   1.892  
   1.893 -constdefs
   1.894 -  PREFIX :: "('a => bool) => 'a list => 'a list" 
   1.895 +definition PREFIX :: "('a => bool) => 'a list => 'a list" where 
   1.896    "PREFIX == %(P::'a::type => bool) l::'a::type list. fst (SPLITP (Not o P) l)"
   1.897  
   1.898  lemma PREFIX_DEF: "ALL (P::'a::type => bool) l::'a::type list.
   1.899     PREFIX P l = fst (SPLITP (Not o P) l)"
   1.900    by (import rich_list PREFIX_DEF)
   1.901  
   1.902 -constdefs
   1.903 -  SUFFIX :: "('a => bool) => 'a list => 'a list" 
   1.904 +definition SUFFIX :: "('a => bool) => 'a list => 'a list" where 
   1.905    "SUFFIX ==
   1.906  %P::'a::type => bool.
   1.907     foldl (%(l'::'a::type list) x::'a::type. if P x then SNOC x l' else [])
   1.908 @@ -4837,15 +4744,13 @@
   1.909      [] l"
   1.910    by (import rich_list SUFFIX_DEF)
   1.911  
   1.912 -constdefs
   1.913 -  UNZIP_FST :: "('a * 'b) list => 'a list" 
   1.914 +definition UNZIP_FST :: "('a * 'b) list => 'a list" where 
   1.915    "UNZIP_FST == %l::('a::type * 'b::type) list. fst (unzip l)"
   1.916  
   1.917  lemma UNZIP_FST_DEF: "ALL l::('a::type * 'b::type) list. UNZIP_FST l = fst (unzip l)"
   1.918    by (import rich_list UNZIP_FST_DEF)
   1.919  
   1.920 -constdefs
   1.921 -  UNZIP_SND :: "('a * 'b) list => 'b list" 
   1.922 +definition UNZIP_SND :: "('a * 'b) list => 'b list" where 
   1.923    "UNZIP_SND == %l::('a::type * 'b::type) list. snd (unzip l)"
   1.924  
   1.925  lemma UNZIP_SND_DEF: "ALL l::('a::type * 'b::type) list. UNZIP_SND l = snd (unzip l)"
   1.926 @@ -5916,8 +5821,7 @@
   1.927  
   1.928  ;setup_theory state_transformer
   1.929  
   1.930 -constdefs
   1.931 -  UNIT :: "'b => 'a => 'b * 'a" 
   1.932 +definition UNIT :: "'b => 'a => 'b * 'a" where 
   1.933    "(op ==::('b::type => 'a::type => 'b::type * 'a::type)
   1.934          => ('b::type => 'a::type => 'b::type * 'a::type) => prop)
   1.935   (UNIT::'b::type => 'a::type => 'b::type * 'a::type)
   1.936 @@ -5926,8 +5830,7 @@
   1.937  lemma UNIT_DEF: "ALL x::'b::type. UNIT x = Pair x"
   1.938    by (import state_transformer UNIT_DEF)
   1.939  
   1.940 -constdefs
   1.941 -  BIND :: "('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a" 
   1.942 +definition BIND :: "('a => 'b * 'a) => ('b => 'a => 'c * 'a) => 'a => 'c * 'a" where 
   1.943    "(op ==::(('a::type => 'b::type * 'a::type)
   1.944           => ('b::type => 'a::type => 'c::type * 'a::type)
   1.945              => 'a::type => 'c::type * 'a::type)
   1.946 @@ -5967,8 +5870,7 @@
   1.947               g)))"
   1.948    by (import state_transformer BIND_DEF)
   1.949  
   1.950 -constdefs
   1.951 -  MMAP :: "('c => 'b) => ('a => 'c * 'a) => 'a => 'b * 'a" 
   1.952 +definition MMAP :: "('c => 'b) => ('a => 'c * 'a) => 'a => 'b * 'a" where 
   1.953    "MMAP ==
   1.954  %(f::'c::type => 'b::type) m::'a::type => 'c::type * 'a::type.
   1.955     BIND m (UNIT o f)"
   1.956 @@ -5977,8 +5879,7 @@
   1.957     MMAP f m = BIND m (UNIT o f)"
   1.958    by (import state_transformer MMAP_DEF)
   1.959  
   1.960 -constdefs
   1.961 -  JOIN :: "('a => ('a => 'b * 'a) * 'a) => 'a => 'b * 'a" 
   1.962 +definition JOIN :: "('a => ('a => 'b * 'a) * 'a) => 'a => 'b * 'a" where 
   1.963    "JOIN ==
   1.964  %z::'a::type => ('a::type => 'b::type * 'a::type) * 'a::type. BIND z I"
   1.965