class.ml

   1 (* ========================================================================= *)
   2 (* Extensional, classical reasoning with AC starts now!                      *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "ind_defs.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Eta-axiom, corresponding conversion, and extensionality.                  *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let ETA_AX = new_axiom
  17   `!t:A->B. (\x. t x) = t`;;
  18
  19 let ETA_CONV =
  20   let t = `t:A->B` in
  21   let pth = prove(`(\x. (t:A->B) x) = t`,MATCH_ACCEPT_TAC ETA_AX) in
  22   fun tm ->
  23     try let bv,bod = dest_abs tm in
  24         let l,r = dest_comb bod in
  25         if r = bv & not (vfree_in bv l) then
  26           TRANS (REFL tm) (PINST [type_of bv,aty; type_of bod,bty] [l,t] pth)
  27         else fail()
  28     with Failure _ -> failwith "ETA_CONV";;
  29
  30 let EQ_EXT = prove
  31  (`!(f:A->B) g. (!x. f x = g x) ==> f = g`,
  32   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o ABS `x:A` o SPEC `x:A`) THEN
  33   REWRITE_TAC[ETA_AX]);;
  34
  35 let FUN_EQ_THM = prove
  36  (`!(f:A->B) g. f = g <=> (!x. f x = g x)`,
  37   REPEAT GEN_TAC THEN EQ_TAC THENL
  38    [DISCH_THEN SUBST1_TAC THEN GEN_TAC THEN REFL_TAC;
  39     MATCH_ACCEPT_TAC EQ_EXT]);;
  40
  41 (* ------------------------------------------------------------------------- *)
  42 (* Indefinite descriptor (giving AC).                                        *)
  43 (* ------------------------------------------------------------------------- *)
  44
  45 new_constant("@",`:(A->bool)->A`);;
  46
  47 parse_as_binder "@";;
  48
  49 let is_select = is_binder "@";;
  50 let dest_select = dest_binder "@";;
  51 let mk_select = mk_binder "@";;
  52
  53 let SELECT_AX = new_axiom
  54  `!P (x:A). P x ==> P((@) P)`;;
  55
  56 (* ------------------------------------------------------------------------- *)
  57 (* Useful for compatibility. (The old EXISTS_DEF.)                           *)
  58 (* ------------------------------------------------------------------------- *)
  59
  60 let EXISTS_THM = prove
  61  (`(?) = \P:A->bool. P ((@) P)`,
  62   MATCH_MP_TAC EQ_EXT THEN BETA_TAC THEN X_GEN_TAC `P:A->bool` THEN
  63   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
  64   EQ_TAC THENL
  65    [DISCH_THEN(CHOOSE_THEN MP_TAC) THEN MATCH_ACCEPT_TAC SELECT_AX;
  66     DISCH_TAC THEN EXISTS_TAC `((@) P):A` THEN POP_ASSUM ACCEPT_TAC]);;
  67
  68 (* ------------------------------------------------------------------------- *)
  69 (* Rules and so on for the select operator.                                  *)
  70 (* ------------------------------------------------------------------------- *)
  71
  72 let SELECT_RULE =
  73   let P = `P:A->bool` in
  74   let pth = prove
  75    (`(?) (P:A->bool) ==> P((@) P)`,
  76     SIMP_TAC[SELECT_AX; ETA_AX]) in
  77   fun th ->
  78     try let abs = rand(concl th) in
  79         let ty = type_of(bndvar abs) in
  80         CONV_RULE BETA_CONV (MP (PINST [ty,aty] [abs,P] pth) th)
  81     with Failure _ -> failwith "SELECT_RULE";;
  82
  83 let SELECT_CONV =
  84   let P = `P:A->bool` in
  85   let pth = prove
  86    (`(P:A->bool)((@) P) = (?) P`,
  87     REWRITE_TAC[EXISTS_THM] THEN BETA_TAC THEN REFL_TAC) in
  88    fun tm ->
  89      try let is_epsok t = is_select t &
  90                           let bv,bod = dest_select t in
  91                           aconv tm (vsubst [t,bv] bod) in
  92          let pickeps = find_term is_epsok tm in
  93          let abs = rand pickeps in
  94          let ty = type_of (bndvar abs) in
  95          CONV_RULE (LAND_CONV BETA_CONV) (PINST [ty,aty] [abs,P] pth)
  96      with Failure _ -> failwith "SELECT_CONV";;
  97
  98 (* ------------------------------------------------------------------------- *)
  99 (* Some basic theorems.                                                      *)
 100 (* ------------------------------------------------------------------------- *)
 101
 102 let SELECT_REFL = prove
 103  (`!x:A. (@y. y = x) = x`,
 104   GEN_TAC THEN CONV_TAC SELECT_CONV THEN
 105   EXISTS_TAC `x:A` THEN REFL_TAC);;
 106
 107 let SELECT_UNIQUE = prove
 108  (`!P x. (!y:A. P y = (y = x)) ==> ((@) P = x)`,
 109   REPEAT STRIP_TAC THEN
 110   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
 111   ASM_REWRITE_TAC[SELECT_REFL]);;
 112
 113 extend_basic_rewrites [SELECT_REFL];;
 114
 115 (* ------------------------------------------------------------------------- *)
 116 (* Now we can derive type definitions from existence; check benignity.       *)
 117 (* ------------------------------------------------------------------------- *)
 118
 119 let the_type_definitions = ref ([]:((string*string*string)*(thm*thm))list);;
 120
 121 let new_type_definition tyname (absname,repname) th =
 122   try let th',tth' = assoc (tyname,absname,repname) (!the_type_definitions) in
 123       if concl th' <> concl th then failwith "" else
 124       (warn true "Benign redefinition of type"; tth')
 125   with Failure _ ->
 126     let th0 =
 127      CONV_RULE (RATOR_CONV (REWR_CONV EXISTS_THM) THENC BETA_CONV) th in
 128     let th1,th2 = new_basic_type_definition tyname (absname,repname) th0 in
 129     let tth = CONJ (GEN_ALL th1)
 130                    (GEN_ALL (CONV_RULE(LAND_CONV (TRY_CONV BETA_CONV)) th2)) in
 131     the_type_definitions := ((tyname,absname,repname),(th,tth))::
 132                             (!the_type_definitions);
 133     tth;;
 134
 135 (* ------------------------------------------------------------------------- *)
 136 (* Derive excluded middle. The proof is an optimization due to Mark Adams of *)
 137 (* the original Diaconescu proof as presented in Beeson's book.              *)
 138 (* ------------------------------------------------------------------------- *)
 139
 140 let EXCLUDED_MIDDLE = prove
 141  (`!t. t \/ ~t`,
 142   GEN_TAC THEN SUBGOAL_THEN
 143    `(((@x. (x <=> F) \/ t) <=> F) \/ t) /\ (((@x. (x <=> T) \/ t) <=> T) \/ t)`
 144   MP_TAC THENL
 145    [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL
 146      [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN
 147     DISJ1_TAC THEN REFL_TAC;
 148     DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 149     TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN
 150     DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~(T <=> F)`) THEN
 151     PURE_ONCE_ASM_REWRITE_TAC[] THEN
 152     ASM_REWRITE_TAC[ITAUT `p \/ T <=> T`]]);;
 153
 154 let BOOL_CASES_AX = prove
 155  (`!t. (t <=> T) \/ (t <=> F)`,
 156   GEN_TAC THEN DISJ_CASES_TAC(SPEC `t:bool` EXCLUDED_MIDDLE) THEN
 157   ASM_REWRITE_TAC[]);;
 158
 159 (* ------------------------------------------------------------------------- *)
 160 (* Classically based tactics. (See also COND_CASES_TAC later on.)            *)
 161 (* ------------------------------------------------------------------------- *)
 162
 163 let BOOL_CASES_TAC p = STRUCT_CASES_TAC (SPEC p BOOL_CASES_AX);;
 164
 165 let ASM_CASES_TAC t = DISJ_CASES_TAC(SPEC t EXCLUDED_MIDDLE);;
 166
 167 (* ------------------------------------------------------------------------- *)
 168 (* Set up a reasonable tautology checker for classical logic.                *)
 169 (* ------------------------------------------------------------------------- *)
 170
 171 let TAUT =
 172   let PROP_REWRITE_TAC = REWRITE_TAC[] in
 173   let RTAUT_TAC (asl,w) =
 174     let ok t = type_of t = bool_ty & can (find_term is_var) t & free_in t w in
 175     (PROP_REWRITE_TAC THEN
 176      W((fun t1 t2 -> t1 THEN t2) (REWRITE_TAC[]) o BOOL_CASES_TAC o
 177        hd o sort free_in o find_terms ok o snd)) (asl,w) in
 178   let TAUT_TAC = REPEAT(GEN_TAC ORELSE CONJ_TAC) THEN REPEAT RTAUT_TAC in
 179   fun tm -> prove(tm,TAUT_TAC);;
 180
 181 (* ------------------------------------------------------------------------- *)
 182 (* A few useful classical tautologies.                                       *)
 183 (* ------------------------------------------------------------------------- *)
 184
 185 let DE_MORGAN_THM = TAUT
 186   `!t1 t2. (~(t1 /\ t2) <=> ~t1 \/ ~t2) /\ (~(t1 \/ t2) <=> ~t1 /\ ~t2)`;;
 187
 188 let NOT_CLAUSES =
 189   TAUT `(!t. ~ ~t <=> t) /\ (~T <=> F) /\ (~F <=> T)`;;
 190
 191 let NOT_IMP = TAUT `!t1 t2. ~(t1 ==> t2) <=> t1 /\ ~t2`;;
 192
 193 let CONTRAPOS_THM = TAUT `!t1 t2. (~t1 ==> ~t2) <=> (t2 ==> t1)`;;
 194
 195 extend_basic_rewrites [CONJUNCT1 NOT_CLAUSES];;
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* Some classically based rules.                                             *)
 199 (* ------------------------------------------------------------------------- *)
 200
 201 let CCONTR =
 202   let P = `P:bool` in
 203   let pth = TAUT `(~P ==> F) ==> P` in
 204   fun tm th ->
 205     try let tm' = mk_neg tm in
 206         MP (INST [tm,P] pth) (DISCH tm' th)
 207     with Failure _ -> failwith "CCONTR";;
 208
 209 let CONTRAPOS_CONV =
 210   let a = `a:bool` and b = `b:bool` in
 211   let pth = TAUT `(a ==> b) <=> (~b ==> ~a)` in
 212   fun tm ->
 213     try let P,Q = dest_imp tm in
 214         INST [P,a; Q,b] pth
 215     with Failure _ -> failwith "CONTRAPOS_CONV";;
 216
 217 (* ------------------------------------------------------------------------- *)
 218 (* A classicalal "refutation" tactic.                                        *)
 219 (* ------------------------------------------------------------------------- *)
 220
 221 let REFUTE_THEN =
 222   let f_tm = `F`
 223   and conv = REWR_CONV(TAUT `p <=> ~p ==> F`) in
 224   fun ttac (asl,w as gl) ->
 225     if w = f_tm then ALL_TAC gl
 226     else if is_neg w then DISCH_THEN ttac gl
 227     else (CONV_TAC conv THEN DISCH_THEN ttac) gl;;
 228
 229 (* ------------------------------------------------------------------------- *)
 230 (* Infinite de Morgan laws.                                                  *)
 231 (* ------------------------------------------------------------------------- *)
 232
 233 let NOT_EXISTS_THM = prove
 234  (`!P. ~(?x:A. P x) <=> (!x. ~(P x))`,
 235   GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
 236    [GEN_TAC THEN DISCH_TAC THEN UNDISCH_TAC `~(?x:A. P x)` THEN
 237     REWRITE_TAC[] THEN EXISTS_TAC `x:A` THEN POP_ASSUM ACCEPT_TAC;
 238     DISCH_THEN(CHOOSE_THEN MP_TAC) THEN ASM_REWRITE_TAC[]]);;
 239
 240 let EXISTS_NOT_THM = prove
 241  (`!P. (?x:A. ~(P x)) <=> ~(!x. P x)`,
 242   ONCE_REWRITE_TAC[TAUT `(a <=> ~b) <=> (~a <=> b)`] THEN
 243   REWRITE_TAC[NOT_EXISTS_THM]);;
 244
 245 let NOT_FORALL_THM = prove
 246  (`!P. ~(!x. P x) <=> (?x:A. ~(P x))`,
 247   MATCH_ACCEPT_TAC(GSYM EXISTS_NOT_THM));;
 248
 249 let FORALL_NOT_THM = prove
 250  (`!P. (!x. ~(P x)) <=> ~(?x:A. P x)`,
 251   MATCH_ACCEPT_TAC(GSYM NOT_EXISTS_THM));;
 252
 253 (* ------------------------------------------------------------------------- *)
 254 (* Expand quantification over Booleans.                                      *)
 255 (* ------------------------------------------------------------------------- *)
 256
 257 let FORALL_BOOL_THM = prove
 258   (`(!b. P b) <=> P T /\ P F`,
 259    EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
 260    GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN ASM_REWRITE_TAC[]);;
 261
 262 let EXISTS_BOOL_THM = prove
 263  (`(?b. P b) <=> P T \/ P F`,
 264   MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
 265   REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_BOOL_THM]);;
 266
 267 (* ------------------------------------------------------------------------- *)
 268 (* Universal quantifier and disjunction                                      *)
 269 (* ------------------------------------------------------------------------- *)
 270
 271 let LEFT_FORALL_OR_THM = prove
 272  (`!P Q. (!x:A. P x \/ Q) <=> (!x. P x) \/ Q`,
 273   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
 274   REWRITE_TAC[NOT_FORALL_THM; DE_MORGAN_THM; LEFT_EXISTS_AND_THM]);;
 275
 276 let RIGHT_FORALL_OR_THM = prove
 277  (`!P Q. (!x:A. P \/ Q x) <=> P \/ (!x. Q x)`,
 278   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
 279   REWRITE_TAC[NOT_FORALL_THM; DE_MORGAN_THM; RIGHT_EXISTS_AND_THM]);;
 280
 281 let LEFT_OR_FORALL_THM = prove
 282  (`!P Q. (!x:A. P x) \/ Q <=> (!x. P x \/ Q)`,
 283   MATCH_ACCEPT_TAC(GSYM LEFT_FORALL_OR_THM));;
 284
 285 let RIGHT_OR_FORALL_THM = prove
 286  (`!P Q. P \/ (!x:A. Q x) <=> (!x. P \/ Q x)`,
 287   MATCH_ACCEPT_TAC(GSYM RIGHT_FORALL_OR_THM));;
 288
 289 (* ------------------------------------------------------------------------- *)
 290 (* Implication and quantifiers.                                              *)
 291 (* ------------------------------------------------------------------------- *)
 292
 293 let LEFT_IMP_FORALL_THM = prove
 294  (`!P Q. ((!x:A. P x) ==> Q) <=> (?x. P x ==> Q)`,
 295   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
 296   REWRITE_TAC[NOT_EXISTS_THM; NOT_IMP; LEFT_AND_FORALL_THM]);;
 297
 298 let LEFT_EXISTS_IMP_THM = prove
 299  (`!P Q. (?x. P x ==> Q) <=> ((!x:A. P x) ==> Q)`,
 300   MATCH_ACCEPT_TAC(GSYM LEFT_IMP_FORALL_THM));;
 301
 302 let RIGHT_IMP_EXISTS_THM = prove
 303  (`!P Q. (P ==> ?x:A. Q x) <=> (?x:A. P ==> Q x)`,
 304   REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[TAUT `(a <=> b) <=> (~a <=> ~b)`] THEN
 305   REWRITE_TAC[NOT_EXISTS_THM; NOT_IMP; RIGHT_AND_FORALL_THM]);;
 306
 307 let RIGHT_EXISTS_IMP_THM = prove
 308  (`!P Q. (?x:A. P ==> Q x) <=> (P ==> ?x:A. Q x)`,
 309   MATCH_ACCEPT_TAC(GSYM RIGHT_IMP_EXISTS_THM));;
 310
 311 (* ------------------------------------------------------------------------- *)
 312 (* The conditional.                                                          *)
 313 (* ------------------------------------------------------------------------- *)
 314
 315 let COND_DEF = new_definition
 316   `COND = \t t1 t2. @x:A. ((t <=> T) ==> (x = t1)) /\
 317                           ((t <=> F) ==> (x = t2))`;;
 318
 319 let COND_CLAUSES = prove
 320  (`!(t1:A) t2. ((if T then t1 else t2) = t1) /\
 321                ((if F then t1 else t2) = t2)`,
 322   REWRITE_TAC[COND_DEF]);;
 323
 324 let is_cond tm =
 325   try fst(dest_const(rator(rator (rator tm)))) = "COND"
 326   with Failure _ -> false;;
 327
 328 let mk_cond (b,x,y) =
 329   try let c = mk_const("COND",[type_of x,aty]) in
 330       mk_comb(mk_comb(mk_comb(c,b),x),y)
 331   with Failure _ -> failwith "mk_cond";;
 332
 333 let dest_cond tm =
 334   try let tm1,y = dest_comb tm in
 335       let tm2,x = dest_comb tm1 in
 336       let c,b = dest_comb tm2 in
 337       if fst(dest_const c) = "COND" then (b,(x,y)) else fail()
 338   with Failure _ -> failwith "dest_cond";;
 339
 340 extend_basic_rewrites [COND_CLAUSES];;
 341
 342 let COND_EXPAND = prove
 343  (`!b t1 t2. (if b then t1 else t2) <=> (~b \/ t1) /\ (b \/ t2)`,
 344   REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN
 345   REWRITE_TAC[]);;
 346
 347 let COND_ID = prove
 348  (`!b (t:A). (if b then t else t) = t`,
 349   REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
 350
 351 let COND_RAND = prove
 352  (`!b (f:A->B) x y. f (if b then x else y) = (if b then f x else f y)`,
 353   REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
 354
 355 let COND_RATOR = prove
 356  (`!b (f:A->B) g x. (if b then f else g)(x) = (if b then f x else g x)`,
 357   REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[]);;
 358
 359 let COND_ABS = prove
 360  (`!b (f:A->B) g. (\x. if b then f x else g x) = (if b then f else g)`,
 361   REPEAT GEN_TAC THEN BOOL_CASES_TAC `b:bool` THEN REWRITE_TAC[ETA_AX]);;
 362
 363 (* ------------------------------------------------------------------------- *)
 364 (* Redefine TAUT to freeze in the rewrites including COND.                   *)
 365 (* ------------------------------------------------------------------------- *)
 366
 367 let TAUT =
 368   let PROP_REWRITE_TAC = REWRITE_TAC[] in
 369   let RTAUT_TAC (asl,w) =
 370     let ok t = type_of t = bool_ty & can (find_term is_var) t & free_in t w in
 371     (PROP_REWRITE_TAC THEN
 372      W((fun t1 t2 -> t1 THEN t2) (REWRITE_TAC[]) o BOOL_CASES_TAC o
 373        hd o sort free_in o find_terms ok o snd)) (asl,w) in
 374   let TAUT_TAC = REPEAT(GEN_TAC ORELSE CONJ_TAC) THEN REPEAT RTAUT_TAC in
 375   fun tm -> prove(tm,TAUT_TAC);;
 376
 377 (* ------------------------------------------------------------------------- *)
 378 (* Throw monotonicity in.                                                    *)
 379 (* ------------------------------------------------------------------------- *)
 380
 381 let MONO_COND = prove
 382  (`(A ==> B) /\ (C ==> D) ==> (if b then A else C) ==> (if b then B else D)`,
 383   STRIP_TAC THEN BOOL_CASES_TAC `b:bool` THEN
 384   ASM_REWRITE_TAC[]);;
 385
 386 monotonicity_theorems := MONO_COND::(!monotonicity_theorems);;
 387
 388 (* ------------------------------------------------------------------------- *)
 389 (* Tactic for splitting over an arbitrarily chosen conditional.              *)
 390 (* ------------------------------------------------------------------------- *)
 391
 392 let COND_ELIM_THM = prove
 393  (`(P:A->bool) (if c then x else y) <=> (c ==> P x) /\ (~c ==> P y)`,
 394   BOOL_CASES_TAC `c:bool` THEN REWRITE_TAC[]);;
 395
 396 let COND_ELIM_CONV = HIGHER_REWRITE_CONV[COND_ELIM_THM] true;;
 397
 398 let (COND_CASES_TAC :tactic) =
 399   let DENEG_RULE = GEN_REWRITE_RULE I [TAUT `~ ~ p <=> p`] in
 400   CONV_TAC COND_ELIM_CONV THEN CONJ_TAC THENL
 401     [DISCH_THEN(fun th -> ASSUME_TAC th THEN SUBST1_TAC(EQT_INTRO th));
 402      DISCH_THEN(fun th -> try let th' = DENEG_RULE th in
 403                               ASSUME_TAC th' THEN SUBST1_TAC(EQT_INTRO th')
 404                           with Failure _ ->
 405                               ASSUME_TAC th THEN SUBST1_TAC(EQF_INTRO th))];;
 406
 407 (* ------------------------------------------------------------------------- *)
 408 (* Skolemization.                                                            *)
 409 (* ------------------------------------------------------------------------- *)
 410
 411 let SKOLEM_THM = prove
 412  (`!P. (!x:A. ?y:B. P x y) <=> (?y. !x. P x (y x))`,
 413   REPEAT(STRIP_TAC ORELSE EQ_TAC) THENL
 414    [EXISTS_TAC `\x:A. @y:B. P x y` THEN GEN_TAC THEN
 415     BETA_TAC THEN CONV_TAC SELECT_CONV;
 416     EXISTS_TAC `(y:A->B) x`] THEN
 417   POP_ASSUM MATCH_ACCEPT_TAC);;
 418
 419 let SKOLEM_THM_GEN = prove
 420  (`!P s. (!x. P x ==> ?y. R x y) <=> (?f. !x. P x ==> R x (f x))`,
 421   REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM]);;
 422
 423 (* ------------------------------------------------------------------------- *)
 424 (* NB: this one is true intutionistically and intensionally.                 *)
 425 (* ------------------------------------------------------------------------- *)
 426
 427 let UNIQUE_SKOLEM_ALT = prove
 428  (`!P:A->B->bool. (!x. ?!y. P x y) <=> ?f. !x y. P x y <=> (f x = y)`,
 429   GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_ALT; SKOLEM_THM]);;
 430
 431 (* ------------------------------------------------------------------------- *)
 432 (* and this one intuitionistically and extensionally.                        *)
 433 (* ------------------------------------------------------------------------- *)
 434
 435 let UNIQUE_SKOLEM_THM = prove
 436  (`!P. (!x:A. ?!y:B. P x y) <=> (?!f. !x. P x (f x))`,
 437   GEN_TAC THEN REWRITE_TAC[EXISTS_UNIQUE_THM; SKOLEM_THM; FORALL_AND_THM] THEN
 438   EQ_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
 439   ASM_REWRITE_TAC[] THENL
 440    [REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[FUN_EQ_THM] THEN
 441     X_GEN_TAC `x:A` THEN FIRST_ASSUM MATCH_MP_TAC THEN
 442     EXISTS_TAC `x:A` THEN ASM_REWRITE_TAC[];
 443     MAP_EVERY X_GEN_TAC [`x:A`; `y1:B`; `y2:B`] THEN STRIP_TAC THEN
 444     FIRST_ASSUM(X_CHOOSE_TAC `f:A->B`) THEN
 445     SUBGOAL_THEN `(\z. if z = x then y1 else (f:A->B) z) =
 446                   (\z. if z = x then y2 else (f:A->B) z)` MP_TAC THENL
 447      [FIRST_ASSUM MATCH_MP_TAC THEN
 448       REPEAT STRIP_TAC THEN BETA_TAC THEN COND_CASES_TAC THEN
 449       ASM_REWRITE_TAC[];
 450       DISCH_THEN(MP_TAC o C AP_THM `x:A`) THEN REWRITE_TAC[]]]);;
 451
 452 (* ------------------------------------------------------------------------- *)
 453 (* Extend default congruences for contextual rewriting.                      *)
 454 (* ------------------------------------------------------------------------- *)
 455
 456 let COND_CONG =
 457   TAUT `(g = g') ==>
 458         (g' ==> (t = t')) ==>
 459         (~g' ==> (e = e')) ==>
 460         ((if g then t else e) = (if g' then t' else e'))` in
 461   extend_basic_congs [COND_CONG];;
 462
 463 let COND_EQ_CLAUSE = prove
 464  (`(if x = x then y else z) = y`,
 465   REWRITE_TAC[]) in
 466  extend_basic_rewrites [COND_EQ_CLAUSE];;
 467
 468 (* ------------------------------------------------------------------------- *)
 469 (* We can now treat "bool" as an enumerated type for some purposes.          *)
 470 (* ------------------------------------------------------------------------- *)
 471
 472 let bool_INDUCT = prove
 473  (`!P. P F /\ P T ==> !x. P x`,
 474   REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SPEC `x:bool` BOOL_CASES_AX) THEN
 475   ASM_REWRITE_TAC[]);;
 476
 477 let bool_RECURSION = prove
 478  (`!a b:A. ?f. f F = a /\ f T = b`,
 479   REPEAT GEN_TAC THEN EXISTS_TAC `\x. if x then b:A else a` THEN
 480   REWRITE_TAC[]);;
 481
 482 let inductive_type_store = ref
 483  ["bool",(2,bool_INDUCT,bool_RECURSION)];;