labels_flag:= true;;


let dirac_delta = new_definition `dirac_delta (i:num) =
     (\j. if (i=j) then (&.1) else (&.0))`;;


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_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_TAC `!m. (n<=|m) ==> (b m =0)`;
  GEN_TAC;
  ASM_CASES_TAC `m = (n:num)`;
  ASM_REWRITE_TAC[];
  SUBGOAL_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_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 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_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_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_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_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_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_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_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_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_TAC `(n = j'-|i)`;
  UND 2;
  ASM_REWRITE_TAC[];
  ARITH_TAC;
  DISCH_TAC;
  SUBGOAL_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_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_TAC `(n = j'-|i)`;
  UND 2;
  ASM_REWRITE_TAC[];
  ARITH_TAC;
  DISCH_TAC;
  SUBGOAL_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_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_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_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(
  `?INV. (! (f:A->B) a b. (SURJ f a b) ==> ((INJ (INV f a b) b a) /\
       (!(x:B). (x IN b) ==> (f ((INV 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_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 ["INV"] INVERSE_FN;;


let INVERSE_BIJ = 
prove_by_refinement(
  `!(f:A->B) a b. (BIJ f a b) ==> ((BIJ (INV 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) (INV 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 [`INV (f:A->B) a b (f x)`;`x:A`] th));
  ASM_REWRITE_TAC[];
  DISCH_ALL_TAC;
  SUBGOAL_THEN `INV (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) ==> ((INV 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 = 
prove_by_refinement(
  `!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)))))))`);;


(* ------------------------------------------------------------------ *)
(* Basic Definitions of Euclidean Space, Metric Spaces, and Topology *)
(* ------------------------------------------------------------------ *)

(* ------------------------------------------------------------------ *)
(* Interface *)
(* ------------------------------------------------------------------ *)

let euclid_def = local_definition "euclid";;
mk_local_interface "euclid";;

overload_interface
 ("+", `euclid'euclid_plus:(num->real)->(num->real)->(num->real)`);;

make_overloadable "*#" `:A -> B -> B`;;

let euclid_scale = euclid_def
  `euclid_scale t f = \ (i:num). (t*. (f i))`;;

overload_interface ("*#",`euclid'euclid_scale`);;

parse_as_infix("*#",(20,"right"));;

let euclid_neg = euclid_def `euclid_neg f = \ (i:num). (--. (f i))`;;

(* This is highly ambiguous: -- f x can be read as
   (-- f) x or as -- (f x).  *)
overload_interface ("--",`euclid'euclid_neg`);;

overload_interface
  ("-", `euclid'euclid_minus:(num->real)->(num->real)->(num->real)`);;

(* ------------------------------------------------------------------ *)
(* Euclidean Space *)
(* ------------------------------------------------------------------ *)

let euclid_plus = euclid_def
  `euclid_plus f g = \ (i:num). (f i) +. (g i)`;;

let euclid = euclid_def `euclid n v <=> !m. (n <=| m) ==> (v m = &.0)`;;

let euclidean = euclid_def `euclidean v <=> ?n. euclid n v`;;

let euclid_minus = euclid_def
  `euclid_minus f g = \(i:num). (f i) -. (g i)`;;

let euclid0 = euclid_def `euclid0 = \(i:num). &.0`;;

let coord = euclid_def `coord i (f:num->real) = f i`;;

let dot = euclid_def `dot f g =
  let (n = (min_num (\m. (euclid m f) /\ (euclid m g)))) in
  sum (0,n) (\i. (f i)*(g i))`;;

let norm = euclid_def `norm f = sqrt(dot f f)`;;

let d_euclid = euclid_def `d_euclid f g = norm (f - g)`;;



(* ------------------------------------------------------------------ *)
(* Euclidean and Convex geometry *)
(* ------------------------------------------------------------------ *)



let sum_vector_EXISTS = 
prove_by_refinement(
  `?sum_vector. (!f n. sum_vector(n,0) f = (\n. &.0)) /\
    (!f m n. sum_vector(n,SUC m) f = sum_vector(n,m) f + f(n + m))`,

  (* {{{ proof *)
  [
  (CHOOSE_TAC o prove_recursive_functions_exist num_RECURSION) `(!f n. sm n 0 f = (\n. &0)) /\ (!f m n. sm  n (SUC m) f = sm n m f + f(n + m))`;
  EXISTS_TAC `\(n,m) f. (sm:num->num->(num->(num->real))->(num->real)) n m f`;
  CONV_TAC(DEPTH_CONV GEN_BETA_CONV);
  ASM_REWRITE_TAC[];
  ]);;
  (* }}} *)


