(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Jordan                                                               *)
(* Copied from HOL Light jordan directory *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-07-08                                                           *)
(* ========================================================================== *)

(* 
The file in the HOL Light distribution is longer, with results about
Euclidan space that are not relevant here.

May 7, 2011, renamed INV -> INVERSE to avoid clash with HOL Library/rstc.ml 
*)

module Misc_defs_and_lemmas = struct

open Tactics_jordan;;
open Tactics_jordan;;
open Parse_ext_override_interface;;
(* open Refinement;; *)
open Real_ext;;
open Float;;

(* labels_flag:= true;; *)

let prove_by_refinement = Refinement.enhanced_prove_by_refinement true ALL_TAC;;

let LABEL_ALL_TAC = Refinement.LABEL_ALL_TAC;;

unambiguous_interface();;


let dirac_delta = new_definition `dirac_delta i = 
   \j. if (i=j) then &1  else &0`;;
(* let dirac_delta = new_definition `dirac_delta (i:num) j = if (i=j) then &. 1 else &. 0`;; *) (* let dirac_delta = prove_by_refinement(`!i. dirac_delta i = (\j. if (i=j) then &. 1 else &. 0)`, [ GEN_TAC; ONCE_REWRITE_TAC[FUN_EQ_THM]; REWRITE_TAC[dirac_delta_thm]; BETA_TAC; ] );; *)
let min_num = new_definition
  `min_num (X:num->bool) = @m. (m IN X) /\ (!n. (n IN X) ==> (m <= n))`;;
let min_least = 
prove_by_refinement ( `!(X:num->bool) c. (X c) ==> (X (min_num X) /\ (min_num X <=| c))`,
(* {{{ proof *) [ REWRITE_TAC[min_num;IN]; REPEAT GEN_TAC; DISCH_TAC; SUBGOAL_THEN `?n. (X:num->bool) n /\ (!m. m <| n ==> ~X m)` MP_TAC; REWRITE_TAC[(GSYM (ISPEC `X:num->bool` num_WOP))]; ASM_MESON_TAC[]; DISCH_THEN CHOOSE_TAC; ASSUME_TAC (select_thm `\m. (X:num->bool) m /\ (!n. X n ==> m <=| n)` `n:num`); ABBREV_TAC `r = @m. (X:num->bool) m /\ (!n. X n ==> m <=| n)`; ASM_MESON_TAC[ ARITH_RULE `~(n' < n) ==> (n <=| n') `] ]);;
(* }}} *)
let max_real = new_definition(`max_real x y =
        if (y <. x) then x else y`);;
let min_real = new_definition(`min_real x y =
        if (x <. y) then x else y`);;
