colo12-c703.uibk.ac.at Git - Model of HOL/.git/blob - Model/modelset.ml

   1 (* ========================================================================= *)
   2 (* Set-theoretic hierarchy for modelling HOL inside itself.                  *)
   3 (* ========================================================================= *)
   4
   5 let INJ_LEMMA = prove
   6  (`(!x y. (f x = f y) ==> (x = y)) <=> (!x y. (f x = f y) <=> (x = y))`,
   7   MESON_TAC[]);;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Useful to have a niceish "function update" notation.                      *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 parse_as_infix("|->",(12,"right"));;
  14
  15 let valmod = new_definition
  16   `(x |-> a) (v:A->B) = \y. if y = x then a else v(y)`;;
  17
  18 let VALMOD = prove
  19  (`!v x y a. ((x |-> y) v) a = if a = x then y else v(a)`,
  20   REWRITE_TAC[valmod]);;
  21
  22 let VALMOD_BASIC = prove
  23  (`!v x y. (x |-> y) v x = y`,
  24   REWRITE_TAC[valmod]);;
  25
  26 let VALMOD_VALMOD_BASIC = prove
  27  (`!v a b x. (x |-> a) ((x |-> b) v) = (x |-> a) v`,
  28   REWRITE_TAC[valmod; FUN_EQ_THM] THEN
  29   REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
  30
  31 let VALMOD_REPEAT = prove
  32  (`!v x. (x |-> v(x)) v = v`,
  33   REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
  34
  35 let FORALL_VALMOD = prove
  36  (`!x. (!v a. P((x |-> a) v)) = (!v. P v)`,
  37   MESON_TAC[VALMOD_REPEAT]);;
  38
  39 let VALMOD_SWAP = prove
  40  (`!v x y a b.
  41      ~(x = y) ==> ((x |-> a) ((y |-> b) v) = (y |-> b) ((x |-> a) v))`,
  42   REWRITE_TAC[valmod; FUN_EQ_THM] THEN MESON_TAC[]);;
  43
  44 (* ------------------------------------------------------------------------- *)
  45 (* A dummy finite type inadequately modelling ":ind".                        *)
  46 (* ------------------------------------------------------------------------- *)
  47
  48 let ind_model_tybij_th =
  49   prove(`?x. x IN @s:num->bool. ~(s = {}) /\ FINITE s`,
  50          MESON_TAC[MEMBER_NOT_EMPTY; IN_SING; FINITE_RULES]);;
  51
  52 let ind_model_tybij =
  53   new_type_definition "ind_model" ("mk_ind","dest_ind") ind_model_tybij_th;;
  54
  55 (* ------------------------------------------------------------------------- *)
  56 (* Introduce a type whose universe is "inaccessible" starting from           *)
  57 (* "ind_model". Since "ind_model" is finite, we can just use any             *)
  58 (* infinite set. In order to make "ind_model" infinite, we would need        *)
  59 (* a new axiom. In order to keep things generic we try to deduce             *)
  60 (* everything from this one uniform "axiom". Note that even in the           *)
  61 (* infinite case, this can still be a small set in ZF terms, not a real      *)
  62 (* inaccessible cardinal.                                                    *)
  63 (* ------------------------------------------------------------------------- *)
  64
  65 (****** Here's what we'd do in the infinite case
  66
  67  new_type("I",0);;
  68
  69  let I_AXIOM = new_axiom
  70   `UNIV:ind_model->bool <_c UNIV:I->bool /\
  71    (!s:A->bool. s <_c UNIV:I->bool ==> {t | t SUBSET s} <_c UNIV:I->bool)`;;
  72
  73  *******)
  74
  75 let inacc_tybij_th = prove
  76  (`?x:num. x IN UNIV`,REWRITE_TAC[IN_UNIV]);;
  77
  78 let inacc_tybij =
  79   new_type_definition "I" ("mk_I","dest_I") inacc_tybij_th;;
  80
  81 let I_AXIOM = prove
  82  (`UNIV:ind_model->bool <_c UNIV:I->bool /\
  83    (!s:A->bool. s <_c UNIV:I->bool ==> {t | t SUBSET s} <_c UNIV:I->bool)`,
  84   let lemma = prove
  85    (`!s. s <_c UNIV:I->bool <=> FINITE s`,
  86     GEN_TAC THEN REWRITE_TAC[FINITE_CARD_LT] THEN
  87     MATCH_MP_TAC CARD_LT_CONG THEN REWRITE_TAC[CARD_EQ_REFL] THEN
  88     REWRITE_TAC[GSYM CARD_LE_ANTISYM; le_c; IN_UNIV] THEN
  89     MESON_TAC[inacc_tybij; IN_UNIV]) in
  90   REWRITE_TAC[lemma; FINITE_POWERSET] THEN
  91   SUBGOAL_THEN `UNIV = IMAGE mk_ind (@s. ~(s = {}) /\ FINITE s)`
  92   SUBST1_TAC THENL
  93    [MESON_TAC[EXTENSION; IN_IMAGE; IN_UNIV; ind_model_tybij];
  94     MESON_TAC[FINITE_IMAGE; NOT_INSERT_EMPTY; FINITE_RULES]]);;
  95
  96 (* ------------------------------------------------------------------------- *)
  97 (* I is infinite and therefore admits an injective pairing.                  *)
  98 (* ------------------------------------------------------------------------- *)
  99
 100 let I_INFINITE = prove
 101  (`INFINITE(UNIV:I->bool)`,
 102   REWRITE_TAC[INFINITE] THEN DISCH_TAC THEN
 103   MP_TAC(ISPEC `{n | n < CARD(UNIV:I->bool) - 1}` (CONJUNCT2 I_AXIOM)) THEN
 104   ASM_SIMP_TAC[CARD_LT_CARD; FINITE_NUMSEG_LT; FINITE_POWERSET] THEN
 105   SIMP_TAC[CARD_NUMSEG_LT; CARD_POWERSET; FINITE_NUMSEG_LT] THEN
 106   SUBGOAL_THEN `~(CARD(UNIV:I->bool) = 0)` MP_TAC THENL
 107    [ASM_SIMP_TAC[CARD_EQ_0; GSYM MEMBER_NOT_EMPTY; IN_UNIV]; ALL_TAC] THEN
 108   SIMP_TAC[ARITH_RULE `~(n = 0) ==> n - 1 < n`; NOT_LT] THEN
 109   MATCH_MP_TAC(ARITH_RULE `a - 1 < b ==> ~(a = 0) ==> a <= b`) THEN
 110   SPEC_TAC(`CARD(UNIV:I->bool) - 1`,`n:num`) THEN POP_ASSUM(K ALL_TAC) THEN
 111   INDUCT_TAC THEN REWRITE_TAC[EXP; ARITH] THEN POP_ASSUM MP_TAC THEN
 112   ARITH_TAC);;
 113
 114 let I_PAIR_EXISTS = prove
 115  (`?f:I#I->I. !x y. (f x = f y) ==> (x = y)`,
 116   SUBGOAL_THEN `UNIV:I#I->bool <=_c UNIV:I->bool` MP_TAC THENL
 117    [ALL_TAC; REWRITE_TAC[le_c; IN_UNIV]] THEN
 118   MATCH_MP_TAC CARD_EQ_IMP_LE THEN
 119   MP_TAC(MATCH_MP CARD_SQUARE_INFINITE I_INFINITE) THEN
 120   MATCH_MP_TAC(TAUT `(a = b) ==> a ==> b`) THEN
 121   AP_THM_TAC THEN AP_TERM_TAC THEN
 122   REWRITE_TAC[EXTENSION; mul_c; IN_ELIM_THM; IN_UNIV] THEN MESON_TAC[PAIR]);;
 123
 124 let I_PAIR = REWRITE_RULE[INJ_LEMMA]
 125  (new_specification ["I_PAIR"] I_PAIR_EXISTS);;
 126
 127 (* ------------------------------------------------------------------------- *)
 128 (* It also admits injections from "bool" and "ind_model".                    *)
 129 (* ------------------------------------------------------------------------- *)
 130
 131 let CARD_BOOL_LT_I = prove
 132  (`UNIV:bool->bool <_c UNIV:I->bool`,
 133   REWRITE_TAC[GSYM CARD_NOT_LE] THEN
 134   DISCH_TAC THEN MP_TAC I_INFINITE THEN REWRITE_TAC[INFINITE] THEN
 135   SUBGOAL_THEN `FINITE(UNIV:bool->bool)`
 136    (fun th -> ASM_MESON_TAC[th; CARD_LE_FINITE]) THEN
 137   SUBGOAL_THEN `UNIV:bool->bool = {F,T}` SUBST1_TAC THENL
 138    [REWRITE_TAC[EXTENSION; IN_UNIV; IN_INSERT] THEN MESON_TAC[];
 139     SIMP_TAC[FINITE_RULES]]);;
 140
 141 let I_BOOL_EXISTS = prove
 142  (`?f:bool->I. !x y. (f x = f y) ==> (x = y)`,
 143   MP_TAC(MATCH_MP CARD_LT_IMP_LE CARD_BOOL_LT_I) THEN
 144   SIMP_TAC[lt_c; le_c; IN_UNIV]);;
 145
 146 let I_BOOL = REWRITE_RULE[INJ_LEMMA]
 147  (new_specification ["I_BOOL"] I_BOOL_EXISTS);;
 148
 149 let I_IND_EXISTS = prove
 150  (`?f:ind_model->I. !x y. (f x = f y) ==> (x = y)`,
 151   MP_TAC(CONJUNCT1 I_AXIOM) THEN SIMP_TAC[lt_c; le_c; IN_UNIV]);;
 152
 153 let I_IND = REWRITE_RULE[INJ_LEMMA]
 154  (new_specification ["I_IND"] I_IND_EXISTS);;
 155
 156 (* ------------------------------------------------------------------------- *)
 157 (* And the injection from powerset of any accessible set.                    *)
 158 (* ------------------------------------------------------------------------- *)
 159
 160 let I_SET_EXISTS = prove
 161  (`!s:I->bool.
 162         s <_c UNIV:I->bool
 163         ==> ?f:(I->bool)->I. !t u. t SUBSET s /\ u SUBSET s /\ (f t = f u)
 164                                    ==> (t = u)`,
 165   GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP(CONJUNCT2 I_AXIOM)) THEN
 166   DISCH_THEN(MP_TAC o MATCH_MP CARD_LT_IMP_LE) THEN
 167   REWRITE_TAC[le_c; IN_UNIV; IN_ELIM_THM]);;
 168
 169 let I_SET = new_specification ["I_SET"]
 170  (REWRITE_RULE[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] I_SET_EXISTS);;
 171
 172 (* ------------------------------------------------------------------------- *)
 173 (* Define a type for "levels" of our set theory.                             *)
 174 (* ------------------------------------------------------------------------- *)
 175
 176 let setlevel_INDUCT,setlevel_RECURSION = define_type
 177  "setlevel = Ur_bool
 178            | Ur_ind
 179            | Powerset setlevel
 180            | Cartprod setlevel setlevel";;
 181
 182 let setlevel_DISTINCT = distinctness "setlevel";;
 183 let setlevel_INJ = injectivity "setlevel";;
 184
 185 (* ------------------------------------------------------------------------- *)
 186 (* Now define a subset of I corresponding to each.                           *)
 187 (* ------------------------------------------------------------------------- *)
 188
 189 let setlevel = new_recursive_definition setlevel_RECURSION
 190  `(setlevel Ur_bool = IMAGE I_BOOL UNIV) /\
 191   (setlevel Ur_ind = IMAGE I_IND UNIV) /\
 192   (setlevel (Cartprod l1 l2) =
 193            IMAGE I_PAIR {x,y | x IN setlevel l1 /\ y IN setlevel l2}) /\
 194   (setlevel (Powerset l) = IMAGE (I_SET (setlevel l))
 195                                  {s | s SUBSET (setlevel l)})`;;
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* Show they all satisfy the cardinal limits.                                *)
 199 (* ------------------------------------------------------------------------- *)
 200
 201 let SETLEVEL_CARD = prove
 202  (`!l. setlevel l <_c UNIV:I->bool`,
 203   MATCH_MP_TAC setlevel_INDUCT THEN REWRITE_TAC[setlevel] THEN
 204   REPEAT CONJ_TAC THENL
 205    [TRANS_TAC CARD_LET_TRANS `UNIV:bool->bool` THEN
 206     REWRITE_TAC[CARD_LE_IMAGE; CARD_BOOL_LT_I];
 207     TRANS_TAC CARD_LET_TRANS `UNIV:ind_model->bool` THEN
 208     REWRITE_TAC[CARD_LE_IMAGE; I_AXIOM];
 209     X_GEN_TAC `l:setlevel` THEN DISCH_TAC THEN
 210     TRANS_TAC CARD_LET_TRANS `{s | s SUBSET (setlevel l)}` THEN
 211     ASM_SIMP_TAC[I_AXIOM; CARD_LE_IMAGE];
 212     ALL_TAC] THEN
 213   MAP_EVERY X_GEN_TAC [`l1:setlevel`; `l2:setlevel`] THEN STRIP_TAC THEN
 214   TRANS_TAC CARD_LET_TRANS `setlevel l1 *_c setlevel l2` THEN
 215   ASM_SIMP_TAC[CARD_MUL_LT_INFINITE; I_INFINITE; GSYM mul_c; CARD_LE_IMAGE]);;
 216
 217 (* ------------------------------------------------------------------------- *)
 218 (* Hence the injectivity of the mapping from powerset.                       *)
 219 (* ------------------------------------------------------------------------- *)
 220
 221 let I_SET_SETLEVEL = prove
 222  (`!l s t. s SUBSET setlevel l /\ t SUBSET setlevel l /\
 223           (I_SET (setlevel l) s = I_SET (setlevel l) t)
 224           ==> (s = t)`,
 225   MESON_TAC[SETLEVEL_CARD; I_SET]);;
 226
 227 (* ------------------------------------------------------------------------- *)
 228 (* Now our universe of sets and (ur)elements.                                *)
 229 (* ------------------------------------------------------------------------- *)
 230
 231 let universe = new_definition
 232  `universe = {(t,x) | x IN setlevel t}`;;
 233
 234 (* ------------------------------------------------------------------------- *)
 235 (* Define an actual type V.                                                  *)
 236 (*                                                                           *)
 237 (* This satisfies a suitable number of the ZF axioms. It isn't extensional   *)
 238 (* but we could then construct a quotient structure if desired. Anyway it's  *)
 239 (* only empty sets that aren't. A more significant difference is that we     *)
 240 (* have urelements and the hierarchy levels are all distinct rather than     *)
 241 (* being cumulative.                                                         *)
 242 (* ------------------------------------------------------------------------- *)
 243
 244 let v_tybij_th = prove
 245  (`?a. a IN universe`,
 246   EXISTS_TAC `Ur_bool,I_BOOL T` THEN
 247   REWRITE_TAC[universe; IN_ELIM_THM; PAIR_EQ; CONJ_ASSOC;
 248               ONCE_REWRITE_RULE[CONJ_SYM] UNWIND_THM1;
 249               setlevel; IN_IMAGE; IN_UNIV] THEN
 250   MESON_TAC[]);;
 251
 252 let v_tybij =
 253   new_type_definition "V" ("mk_V","dest_V") v_tybij_th;;
 254
 255 let V_TYBIJ = prove
 256  (`!l e. e IN setlevel l <=> (dest_V(mk_V(l,e)) = (l,e))`,
 257   REWRITE_TAC[GSYM(CONJUNCT2 v_tybij)] THEN
 258   REWRITE_TAC[IN_ELIM_THM; universe; FORALL_PAIR_THM; PAIR_EQ] THEN
 259   MESON_TAC[]);;
 260
 261 (* ------------------------------------------------------------------------- *)
 262 (* Drop a level; test if something is a set.                                 *)
 263 (* ------------------------------------------------------------------------- *)
 264
 265 let droplevel = new_recursive_definition setlevel_RECURSION
 266   `droplevel(Powerset l) = l`;;
 267
 268 let isasetlevel = new_recursive_definition setlevel_RECURSION
 269  `(isasetlevel Ur_bool = F) /\
 270   (isasetlevel Ur_ind = F) /\
 271   (isasetlevel (Cartprod l1 l2) = F) /\
 272   (isasetlevel (Powerset l) = T)`;;
 273
 274 (* ------------------------------------------------------------------------- *)
 275 (* Define some useful inversions.                                            *)
 276 (* ------------------------------------------------------------------------- *)
 277
 278 let level = new_definition
 279  `level x = FST(dest_V x)`;;
 280
 281 let element = new_definition
 282  `element x = SND(dest_V x)`;;
 283
 284 let ELEMENT_IN_LEVEL = prove
 285  (`!x. (element x) IN setlevel(level x)`,
 286   REWRITE_TAC[V_TYBIJ; v_tybij; level; element; PAIR]);;
 287
 288 let SET = prove
 289  (`!x. mk_V(level x,element x) = x`,
 290  REWRITE_TAC[level; element; PAIR; v_tybij]);;
 291
 292 let set = new_definition
 293  `set x = @s. s SUBSET (setlevel(droplevel(level x))) /\
 294               (I_SET (setlevel(droplevel(level x))) s = element x)`;;
 295
 296 let isaset = new_definition
 297  `isaset x <=> ?l. level x = Powerset l`;;
 298
 299 (* ------------------------------------------------------------------------- *)
 300 (* Now all the critical relations.                                           *)
 301 (* ------------------------------------------------------------------------- *)
 302
 303 parse_as_infix("<:",(11,"right"));;
 304
 305 let inset = new_definition
 306  `x <: s <=> (level s = Powerset(level x)) /\ (element x) IN (set s)`;;
 307
 308 parse_as_infix("<=:",(12,"right"));;
 309
 310 let subset_def = new_definition
 311  `s <=: t <=> (level s = level t) /\ !x. x <: s ==> x <: t`;;
 312
 313 (* ------------------------------------------------------------------------- *)
 314 (* If something has members, it's a set.                                     *)
 315 (* ------------------------------------------------------------------------- *)
 316
 317 let MEMBERS_ISASET = prove
 318  (`!x s. x <: s ==> isaset s`,
 319   REWRITE_TAC[inset; isaset] THEN MESON_TAC[]);;
 320
 321 (* ------------------------------------------------------------------------- *)
 322 (* Each level is nonempty.                                                   *)
 323 (* ------------------------------------------------------------------------- *)
 324
 325 let LEVEL_NONEMPTY = prove
 326  (`!l. ?x. x IN setlevel l`,
 327   REWRITE_TAC[MEMBER_NOT_EMPTY] THEN
 328   MATCH_MP_TAC setlevel_INDUCT THEN REWRITE_TAC[setlevel; IMAGE_EQ_EMPTY] THEN
 329   REWRITE_TAC[GSYM MEMBER_NOT_EMPTY; IN_UNIV] THEN
 330   REWRITE_TAC[EXISTS_PAIR_THM; IN_ELIM_THM] THEN
 331   MESON_TAC[EMPTY_SUBSET]);;
 332
 333 let LEVEL_SET_EXISTS = prove
 334  (`!l. ?s. level s = l`,
 335   MP_TAC LEVEL_NONEMPTY THEN MATCH_MP_TAC MONO_FORALL THEN
 336   REWRITE_TAC[level] THEN MESON_TAC[FST; PAIR; V_TYBIJ]);;
 337
 338 (* ------------------------------------------------------------------------- *)
 339 (* Empty sets (or non-sets, of course) exist at all set levels.              *)
 340 (* ------------------------------------------------------------------------- *)
 341
 342 let MK_V_CLAUSES = prove
 343  (`e IN setlevel l
 344    ==> (level(mk_V(l,e)) = l) /\ (element(mk_V(l,e)) = e)`,
 345   REWRITE_TAC[level; element; PAIR; GSYM PAIR_EQ; V_TYBIJ]);;
 346
 347 let MK_V_SET = prove
 348  (`s SUBSET setlevel l
 349    ==> (set(mk_V(Powerset l,I_SET (setlevel l) s)) = s) /\
 350        (level(mk_V(Powerset l,I_SET (setlevel l) s)) = Powerset l) /\
 351        (element(mk_V(Powerset l,I_SET (setlevel l) s)) = I_SET (setlevel l) s)`,
 352   REPEAT GEN_TAC THEN DISCH_TAC THEN
 353   SUBGOAL_THEN `I_SET (setlevel l) s IN setlevel(Powerset l)` ASSUME_TAC THENL
 354    [REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[];
 355     ALL_TAC] THEN
 356   ASM_SIMP_TAC[MK_V_CLAUSES; set] THEN
 357   SUBGOAL_THEN `I_SET (setlevel l) s IN setlevel(Powerset l)` ASSUME_TAC THENL
 358    [REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN ASM_MESON_TAC[];
 359     ALL_TAC] THEN
 360   ASM_SIMP_TAC[MK_V_CLAUSES; droplevel] THEN
 361   MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[] THEN
 362   ASM_MESON_TAC[I_SET_SETLEVEL]);;
 363
 364 let EMPTY_EXISTS = prove
 365  (`!l. ?s. (level s = l) /\ !x. ~(x <: s)`,
 366   MATCH_MP_TAC setlevel_INDUCT THEN
 367   REPEAT CONJ_TAC THENL
 368    [ALL_TAC; ALL_TAC;
 369     X_GEN_TAC `l:setlevel` THEN DISCH_THEN(K ALL_TAC) THEN
 370     EXISTS_TAC `mk_V(Powerset l,I_SET (setlevel l) {})` THEN
 371     SIMP_TAC[inset; MK_V_CLAUSES; MK_V_SET; EMPTY_SUBSET; NOT_IN_EMPTY];
 372     ALL_TAC] THEN
 373  MESON_TAC[LEVEL_SET_EXISTS; MEMBERS_ISASET; isaset;
 374            setlevel_DISTINCT]);;
 375
 376 let EMPTY_SET = new_specification ["emptyset"]
 377         (REWRITE_RULE[SKOLEM_THM] EMPTY_EXISTS);;
 378
 379 (* ------------------------------------------------------------------------- *)
 380 (* Comprehension principle, with no change of levels.                        *)
 381 (* ------------------------------------------------------------------------- *)
 382
 383 let COMPREHENSION_EXISTS = prove
 384  (`!s p. ?t. (level t = level s) /\ !x. x <: t <=> x <: s /\ p x`,
 385   REPEAT GEN_TAC THEN ASM_CASES_TAC `isaset s` THENL
 386    [ALL_TAC; ASM_MESON_TAC[MEMBERS_ISASET]] THEN
 387   POP_ASSUM(X_CHOOSE_TAC `l:setlevel` o REWRITE_RULE[isaset]) THEN
 388   MP_TAC(SPEC `s:V` ELEMENT_IN_LEVEL) THEN
 389   ASM_REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN
 390   DISCH_THEN(X_CHOOSE_THEN `u:I->bool` STRIP_ASSUME_TAC) THEN
 391   EXISTS_TAC `mk_V(Powerset l,
 392                    I_SET(setlevel l)
 393                    {i | i IN u /\ p(mk_V(l,i))})` THEN
 394   SUBGOAL_THEN `{i | i IN u /\ p (mk_V (l,i))} SUBSET (setlevel l)`
 395   ASSUME_TAC THENL
 396    [REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN ASM_MESON_TAC[SUBSET];
 397     ALL_TAC] THEN
 398   ASM_SIMP_TAC[MK_V_SET; inset] THEN X_GEN_TAC `x:V` THEN
 399   REWRITE_TAC[setlevel_INJ] THEN
 400   REWRITE_TAC[IN_ELIM_THM] THEN ASM_MESON_TAC[SET; MK_V_SET]);;
 401
 402 parse_as_infix("suchthat",(21,"left"));;
 403
 404 let SUCHTHAT = new_specification ["suchthat"]
 405      (REWRITE_RULE[SKOLEM_THM] COMPREHENSION_EXISTS);;
 406
 407 (* ------------------------------------------------------------------------- *)
 408 (* Each setlevel exists as a set.                                            *)
 409 (* ------------------------------------------------------------------------- *)
 410
 411 let SETLEVEL_EXISTS = prove
 412  (`!l. ?s. (level s = Powerset l) /\
 413            !x. x <: s <=> (level x = l) /\ element(x) IN setlevel l`,
 414   GEN_TAC THEN
 415   EXISTS_TAC `mk_V(Powerset l,I_SET (setlevel l) (setlevel l))` THEN
 416   SIMP_TAC[MK_V_SET; SUBSET_REFL; inset; setlevel_INJ] THEN MESON_TAC[]);;
 417
 418 (* ------------------------------------------------------------------------- *)
 419 (* Conversely, set(s) belongs in the appropriate level.                      *)
 420 (* ------------------------------------------------------------------------- *)
 421
 422 let SET_DECOMP = prove
 423  (`!s. isaset s
 424        ==> (set s) SUBSET (setlevel(droplevel(level s))) /\
 425            (I_SET (setlevel(droplevel(level s))) (set s) = element s)`,
 426   REPEAT GEN_TAC THEN REWRITE_TAC[isaset] THEN
 427   DISCH_THEN(X_CHOOSE_TAC `l:setlevel`) THEN
 428   REWRITE_TAC[set] THEN CONV_TAC SELECT_CONV THEN
 429   ASM_REWRITE_TAC[setlevel; droplevel] THEN
 430   MP_TAC(SPEC `s:V` ELEMENT_IN_LEVEL) THEN
 431   ASM_REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN
 432   MESON_TAC[]);;
 433
 434 let SET_SUBSET_SETLEVEL = prove
 435  (`!s. isaset s ==> set(s) SUBSET setlevel(droplevel(level s))`,
 436   MESON_TAC[SET_DECOMP]);;
 437
 438 (* ------------------------------------------------------------------------- *)
 439 (* Power set exists.                                                         *)
 440 (* ------------------------------------------------------------------------- *)
 441
 442 let POWERSET_EXISTS = prove
 443  (`!s. ?t. (level t = Powerset(level s)) /\ !x. x <: t <=> x <=: s`,
 444   GEN_TAC THEN ASM_CASES_TAC `isaset s` THENL
 445    [FIRST_ASSUM(MP_TAC o GSYM o MATCH_MP SET_DECOMP) THEN
 446     FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [isaset]) THEN
 447     DISCH_THEN(X_CHOOSE_THEN `l:setlevel` STRIP_ASSUME_TAC) THEN
 448     ASM_REWRITE_TAC[droplevel] THEN STRIP_TAC THEN
 449     X_CHOOSE_THEN `t:V` STRIP_ASSUME_TAC
 450       (SPEC `Powerset l` SETLEVEL_EXISTS) THEN
 451     MP_TAC(SPECL [`t:V`; `\v. !x. x <: v ==> x <: s`]
 452       COMPREHENSION_EXISTS) THEN
 453     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:V` THEN
 454     STRIP_TAC THEN ASM_REWRITE_TAC[subset_def] THEN
 455     ASM_MESON_TAC[ELEMENT_IN_LEVEL];
 456     MP_TAC(SPEC `level s` SETLEVEL_EXISTS) THEN
 457     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `t:V` THEN
 458     STRIP_TAC THEN ASM_REWRITE_TAC[subset_def] THEN
 459     ASM_MESON_TAC[ELEMENT_IN_LEVEL; MEMBERS_ISASET; isaset]]);;
 460
 461 let POWERSET = new_specification ["powerset"]
 462      (REWRITE_RULE[SKOLEM_THM] POWERSET_EXISTS);;
 463
 464 (* ------------------------------------------------------------------------- *)
 465 (* Pairing operation.                                                        *)
 466 (* ------------------------------------------------------------------------- *)
 467
 468 let pair = new_definition
 469  `pair x y =
 470         mk_V(Cartprod (level x) (level y),I_PAIR(element x,element y))`;;
 471
 472 let PAIR_IN_LEVEL = prove
 473  (`!x y l m. x IN setlevel l /\ y IN setlevel m
 474              ==> I_PAIR(x,y) IN setlevel (Cartprod l m)`,
 475   REWRITE_TAC[setlevel; IN_IMAGE; IN_ELIM_THM] THEN MESON_TAC[]);;
 476
 477 let DEST_MK_PAIR = prove
 478  (`dest_V(mk_V(Cartprod (level x) (level y),I_PAIR(element x,element y))) =
 479         Cartprod (level x) (level y),I_PAIR(element x,element y)`,
 480   REWRITE_TAC[GSYM V_TYBIJ] THEN SIMP_TAC[PAIR_IN_LEVEL; ELEMENT_IN_LEVEL]);;
 481
 482 let PAIR_INJ = prove
 483  (`!x1 y1 x2 y2. (pair x1 y1 = pair x2 y2) <=> (x1 = x2) /\ (y1 = y2)`,
 484   REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; SIMP_TAC[]] THEN
 485   REWRITE_TAC[pair] THEN
 486   DISCH_THEN(MP_TAC o AP_TERM `dest_V`) THEN REWRITE_TAC[DEST_MK_PAIR] THEN
 487   REWRITE_TAC[setlevel_INJ; PAIR_EQ; I_PAIR] THEN
 488   REWRITE_TAC[level; element] THEN MESON_TAC[PAIR; CONJUNCT1 v_tybij]);;
 489
 490 let LEVEL_PAIR = prove
 491  (`!x y. level(pair x y) = Cartprod (level x) (level y)`,
 492   REWRITE_TAC[level;
 493               REWRITE_RULE[DEST_MK_PAIR] (AP_TERM `dest_V` (SPEC_ALL pair))]);;
 494
 495 (* ------------------------------------------------------------------------- *)
 496 (* Decomposition functions.                                                  *)
 497 (* ------------------------------------------------------------------------- *)
 498
 499 let fst_def = new_definition
 500   `fst p = @x. ?y. p = pair x y`;;
 501
 502 let snd_def = new_definition
 503   `snd p = @y. ?x. p = pair x y`;;
 504
 505 let PAIR_CLAUSES = prove
 506  (`!x y. (fst(pair x y) = x) /\ (snd(pair x y) = y)`,
 507   REWRITE_TAC[fst_def; snd_def] THEN MESON_TAC[PAIR_INJ]);;
 508
 509 (* ------------------------------------------------------------------------- *)
 510 (* And the Cartesian product space.                                          *)
 511 (* ------------------------------------------------------------------------- *)
 512
 513 let CARTESIAN_EXISTS = prove
 514  (`!s t. ?u. (level u =
 515                   Powerset(Cartprod (droplevel(level s))
 516                                     (droplevel(level t)))) /\
 517                  !z. z <: u <=> ?x y. (z = pair x y) /\ x <: s /\ y <: t`,
 518   REPEAT GEN_TAC THEN
 519   ASM_CASES_TAC `isaset s` THENL
 520    [ALL_TAC; ASM_MESON_TAC[EMPTY_EXISTS; MEMBERS_ISASET]] THEN
 521   SUBGOAL_THEN `?l. (level s = Powerset l)` CHOOSE_TAC THENL
 522    [ASM_MESON_TAC[isaset]; ALL_TAC] THEN
 523   ASM_CASES_TAC `isaset t` THENL
 524    [ALL_TAC; ASM_MESON_TAC[EMPTY_EXISTS; MEMBERS_ISASET]] THEN
 525   SUBGOAL_THEN `?m. (level t = Powerset m)` CHOOSE_TAC THENL
 526    [ASM_MESON_TAC[isaset]; ALL_TAC] THEN
 527   MP_TAC(SPEC `Cartprod l m` SETLEVEL_EXISTS) THEN
 528   ASM_REWRITE_TAC[droplevel] THEN
 529   DISCH_THEN(X_CHOOSE_THEN `u:V` STRIP_ASSUME_TAC) THEN
 530   MP_TAC(SPECL [`u:V`; `\z. ?x y. (z = pair x y) /\ x <: s /\ y <: t`]
 531                COMPREHENSION_EXISTS) THEN
 532   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `w:V` THEN
 533   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 534   X_GEN_TAC `z:V` THEN
 535   MATCH_MP_TAC(TAUT `(a ==> b) /\ (c ==> a) ==> ((a /\ b) /\ c <=> c)`) THEN
 536   CONJ_TAC THENL [MESON_TAC[ELEMENT_IN_LEVEL]; ALL_TAC] THEN
 537   STRIP_TAC THEN ASM_REWRITE_TAC[LEVEL_PAIR] THEN BINOP_TAC THEN
 538   ASM_MESON_TAC[inset; setlevel_INJ]);;
 539
 540 let PRODUCT = new_specification ["product"]
 541        (REWRITE_RULE[SKOLEM_THM] CARTESIAN_EXISTS);;
 542
 543 (* ------------------------------------------------------------------------- *)
 544 (* Extensionality for sets at the same level.                                *)
 545 (* ------------------------------------------------------------------------- *)
 546
 547 let IN_SET_ELEMENT = prove
 548  (`!s. isaset s /\ e IN set(s)
 549        ==> ?x. (e = element x) /\ (level s = Powerset(level x)) /\ x <: s`,
 550   REPEAT STRIP_TAC THEN
 551   FIRST_ASSUM(X_CHOOSE_TAC `l:setlevel` o REWRITE_RULE[isaset]) THEN
 552   EXISTS_TAC `mk_V(l,e)` THEN REWRITE_TAC[inset] THEN
 553   SUBGOAL_THEN `e IN setlevel l` (fun t -> ASM_SIMP_TAC[t; MK_V_CLAUSES]) THEN
 554   ASM_MESON_TAC[SET_SUBSET_SETLEVEL; SUBSET; droplevel]);;
 555
 556 let SUBSET_ALT = prove
 557  (`isaset s /\ isaset t
 558    ==> (s <=: t <=> (level s = level t) /\ set(s) SUBSET set(t))`,
 559   REPEAT GEN_TAC THEN REWRITE_TAC[subset_def; inset] THEN
 560   ASM_CASES_TAC `level s = level t` THEN ASM_REWRITE_TAC[SUBSET] THEN
 561   STRIP_TAC THEN EQ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
 562   ASM_MESON_TAC[IN_SET_ELEMENT]);;
 563
 564 let SUBSET_ANTISYM_LEVEL = prove
 565  (`!s t. isaset s /\ isaset t /\ s <=: t /\ t <=: s ==> (s = t)`,
 566   REPEAT GEN_TAC THEN
 567   REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 568   ASM_SIMP_TAC[SUBSET_ALT]  THEN
 569   EVERY_ASSUM(MP_TAC o GSYM o MATCH_MP SET_DECOMP) THEN
 570   REPEAT STRIP_TAC THEN
 571   MP_TAC(SPEC `s:V` SET) THEN MP_TAC(SPEC `t:V` SET) THEN
 572   REPEAT(DISCH_THEN(SUBST1_TAC o SYM)) THEN
 573   AP_TERM_TAC THEN BINOP_TAC THEN ASM_MESON_TAC[SUBSET_ANTISYM]);;
 574
 575 let EXTENSIONALITY_LEVEL = prove
 576  (`!s t. isaset s /\ isaset t /\ (level s = level t) /\ (!x. x <: s <=> x <: t)
 577          ==> (s = t)`,
 578   MESON_TAC[SUBSET_ANTISYM_LEVEL; subset_def]);;
 579
 580 (* ------------------------------------------------------------------------- *)
 581 (* And hence for any nonempty sets.                                          *)
 582 (* ------------------------------------------------------------------------- *)
 583
 584 let EXTENSIONALITY_NONEMPTY = prove
 585  (`!s t. (?x. x <: s) /\ (?x. x <: t) /\ (!x. x <: s <=> x <: t)
 586          ==> (s = t)`,
 587   REPEAT STRIP_TAC THEN MATCH_MP_TAC EXTENSIONALITY_LEVEL THEN
 588   ASM_MESON_TAC[MEMBERS_ISASET; inset]);;
 589
 590 (* ------------------------------------------------------------------------- *)
 591 (* Union set exists. I don't need this but if might be a sanity check.       *)
 592 (* ------------------------------------------------------------------------- *)
 593
 594 let UNION_EXISTS = prove
 595  (`!s. ?t. (level t = droplevel(level s)) /\
 596            !x. x <: t <=> ?u. x <: u /\ u <: s`,
 597   GEN_TAC THEN ASM_CASES_TAC `isaset s` THENL
 598    [ALL_TAC;
 599     MP_TAC(SPEC `droplevel(level s)` EMPTY_EXISTS) THEN
 600     MATCH_MP_TAC MONO_EXISTS THEN ASM_MESON_TAC[MEMBERS_ISASET]] THEN
 601   FIRST_ASSUM(X_CHOOSE_TAC `l:setlevel` o REWRITE_RULE[isaset]) THEN
 602   ASM_REWRITE_TAC[droplevel] THEN ASM_CASES_TAC `?m. l = Powerset m` THENL
 603    [ALL_TAC;
 604     MP_TAC(SPEC `l:setlevel` EMPTY_EXISTS) THEN MATCH_MP_TAC MONO_EXISTS THEN
 605     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[inset] THEN
 606     ASM_MESON_TAC[setlevel_INJ]] THEN
 607   FIRST_X_ASSUM(X_CHOOSE_THEN `m:setlevel` SUBST_ALL_TAC) THEN
 608   MP_TAC(SPEC `m:setlevel` SETLEVEL_EXISTS) THEN
 609   ASM_REWRITE_TAC[droplevel] THEN
 610   DISCH_THEN(X_CHOOSE_THEN `t:V` STRIP_ASSUME_TAC) THEN
 611   MP_TAC(SPECL [`t:V`; `\x. ?u. x <: u /\ u <: s`]
 612       COMPREHENSION_EXISTS) THEN
 613   MATCH_MP_TAC MONO_EXISTS THEN
 614   GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 615   ASM_MESON_TAC[inset; ELEMENT_IN_LEVEL; setlevel_INJ]);;
 616
 617 let SETUNION = new_specification ["setunion"]
 618         (REWRITE_RULE[SKOLEM_THM] UNION_EXISTS);;
 619
 620 (* ------------------------------------------------------------------------- *)
 621 (* Boolean stuff.                                                            *)
 622 (* ------------------------------------------------------------------------- *)
 623
 624 let true_def = new_definition
 625  `true = mk_V(Ur_bool,I_BOOL T)`;;
 626
 627 let false_def = new_definition
 628  `false = mk_V(Ur_bool,I_BOOL F)`;;
 629
 630 let boolset = new_definition
 631  `boolset =
 632      mk_V(Powerset Ur_bool,I_SET (setlevel Ur_bool) (setlevel Ur_bool))`;;
 633
 634 let IN_BOOL = prove
 635  (`!x. x <: boolset <=> (x = true) \/ (x = false)`,
 636   REWRITE_TAC[inset; boolset; true_def; false_def] THEN
 637   SIMP_TAC[MK_V_SET; SUBSET_REFL] THEN
 638   REWRITE_TAC[setlevel_INJ; setlevel] THEN
 639   SUBGOAL_THEN `IMAGE I_BOOL UNIV = {I_BOOL F,I_BOOL T}` SUBST1_TAC THENL
 640    [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_UNIV; IN_INSERT; NOT_IN_EMPTY] THEN
 641     MESON_TAC[I_BOOL];
 642     ALL_TAC] THEN
 643   GEN_TAC THEN
 644   GEN_REWRITE_TAC (RAND_CONV o BINOP_CONV o LAND_CONV) [GSYM SET] THEN
 645   REWRITE_TAC[IN_INSERT; NOT_IN_EMPTY] THEN
 646   SUBGOAL_THEN `!b. (I_BOOL b) IN setlevel Ur_bool` ASSUME_TAC THENL
 647    [REWRITE_TAC[setlevel; IN_IMAGE; IN_UNIV] THEN MESON_TAC[];
 648     ASM_MESON_TAC[V_TYBIJ; ELEMENT_IN_LEVEL; PAIR_EQ]]);;
 649
 650 let TRUE_NE_FALSE = prove
 651  (`~(true = false)`,
 652   REWRITE_TAC[true_def; false_def] THEN
 653   DISCH_THEN(MP_TAC o AP_TERM `dest_V`) THEN
 654   SUBGOAL_THEN `!b. (I_BOOL b) IN setlevel Ur_bool` ASSUME_TAC THENL
 655    [REWRITE_TAC[setlevel; IN_IMAGE; IN_UNIV] THEN MESON_TAC[];
 656     ASM_MESON_TAC[V_TYBIJ; I_BOOL; PAIR_EQ]]);;
 657
 658 let BOOLEAN_EQ = prove
 659  (`!x y. x <: boolset /\ y <: boolset /\
 660          ((x = true) <=> (y = true))
 661          ==> (x = y)`,
 662   MESON_TAC[TRUE_NE_FALSE; IN_BOOL]);;
 663
 664 (* ------------------------------------------------------------------------- *)
 665 (* Ind stuff.                                                                *)
 666 (* ------------------------------------------------------------------------- *)
 667
 668 let indset = new_definition
 669  `indset = mk_V(Powerset Ur_ind,I_SET (setlevel Ur_ind) (setlevel Ur_ind))`;;
 670
 671 let INDSET_IND_MODEL = prove
 672  (`?f. (!i:ind_model. f(i) <: indset) /\ (!i j. (f i = f j) ==> (i = j))`,
 673   EXISTS_TAC `\i. mk_V(Ur_ind,I_IND i)` THEN REWRITE_TAC[] THEN
 674   SUBGOAL_THEN `!i. (I_IND i) IN setlevel Ur_ind` ASSUME_TAC THENL
 675    [REWRITE_TAC[setlevel; IN_IMAGE; IN_UNIV] THEN MESON_TAC[]; ALL_TAC] THEN
 676   ASM_SIMP_TAC[MK_V_SET; SUBSET_REFL; inset; indset; MK_V_CLAUSES] THEN
 677   ASM_MESON_TAC[V_TYBIJ; I_IND; ELEMENT_IN_LEVEL; PAIR_EQ]);;
 678
 679 let INDSET_INHABITED = prove
 680  (`?x. x <: indset`,
 681   MESON_TAC[INDSET_IND_MODEL]);;
 682
 683 (* ------------------------------------------------------------------------- *)
 684 (* Axiom of choice (this is trivially so in HOL anyway, but...)              *)
 685 (* ------------------------------------------------------------------------- *)
 686
 687 let ch =
 688   let th = prove
 689    (`?ch. !s. (?x. x <: s) ==> ch(s) <: s`,
 690     REWRITE_TAC[GSYM SKOLEM_THM] THEN MESON_TAC[]) in
 691   new_specification ["ch"] th;;
 692
 693 (* ------------------------------------------------------------------------- *)
 694 (* Sanity check lemmas.                                                      *)
 695 (* ------------------------------------------------------------------------- *)
 696
 697 let IN_POWERSET = prove
 698  (`!x s. x <: powerset s <=> x <=: s`,
 699   MESON_TAC[POWERSET]);;
 700
 701 let IN_PRODUCT = prove
 702  (`!z s t. z <: product s t <=> ?x y. (z = pair x y) /\ x <: s /\ y <: t`,
 703   MESON_TAC[PRODUCT]);;
 704
 705 let IN_COMPREHENSION = prove
 706  (`!p s x. x <: s suchthat p <=> x <: s /\ p x`,
 707   MESON_TAC[SUCHTHAT]);;
 708
 709 let PRODUCT_INHABITED = prove
 710  (`(?x. x <: s) /\ (?y. y <: t) ==> ?z. z <: product s t`,
 711   MESON_TAC[IN_PRODUCT]);;
 712
 713 (* ------------------------------------------------------------------------- *)
 714 (* Definition of function space.                                             *)
 715 (* ------------------------------------------------------------------------- *)
 716
 717 let funspace = new_definition
 718   `funspace s t =
 719       powerset(product s t) suchthat
 720       (\u. !x. x <: s ==> ?!y. pair x y <: u)`;;
 721
 722 let apply_def = new_definition
 723   `apply f x = @y. pair x y <: f`;;
 724
 725 let abstract = new_definition
 726   `abstract s t f =
 727         (product s t) suchthat (\z. !x y. (pair x y = z) ==> (y = f x))`;;
 728
 729 let APPLY_ABSTRACT = prove
 730  (`!x s t. x <: s /\ f(x) <: t ==> (apply(abstract s t f) x = f(x))`,
 731   REPEAT STRIP_TAC THEN
 732   REWRITE_TAC[apply_def; abstract; IN_PRODUCT; SUCHTHAT] THEN
 733   MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[PAIR_INJ] THEN
 734   ASM_MESON_TAC[]);;
 735
 736 let APPLY_IN_RANSPACE = prove
 737  (`!f x s t. x <: s /\ f <: funspace s t ==> apply f x <: t`,
 738   REWRITE_TAC[funspace; SUCHTHAT; IN_POWERSET; IN_PRODUCT; subset_def] THEN
 739   REWRITE_TAC[apply_def] THEN MESON_TAC[PAIR_INJ]);;
 740
 741 let ABSTRACT_IN_FUNSPACE = prove
 742  (`!f x s t. (!x. x <: s ==> f(x) <: t)
 743              ==> abstract s t f <: funspace s t`,
 744   REWRITE_TAC[funspace; abstract; SUCHTHAT; IN_POWERSET; IN_PRODUCT;
 745               subset_def; PAIR_INJ] THEN
 746   SIMP_TAC[LEFT_FORALL_IMP_THM; GSYM CONJ_ASSOC; RIGHT_EXISTS_AND_THM] THEN
 747   REWRITE_TAC[UNWIND_THM1; EXISTS_REFL] THEN MESON_TAC[]);;
 748
 749 let FUNSPACE_INHABITED = prove
 750  (`!s t. ((?x. x <: s) ==> (?y. y <: t)) ==> ?f. f <: funspace s t`,
 751   REPEAT STRIP_TAC THEN
 752   EXISTS_TAC `abstract s t (\x. @y. y <: t)` THEN
 753   MATCH_MP_TAC ABSTRACT_IN_FUNSPACE THEN ASM_MESON_TAC[]);;
 754
 755 let ABSTRACT_EQ = prove
 756  (`!s t1 t2 f g.
 757         (?x. x <: s) /\
 758         (!x. x <: s ==> f(x) <: t1 /\ g(x) <: t2 /\ (f x = g x))
 759         ==> (abstract s t1 f = abstract s t2 g)`,
 760   REWRITE_TAC[abstract] THEN REPEAT STRIP_TAC THEN
 761   MATCH_MP_TAC EXTENSIONALITY_NONEMPTY THEN
 762   REWRITE_TAC[SUCHTHAT; IN_PRODUCT] THEN REPEAT CONJ_TAC THEN
 763   REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
 764   SIMP_TAC[TAUT `(a /\ b /\ c) /\ d <=> ~(a ==> b /\ c ==> ~d)`] THEN
 765   REWRITE_TAC[PAIR_INJ] THEN SIMP_TAC[LEFT_FORALL_IMP_THM] THENL
 766    [ASM_MESON_TAC[]; ASM_MESON_TAC[]; ALL_TAC] THEN
 767   ASM_REWRITE_TAC[PAIR_INJ] THEN
 768   REWRITE_TAC[RIGHT_EXISTS_AND_THM; EXISTS_REFL] THEN
 769   REWRITE_TAC[NOT_IMP] THEN GEN_TAC THEN EQ_TAC THEN STRIP_TAC THEN
 770   ASM_REWRITE_TAC[PAIR_INJ] THEN ASM_MESON_TAC[]);;
 771
 772 (* ------------------------------------------------------------------------- *)
 773 (* Special case of treating a Boolean function as a set.                     *)
 774 (* ------------------------------------------------------------------------- *)
 775
 776 let boolean = new_definition
 777   `boolean b = if b then true else false`;;
 778
 779 let holds = new_definition
 780   `holds s x <=> (apply s x = true)`;;
 781
 782 let BOOLEAN_IN_BOOLSET = prove
 783  (`!b. boolean b <: boolset`,
 784   REWRITE_TAC[boolean] THEN MESON_TAC[IN_BOOL]);;
 785
 786 let BOOLEAN_EQ_TRUE = prove
 787  (`!b. (boolean b = true) <=> b`,
 788   REWRITE_TAC[boolean] THEN MESON_TAC[TRUE_NE_FALSE]);;