let sum_vector = new_specification ["sum_vector"] sum_vector_EXISTS;;

let mk_segment = euclid_def
  `mk_segment x y = { u | ?a. (&.0 <=. a) /\ (a <=. &.1) /\
        (u = a *# x + (&.1 - a) *# y) }`;;

let mk_open_segment = euclid_def
  `mk_open_segment x y = { u | ?a. (&.0 <. a) /\ (a <. &.1) /\
        (u = a *# x + (&.1 - a) *# y) }`;;

let convex = euclid_def
  `convex S <=> !x y. (S x) /\ (S y) ==> (mk_segment x y SUBSET S)`;;

let convex_hull = euclid_def
  `convex_hull S = { u | ?f alpha m. (!n. (n< m) ==> (S (f n))) /\
    (sum(0,m) alpha = &.1) /\ (!n. (n< m) ==> (&.0 <=. (alpha n))) /\
    (u = sum_vector(0,m) (\n. (alpha n) *# (f n)))}`;;

let affine_hull = euclid_def
  `affine_hull S = { u | ?f alpha m. (!n. (n< m) ==> (S (f n))) /\
    (sum(0,m) alpha = &.1) /\
    (u = sum_vector(0,m) (\n. (alpha n) *# (f n)))}`;;

let mk_line = euclid_def `mk_line x y =
   {z| ?t. (z = (t *# x) + ((&.1 - t) *# y)) }`;;

let affine = euclid_def
  `affine S <=> !x y. (S x ) /\ (S y) ==> (mk_line x y SUBSET S)`;;

let affine_dim = euclid_def
  `affine_dim n S <=>
    (?T. (T HAS_SIZE (SUC n)) /\ (affine_hull T = affine_hull S)) /\
    (!T m. (T HAS_SIZE (SUC m)) /\ (m < n) ==> ~(affine_hull T = affine_hull S))`;;

let collinear = euclid_def
  `collinear S <=> (?n. affine_dim n S /\ (n < 2))`;;

let coplanar = euclid_def
  `coplanar S <=> (?n. affine_dim n S /\ (n < 3))`;;

let line = euclid_def
  `line L <=> (affine L) /\ (affine_dim 1 L)`;;

let plane = euclid_def
  `plane P <=> (affine P) /\ (affine_dim 2 P)`;;

let space = euclid_def
  `space R <=> (affine R) /\ (affine_dim 3 R)`;;

(*

General constructor of conical objects, including
  rays, cones, half-planes, etc.

L is the edge.  C is the set of generators in the positive
direction.

If L is a line, and C = {c}, we get the half-plane bounded by
L and containing c.

If L is a point, and C is general, we get the cone at L generated
by C.

If L and C are both singletons, we get the ray ending at L.

  *)

let mk_open_half_set = euclid_def
  `mk_open_half_set L S  =
   { u | ?t v c. (L v) /\ (S c) /\ (&.0 < t) /\
      (u = (t *# (c - v) + (&.1 - t) *# v)) }`;;

let mk_half_set = euclid_def
  `mk_half_set L S  =
   { u | ?t v c. (L v) /\ (S c) /\ (&.0 <=. t) /\
      (u = (t *# (c - v) + (&.1 - t) *# v)) }`;;


let mk_angle = euclid_def `mk_angle x y z =
   (mk_half_set {x} {y}) UNION (mk_half_set {x} {z})`;;

let mk_signed_angle = euclid_def `mk_signed_angle x y z =
   (mk_half_set {x} {y} , mk_half_set {x} {z})`;;

let mk_convex_cone = euclid_def
  `mk_convex_cone v (S:(num->real)->bool) =
    mk_half_set {v} (convex_hull S)`;;

(* we always normalize the radius of balls in a packing to 1 *)
let packing = euclid_def(`packing (S:(num->real)->bool) <=>
        !x y. ( ((S x) /\ (S y) /\ ((d_euclid x y) < (&.2))) ==>
                (x = y))`);;

let saturated_packing = euclid_def(`saturated_packing S <=>
        (( packing S) /\
        (!z. (affine_hull S z)  ==>
               (?x. ((S x) /\ ((d_euclid x z) < (&.2))))))`);;