(* let deriv = new_definition(`deriv f x = @d. (f diffl d)(x)`);; let deriv2 = new_definition(`deriv2 f = (deriv (deriv f))`);; *)
let square_le = 
prove_by_refinement( `!x y. (&.0 <=. x) /\ (&.0 <=. y) /\ (x*.x <=. y*.y) ==> (x <=. y)`,
(* {{{ proof *) [ DISCH_ALL_TAC; UNDISCH_FIND_TAC `( *. )` ; ONCE_REWRITE_TAC[REAL_ARITH `(a <=. b) <=> (&.0 <= (b - a))`]; REWRITE_TAC[GSYM REAL_DIFFSQ]; DISCH_TAC; DISJ_CASES_TAC (REAL_ARITH `&.0 < (y+x) \/ (y+x <=. (&.0))`); MATCH_MP_TAC (SPEC `(y+x):real` REAL_LE_LCANCEL_IMP); ASM_REWRITE_TAC [REAL_ARITH `x * (&.0) = (&.0)`]; CLEAN_ASSUME_TAC (REAL_ARITH `(&.0 <= y) /\ (&.0 <=. x) /\ (y+x <= (&.0)) ==> ((x= &.0) /\ (y= &.0))`); ASM_REWRITE_TAC[REAL_ARITH `&.0 <=. (&.0 -. (&.0))`]; ]);;
(* }}} *)
let max_num_sequence = 
prove_by_refinement( `!(t:num->num). (?n. !m. (n <=| m) ==> (t m = 0)) ==> (?M. !i. (t i <=| M))`,
(* {{{ proof *) [ GEN_TAC; REWRITE_TAC[GSYM LEFT_FORALL_IMP_THM]; GEN_TAC; SPEC_TAC (`t:num->num`,`t:num->num`); SPEC_TAC (`n:num`,`n:num`); INDUCT_TAC; GEN_TAC; REWRITE_TAC[ARITH_RULE `0<=|m`]; DISCH_TAC; EXISTS_TAC `0`; ASM_MESON_TAC[ARITH_RULE`(a=0) ==> (a <=|0)`]; DISCH_ALL_TAC; ABBREV_TAC `b = \m. (if (m=n) then 0 else (t (m:num)) )`; FIRST_ASSUM (fun t-> ASSUME_TAC (SPEC `b:num->num` t)); SUBGOAL_MP_TAC `((b:num->num) (n) = 0) /\ (!m. ~(m=n) ==> (b m = t m))`; EXPAND_TAC "b";
CONJ_TAC; COND_CASES_TAC; REWRITE_TAC[]; ASM_MESON_TAC[]; GEN_TAC; COND_CASES_TAC; REWRITE_TAC[]; REWRITE_TAC[]; DISCH_ALL_TAC; FIRST_ASSUM (fun t-> MP_TAC(SPEC `b:num->num` t)); SUBGOAL_MP_TAC `!m. (n<=|m) ==> (b m =0)`; GEN_TAC; ASM_CASES_TAC `m = (n:num)`; ASM_REWRITE_TAC[]; SUBGOAL_MP_TAC ( `(n <=| m) /\ (~(m = n)) ==> (SUC n <=| m)`); ARITH_TAC; ASM_REWRITE_TAC[]; DISCH_ALL_TAC; ASM_MESON_TAC[]; (* good *) DISCH_THEN (fun t-> REWRITE_TAC[t]); DISCH_THEN CHOOSE_TAC; EXISTS_TAC `(M:num) + (t:num->num) n`; GEN_TAC; ASM_CASES_TAC `(i:num) = n`; ASM_REWRITE_TAC[]; ARITH_TAC; MATCH_MP_TAC (ARITH_RULE `x <=| M ==> (x <=| M+ u)`); ASM_MESON_TAC[]; ]);; (* }}} *)
let REAL_INV_LT = 
prove_by_refinement( `!x y z. (&.0 <. x) ==> ((inv(x)*y < z) <=> (y <. x*z))`,
(* {{{ proof *) [ REPEAT GEN_TAC; DISCH_TAC; REWRITE_TAC[REAL_ARITH `inv x * y = y* inv x`]; REWRITE_TAC[GSYM real_div]; ASM_SIMP_TAC[REAL_LT_LDIV_EQ]; REAL_ARITH_TAC; ]);;
(* }}} *)
let REAL_MUL_NN = 
prove_by_refinement( `!x y. (&.0 <= x*y) <=> ((&.0 <= x /\ (&.0 <=. y)) \/ ((x <= &.0) /\ (y <= &.0) ))`,
(* {{{ proof *) [ DISCH_ALL_TAC; SUBGOAL_MP_TAC `! x y. ((&.0 < x) ==> ((&.0 <= x*y) <=> ((&.0 <= x /\ (&.0 <=. y)) \/ ((x <= &.0) /\ (y <= &.0) ))))`; DISCH_ALL_TAC; ASM_SIMP_TAC[REAL_ARITH `((&.0 <. x) ==> (&.0 <=. x))`;REAL_ARITH `(&.0 <. x) ==> ~(x <=. &.0)`]; EQ_TAC; ASM_MESON_TAC[REAL_PROP_NN_LCANCEL]; ASM_MESON_TAC[REAL_LE_MUL;REAL_LT_IMP_LE]; DISCH_TAC; DISJ_CASES_TAC (REAL_ARITH `(&.0 < x) \/ (x = &.0) \/ (x < &.0)`); ASM_MESON_TAC[]; UND 1 THEN DISCH_THEN DISJ_CASES_TAC; ASM_REWRITE_TAC[]; REAL_ARITH_TAC; ASM_SIMP_TAC[REAL_ARITH `((x <. &.0) ==> ~(&.0 <=. x))`;REAL_ARITH `(x <. &.0) ==> (x <=. &.0)`]; USE 0 (SPECL [`--. (x:real)`;`--. (y:real)`]); UND 0; REDUCE_TAC; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[REAL_ARITH `((x <. &.0) ==> ~(&.0 <=. x))`;REAL_ARITH `(x <. &.0) ==> (x <=. &.0)`]; ]);;
(* }}} *)
let ABS_SQUARE = 
prove_by_refinement( `!t u. abs(t) <. u ==> t*t <. u*u`,
(* {{{ proof *) [ REP_GEN_TAC; CONV_TAC (SUBS_CONV[SPEC `t:real` (REWRITE_RULE[POW_2] (GSYM REAL_POW2_ABS))]); ASSUME_TAC REAL_ABS_POS; USE 0 (SPEC `t:real`); ABBREV_TAC `(b:real) = (abs t)`; KILL 1; DISCH_ALL_TAC; MATCH_MP_TAC REAL_PROP_LT_LRMUL; ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let ABS_SQUARE_LE = 
prove_by_refinement( `!t u. abs(t) <=. u ==> t*t <=. u*u`,
(* {{{ proof *) [ REP_GEN_TAC; CONV_TAC (SUBS_CONV[SPEC `t:real` (REWRITE_RULE[POW_2] (GSYM REAL_POW2_ABS))]); ASSUME_TAC REAL_ABS_POS; USE 0 (SPEC `t:real`); ABBREV_TAC `(b:real) = (abs t)`; KILL 1; DISCH_ALL_TAC; MATCH_MP_TAC REAL_PROP_LE_LRMUL; ASM_REWRITE_TAC[]; ]);;
(* }}} *) let POW_2_LE1 = REAL_LE_POW2;; let REAL_ADD = REAL_OF_NUM_ADD;;
let POW_2_LT = 
prove_by_refinement( `!n. &n < &2 pow n`,
[ INDUCT_TAC; REWRITE_TAC[pow; REAL_LT_01] ; REWRITE_TAC[pow;ADD1; GSYM REAL_ADD; GSYM REAL_DOUBLE]; MATCH_MP_TAC REAL_LTE_ADD2; ASM_REWRITE_TAC[POW_2_LE1]; ]);;
let twopow_eps = 
prove_by_refinement( `!R e. ?n. (&.0 <. R)/\ (&.0 <. e) ==> R*(twopow(--: (&:n))) <. e`,
(* {{{ proof *) [ DISCH_ALL_TAC; REWRITE_TAC[TWOPOW_NEG]; (* cs6b *) ASSUME_TAC (prove(`!n. &.0 < &.2 pow n`,REDUCE_TAC THEN ARITH_TAC)); ONCE_REWRITE_TAC[REAL_MUL_AC]; ASM_SIMP_TAC[REAL_INV_LT]; ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ]; CONV_TAC (quant_right_CONV "n"); DISCH_ALL_TAC; ASSUME_TAC (SPEC `R/e` REAL_ARCH_SIMPLE); CHO 3; EXISTS_TAC `n:num`; UND 3; MESON_TAC[POW_2_LT;REAL_LET_TRANS]; ]);;
(* }}} *) (* ------------------------------------------------------------------ *) (* finite products, in imitation of finite sums *) (* ------------------------------------------------------------------ *)
let prod_EXISTS = 
prove_by_refinement( `?prod. (!f n. prod(n,0) f = &1) /\ (!f m n. prod(n,SUC m) f = prod(n,m) f * f(n + m))`,
(* {{{ proof *) [ (CHOOSE_TAC o prove_recursive_functions_exist num_RECURSION) `(!f n. sm n 0 f = &1) /\ (!f m n. sm n (SUC m) f = sm n m f * f(n + m))` ; EXISTS_TAC `\(n,m) f. (sm:num->num->(num->real)->real) n m f`; CONV_TAC(DEPTH_CONV GEN_BETA_CONV) THEN ASM_REWRITE_TAC[] ]);;
(* }}} *)
let prod_DEF = new_specification ["prod"] prod_EXISTS;;
let prod = 
prove (`!n m. (prod(n,0) f = &1) /\ (prod(n,SUC m) f = prod(n,m) f * f(n + m))`,
(* {{{ proof *) REWRITE_TAC[prod_DEF]);;
(* }}} *)
let PROD_TWO = 
prove_by_refinement( `!f n p. prod(0,n) f * prod(n,p) f = prod(0,n + p) f`,
(* {{{ proof *) [ GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod; REAL_MUL_RID; MULT_CLAUSES;ADD_0]; REWRITE_TAC[ARITH_RULE `n+| (SUC p) = (SUC (n+|p))`;prod;ARITH_RULE `0+|n = n`]; ASM_REWRITE_TAC[REAL_MUL_ASSOC]; ]);;
(* }}} *)
let ABS_PROD = 
prove_by_refinement( `!f m n. abs(prod(m,n) f) = prod(m,n) (\n. abs(f n))`,
(* {{{ proof *) [ GEN_TAC THEN GEN_TAC THEN INDUCT_TAC; REWRITE_TAC[prod]; REAL_ARITH_TAC; ASM_REWRITE_TAC[prod;ABS_MUL] ]);;
(* }}} *)
let PROD_EQ = 
prove_by_refinement (`!f g m n. (!r. m <= r /\ r < (n + m) ==> (f(r) = g(r))) ==> (prod(m,n) f = prod(m,n) g)`,
(* {{{ proof *) [ GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod]; REWRITE_TAC[prod]; DISCH_THEN (fun th -> MP_TAC th THEN (MP_TAC (SPEC `m+|n` th))); REWRITE_TAC[ARITH_RULE `(m<=| (m+|n))/\ (m +| n <| (SUC n +| m))`]; DISCH_ALL_TAC; ASM_REWRITE_TAC[]; AP_THM_TAC THEN AP_TERM_TAC; FIRST_X_ASSUM MATCH_MP_TAC; GEN_TAC THEN DISCH_TAC; FIRST_X_ASSUM MATCH_MP_TAC; ASM_MESON_TAC[ARITH_RULE `r <| (n+| m) ==> (r <| (SUC n +| m))`] ]);;
(* }}} *)
let PROD_POS = 
prove_by_refinement (`!f. (!n. &0 <= f(n)) ==> !m n. &0 <= prod(m,n) f`,
(* {{{ proof *) [ GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[prod]; REAL_ARITH_TAC; ASM_MESON_TAC[REAL_LE_MUL] ]);;
(* }}} *)
let PROD_POS_GEN = 
prove_by_refinement (`!f m n. (!n. m <= n ==> &0 <= f(n)) ==> &0 <= prod(m,n) f`,
(* {{{ proof *) [ REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN REWRITE_TAC[prod]; REAL_ARITH_TAC; ASM_MESON_TAC[REAL_LE_MUL;ARITH_RULE `m <=| (m +| n)`] ]);;
(* }}} *)
let PROD_ABS = 
prove (`!f m n. abs(prod(m,n) (\m. abs(f m))) = prod(m,n) (\m. abs(f m))`,
(* {{{ proof *) REWRITE_TAC[ABS_PROD;REAL_ARITH `||. (||. x) = (||. x)`]);;
(* }}} *)
let PROD_ZERO = 
prove_by_refinement (`!f m n. (?p. (m <= p /\ (p < (n+| m)) /\ (f p = (&.0)))) ==> (prod(m,n) f = &0)`,
(* {{{ proof *) [ GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN (REWRITE_TAC[prod]); ARITH_TAC; DISCH_THEN CHOOSE_TAC; ASM_CASES_TAC `p <| (n+| m)`; MATCH_MP_TAC (prove (`(x = (&.0)) ==> (x *. y = (&.0))`,(DISCH_THEN (fun th -> (REWRITE_TAC[th]))) THEN REAL_ARITH_TAC)); FIRST_X_ASSUM MATCH_MP_TAC; ASM_MESON_TAC[]; POP_ASSUM (fun th -> ASSUME_TAC (MATCH_MP (ARITH_RULE `(~(p <| (n+|m)) ==> ((p <| ((SUC n) +| m)) ==> (p = ((m +| n)))))`) th)); MATCH_MP_TAC (prove (`(x = (&.0)) ==> (y *. x = (&.0))`,(DISCH_THEN (fun th -> (REWRITE_TAC[th]))) THEN REAL_ARITH_TAC)); ASM_MESON_TAC[] ]);;
(* }}} *)
let PROD_MUL = 
prove_by_refinement( `!f g m n. prod(m,n) (\n. f(n) * g(n)) = prod(m,n) f * prod(m,n) g`,
(* {{{ proof *) [ EVERY(replicate GEN_TAC 3) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[prod]; REAL_ARITH_TAC; REWRITE_TAC[REAL_MUL_AC]; ]);;
(* }}} *)
let PROD_CMUL = 
prove_by_refinement( `!f c m n. prod(m,n) (\n. c * f(n)) = (c **. n) * prod(m,n) f`,
(* {{{ proof *) [ EVERY(replicate GEN_TAC 3) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[prod;pow]; REAL_ARITH_TAC; REWRITE_TAC[REAL_MUL_AC]; ]);;
(* }}} *) (* ------------------------------------------------------------------ *) (* LEMMAS ABOUT SETS *) (* ------------------------------------------------------------------ *) (* IN_ELIM_THM produces garbled results at times. I like this better: *) (*** JRH replaced this with the "new" IN_ELIM_THM; see how it works. let IN_ELIM_THM' = prove_by_refinement( `(!P. !x:A. x IN (GSPEC P) <=> P x) /\ (!P. !x:A. x IN (\x. P x) <=> P x) /\ (!P. !x:A. (GSPEC P) x <=> P x) /\ (!P (x:A) (t:A). (\t. (?y:A. P y /\ (t = y))) x <=> P x)`, (* {{{ proof *) [ REWRITE_TAC[IN; GSPEC]; MESON_TAC[]; ]);; (* }}} *) ****) let IN_ELIM_THM' = IN_ELIM_THM;;
let SURJ_IMAGE = 
prove_by_refinement( `!(f:A->B) a b. SURJ f a b ==> (b = (IMAGE f a))`,
(* {{{ proof *) [ REPEAT GEN_TAC; REWRITE_TAC[SURJ;IMAGE]; DISCH_ALL_TAC; REWRITE_TAC[EXTENSION]; GEN_TAC; REWRITE_TAC[IN_ELIM_THM]; ASM_MESON_TAC[]] (* }}} *) );;
let SURJ_FINITE = 
prove_by_refinement( `!a b (f:A->B). FINITE a /\ (SURJ f a b) ==> FINITE b`,
(* {{{ *) [ ASM_MESON_TAC[SURJ_IMAGE;FINITE_IMAGE] ]);;
(* }}} *)
let BIJ_INVERSE = 
prove_by_refinement( `!a b (f:A->B). (SURJ f a b) ==> (?(g:B->A). (INJ g b a))`,
(* {{{ proof *) [ REPEAT GEN_TAC; DISCH_ALL_TAC; SUBGOAL_THEN `!y. ?u. ((y IN b) ==> ((u IN a) /\ ((f:A->B) u = y)))` ASSUME_TAC; ASM_MESON_TAC[SURJ]; LABEL_ALL_TAC; H_REWRITE_RULE[THM SKOLEM_THM] (HYP "1"); LABEL_ALL_TAC; H_UNDISCH_TAC (HYP"2"); DISCH_THEN CHOOSE_TAC; EXISTS_TAC `u:B->A`; REWRITE_TAC[INJ] THEN CONJ_TAC THEN (ASM_MESON_TAC[]) ] (* }}} *) );;
(* complement of an intersection is a union of complements *)
let UNIONS_INTERS = 
prove_by_refinement( `!(X:A->bool) V. (X DIFF (INTERS V) = UNIONS (IMAGE ((DIFF) X) V))`,
(* {{{ proof *) [ REPEAT GEN_TAC; MATCH_MP_TAC SUBSET_ANTISYM; CONJ_TAC; REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM]; X_GEN_TAC `c:A`; REWRITE_TAC[IN_DIFF;IN_INTERS;IN_UNIONS;NOT_FORALL_THM]; DISCH_ALL_TAC; UNDISCH_FIND_THEN `(?)` CHOOSE_TAC; EXISTS_TAC `(X DIFF t):A->bool`; REWRITE_TAC[IN_ELIM_THM]; CONJ_TAC; EXISTS_TAC `t:A->bool`; ASM_MESON_TAC[]; REWRITE_TAC[IN_DIFF]; ASM_MESON_TAC[]; REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM]; X_GEN_TAC `c:A`; REWRITE_TAC[IN_DIFF;IN_UNIONS]; DISCH_THEN CHOOSE_TAC; UNDISCH_FIND_TAC `(IN)`; REWRITE_TAC[IN_INTERS;IN_ELIM_THM]; DISCH_ALL_TAC; UNDISCH_FIND_THEN `(?)` CHOOSE_TAC; CONJ_TAC; ASM_MESON_TAC[SUBSET_DIFF;SUBSET]; REWRITE_TAC[NOT_FORALL_THM]; EXISTS_TAC `x:A->bool`; ASM_MESON_TAC[IN_DIFF]; ]);;
(* }}} *)
let INTERS_SUBSET = 
prove_by_refinement ( `!X (A:A->bool). (A IN X) ==> (INTERS X SUBSET A)`,
(* {{{ *) [ REPEAT GEN_TAC; REWRITE_TAC[SUBSET;IN_INTERS]; MESON_TAC[IN]; ]);;
(* }}} *)
let sub_union = 
prove_by_refinement( `!X (U:(A->bool)->bool). (U X) ==> (X SUBSET (UNIONS U))`,
(* {{{ *) [ DISCH_ALL_TAC; REWRITE_TAC[SUBSET;IN_ELIM_THM;UNIONS]; REWRITE_TAC[IN]; DISCH_ALL_TAC; EXISTS_TAC `X:A->bool`; ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let IMAGE_SURJ = 
prove_by_refinement( `!(f:A->B) a. SURJ f a (IMAGE f a)`,
(* {{{ *) [ REWRITE_TAC[SURJ;IMAGE;IN_ELIM_THM]; MESON_TAC[IN]; ]);;
(* }}} *)
let SUBSET_PREIMAGE = 
prove_by_refinement( `!(f:A->B) X Y. (Y SUBSET (IMAGE f X)) ==> (?Z. (Z SUBSET X) /\ (Y = IMAGE f Z))`,
(* {{{ proof *) [ DISCH_ALL_TAC; EXISTS_TAC `{x | (x IN (X:A->bool))/\ (f x IN (Y:B->bool)) }`; CONJ_TAC; REWRITE_TAC[SUBSET;IN_ELIM_THM]; MESON_TAC[]; REWRITE_TAC[EXTENSION]; X_GEN_TAC `y:B`; UNDISCH_FIND_TAC `(SUBSET)`; REWRITE_TAC[SUBSET;IN_IMAGE]; REWRITE_TAC[IN_ELIM_THM]; DISCH_THEN (fun t-> MP_TAC (SPEC `y:B` t)); MESON_TAC[]; ]);;
(* }}} *)
let UNIONS_INTER = 
prove_by_refinement( `!(U:(A->bool)->bool) A. (((UNIONS U) INTER A) = (UNIONS (IMAGE ((INTER) A) U)))`,
(* {{{ proof *) [ REPEAT GEN_TAC; MATCH_MP_TAC (prove(`((C SUBSET (B:A->bool)) /\ (C SUBSET A) /\ ((A INTER B) SUBSET C)) ==> ((B INTER A) = C)`,SET_TAC[])); CONJ_TAC; REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM]; REWRITE_TAC[IN_IMAGE]; SET_TAC[]; REWRITE_TAC[SUBSET;UNIONS;IN_IMAGE]; CONJ_TAC; REWRITE_TAC[IN_ELIM_THM]; X_GEN_TAC `y:A`; DISCH_THEN CHOOSE_TAC; ASM_MESON_TAC[IN_INTER]; REWRITE_TAC[IN_INTER]; REWRITE_TAC[IN_ELIM_THM]; X_GEN_TAC `y:A`; DISCH_ALL_TAC; UNDISCH_FIND_THEN `(?)` CHOOSE_TAC; EXISTS_TAC `A INTER (u:A->bool)`; ASM SET_TAC[]; ]);;
(* }}} *)
let UNIONS_SUBSET = 
prove_by_refinement( `!U (X:A->bool). (!A. (A IN U) ==> (A SUBSET X)) ==> (UNIONS U SUBSET X)`,
(* {{{ *) [ REPEAT GEN_TAC; SET_TAC[]; ]);;
(* }}} *)
let SUBSET_INTER = 
prove_by_refinement( `!X A (B:A->bool). (X SUBSET (A INTER B)) <=> (X SUBSET A) /\ (X SUBSET B)`,
(* {{{ *) [ REWRITE_TAC[SUBSET;INTER;IN_ELIM_THM]; MESON_TAC[IN]; ]);;
(* }}} *)
let EMPTY_EXISTS = 
prove_by_refinement( `!X. ~(X = {}) <=> (? (u:A). (u IN X))`,
(* {{{ *) [ REWRITE_TAC[EXTENSION]; REWRITE_TAC[IN;EMPTY]; MESON_TAC[]; ]);;
(* }}} *)
let UNIONS_UNIONS = 
prove_by_refinement( `!A B. (A SUBSET B) ==>(UNIONS (A:(A->bool)->bool) SUBSET (UNIONS B))`,
(* {{{ *) [ REWRITE_TAC[SUBSET;UNIONS;IN_ELIM_THM]; MESON_TAC[IN]; ]);;
(* }}} *) (* nested union can flatten from outside in, or inside out *)
let UNIONS_IMAGE_UNIONS = 
prove_by_refinement( `!(X:((A->bool)->bool)->bool). UNIONS (UNIONS X) = (UNIONS (IMAGE UNIONS X))`,
(* {{{ proof *) [ GEN_TAC; REWRITE_TAC[EXTENSION;IN_UNIONS]; GEN_TAC; REWRITE_TAC[EXTENSION;IN_UNIONS]; EQ_TAC; DISCH_THEN (CHOOSE_THEN MP_TAC); DISCH_ALL_TAC; FIRST_ASSUM MP_TAC; DISCH_THEN CHOOSE_TAC; EXISTS_TAC `UNIONS (t':(A->bool)->bool)`; REWRITE_TAC[IN_UNIONS;IN_IMAGE]; CONJ_TAC; EXISTS_TAC `(t':(A->bool)->bool)`; ASM_REWRITE_TAC[]; ASM_MESON_TAC[]; DISCH_THEN CHOOSE_TAC; FIRST_ASSUM MP_TAC; REWRITE_TAC[IN_IMAGE]; DISCH_ALL_TAC; FIRST_ASSUM MP_TAC; DISCH_THEN CHOOSE_TAC; UNDISCH_TAC `(x:A) IN t`; FIRST_ASSUM (fun t-> REWRITE_TAC[t]); REWRITE_TAC[IN_UNIONS]; DISCH_THEN (CHOOSE_TAC); EXISTS_TAC `t':(A->bool)`; CONJ_TAC; EXISTS_TAC `x':(A->bool)->bool`; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let INTERS_SUBSET2 = 
prove_by_refinement( `!X A. (?(x:A->bool). (A x /\ (x SUBSET X))) ==> ((INTERS A) SUBSET X)`,
(* {{{ proof *) [ REWRITE_TAC[SUBSET;INTERS;IN_ELIM_THM']; REWRITE_TAC[IN]; MESON_TAC[]; ]);;
(* }}} *) (**** New proof by JRH; old one breaks because of new set comprehensions let INTERS_EMPTY = prove_by_refinement( `INTERS EMPTY = (UNIV:A->bool)`, (* {{{ proof *) [ REWRITE_TAC[INTERS;NOT_IN_EMPTY;IN_ELIM_THM';]; REWRITE_TAC[UNIV;GSPEC]; MATCH_MP_TAC EQ_EXT; GEN_TAC; REWRITE_TAC[IN_ELIM_THM']; MESON_TAC[]; ]);; (* }}} *) ****)
let INTERS_EMPTY = 
prove_by_refinement( `INTERS EMPTY = (UNIV:A->bool)`,
[SET_TAC[]]);;
let preimage = new_definition `preimage dom (f:A->B)
  Z = {x | (x IN dom) /\ (f x IN Z)}`;;
let in_preimage = 
prove_by_refinement( `!f x Z dom. x IN (preimage dom (f:A->B) Z) <=> (x IN dom) /\ (f x IN Z)`,
(* {{{ *) [ REWRITE_TAC[preimage]; REWRITE_TAC[IN_ELIM_THM'] ]);;
(* }}} *) (* Partial functions, which we identify with functions that take the canonical choice of element outside the domain. *)
let supp = new_definition
  `supp (f:A->B) = \ x.  ~(f x = (CHOICE (UNIV:B ->bool)) )`;;
let func = new_definition
  `func a b = (\ (f:A->B). ((!x. (x IN a) ==> (f x IN b)) /\
              ((supp f) SUBSET a))) `;;
(* relations *)
let reflexive = new_definition
  `reflexive (f:A->A->bool) <=> (!x. f x x)`;;
let symmetric = new_definition
  `symmetric (f:A->A->bool) <=> (!x y. f x y ==> f y x)`;;
let transitive = new_definition
  `transitive (f:A->A->bool) <=> (!x y z. f x y /\ f y z ==> f x z)`;;
let equivalence_relation = new_definition
  `equivalence_relation (f:A->A->bool) <=>
    (reflexive f) /\ (symmetric f) /\ (transitive f)`;;
(* We do not introduce the equivalence class of f explicitly, because it is represented directly in HOL by (f a) *)
let partition_DEF = new_definition
  `partition (A:A->bool) SA <=> (UNIONS SA = A) /\
   (!a b. ((a IN SA) /\ (b IN SA) /\ (~(a = b)) ==> ({} = (a INTER b))))`;;
let DIFF_DIFF2 = 
prove_by_refinement( `!X (A:A->bool). (A SUBSET X) ==> ((X DIFF (X DIFF A)) = A)`,
[ SET_TAC[] ]);;
(*** Old proof replaced by JRH: no longer UNWIND_THM[12] clause in IN_ELIM_THM let GSPEC_THM = prove_by_refinement( `!P (x:A). (?y. P y /\ (x = y)) <=> P x`, [REWRITE_TAC[IN_ELIM_THM]]);; ***)
let GSPEC_THM = 
prove_by_refinement( `!P (x:A). (?y. P y /\ (x = y)) <=> P x`,
[MESON_TAC[]]);;
let CARD_GE_REFL = 
prove (`!s:A->bool. s >=_c s`,
GEN_TAC THEN REWRITE_TAC[GE_C] THEN EXISTS_TAC `\x:A. x` THEN MESON_TAC[]);;
let FINITE_HAS_SIZE_LEMMA = 
prove (`!s:A->bool. FINITE s ==> ?n:num. {x | x < n} >=_c s`,
MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL [EXISTS_TAC `0` THEN REWRITE_TAC[NOT_IN_EMPTY; GE_C; IN_ELIM_THM]; REPEAT GEN_TAC THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `SUC N` THEN POP_ASSUM MP_TAC THEN PURE_REWRITE_TAC[GE_C] THEN DISCH_THEN(X_CHOOSE_TAC `f:num->A`) THEN EXISTS_TAC `\n:num. if n = N then x:A else f n` THEN X_GEN_TAC `y:A` THEN PURE_REWRITE_TAC[IN_INSERT] THEN DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC (ANTE_RES_THEN MP_TAC)) THENL [EXISTS_TAC `N:num` THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN ARITH_TAC; DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN REWRITE_TAC[IN_ELIM_THM] THEN STRIP_TAC THEN EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `n:num < N` THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[LT_REFL] THEN ARITH_TAC]]);;
let NUM_COUNTABLE = 
prove_by_refinement( `COUNTABLE (UNIV:num->bool)`,
(* {{{ proof *) [ REWRITE_TAC[COUNTABLE;CARD_GE_REFL]; ]);;
(* }}} *)
let NUM2_COUNTABLE = 
prove_by_refinement( `COUNTABLE {((x:num),(y:num)) | T}`,
(* {{{ proof *) [ CHOOSE_TAC (ISPECL[`(0,0)`;`(\ (a:num,b:num) (n:num) . if (b=0) then (0,a+b+1) else (a+1,b-1))`] num_RECURSION); REWRITE_TAC[COUNTABLE;GE_C;IN_ELIM_THM']; NAME_CONFLICT_TAC; EXISTS_TAC `fn:num -> (num#num)`; X_GEN_TAC `p:num#num`; REPEAT (DISCH_THEN (CHOOSE_THEN MP_TAC)); DISCH_THEN (fun t->REWRITE_TAC[t]); REWRITE_TAC[IN_UNIV]; SUBGOAL_MP_TAC `?t. t = x'+|y'`; MESON_TAC[]; SPEC_TAC (`x':num`,`a:num`); SPEC_TAC (`y':num`,`b:num`); CONV_TAC (quant_left_CONV "t"); CONV_TAC (quant_left_CONV "t"); CONV_TAC (quant_left_CONV "t"); INDUCT_TAC; REDUCE_TAC; REP_GEN_TAC; DISCH_THEN (fun t -> REWRITE_TAC[t]); EXISTS_TAC `0`; ASM_REWRITE_TAC[]; CONV_TAC (quant_left_CONV "a"); INDUCT_TAC; REDUCE_TAC; GEN_TAC; USE 1 (SPECL [`0`;`t:num`]); UND 1 THEN REDUCE_TAC; DISCH_THEN (X_CHOOSE_TAC `n:num`); AND 0; USE 0 (SPEC `n:num`); UND 0; UND 1; DISCH_THEN (fun t-> REWRITE_TAC[GSYM t]); CONV_TAC (ONCE_DEPTH_CONV GEN_BETA_CONV); BETA_TAC; REDUCE_TAC; DISCH_ALL_TAC; EXISTS_TAC `SUC n`; EXPAND_TAC "b";
KILL 0; ASM_REWRITE_TAC[]; REWRITE_TAC [ARITH_RULE `SUC t = t+|1`]; GEN_TAC; ABBREV_TAC `t' = SUC t`; USE 2 (SPEC `SUC b`); DISCH_TAC; UND 2; ASM_REWRITE_TAC[]; REWRITE_TAC[ARITH_RULE `SUC a +| b = a +| SUC b`]; DISCH_THEN (X_CHOOSE_TAC `n:num`); EXISTS_TAC `SUC n`; AND 0; USE 0 (SPEC `n:num`); UND 0; UND 2; DISCH_THEN (fun t->REWRITE_TAC[GSYM t]); CONV_TAC (ONCE_DEPTH_CONV GEN_BETA_CONV); BETA_TAC; REDUCE_TAC; DISCH_THEN (fun t->REWRITE_TAC[t]); REWRITE_TAC[ARITH_RULE `SUC a = a+| 1`]; ]);; (* }}} *)
let COUNTABLE_UNIONS = 
prove_by_refinement( `!A:(A->bool)->bool. (COUNTABLE A) /\ (!a. (a IN A) ==> (COUNTABLE a)) ==> (COUNTABLE (UNIONS A))`,
(* {{{ proof *) [ GEN_TAC; DISCH_ALL_TAC; USE 0 (REWRITE_RULE[COUNTABLE;GE_C;IN_UNIV]); CHO 0; USE 0 (CONV_RULE (quant_left_CONV "x")); USE 0 (CONV_RULE (quant_left_CONV "x")); CHO 0; USE 1 (REWRITE_RULE[COUNTABLE;GE_C;IN_UNIV]); USE 1 (CONV_RULE (quant_left_CONV "f")); USE 1 (CONV_RULE (quant_left_CONV "f")); UND 1; DISCH_THEN (X_CHOOSE_TAC `g:(A->bool)->num->A`); SUBGOAL_MP_TAC `!a y. (a IN (A:(A->bool)->bool)) /\ (y IN a) ==> (? (u:num) (v:num). ( a = f u) /\ (y = g a v))`; REP_GEN_TAC; DISCH_ALL_TAC; USE 1 (SPEC `a:A->bool`); USE 0 (SPEC `a:A->bool`); EXISTS_TAC `(x:(A->bool)->num) a`; ASM_SIMP_TAC[]; ASSUME_TAC NUM2_COUNTABLE; USE 2 (REWRITE_RULE[COUNTABLE;GE_C;IN_ELIM_THM';
IN_UNIV]); USE 2 (CONV_RULE NAME_CONFLICT_CONV); UND 2 THEN (DISCH_THEN (X_CHOOSE_TAC `h:num->(num#num)`)); DISCH_TAC; REWRITE_TAC[COUNTABLE;GE_C;IN_ELIM_THM';IN_UNIV;IN_UNIONS]; EXISTS_TAC `(\p. (g:(A->bool)->num->A) ((f:num->(A->bool)) (FST ((h:num->(num#num)) p))) (SND (h p)))`; BETA_TAC; GEN_TAC; DISCH_THEN (CHOOSE_THEN MP_TAC); DISCH_ALL_TAC; USE 3 (SPEC `t:A->bool`); USE 3 (SPEC `y:A`); UND 3 THEN (ASM_REWRITE_TAC[]); REPEAT (DISCH_THEN(CHOOSE_THEN (MP_TAC))); DISCH_ALL_TAC; USE 2 (SPEC `(u:num,v:num)`); SUBGOAL_MP_TAC `?x' y'. (u:num,v:num) = (x',y')`; MESON_TAC[]; DISCH_TAC; UND 2; ASM_REWRITE_TAC[]; DISCH_THEN (CHOOSE_THEN (ASSUME_TAC o GSYM)); EXISTS_TAC `x':num`; ASM_REWRITE_TAC[]; ]);; (* }}} *)
let COUNTABLE_IMAGE = 
prove_by_refinement( `!(A:A->bool) (B:B->bool) . (COUNTABLE A) /\ (?f. (B SUBSET IMAGE f A)) ==> (COUNTABLE B)`,
(* {{{ proof *) [ REWRITE_TAC[COUNTABLE;GE_C;IN_UNIV;IN_ELIM_THM';
SUBSET]; DISCH_ALL_TAC; CHO 0; USE 1 (REWRITE_RULE[IMAGE;IN_ELIM_THM']); CHO 1; USE 1 (REWRITE_RULE[IN_ELIM_THM']); USE 1 (CONV_RULE NAME_CONFLICT_CONV); EXISTS_TAC `(f':A->B) o (f:num->A)`; REWRITE_TAC[o_DEF]; DISCH_ALL_TAC; USE 1 (SPEC `y:B`); UND 1; ASM_REWRITE_TAC[]; DISCH_THEN CHOOSE_TAC; USE 0 (SPEC `x':A`); UND 0 THEN (ASM_REWRITE_TAC[]) THEN DISCH_TAC; ASM_MESON_TAC[]; ]);; (* }}} *)
let COUNTABLE_CARD = 
prove_by_refinement( `!(A:A->bool) (B:B->bool). (COUNTABLE A) /\ (A >=_c B) ==> (COUNTABLE B)`,
(* {{{ proof *) [ DISCH_ALL_TAC; MATCH_MP_TAC COUNTABLE_IMAGE; EXISTS_TAC `A:A->bool`; ASM_REWRITE_TAC[]; REWRITE_TAC[IMAGE;SUBSET;IN_ELIM_THM']; USE 1 (REWRITE_RULE[GE_C]); CHO 1; EXISTS_TAC `f:A->B`; ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let COUNTABLE_NUMSEG = 
prove_by_refinement( `!n. COUNTABLE {x | x <| n}`,
(* {{{ proof *) [ GEN_TAC; REWRITE_TAC[COUNTABLE;GE_C;IN_UNIV]; EXISTS_TAC `I:num->num`; REDUCE_TAC; REWRITE_TAC[IN_ELIM_THM']; MESON_TAC[]; ]);;
(* }}} *)
let FINITE_COUNTABLE = 
prove_by_refinement( `!(A:A->bool). (FINITE A) ==> (COUNTABLE A)`,
(* {{{ proof *) [ DISCH_ALL_TAC; USE 0 (MATCH_MP FINITE_HAS_SIZE_LEMMA); CHO 0; ASSUME_TAC(SPEC `n:num` COUNTABLE_NUMSEG); JOIN 1 0; USE 0 (MATCH_MP COUNTABLE_CARD); ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let num_infinite = 
prove_by_refinement( `~ (FINITE (UNIV:num->bool))`,
(* {{{ proof *) [ PROOF_BY_CONTR_TAC; USE 0 (REWRITE_RULE[]); USE 0 (MATCH_MP num_FINITE_AVOID); USE 0 (REWRITE_RULE[IN_UNIV]); ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let num_SEG_UNION = 
prove_by_refinement( `!i. ({u | i <| u} UNION {m | m <=| i}) = UNIV`,
(* {{{ proof *) [ REP_BASIC_TAC; SUBGOAL_MP_TAC `({u | i <| u} UNION {m | m <=| i}) = UNIV`; MATCH_MP_TAC EQ_EXT; GEN_TAC; REWRITE_TAC[UNIV;UNION;IN_ELIM_THM']; ARITH_TAC; REWRITE_TAC[]; ]);;
(* }}} *)
let num_above_infinite = 
prove_by_refinement( `!i. ~ (FINITE {u | i <| u})`,
(* {{{ proof *) [ GEN_TAC; PROOF_BY_CONTR_TAC; USE 0 (REWRITE_RULE[]); ASSUME_TAC(SPEC `i:num` FINITE_NUMSEG_LE); JOIN 0 1; USE 0 (MATCH_MP FINITE_UNION_IMP); SUBGOAL_MP_TAC `({u | i <| u} UNION {m | m <=| i}) = UNIV`; REWRITE_TAC[num_SEG_UNION]; DISCH_TAC; UND 0; ASM_REWRITE_TAC[]; REWRITE_TAC[num_infinite]; ]);;
(* }}} *)
let INTER_FINITE = 
prove_by_refinement( `!s (t:A->bool). (FINITE s ==> FINITE(s INTER t)) /\ (FINITE t ==> FINITE (s INTER t))`,
(* {{{ proof *) [ CONV_TAC (quant_right_CONV "t"); CONV_TAC (quant_right_CONV "s"); SUBCONJ_TAC; DISCH_ALL_TAC; SUBGOAL_MP_TAC `s INTER t SUBSET (s:A->bool)`; SET_TAC[]; ASM_MESON_TAC[FINITE_SUBSET]; MESON_TAC[INTER_COMM]; ]);;
(* }}} *)
let num_above_finite = 
prove_by_refinement( `!i J. (FINITE (J INTER {u | (i <| u)})) ==> (FINITE J)`,
(* {{{ proof *) [ DISCH_ALL_TAC; SUBGOAL_MP_TAC `J = (J INTER {u | (i <| u)}) UNION (J INTER {m | m <=| i})`; REWRITE_TAC[GSYM UNION_OVER_INTER;num_SEG_UNION;INTER_UNIV]; DISCH_TAC; ASM (ONCE_REWRITE_TAC)[]; REWRITE_TAC[FINITE_UNION]; ASM_REWRITE_TAC[]; MP_TAC (SPEC `i:num` FINITE_NUMSEG_LE); REWRITE_TAC[INTER_FINITE]; ]);;
(* }}} *)
let SUBSET_SUC = 
prove_by_refinement( `!(f:num->A->bool). (!i. f i SUBSET f (SUC i)) ==> (! i j. ( i <=| j) ==> (f i SUBSET f j))`,
(* {{{ proof *) [ GEN_TAC; DISCH_TAC; REP_GEN_TAC; MP_TAC (prove( `?n. n = j -| i`,MESON_TAC[])); CONV_TAC (quant_left_CONV "n"); SPEC_TAC (`i:num`,`i:num`); SPEC_TAC (`j:num`,`j:num`); REP 2( CONV_TAC (quant_left_CONV "n")); INDUCT_TAC; REP_GEN_TAC; DISCH_ALL_TAC; JOIN 1 2; USE 1 (CONV_RULE REDUCE_CONV); ASM_REWRITE_TAC[SUBSET]; REP_GEN_TAC; DISCH_TAC; SUBGOAL_MP_TAC `?j'. j = SUC j'`; DISJ_CASES_TAC (SPEC `j:num` num_CASES); UND 2; ASM_REWRITE_TAC[]; REDUCE_TAC; ASM_REWRITE_TAC[]; DISCH_THEN CHOOSE_TAC; ASM_REWRITE_TAC[]; USE 0 (SPEC `j':num`); USE 1(SPECL [`j':num`;`i:num`]); DISCH_TAC; SUBGOAL_MP_TAC `(n = j'-|i)`; UND 2; ASM_REWRITE_TAC[]; ARITH_TAC; DISCH_TAC; SUBGOAL_MP_TAC `(i<=| j')`; USE 2 (MATCH_MP(ARITH_RULE `(SUC n = j -| i) ==> (0 < j -| i)`)); UND 2; ASM_REWRITE_TAC[]; ARITH_TAC; UND 1; ASM_REWRITE_TAC []; DISCH_ALL_TAC; REWR 6; ASM_MESON_TAC[SUBSET_TRANS]; ]);;
(* }}} *)
let SUBSET_SUC2 = 
prove_by_refinement( `!(f:num->A->bool). (!i. f (SUC i) SUBSET (f i)) ==> (! i j. ( i <=| j) ==> (f j SUBSET f i))`,
(* {{{ proof *) [ GEN_TAC; DISCH_TAC; REP_GEN_TAC; MP_TAC (prove( `?n. n = j -| i`,MESON_TAC[])); CONV_TAC (quant_left_CONV "n"); SPEC_TAC (`i:num`,`i:num`); SPEC_TAC (`j:num`,`j:num`); REP 2( CONV_TAC (quant_left_CONV "n")); INDUCT_TAC; REP_GEN_TAC; DISCH_ALL_TAC; JOIN 1 2; USE 1 (CONV_RULE REDUCE_CONV); ASM_REWRITE_TAC[SUBSET]; REP_GEN_TAC; DISCH_TAC; SUBGOAL_MP_TAC `?j'. j = SUC j'`; DISJ_CASES_TAC (SPEC `j:num` num_CASES); UND 2; ASM_REWRITE_TAC[]; REDUCE_TAC; ASM_REWRITE_TAC[]; DISCH_THEN CHOOSE_TAC; ASM_REWRITE_TAC[]; USE 0 (SPEC `j':num`); USE 1(SPECL [`j':num`;`i:num`]); DISCH_TAC; SUBGOAL_MP_TAC `(n = j'-|i)`; UND 2; ASM_REWRITE_TAC[]; ARITH_TAC; DISCH_TAC; SUBGOAL_MP_TAC `(i<=| j')`; USE 2 (MATCH_MP(ARITH_RULE `(SUC n = j -| i) ==> (0 < j -| i)`)); UND 2; ASM_REWRITE_TAC[]; ARITH_TAC; UND 1; ASM_REWRITE_TAC []; DISCH_ALL_TAC; REWR 6; ASM_MESON_TAC[SUBSET_TRANS]; ]);;
(* }}} *)
let INFINITE_PIGEONHOLE = 
prove_by_refinement( `!I (f:A->B) B C. (~(FINITE {i | (I i) /\ (C (f i))})) /\ (FINITE B) /\ (C SUBSET (UNIONS B)) ==> (?b. (B b) /\ ~(FINITE {i | (I i) /\ (C INTER b) (f i) }))`,
(* {{{ proof *) [ DISCH_ALL_TAC; PROOF_BY_CONTR_TAC; USE 3 ( CONV_RULE (quant_left_CONV "b")); UND 0; TAUT_TAC `P ==> (~P ==> F)`; SUBGOAL_MP_TAC `{i | I' i /\ (C ((f:A->B) i))} = UNIONS (IMAGE (\b. {i | I' i /\ ((C INTER b) (f i))}) B)`; REWRITE_TAC[UNIONS;IN_IMAGE]; MATCH_MP_TAC EQ_EXT; GEN_TAC; REWRITE_TAC[IN_ELIM_THM']; ABBREV_TAC `j = (x:A)`; EQ_TAC; DISCH_ALL_TAC; USE 2 (REWRITE_RULE [SUBSET;UNIONS]); USE 2 (REWRITE_RULE[IN_ELIM_THM']); USE 2 (SPEC `(f:A->B) j`); USE 2 (REWRITE_RULE[IN]); REWR 2; CHO 2; CONV_TAC (quant_left_CONV "x"); CONV_TAC (quant_left_CONV "x"); EXISTS_TAC (`u:B->bool`); NAME_CONFLICT_TAC; EXISTS_TAC (`{i' | I' i' /\ (C INTER u) ((f:A->B) i')}`); ASM_REWRITE_TAC[]; REWRITE_TAC[IN_ELIM_THM';
INTER]; REWRITE_TAC[IN]; ASM_REWRITE_TAC[]; DISCH_TAC; CHO 4; AND 4; CHO 5; REWR 4; USE 4 (REWRITE_RULE[IN_ELIM_THM';INTER]); USE 4 (REWRITE_RULE[IN]); ASM_REWRITE_TAC[]; DISCH_TAC; ASM_REWRITE_TAC[]; SUBGOAL_MP_TAC `FINITE (IMAGE (\b. {i | I' i /\ (C INTER b) ((f:A->B) i)}) B)`; MATCH_MP_TAC FINITE_IMAGE; ASM_REWRITE_TAC[]; SIMP_TAC[FINITE_UNIONS]; DISCH_TAC; GEN_TAC; REWRITE_TAC[IN_IMAGE]; DISCH_THEN (X_CHOOSE_TAC `b:B->bool`); ASM_REWRITE_TAC[]; USE 3 (SPEC `b:B->bool`); UND 3; AND 5; UND 3; ABBREV_TAC `r = {i | I' i /\ (C INTER b) ((f:A->B) i)}`; MESON_TAC[IN]; ]);; (* }}} *)
let real_FINITE = 
prove_by_refinement( `!(s:real->bool). FINITE s ==> (?a. !x. x IN s ==> (x <=. a))`,
(* {{{ proof *) [ DISCH_ALL_TAC; ASSUME_TAC REAL_ARCH_SIMPLE; USE 1 (CONV_RULE (quant_left_CONV "n")); CHO 1; SUBGOAL_MP_TAC `FINITE (IMAGE (n:real->num) s)`; ASM_MESON_TAC[FINITE_IMAGE]; (*** JRH -- num_FINITE is now an equivalence not an implication ASSUME_TAC (SPEC `IMAGE (n:real->num) s` num_FINITE); ***) ASSUME_TAC(fst(EQ_IMP_RULE(SPEC `IMAGE (n:real->num) s` num_FINITE))); DISCH_TAC; REWR 2; CHO 2; USE 2 (REWRITE_RULE[IN_IMAGE]); USE 2 (CONV_RULE NAME_CONFLICT_CONV); EXISTS_TAC `&.a`; GEN_TAC; USE 2 (CONV_RULE (quant_left_CONV "x'")); USE 2 (CONV_RULE (quant_left_CONV "x'")); USE 2 (SPEC `x:real`); USE 2 (SPEC `(n:real->num) x`); DISCH_TAC; REWR 2; USE 1 (SPEC `x:real`); UND 1; MATCH_MP_TAC (REAL_ARITH `a<=b ==> ((x <= a) ==> (x <=. b))`); REDUCE_TAC; ASM_REWRITE_TAC []; ]);;
(* }}} *)
let UNIONS_DELETE = 
prove_by_refinement( `!s. (UNIONS (s:(A->bool)->bool)) = (UNIONS (s DELETE (EMPTY)))`,
(* {{{ proof *) [ REWRITE_TAC[UNIONS;DELETE;EMPTY]; GEN_TAC; MATCH_MP_TAC EQ_EXT; REWRITE_TAC[IN_ELIM_THM']; GEN_TAC; REWRITE_TAC[IN]; MESON_TAC[]; ]);;
(* }}} *) (* ------------------------------------------------------------------ *) (* Partial functions, which we identify with functions that take the canonical choice of element outside the domain. *) (* ------------------------------------------------------------------ *)
let SUPP = new_definition
  `SUPP (f:A->B) = \ x.  ~(f x = (CHOICE (UNIV:B ->bool)) )`;;
let FUN = new_definition
  `FUN a b = (\ (f:A->B). ((!x. (x IN a) ==> (f x IN b)) /\
              ((SUPP f) SUBSET a))) `;;
(* ------------------------------------------------------------------ *) (* compositions *) (* ------------------------------------------------------------------ *)
let compose = new_definition
  `compose f g = \x. (f (g x))`;;
let COMP_ASSOC = 
prove_by_refinement( `!(f:num ->num) (g:num->num) (h:num->num). (compose f (compose g h)) = (compose (compose f g) h)`,
(* {{{ proof *) [ REPEAT GEN_TAC THEN REWRITE_TAC[compose]; ]);;
(* }}} *)
let COMP_INJ = 
prove (`!(f:A->B) (g:B->C) s t u. INJ f s t /\ (INJ g t u) ==> (INJ (compose g f) s u)`,
(* {{{ proof *) EVERY[REPEAT GEN_TAC; REWRITE_TAC[INJ;compose]; DISCH_ALL_TAC; ASM_MESON_TAC[]]);;
(* }}} *)
let COMP_SURJ = 
prove (`!(f:A->B) (g:B->C) s t u. SURJ f s t /\ (SURJ g t u) ==> (SURJ (compose g f) s u)`,
(* {{{ proof *) EVERY[REWRITE_TAC[SURJ;compose]; DISCH_ALL_TAC; ASM_MESON_TAC[]]);;
(* }}} *)
let COMP_BIJ = 
prove (`!(f:A->B) s t (g:B->C) u. BIJ f s t /\ (BIJ g t u) ==> (BIJ (compose g f) s u)`,
(* {{{ proof *) EVERY[ REPEAT GEN_TAC; REWRITE_TAC[BIJ]; DISCH_ALL_TAC; ASM_MESON_TAC[COMP_INJ;COMP_SURJ]]);;
(* }}} *) (* ------------------------------------------------------------------ *) (* general construction of an inverse function on a domain *) (* ------------------------------------------------------------------ *)
let INVERSE_FN = 
prove_by_refinement( `?INVERSE. (! (f:A->B) a b. (SURJ f a b) ==> ((INJ (INVERSE f a b) b a) /\ (!(x:B). (x IN b) ==> (f ((INVERSE f a b) x) = x))))`,
(* {{{ proof *) [ REWRITE_TAC[GSYM SKOLEM_THM]; REPEAT GEN_TAC; MATCH_MP_TAC (prove_by_refinement( `!A B. (A ==> (?x. (B x))) ==> (?(x:B->A). (A ==> (B x)))`,[MESON_TAC[]])) ; REWRITE_TAC[SURJ;INJ]; DISCH_ALL_TAC; SUBGOAL_MP_TAC `?u. !y. ((y IN b)==> ((u y IN a) /\ ((f:A->B) (u y) = y)))`; REWRITE_TAC[GSYM SKOLEM_THM]; GEN_TAC; ASM_MESON_TAC[]; DISCH_THEN CHOOSE_TAC; EXISTS_TAC `u:B->A`; REPEAT CONJ_TAC; ASM_MESON_TAC[]; REPEAT GEN_TAC; DISCH_ALL_TAC; FIRST_X_ASSUM (fun th -> ASSUME_TAC (AP_TERM `f:A->B` th)); ASM_MESON_TAC[]; ASM_MESON_TAC[] ]);;
(* }}} *)
let INVERSE_DEF = new_specification ["INVERSE"] INVERSE_FN;;
let INVERSE_BIJ = 
prove_by_refinement( `!(f:A->B) a b. (BIJ f a b) ==> ((BIJ (INVERSE f a b) b a))`,
(* {{{ proof *) [ REPEAT GEN_TAC; REWRITE_TAC[BIJ]; DISCH_ALL_TAC; ASM_SIMP_TAC[INVERSE_DEF]; REWRITE_TAC[SURJ]; CONJ_TAC; ASM_MESON_TAC[INVERSE_DEF;INJ]; GEN_TAC THEN DISCH_TAC; EXISTS_TAC `(f:A->B) x`; CONJ_TAC; ASM_MESON_TAC[INJ]; SUBGOAL_THEN `((f:A->B) x) IN b` ASSUME_TAC; ASM_MESON_TAC[INJ]; SUBGOAL_THEN `(f:A->B) (INVERSE f a b (f x)) = (f x)` ASSUME_TAC; ASM_MESON_TAC[INVERSE_DEF]; H_UNDISCH_TAC (HYP "0"); REWRITE_TAC[INJ]; DISCH_ALL_TAC; FIRST_X_ASSUM (fun th -> MP_TAC (SPECL [`INVERSE (f:A->B) a b (f x)`;`x:A`] th)); ASM_REWRITE_TAC[]; DISCH_ALL_TAC; SUBGOAL_THEN `INVERSE (f:A->B) a b (f x) IN a` ASSUME_TAC; ASM_MESON_TAC[INVERSE_DEF;INJ]; ASM_MESON_TAC[]; ]);;
(* }}} *)
let INVERSE_XY = 
prove_by_refinement( `!(f:A->B) a b x y. (BIJ f a b) /\ (x IN a) /\ (y IN b) ==> ((INVERSE f a b y = x) <=> (f x = y))`,
(* {{{ proof *) [ REPEAT GEN_TAC; DISCH_ALL_TAC; EQ_TAC; FIRST_X_ASSUM (fun th -> (ASSUME_TAC th THEN (ASSUME_TAC (MATCH_MP INVERSE_DEF (CONJUNCT2 (REWRITE_RULE[BIJ] th)))))); ASM_MESON_TAC[]; POP_ASSUM (fun th -> (ASSUME_TAC th THEN (ASSUME_TAC (CONJUNCT2 (REWRITE_RULE[INJ] (CONJUNCT1 (REWRITE_RULE[BIJ] th))))))); DISCH_THEN (fun th -> ASSUME_TAC th THEN (REWRITE_TAC[GSYM th])); FIRST_X_ASSUM MATCH_MP_TAC; REPEAT CONJ_TAC; ASM_REWRITE_TAC[]; IMP_RES_THEN ASSUME_TAC INVERSE_BIJ; ASM_MESON_TAC[BIJ;INJ]; ASM_REWRITE_TAC[]; FIRST_X_ASSUM (fun th -> (ASSUME_TAC (CONJUNCT2 (REWRITE_RULE[BIJ] th)))); IMP_RES_THEN (fun th -> ASSUME_TAC (CONJUNCT2 th)) INVERSE_DEF; ASM_MESON_TAC[]; ]);;
(* }}} *)
let FINITE_BIJ = 
prove( `!a b (f:A->B). FINITE a /\ (BIJ f a b) ==> (FINITE b)`,
(* {{{ proof *) MESON_TAC[SURJ_IMAGE;BIJ;INJ;FINITE_IMAGE] );;
(* }}} *)
let FINITE_INJ = 
prove_by_refinement( `!a b (f:A->B). FINITE b /\ (INJ f a b) ==> (FINITE a)`,
(* {{{ proof *) [ REPEAT GEN_TAC; DISCH_ALL_TAC; MP_TAC (SPECL [`f:A->B`;`b:B->bool`;`a:A->bool`] FINITE_IMAGE_INJ_GENERAL); DISCH_ALL_TAC; SUBGOAL_THEN `(a:A->bool) SUBSET ({x | (x IN a) /\ ((f:A->B) x IN b)})` ASSUME_TAC; REWRITE_TAC[SUBSET]; GEN_TAC ; REWRITE_TAC[IN_ELIM_THM]; POPL_TAC[0;1]; ASM_MESON_TAC[BIJ;INJ]; MATCH_MP_TAC FINITE_SUBSET; EXISTS_TAC `({x | (x IN a) /\ ((f:A->B) x IN b)})` ; CONJ_TAC; FIRST_X_ASSUM (fun th -> MATCH_MP_TAC th); CONJ_TAC; ASM_MESON_TAC[BIJ;INJ]; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; ] );;
(* }}} *)
let FINITE_BIJ2 = 
prove_by_refinement( `!a b (f:A->B). FINITE b /\ (BIJ f a b) ==> (FINITE a)`,
(* {{{ proof *) [ MESON_TAC[BIJ;FINITE_INJ] ]);;
(* }}} *)
let BIJ_CARD = 
prove_by_refinement( `!a b (f:A->B). FINITE a /\ (BIJ f a b) ==> (CARD a = (CARD b))`,
(* {{{ proof *) [ ASM_MESON_TAC[SURJ_IMAGE;BIJ;INJ;CARD_IMAGE_INJ]; ]);;
(* }}} *)
let PAIR_LEMMA = 
prove_by_refinement( `!(x:num#num) i j. ((FST x = i) /\ (SND x = j)) <=> (x = (i,j))` ,
(* {{{ proof *) [ MESON_TAC[FST;SND;PAIR]; ]);;
(* }}} *)
let CARD_SING = 
prove_by_refinement( `!(u:A->bool). (SING u ) ==> (CARD u = 1)`,
(* {{{ proof *) [ REWRITE_TAC[SING]; GEN_TAC; DISCH_THEN (CHOOSE_TAC); ASM_REWRITE_TAC[]; ASSUME_TAC FINITE_RULES; ASM_SIMP_TAC[CARD_CLAUSES;NOT_IN_EMPTY]; ACCEPT_TAC (NUM_RED_CONV `SUC 0`) ]);;
(* }}} *)
let FINITE_SING = 
prove_by_refinement( `!(x:A). FINITE ({x})`,
(* {{{ proof *) [ MESON_TAC[FINITE_RULES] ]);;
(* }}} *)
let NUM_INTRO = 
prove_by_refinement( `!f P.((!(n:num). !(g:A). (f g = n) ==> (P g)) ==> (!g. (P g)))`,
(* {{{ proof *) [ REPEAT GEN_TAC; DISCH_ALL_TAC; GEN_TAC; H_VAL (SPECL [`(f:A->num) (g:A)`; `g:A`]) (HYP "0"); ASM_MESON_TAC[]; ]);;
(* }}} *) (* ------------------------------------------------------------------ *) (* Lemmas about the support of a function *) (* ------------------------------------------------------------------ *) (* Law of cardinal exponents B^0 = 1 *)
let DOMAIN_EMPTY = 
prove_by_refinement( `!b. FUN (EMPTY:A->bool) b = { (\ (u:A). (CHOICE (UNIV:B->bool))) }`,
(* {{{ proof *) [ GEN_TAC; REWRITE_TAC[EXTENSION;FUN]; X_GEN_TAC `f:A->B`; REWRITE_TAC[IN_ELIM_THM;INSERT;NOT_IN_EMPTY;SUBSET_EMPTY;SUPP]; REWRITE_TAC[EMPTY]; ONCE_REWRITE_TAC[EXTENSION]; REWRITE_TAC[IN]; EQ_TAC; DISCH_TAC THEN (MATCH_MP_TAC EQ_EXT); BETA_TAC; ASM_REWRITE_TAC[]; DISCH_TAC THEN (ASM_REWRITE_TAC[]) THEN BETA_TAC; ]);;
(* }}} *) (* Law of cardinal exponents B^A * B = B^(A+1) *)
let DOMAIN_INSERT = 
prove_by_refinement( `!a b s. (~((s:A) IN a) ==> (?F. (BIJ F (FUN (s INSERT a) b) { (u,v) | (u IN (FUN a b)) /\ ((v:B) IN b) } )))`,
(* {{{ proof *) [ REPEAT GEN_TAC; DISCH_TAC; EXISTS_TAC `\ f. ((\ x. (if (x=(s:A)) then (CHOICE (UNIV:B->bool)) else (f x))),(f s))`; REWRITE_TAC[BIJ;INJ;SURJ]; TAUT_TAC `(A /\ (A ==> B) /\ (A ==>C)) ==> ((A/\ B) /\ (A /\ C))`; REPEAT CONJ_TAC; X_GEN_TAC `(f:A->B)`; REWRITE_TAC[FUN;IN_ELIM_THM]; REWRITE_TAC[INSERT;SUBSET]; REWRITE_TAC[IN_ELIM_THM;SUPP]; STRIP_TAC; ABBREV_TAC `g = \ x. (if (x=(s:A)) then (CHOICE (UNIV:B->bool)) else (f x)) `; EXISTS_TAC `g:A->B`; EXISTS_TAC `(f:A->B) s`; REWRITE_TAC[]; REPEAT CONJ_TAC; EXPAND_TAC "g" THEN BETA_TAC; GEN_TAC; REWRITE_TAC[IN;COND_ELIM_THM]; ASM_MESON_TAC[IN]; (* next *) ALL_TAC; EXPAND_TAC "g" THEN BETA_TAC; GEN_TAC; ASM_CASES_TAC `(x:A) = s`; ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[]; ASM_MESON_TAC[]; (* next *) ALL_TAC; ASM_MESON_TAC[]; (* INJ *) ALL_TAC; REWRITE_TAC[FUN;SUPP]; DISCH_TAC; X_GEN_TAC `f1:A->B`; X_GEN_TAC `f2:A->B`; REWRITE_TAC[IN]; DISCH_ALL_TAC; MATCH_MP_TAC EQ_EXT; GEN_TAC; ASM_CASES_TAC `(x:A) = s`; POPL_TAC[1;2;3;4;6;7]; ASM_REWRITE_TAC[]; ASM_MESON_TAC[PAIR;FST;SND]; POPL_TAC[1;2;3;4;6;7]; FIRST_X_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[FST] (AP_TERM `FST:((A->B)#B)->(A->B)` th))) ; FIRST_X_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[COND_ELIM_THM] (BETA_RULE (AP_THM th `x:A`)))); LABEL_ALL_TAC; H_UNDISCH_TAC (HYP "0"); COND_CASES_TAC; ASM_MESON_TAC[]; ASM_MESON_TAC[]; (* SURJ *) ALL_TAC; REWRITE_TAC[FUN;SUPP;IN_ELIM_THM]; REWRITE_TAC[IN;INSERT;SUBSET]; DISCH_ALL_TAC; X_GEN_TAC `p:(A->B)#B`; DISCH_THEN CHOOSE_TAC; FIRST_X_ASSUM (fun th -> MP_TAC th); DISCH_THEN CHOOSE_TAC; FIRST_X_ASSUM MP_TAC; DISCH_ALL_TAC; ASM_REWRITE_TAC[]; EXISTS_TAC `\ (x:A). if (x = s) then (v:B) else (u x)`; REPEAT CONJ_TAC; X_GEN_TAC `t:A`; BETA_TAC; REWRITE_TAC[IN_ELIM_THM;COND_ELIM_THM]; POPL_TAC[1;3;4;5]; ASM_MESON_TAC[]; X_GEN_TAC `t:A`; BETA_TAC; REWRITE_TAC[IN_ELIM_THM;COND_ELIM_THM]; ASM_CASES_TAC `(t:A) = s`; POPL_TAC[1;3;4;5;6]; ASM_REWRITE_TAC[]; POPL_TAC[1;3;4;5;6]; FIRST_X_ASSUM (fun th -> ASSUME_TAC (SPEC `t:A` th)); ASM_SIMP_TAC[prove(`~((t:A)=s) ==> ((t=s)=F)`,MESON_TAC[])]; BETA_TAC; REWRITE_TAC[]; POPL_TAC[0;2;3;4]; AP_THM_TAC; AP_TERM_TAC; MATCH_MP_TAC EQ_EXT; X_GEN_TAC `t:A`; BETA_TAC; DISJ_CASES_TAC (prove(`(((t:A)=s) <=> T) \/ ((t=s) <=> F)`,MESON_TAC[])); ASM_REWRITE_TAC[]; ASM_MESON_TAC[IN]; ASM_REWRITE_TAC[] ]);;
(* }}} *)
let CARD_DELETE_CHOICE = 
prove_by_refinement( `!(a:(A->bool)). ((FINITE a) /\ (~(a=EMPTY))) ==> (SUC (CARD (a DELETE (CHOICE a))) = (CARD a))`,
(* {{{ proof *) [ REPEAT GEN_TAC; DISCH_ALL_TAC; ASM_SIMP_TAC[CARD_DELETE]; ASM_SIMP_TAC[CHOICE_DEF]; MATCH_MP_TAC (ARITH_RULE `~(x=0) ==> (SUC (x -| 1) = x)`); ASM_MESON_TAC[HAS_SIZE_0;HAS_SIZE]; ]);;
(* }}} *) (* let dets_flag = ref true;; dets_flag:= !labels_flag;; *) (* labels_flag:=false;; *) (* Law of cardinals |B^A| = |B|^|A| *) let FUN_SIZE = Refinement.enhanced_prove_by_refinement false ALL_TAC ( `!b a. (FINITE (a:A->bool)) /\ (FINITE (b:B->bool)) ==> ((FUN a b) HAS_SIZE ((CARD b) EXP (CARD a)))`, (* {{{ proof *) [ GEN_TAC; MATCH_MP_TAC (SPEC `CARD:(A->bool)->num` ((INST_TYPE) [`:A->bool`,`:A`] NUM_INTRO)); INDUCT_TAC; GEN_TAC; DISCH_ALL_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC [EXP]; SUBGOAL_THEN `(a:A->bool) = EMPTY` ASSUME_TAC; ASM_REWRITE_TAC[GSYM HAS_SIZE_0;HAS_SIZE]; ASM_REWRITE_TAC[HAS_SIZE;DOMAIN_EMPTY]; CONJ_TAC; REWRITE_TAC[FINITE_SING]; MATCH_MP_TAC CARD_SING; REWRITE_TAC[SING]; MESON_TAC[]; GEN_TAC; FIRST_X_ASSUM (fun th -> ASSUME_TAC (SPEC `(a:A->bool) DELETE (CHOICE a)` th)) ; DISCH_ALL_TAC; SUBGOAL_THEN `CARD ((a:A->bool) DELETE (CHOICE a)) = n` ASSUME_TAC; ASM_SIMP_TAC[CARD_DELETE]; SUBGOAL_THEN `CHOICE (a:A->bool) IN a` ASSUME_TAC; MATCH_MP_TAC CHOICE_DEF; ASSUME_TAC( ARITH_RULE `!x. (x = (SUC n)) ==> (~(x = 0))`); REWRITE_TAC[GSYM HAS_SIZE_0;HAS_SIZE]; ASM_MESON_TAC[]; ASM_REWRITE_TAC[]; MESON_TAC[ ( ARITH_RULE `!n. (SUC n -| 1) = n`)]; LABEL_ALL_TAC; H_MATCH_MP (HYP "3") (HYP "4"); SUBGOAL_THEN `FUN ((a:A->bool) DELETE CHOICE a) (b:B->bool) HAS_SIZE CARD b **| CARD (a DELETE CHOICE a)` ASSUME_TAC; ASM_MESON_TAC[FINITE_DELETE]; ASSUME_TAC (SPECL [`((a:A->bool) DELETE (CHOICE a))`;`b:B->bool`;`(CHOICE (a:A->bool))` ] DOMAIN_INSERT); LABEL_ALL_TAC; H_UNDISCH_TAC (HYP "5"); REWRITE_TAC[IN_DELETE]; SUBGOAL_THEN `~((a:A->bool) = EMPTY)` ASSUME_TAC; REWRITE_TAC[GSYM HAS_SIZE_0;HAS_SIZE]; ASSUME_TAC( ARITH_RULE `!x. (x = (SUC n)) ==> (~(x = 0))`); ASM_MESON_TAC[]; ASM_SIMP_TAC[INSERT_DELETE;CHOICE_DEF]; DISCH_THEN CHOOSE_TAC; REWRITE_TAC[HAS_SIZE]; SUBGOAL_THEN `FINITE (FUN (a:A->bool) (b:B->bool))` ASSUME_TAC; (* CONJ_TAC; *) ALL_TAC; MATCH_MP_TAC (SPEC `FUN (a:A->bool) (b:B->bool)` (PINST[(`:A->B`,`:A`);(`:(A->B)#B`,`:B`)] [] FINITE_BIJ2)); EXISTS_TAC `{u,v | (u:A->B) IN FUN (a DELETE CHOICE a) b /\ (v:B) IN b}`; EXISTS_TAC `F':(A->B)->((A->B)#B)`; ASM_REWRITE_TAC[]; MATCH_MP_TAC FINITE_PRODUCT; ASM_REWRITE_TAC[]; ASM_MESON_TAC[HAS_SIZE]; ASM_REWRITE_TAC[]; SUBGOAL_THEN `CARD (FUN (a:A->bool) (b:B->bool)) = (CARD {u,v | (u:A->B) IN FUN (a DELETE CHOICE a) b /\ (v:B) IN b})` ASSUME_TAC; MATCH_MP_TAC BIJ_CARD; EXISTS_TAC `F':(A->B)->((A->B)#B)`; ASM_REWRITE_TAC[]; (* *) ALL_TAC; ASM_REWRITE_TAC[]; SUBGOAL_THEN `FINITE (a DELETE CHOICE (a:A->bool))` ASSUME_TAC; ASM_MESON_TAC[FINITE_DELETE]; SUBGOAL_THEN `(FUN ((a:A->bool) DELETE CHOICE a) (b:B->bool)) HAS_SIZE (CARD b **| (CARD (a DELETE CHOICE a)))` ASSUME_TAC; POPL_TAC[1;2;3;4;5;10;11]; ASM_MESON_TAC[CARD_DELETE]; POP_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[HAS_SIZE] th) THEN (ASSUME_TAC th)); ASM_SIMP_TAC[CARD_PRODUCT]; REWRITE_TAC[EXP;MULT_AC] ]);; (* }}} *) (* labels_flag:= true;; *) (* ------------------------------------------------------------------ *) (* ------------------------------------------------------------------ *) (* Definitions in math tend to be n-tuples of data. Let's make it easy to pick out the individual components of a definition *) (* pick out the rest of n-tuples. Indexing consistent with lib.drop *)
let drop0 = new_definition(`drop0 (u:A#B) = SND u`);;
let drop1 = new_definition(`drop1 (u:A#B#C) = SND (SND u)`);;
let drop2 = new_definition(`drop2 (u:A#B#C#D) = SND (SND (SND u))`);;
let drop3 = new_definition(`drop3 (u:A#B#C#D#E) = SND (SND (SND (SND u)))`);;
(* pick out parts of n-tuples *)
let part0 = new_definition(`part0 (u:A#B) = FST u`);;
let part1 = new_definition(`part1 (u:A#B#C) = FST (drop0 u)`);;
let part2 = new_definition(`part2 (u:A#B#C#D) = FST (drop1 u)`);;
let part3 = new_definition(`part3 (u:A#B#C#D#E) = FST (drop2 u)`);;
let part4 = new_definition(`part4 (u:A#B#C#D#E#F) = FST (drop3 u)`);;
let part5 = new_definition(`part5 (u:A#B#C#D#E#F#G) =
   FST (SND (SND (SND (SND (SND u)))))`);;
let part6 = new_definition(`part6 (u:A#B#C#D#E#F#G#H) =
   FST (SND (SND (SND (SND (SND (SND u))))))`);;
let part7 = new_definition(`part7 (u:A#B#C#D#E#F#G#H#I) =
   FST (SND (SND (SND (SND (SND (SND (SND u)))))))`);;
let part8 = new_definition(`part8 (u:A#B#C#D#E#F#G#H#I#J) =
   FST (SND (SND (SND (SND (SND (SND (SND (SND u))))))))`);;
pop_priority();; end;;