(* 3 dimensions specific:  *)
let cross_product3 = euclid_def(`cross_product3 v1 v2 =
        let (x1 = v1 0) and (x2 = v1 1) and (x3 = v1 2) in
        let (y1 = v2 0) and (y2 = v2 1) and (y3 = v2 2) in
        (\k.
                (if (k=0) then (x2*y3-x3*y2)
                else if (k=1) then (x3*y1-x1*y3)
                else if (k=2) then (x1*y2-x2*y1)
                else (&0)))`);;

let triple_product = euclid_def(`triple_product v1 v2 v3 =
        dot v1 (cross_product3 v2 v3)`);;

(* the bounding edge *)
let mk_triangle = euclid_def `mk_triangle v1 v2 v3 =
  (mk_segment v1 v2) UNION (mk_segment v2 v3) UNION (mk_segment v3 v1)`;;

(* the interior *)
let mk_interior_triangle = euclid_def
  `mk_interior_triangle v1 v2 v3 =
     mk_open_half_set (mk_line v1 v2) {v3} INTER
       (mk_open_half_set (mk_line v2 v3) {v1}) INTER
       (mk_open_half_set (mk_line v3 v1) {v2})`;;

let mk_triangular_region = euclid_def
  `mk_triangular_region v1 v2 v3 =
    (mk_triangle v1 v2 v3) UNION (mk_interior_triangle v1 v2 v3)`;;


(* ------------------------------------------------------------------ *)
(* Statements of Theorems in Euclidean Geometry (no proofs *)
(* ------------------------------------------------------------------ *)

let half_set_convex = `!L S. convex (mk_half_set L S)`;;

let open_half_set_convex = `!L S . convex (mk_open_half_set L S )`;;

let affine_dim0 = `!S. (affine_dim 0 S) = (SING S)`;;

let hull_convex = `!S. (convex (convex_hull S))`;;

let hull_minimal = `!S T. (convex T) /\ (S SUBSET T) ==>
     (convex_hull S) SUBSET T`;;

let affine_hull_affine = `!S. (affine (affine_hull S))`;;

let affine_hull_minimal = `!S T. (affine T) /\ (S SUBSET T) ==>
     (affine_hull S) SUBSET T`;;

let mk_line_dim = `!x y. ~(x = y) ==> affine_dim 1 (mk_line x y)`;;

let affine_convex_hull = `!S. (affine_hull S) = (affine_hull (convex_hull S))`;;

let convex_hull_hull = `!S. (convex_hull S) = (convex_hull (convex_hull S))`;;

let euclid_affine_dim = `!n. affine_dim n (euclid n)`;;

let affine_dim_subset = `!m n T S.
  (affine_dim m T) /\ (affine_dim n S) /\ (T SUBSET S) ==> (m <= n)`;;

(* A few of the Birkhoff postulates of Geometry (incomplete) *)

let line_postulate = `!x y. ~(x = y) ==>
   (?!L. (L x) /\ (L y) /\ (line L))`;;

let ruler_postulate = `!L. (line L) ==>
  (?f. (BIJ f L UNIV) /\
  (!x y. (L x /\ L y ==> (d_euclid x y = abs(f x -. f y)))))`;;

let affine_postulate = `!n. (affine_dim n P) ==> (?S.
  (S SUBSET P) /\ (S HAS_SIZE n) /\ (affine_dim n S))`;;

let line_plane = `!P x y. (plane P) /\ (P x) /\ (P y) ==>
  (mk_line x y SUBSET P)`;;

let plane_of_pt = `!S. (S HAS_SIZE 3) ==> (?P. (plane P) /\
   (S SUBSET P))`;;

let plane_of_pt_unique = `!S. (S HAS_SIZE 3) ==> (collinear S) \/
  (?! P. (plane P) /\ (S SUBSET P))`;;

let plane_inter = `!P Q. (plane P) /\ (plane Q) ==>
  (P INTER Q = EMPTY) \/ (line (P INTER Q)) \/ (P = Q)`;;

(* each line separates a plane into two half-planes *)
let plane_separation =
  `!P L. (plane P) /\ (line L) /\ (L SUBSET P) ==>
  (?A B. (A INTER B = EMPTY) /\ (A INTER L = EMPTY) /\
    (B INTER L = EMPTY) /\ (L UNION A UNION B = P) /\
   (!c u. (P c) /\ (u = mk_open_half_set L {c}) ==>
      (u = A) \/ (u = B) \/ (u = L)) /\
   (!a b. (A a) /\ (B b) ==> ~(segment a b INTER L = EMPTY)))`;;

let space_separation =
  `!R P. (space R) /\ (plane P) /\ (P SUBSET R) ==>
  (?A B. (A INTER B = EMRTY) /\ (A INTER P = EMRTY) /\
    (B INTER P = EMRTY) /\ (P UNION A UNION B = R) /\
   (!c u. (R c) /\ (u = mk_open_half_set P {c}) ==>
      (u = A) \/ (u = B) \/ (u = P)) /\
     (!a b. (A a) /\ (B b) ==> ~(segment a b INTER L = EMPTY)))`;;

(* ------------------------------------------------------------------ *)
(* Metric Space *)
(* ------------------------------------------------------------------ *)

let metric_space = euclid_def `metric_space (X:A->bool,d:A->A->real)
   <=>
   !x y z.
      (X x) /\ (X y) /\ (X z) ==>
         (((&.0) <=. (d x y)) /\
          ((&.0 = d x y) = (x = y)) /\
          (d x y = d y x) /\
          (d x z <=. d x y + d y z))`;;

(* ------------------------------------------------------------------ *)
(* Measure *)
(* ------------------------------------------------------------------ *)

let set_translate = euclid_def
  `set_translate v X = { z | ?x. (X x) /\ (z = v + x) }`;;

let set_scale = euclid_def
  `set_scale r X = { z | ?x. (X x) /\ (z = r *# x) }`;;

let mk_rectangle = euclid_def
  `mk_rectangle a b = { z | !(i:num). (a i <=. z i) /\ (z i <. b i) }`;;

let one_vec = euclid_def
  `one_vec n = (\i. if (i<| n) then (&.1) else (&.0))`;;

let mk_cube = euclid_def
  `mk_cube n k v =
    let (r = twopow (--: (&: k))) in
    let (vv = (\i. (real_of_int (v i)))) in
     mk_rectangle (r *# vv) (r *# (vv + (one_vec n)))`;;

let inner_cube = euclid_def
  `inner_cube n k A =
    { v | (mk_cube n k v SUBSET A) /\
      (!i. (n <| i) ==> (&:0 = v i)) }`;;

let outer_cube = euclid_def
  `outer_cube n k A =
    { v | ~((mk_cube n k v) INTER A = EMPTY) /\
      (!i. (n <| i) ==> (&:0 = v i)) }`;;

let inner_vol = euclid_def
  `inner_vol n k A =
    (&. (CARD (inner_cube n k A)))*(twopow (--: (&: (n*k))))`;;

let outer_vol = euclid_def
  `outer_vol n k A =
    (&. (CARD (outer_cube n k A)))*(twopow (--: (&: (n*k))))`;;

let euclid_bounded = euclid_def
  `euclid_bounded A = (?R. !(x:num->real) i. (A x) ==> (x i <. R))`;;

let vol = euclid_def
  `vol n A = lim (\k. outer_vol n k A)`;;

(* ------------------------------------------------------------------ *)
(* COMPUTING PI *)
(* ------------------------------------------------------------------ *)

unambiguous_interface();;
prioritize_real();;

(* ------------------------------------------------------------------ *)
(* general series approximations *)
(* ------------------------------------------------------------------ *)


let SER_APPROX1 = 
prove_by_refinement(
  `!s f g.  (f sums s) /\ (summable g) ==>
    (!k. ((!n. (||. (f (n+k)) <=. (g (n+k)))) ==>
    ( (s - (sum(0,k) f)) <=. (suminf (\n. (g (n +| k)))))))`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  DISCH_ALL_TAC;
  GEN_TAC;
  DISCH_TAC;
  IMP_RES_THEN ASSUME_TAC SUM_SUMMABLE;
  IMP_RES_THEN (fun th -> (ASSUME_TAC (SPEC `k:num` th))) SER_OFFSET;
  IMP_RES_THEN ASSUME_TAC SUM_UNIQ;
  SUBGOAL_THEN `(\n. (f (n+ k))) sums (s - (sum(0,k) f))` ASSUME_TAC;
  ASM_MESON_TAC[];
  SUBGOAL_THEN `summable (\n. (f (n+k))) /\ (suminf (\n. (f (n+k))) <=. (suminf (\n. (g (n+k)))))` ASSUME_TAC;
  MATCH_MP_TAC SER_LE2;
  BETA_TAC;
  ASM_REWRITE_TAC[];
  IMP_RES_THEN ASSUME_TAC SER_OFFSET;
  FIRST_X_ASSUM (fun th -> ACCEPT_TAC (MATCH_MP SUM_SUMMABLE (((SPEC `k:num`) th))));
  ASM_MESON_TAC[SUM_UNIQ]
  ]);;
  (* }}} *)


let SER_APPROX = 
prove_by_refinement(
  `!s f g.  (f sums s) /\ (!n. (||. (f n) <=. (g n))) /\
       (summable g) ==>
    (!k. (abs (s - (sum(0,k) f)) <=. (suminf (\n. (g (n +| k))))))`,

  (* {{{ proof *)
  [
  REPEAT GEN_TAC;
  DISCH_ALL_TAC;
  GEN_TAC;
  REWRITE_TAC[REAL_ABS_BOUNDS];
  CONJ_TAC;
  SUBGOAL_THEN `(!k. ((!n. (||. ((\p. (--. (f p))) (n+k))) <=. (g (n+k)))) ==> ((--.s) - (sum(0,k) (\p. (--. (f p)))) <=. (suminf (\n. (g (n +k))))))` ASSUME_TAC;
  MATCH_MP_TAC SER_APPROX1;
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC SER_NEG ;
  ASM_REWRITE_TAC[];
  MATCH_MP_TAC (REAL_ARITH (`(--. s -. (--. u) <=. x) ==> (--. x <=. (s -. u))`));
  ONCE_REWRITE_TAC[GSYM SUM_NEG];
  FIRST_X_ASSUM (fun th -> (MATCH_MP_TAC th));
  BETA_TAC;
  ASM_REWRITE_TAC[REAL_ABS_NEG];
  H_VAL2 CONJ (HYP "0") (HYP "2");
  IMP_RES_THEN MATCH_MP_TAC SER_APPROX1 ;
  GEN_TAC;
  ASM_MESON_TAC[];
  ]);;
  (* }}} *)

(* ------------------------------------------------------------------ *)
(* now for pi calculation stuff *)
(* ------------------------------------------------------------------ *)


let local_def = local_definition "trig";;



let PI_EST = 
prove_by_refinement(
               `!n. (1 <=| n) ==> (abs(&4 / &(8 * n + 1) -
            &2 / &(8 * n + 4) -
            &1 / &(8 * n + 5) -
            &1 / &(8 * n + 6)) <= &.622/(&.819))`,

  (* {{{ proof *)
   [
   GEN_TAC THEN DISCH_ALL_TAC;
   REWRITE_TAC[real_div];
   MATCH_MP_TAC (REWRITE_RULE[real_div] (REWRITE_RULE[REAL_RAT_REDUCE_CONV `(&.4/(&.9) +(&.2/(&.12)) + (&.1/(&.13))+ (&.1/(&.14)))`] (REAL_ARITH `(abs((&.4)*.u)<=. (&.4)/(&.9)) /\ (abs((&.2)*.v)<=. (&.2)/(&.12)) /\ (abs((&.1)*w) <=. (&.1)/(&.13)) /\ (abs((&.1)*x) <=. (&.1)/(&.14)) ==> (abs((&.4)*u -(&.2)*v - (&.1)*w - (&.1)*x) <= (&.4/(&.9) +(&.2/(&.12)) + (&.1/(&.13))+ (&.1/(&.14))))`)));
   IMP_RES_THEN ASSUME_TAC (ARITH_RULE `1 <=| n ==> (0 < n)`);
   FIRST_X_ASSUM (fun th -> ASSUME_TAC (REWRITE_RULE[GSYM REAL_OF_NUM_LT] th));
   ASSUME_TAC (prove(`(a<=.b) ==> (&.n*a <=. (&.n)*b)`,MESON_TAC[REAL_PROP_LE_LMUL;REAL_POS]));
   REWRITE_TAC[REAL_ABS_MUL;REAL_ABS_INV;prove(`||.(&.n) = (&.n)`,MESON_TAC[REAL_POS;REAL_ABS_REFL])];
   REPEAT CONJ_TAC THEN (POP_ASSUM (fun th -> MATCH_MP_TAC th)) THEN (MATCH_MP_TAC (prove(`((&.0 <. (&.n)) /\ (&.n <=. a)) ==> (inv(a)<=. (inv(&.n)))`,MESON_TAC[REAL_ABS_REFL;REAL_ABS_INV;REAL_LE_INV2]))) THEN
   REWRITE_TAC[REAL_LT;REAL_LE] THEN (H_UNDISCH_TAC (HYP"0")) THEN
   ARITH_TAC]);;
  (* }}} *)

let pi_fun = local_def `pi_fun n = inv (&.16 **. n) *.
          (&.4 / &.(8 *| n +| 1) -.
           &.2 / &.(8 *| n +| 4) -.
           &.1 / &.(8 *| n +| 5) -.
           &.1 / &.(8 *| n +| 6))`;;

let pi_bound_fun = local_def `pi_bound_fun n = if (n=0) then (&.8) else
    (((&.15)/(&.16))*(inv(&.16 **. n))) `;;


let PI_EST2 = 
prove_by_refinement(
    `!k. abs(pi_fun k) <=. (pi_bound_fun k)`,

  (* {{{ proof *)
   [
   GEN_TAC;
   REWRITE_TAC[pi_fun;pi_bound_fun];
   COND_CASES_TAC;
   ASM_REWRITE_TAC[];
   CONV_TAC (NUM_REDUCE_CONV);
   (CONV_TAC (REAL_RAT_REDUCE_CONV));
   CONV_TAC (RAND_CONV (REWR_CONV (REAL_ARITH `a*b = b*.a`)));
   REWRITE_TAC[REAL_ABS_MUL;REAL_ABS_INV;REAL_ABS_POW;prove(`||.(&.n) = (&.n)`,MESON_TAC[REAL_POS;REAL_ABS_REFL])];
   MATCH_MP_TAC (prove(`!x y z. (&.0 <. z /\ (y <=. x) ==> (z*y <=. (z*x)))`,MESON_TAC[REAL_LE_LMUL_EQ]));
   ASSUME_TAC (REWRITE_RULE[] (REAL_RAT_REDUCE_CONV `(&.622)/(&.819) <=. (&.15)/(&.16)`));
   IMP_RES_THEN ASSUME_TAC (ARITH_RULE `~(k=0) ==> (1<=| k)`);
   IMP_RES_THEN ASSUME_TAC (PI_EST);
   CONJ_TAC;
   SIMP_TAC[REAL_POW_LT;REAL_LT_INV;ARITH_RULE `&.0 < (&.16)`];
   ASM_MESON_TAC[REAL_LE_TRANS];
   ]);;
  (* }}} *)


let GP16 = 
prove_by_refinement(
  `!k. (\n. inv (&16 pow k) * inv (&16 pow n)) sums
         inv (&16 pow k) * &16 / &15`,

  (* {{{ proof *)
  [
  GEN_TAC;
  ASSUME_TAC (REWRITE_RULE[] (REAL_RAT_REDUCE_CONV `abs (&.1 / (&. 16)) <. (&.1)`));
  IMP_RES_THEN (fun th -> ASSUME_TAC (CONV_RULE REAL_RAT_REDUCE_CONV th)) GP;
  MATCH_MP_TAC SER_CMUL;
  ASM_REWRITE_TAC[GSYM REAL_POW_INV;REAL_INV_1OVER];
  ]);;
  (* }}} *)


let GP16a = 
prove_by_refinement(
   `!k. (0<|k) ==> (\n. (pi_bound_fun (n+k))) sums (inv(&.16 **. k))`,

  (* {{{ proof *)
   [
   GEN_TAC;
   DISCH_TAC;
   SUBGOAL_THEN `(\n. pi_bound_fun (n+k)) = (\n. ((&.15/(&.16))* (inv(&.16)**. k) *. inv(&.16 **. n)))` (fun th-> REWRITE_TAC[th]);
   MATCH_MP_TAC EQ_EXT;
   X_GEN_TAC `n:num` THEN BETA_TAC;
   REWRITE_TAC[pi_bound_fun];
   COND_CASES_TAC;
   ASM_MESON_TAC[ARITH_RULE `0<| k ==> (~(n+k = 0))`];
   REWRITE_TAC[GSYM REAL_MUL_ASSOC];
   AP_TERM_TAC;
   REWRITE_TAC[REAL_INV_MUL;REAL_POW_ADD;REAL_POW_INV;REAL_MUL_AC];
   SUBGOAL_THEN `(\n. (&.15/(&.16)) *. ((inv(&.16)**. k)*. inv(&.16 **. n))) sums ((&.15/(&.16)) *.(inv(&.16**. k)*. ((&.16)/(&.15))))` ASSUME_TAC;
   MATCH_MP_TAC SER_CMUL;
   REWRITE_TAC[REAL_POW_INV];
   ACCEPT_TAC (SPEC `k:num` GP16);
   FIRST_X_ASSUM MP_TAC;
   REWRITE_TAC[REAL_MUL_ASSOC];
   MATCH_MP_TAC (prove (`(x=y) ==> ((a sums x) ==> (a sums y))`,MESON_TAC[]));
   MATCH_MP_TAC (REAL_ARITH `(b*(a*c) = (b*(&.1))) ==> ((a*b)*c = b)`);
   AP_TERM_TAC;
   CONV_TAC (REAL_RAT_REDUCE_CONV);
   ]);;
  (* }}} *)


let PI_SER = 
prove_by_refinement(
  `!k. (0<|k) ==> (abs(pi - (sum(0,k) pi_fun)) <=. (inv(&.16 **. (k))))`,

  (* {{{ proof *)
   [
   GEN_TAC THEN DISCH_TAC;
   ASSUME_TAC (ONCE_REWRITE_RULE[ETA_AX] (REWRITE_RULE[GSYM pi_fun] POLYLOG_THM));
   ASSUME_TAC PI_EST2;
   IMP_RES_THEN (ASSUME_TAC) GP16a;
   IMP_RES_THEN (ASSUME_TAC) SUM_SUMMABLE;
   IMP_RES_THEN (ASSUME_TAC) SER_OFFSET_REV;
   IMP_RES_THEN (ASSUME_TAC) SUM_SUMMABLE;
   MP_TAC (SPECL [`pi`;`pi_fun`;`pi_bound_fun` ] SER_APPROX);
   ASM_REWRITE_TAC[];
   DISCH_THEN (fun th -> MP_TAC (SPEC `k:num` th));
   SUBGOAL_THEN `suminf (\n. pi_bound_fun (n + k)) = inv (&.16 **. k)` (fun th -> (MESON_TAC[th]));
   ASM_MESON_TAC[SUM_UNIQ];
   ]);;
  (* }}} *)

(* replace 3 by SUC (SUC (SUC 0)) *)
let SUC_EXPAND_CONV tm =
   let count = dest_numeral tm in
   let rec add_suc i r =
     if (i <=/ (Int 0)) then r
     else add_suc (i -/ (Int 1)) (mk_comb (`SUC`,r)) in
   let tm' = add_suc count `0` in
   REWRITE_RULE[] (ARITH_REWRITE_CONV[] (mk_eq (tm,tm')));;


let inv_twopow = 
prove(
  `!n. inv (&.16 **. n) = (twopow (--: (&:(4*n)))) `,

    REWRITE_TAC[TWOPOW_NEG;GSYM (NUM_RED_CONV `2 EXP 4`);
    REAL_OF_NUM_POW;EXP_MULT]);;

let PI_SERn n =
   let SUM_EXPAND_CONV =
           (ARITH_REWRITE_CONV[]) THENC
           (TOP_DEPTH_CONV SUC_EXPAND_CONV) THENC
           (REWRITE_CONV[sum]) THENC
           (ARITH_REWRITE_CONV[REAL_ADD_LID;GSYM REAL_ADD_ASSOC]) in
   let sum_thm = SUM_EXPAND_CONV (vsubst [n,`i:num`] `sum(0,i) f`) in
   
let gt_thm = ARITH_RULE (vsubst [n,`i:num`] `0 <| i`) in
   ((* CONV_RULE REAL_RAT_REDUCE_CONV *)(CONV_RULE (ARITH_REWRITE_CONV[]) (BETA_RULE (REWRITE_RULE[sum_thm;pi_fun;inv_twopow] (MATCH_MP PI_SER gt_thm)))));;

(* abs(pi - u ) < e *)
let recompute_pi bprec =
   let n = (bprec /4) in
   let pi_ser = PI_SERn (mk_numeral (Int n)) in
   let _ = remove_real_constant `pi` in
   (add_real_constant pi_ser; INTERVAL_OF_TERM bprec `pi`);;

(* ------------------------------------------------------------------ *)
(* restore defaults *)
(* ------------------------------------------------------------------ *)

reduce_local_interface("trig");;
pop_priority();;