text_formalization/nonlinear/formal_tests/hminus.hl

   1 (* Gives an interval approximation of hminus *)
   2 (* hminus ~ 1.2317544220903043901 *)
   3
   4 (* load_path := "/mnt/Repository/formal_ineqs" :: !load_path;; *)
   5
   6 (* tested with base = 100 *)
   7 needs "verifier/m_verifier_main.hl";;
   8
   9 (* module Hminus = struct *)
  10
  11 open M_verifier_main;;
  12
  13
  14 let lmfun_cond_le = (UNDISCH_ALL o prove)(`x <= h0 ==> lmfun x = (h0 - x) / (h0 - &1)`,
  15                                           REWRITE_TAC[Sphere.lmfun] THEN REAL_ARITH_TAC);;
  16
  17 let lmfun_cond_ge = (UNDISCH_ALL o prove)(`h0 <= x ==> lmfun x = &0`,
  18                                           ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> ~(b <= a) \/ a = b`] THEN
  19                                             STRIP_TAC THEN ASM_REWRITE_TAC[Sphere.lmfun] THEN
  20                                             REAL_ARITH_TAC);;
  21
  22 let eq_tm = `marchal_quartic x - lmfun x`;;
  23 let eq_th1, eq_th2 =
  24   let ths = [Sphere.marchal_quartic; Sphere.h0; Sphere.hplus] in
  25     REWRITE_CONV (lmfun_cond_le :: ths) eq_tm,
  26   REWRITE_CONV (REAL_SUB_RZERO :: lmfun_cond_ge :: ths) eq_tm;;
  27
  28 let eq_tm1 = (rand o concl) eq_th1 and
  29     eq_tm2 = (rand o concl) eq_th2;;
  30
  31 let ineq1_concl = mk_binary "real_lt" (eq_tm1, `&0`) and
  32     ineq2_concl = mk_binary "real_lt" (`&0`, eq_tm1) and
  33     ineq3_concl = mk_binary "real_lt" (`&0`, eq_tm2);;
  34
  35 (* A better approximation cannot be achieved directly *)
  36 let bounds1 = `#1.2 <= x /\ x <= #1.2317544220903043901` and
  37     bounds2 = `#1.2317544220903047 <= x /\ x <= #1.26` and
  38     bounds3 = `#1.26 <= x /\ x <= #1.3`;;
  39
  40 let ineq1_tm = mk_imp (bounds1, ineq1_concl) and
  41     ineq2_tm = mk_imp (bounds2, ineq2_concl) and
  42     ineq3_tm = mk_imp (bounds3, ineq3_concl);;
  43
  44 let ineq1_th, _ = verify_ineq default_params 12 ineq1_tm;;
  45 let ineq2_th, _ = verify_ineq default_params 12 ineq2_tm;;
  46 let ineq3_th, _ = verify_ineq default_params 12 ineq3_tm;;
  47
  48 let ineq_th = prove(`(#1.2 <= x /\ x < #1.3) /\
  49                       ~(#1.2317544220903043901 <= x /\ x <= #1.2317544220903047) ==>
  50                       ~(marchal_quartic x = lmfun x)`,
  51                     REWRITE_TAC[DE_MORGAN_THM; REAL_NOT_LE] THEN
  52                       ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a - b = &0`] THEN
  53                       STRIP_TAC THENL [
  54                         MP_TAC (SPEC_ALL ineq1_th) THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
  55                           MP_TAC (DISCH_ALL eq_th1) THEN REWRITE_TAC[Sphere.h0] THEN ANTS_TAC THENL [
  56                             REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
  57                             ALL_TAC
  58                           ] THEN
  59                           DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
  60                           REAL_ARITH_TAC;
  61                         ALL_TAC
  62                       ] THEN
  63                       DISJ_CASES_TAC (REAL_ARITH `x <= #1.26 \/ #1.26 <= x`) THENL [
  64                         MP_TAC (SPEC_ALL ineq2_th) THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
  65                           MP_TAC (DISCH_ALL eq_th1) THEN ASM_REWRITE_TAC[Sphere.h0] THEN
  66                           DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
  67                           REAL_ARITH_TAC;
  68                         ALL_TAC
  69                       ] THEN
  70                       MP_TAC (SPEC_ALL ineq3_th) THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
  71                       MP_TAC (DISCH_ALL eq_th2) THEN ASM_REWRITE_TAC[Sphere.h0] THEN
  72                       DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
  73                       REAL_ARITH_TAC);;
  74
  75
  76 let marchal_quartic_continuous_at = prove(`!x. marchal_quartic real_continuous atreal x`,
  77                                        GEN_TAC THEN
  78                                          new_rewrite [] [`marchal_quartic`] (GSYM ETA_AX) THEN
  79                                          PURE_REWRITE_TAC[Sphere.marchal_quartic] THEN
  80                                          MATCH_MP_TAC REAL_CONTINUOUS_MUL THEN CONJ_TAC THENL [
  81                                            MATCH_MP_TAC REAL_CONTINUOUS_SUB THEN
  82                                              REWRITE_TAC[REAL_CONTINUOUS_CONST; REAL_CONTINUOUS_AT_ID];
  83                                            ALL_TAC
  84                                          ] THEN
  85                                          MATCH_MP_TAC REAL_CONTINUOUS_MUL THEN CONJ_TAC THENL [
  86                                            MATCH_MP_TAC REAL_CONTINUOUS_SUB THEN
  87                                              REWRITE_TAC[REAL_CONTINUOUS_CONST; REAL_CONTINUOUS_AT_ID];
  88                                            ALL_TAC
  89                                          ] THEN
  90                                          REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_CONTINUOUS_MUL THEN
  91                                          REWRITE_TAC[REAL_CONTINUOUS_CONST] THEN
  92                                          MATCH_MP_TAC REAL_CONTINUOUS_ADD THEN
  93                                          REWRITE_TAC[REAL_CONTINUOUS_CONST] THEN
  94                                          MATCH_MP_TAC REAL_CONTINUOUS_SUB THEN CONJ_TAC THENL [
  95                                            MATCH_MP_TAC REAL_CONTINUOUS_LMUL THEN
  96                                              MATCH_MP_TAC REAL_CONTINUOUS_POW THEN
  97                                              REWRITE_TAC[REAL_CONTINUOUS_AT_ID];
  98                                            ALL_TAC
  99                                          ] THEN
 100                                          MATCH_MP_TAC REAL_CONTINUOUS_LMUL THEN
 101                                          REWRITE_TAC[REAL_CONTINUOUS_AT_ID]);;
 102
 103 (* Lemma piecewise_real_continuous *)
 104 let piecewise_real_continuous = section_proof ["a";"b";"t";"f1";"f2";"f"]
 105 `f1 real_continuous_on (real_interval [a,t]) /\ f2 real_continuous_on (real_interval [t,b]) /\
 106         f1 t = f2 t /\ f = (\x. if x <= t then f1 x else f2 x) ==>
 107         f real_continuous_on (real_interval [a,b])`
 108 [
 109    (((repeat_tactic 1 9 (((use_arg_then "real_continuous_on")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 1 9 (((use_arg_then "IN_REAL_INTERVAL")(thm_tac (new_rewrite [] [])))))) THEN ALL_TAC THEN (case THEN (move ["f1_cont"])) THEN (case THEN (move ["f2_cont"])) THEN (case THEN (move ["f12_eq"])) THEN (move ["f_eq"]) THEN (move ["x"]) THEN (move ["e"]) THEN (case THEN ((move ["x_in"]) THEN (move ["e_gt0"]))));
 110    ((THENL) (((fun arg_tac -> arg_tac (Arg_theorem (REAL_ARITH `x < t \/ t < x \/ x = t`))) (disch_tac [])) THEN case) [(move ["h"]); ALL_TAC]);
 111    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then "f1_cont") (fun fst_arg -> (use_arg_then "e_gt0") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then "REAL_LT_IMP_LE") (fun fst_arg -> (use_arg_then "h") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then "x_in")(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))) THEN ALL_TAC THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_gt0"])) THEN (move ["ineq"])));
 112    ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`min d (t - x)`))) (term_tac exists_tac)) THEN (split_tac)) ((((use_arg_then "h") (disch_tac [])) THEN (clear_assumption "h") THEN ((use_arg_then "d_gt0") (disch_tac [])) THEN (clear_assumption "d_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 113    (BETA_TAC THEN (move ["y"]) THEN (case THEN ((move ["y_ineq"]) THEN (move ["xy_lt"]))));
 114    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`y < t`))) (term_tac (have_gen_tac [](move ["y_lt"])))) ((((use_arg_then "h") (disch_tac [])) THEN (clear_assumption "h") THEN ((use_arg_then "xy_lt") (disch_tac [])) THEN (clear_assumption "xy_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 115    (((((use_arg_then "f_eq")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then "REAL_LT_IMP_LE")(thm_tac (new_rewrite [] []))))) THEN ((simp_tac THEN TRY done_tac)) THEN (((use_arg_then "ineq")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "xy_lt") (disch_tac [])) THEN (clear_assumption "xy_lt") THEN ((use_arg_then "y_lt") (disch_tac [])) THEN (clear_assumption "y_lt") THEN ((use_arg_then "y_ineq") (disch_tac [])) THEN (clear_assumption "y_ineq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 116    (case THEN (move ["h"]));
 117    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then "f2_cont") (fun fst_arg -> (use_arg_then "e_gt0") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> (use_arg_then "REAL_LT_IMP_LE") (fun fst_arg -> (use_arg_then "h") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN (((((use_arg_then "x_in")(thm_tac (new_rewrite [] [])))) THEN ((simp_tac THEN TRY done_tac))) THEN ALL_TAC THEN (case THEN (move ["d"])) THEN (case THEN (move ["d_gt0"])) THEN (move ["ineq"])));
 118    ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`min d (x - t)`))) (term_tac exists_tac)) THEN (split_tac)) ((((use_arg_then "h") (disch_tac [])) THEN (clear_assumption "h") THEN ((use_arg_then "d_gt0") (disch_tac [])) THEN (clear_assumption "d_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 119    (BETA_TAC THEN (move ["y"]) THEN (case THEN ((move ["y_ineq"]) THEN (move ["xy_lt"]))));
 120    ((THENL_FIRST) ((fun arg_tac -> arg_tac (Arg_term (`t < y`))) (term_tac (have_gen_tac [](move ["y_lt"])))) ((((use_arg_then "h") (disch_tac [])) THEN (clear_assumption "h") THEN ((use_arg_then "xy_lt") (disch_tac [])) THEN (clear_assumption "xy_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 121    (((((use_arg_then "f_eq")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (repeat_tactic 1 9 (((use_arg_then "REAL_NOT_LT")(gsym_then (thm_tac (new_rewrite [] [])))))) THEN (((use_arg_then "y_lt")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "h")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "ineq")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "xy_lt") (disch_tac [])) THEN (clear_assumption "xy_lt") THEN ((use_arg_then "y_lt") (disch_tac [])) THEN (clear_assumption "y_lt") THEN ((use_arg_then "y_ineq") (disch_tac [])) THEN (clear_assumption "y_ineq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 122    ((((fun arg_tac -> (fun arg_tac -> (use_arg_then "f2_cont") (fun fst_arg -> (use_arg_then "t") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "e_gt0") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN ((fun arg_tac -> (fun arg_tac -> (use_arg_then "f1_cont") (fun fst_arg -> (use_arg_then "t") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "e_gt0") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC) THEN ((((use_arg_then "h")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "REAL_LE_REFL")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "x_in")(thm_tac (new_rewrite [] []))))) THEN (simp_tac)));
 123    (BETA_TAC THEN (case THEN (move ["d1"])) THEN (case THEN (move ["d1_gt0"])) THEN (move ["ineq1"]) THEN (case THEN (move ["d2"])) THEN (case THEN (move ["d2_gt0"])) THEN (move ["ineq2"]));
 124    ((THENL_FIRST) (((fun arg_tac -> arg_tac (Arg_term (`min d1 d2`))) (term_tac exists_tac)) THEN (split_tac)) ((((use_arg_then "d2_gt0") (disch_tac [])) THEN (clear_assumption "d2_gt0") THEN ((use_arg_then "d1_gt0") (disch_tac [])) THEN (clear_assumption "d1_gt0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac)));
 125    (BETA_TAC THEN (move ["y"]) THEN (case THEN ((move ["y_ineq"]) THEN (move ["xy_lt"]))));
 126    (((fun arg_tac -> (fun arg_tac -> (use_arg_then "REAL_LET_TOTAL") (fun fst_arg -> (use_arg_then "y") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "x") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN case THEN (move ["xy_ineq"]));
 127    (((((use_arg_then "f_eq")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "h")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "REAL_LE_REFL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "xy_ineq")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "ineq1")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "xy_ineq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "y_ineq")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "xy_lt") (disch_tac [])) THEN (clear_assumption "xy_lt") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 128    ((((use_arg_then "f_eq")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "h")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "REAL_LE_REFL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_NOT_LT")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "xy_ineq")(thm_tac (new_rewrite [] [])))) THEN (simp_tac) THEN (((use_arg_then "h")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "f12_eq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "h")(gsym_then (thm_tac (new_rewrite [] []))))));
 129    ((((use_arg_then "ineq2")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "xy_lt") (disch_tac [])) THEN (clear_assumption "xy_lt") THEN ((use_arg_then "y_ineq") (disch_tac [])) THEN (clear_assumption "y_ineq") THEN ((use_arg_then "xy_ineq") (disch_tac [])) THEN (clear_assumption "xy_ineq") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
 130 ];;
 131
 132 (* Lemma piecewise_real_continuous_univ *)
 133 let piecewise_real_continuous_univ = section_proof ["t";"f1";"f2";"f"]
 134 `f1 real_continuous_on UNIV /\ f2 real_continuous_on UNIV /\ f1 t = f2 t /\
 135         f = (\x. if x <= t then f1 x else f2 x) ==>
 136         f real_continuous_on UNIV`
 137 [
 138    (BETA_TAC THEN (case THEN (move ["f1_cont"])) THEN (case THEN (move ["f2_con"])) THEN (case THEN (move ["f12_eq"])) THEN (move ["f_eq"]));
 139    (((THENL_ROT 1)) ((fun arg_tac -> arg_tac (Arg_term (`!a b. f real_continuous_on real_interval (a,b)`))) (term_tac (have_gen_tac [](move ["cont_int"])))));
 140    (((((use_arg_then "REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "REAL_OPEN_UNIV")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (move ["x"]) THEN (move ["_"]));
 141    (((fun arg_tac -> (fun arg_tac -> (use_arg_then "cont_int") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x - &1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`x + &1`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC);
 142    (((((use_arg_then "REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "REAL_OPEN_REAL_INTERVAL")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac))) THEN (DISCH_THEN apply_tac));
 143    ((((use_arg_then "IN_REAL_INTERVAL")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 144    ((BETA_TAC THEN (move ["a"]) THEN (move ["b"])) THEN (((use_arg_then "REAL_CONTINUOUS_ON_SUBSET") (disch_tac [])) THEN (clear_assumption "REAL_CONTINUOUS_ON_SUBSET") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`real_interval [a,b]`))) (term_tac exists_tac)));
 145    ((((use_arg_then "REAL_INTERVAL_OPEN_SUBSET_CLOSED")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (fun arg_tac -> (use_arg_then "piecewise_real_continuous") (fun fst_arg -> (use_arg_then "f_eq") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "f12_eq") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
 146    ((split_tac) THEN ((((fun arg_tac -> (use_arg_then "REAL_CONTINUOUS_ON_SUBSET") (fun fst_arg -> (fun arg_tac -> arg_tac (Arg_term (`(:real)`))) (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "SUBSET_UNIV")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 147 ];;
 148
 149 (* Lemma lmfun_continuous *)
 150 let lmfun_continuous = section_proof []
 151 `lmfun real_continuous_on UNIV`
 152 [
 153    ((fun arg_tac -> arg_tac (Arg_term (`lmfun = (\x. if x <= h0 then (h0 - x) / (h0 - &1) else &0)`))) (term_tac (have_gen_tac [](move ["eq"]))));
 154    (((((use_arg_then "eq_ext")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "Sphere.lmfun")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 155    ((THENL_ROT (1)) ((((fun arg_tac -> (use_arg_then "piecewise_real_continuous_univ") (fun fst_arg -> (use_arg_then "eq") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] [])))) THEN (split_tac)));
 156    ((((use_arg_then "REAL_CONTINUOUS_ON_CONST")(thm_tac (new_rewrite [] [])))) THEN (arith_tac) THEN (done_tac));
 157    ((((use_arg_then "real_div")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_CONTINUOUS_ON_RMUL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_CONTINUOUS_ON_SUB")(thm_tac (new_rewrite [] [])))));
 158    (((((use_arg_then "REAL_CONTINUOUS_ON_ID")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_CONTINUOUS_ON_CONST")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
 159 ];;
 160
 161
 162 let root_th = prove(`?x. (#1.2317544220903043901 <= x /\ x <= #1.2317544220903047) /\
 163                       marchal_quartic x = lmfun x`,
 164                     REWRITE_TAC[GSYM IN_REAL_INTERVAL] THEN
 165                       ONCE_REWRITE_TAC[REAL_ARITH `a = b <=> a - b = &0`] THEN
 166                       MATCH_MP_TAC REAL_IVT_INCREASING THEN REPEAT STRIP_TAC THENL [
 167                         REAL_ARITH_TAC;
 168                         MATCH_MP_TAC REAL_CONTINUOUS_ON_SUB THEN CONJ_TAC THENL [
 169                           REWRITE_TAC[REAL_CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
 170                             REPEAT STRIP_TAC THEN
 171                             MATCH_MP_TAC REAL_CONTINUOUS_ATREAL_WITHINREAL THEN
 172                             REWRITE_TAC[marchal_quartic_continuous_at];
 173                           ALL_TAC
 174                         ] THEN
 175                           MATCH_MP_TAC REAL_CONTINUOUS_ON_SUBSET THEN
 176                           EXISTS_TAC `(:real)` THEN
 177                           REWRITE_TAC[SUBSET_UNIV; lmfun_continuous];
 178                         MP_TAC (SPEC `#1.2317544220903043901` ineq1_th) THEN ANTS_TAC THENL [
 179                           REAL_ARITH_TAC;
 180                           ALL_TAC
 181                         ] THEN
 182                           MP_TAC ((SPEC `#1.2317544220903043901` o GEN_ALL o DISCH_ALL) eq_th1) THEN
 183                           ANTS_TAC THENL [
 184                             REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC;
 185                             ALL_TAC
 186                           ] THEN
 187                           DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
 188                           REAL_ARITH_TAC;
 189                         ALL_TAC
 190                       ] THEN
 191                       MP_TAC (SPEC `#1.2317544220903047` ineq2_th) THEN ANTS_TAC THENL [
 192                         REAL_ARITH_TAC;
 193                         ALL_TAC
 194                       ] THEN
 195                       MP_TAC ((SPEC `#1.2317544220903047` o GEN_ALL o DISCH_ALL) eq_th1) THEN
 196                       ANTS_TAC THENL [
 197                         REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC;
 198                         ALL_TAC
 199                       ] THEN
 200                       DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
 201                       REAL_ARITH_TAC);;
 202
 203
 204 let root_lemma = prove(`!P Q P2 y. y = (@x. P x /\ Q x) /\
 205     (!x. P2 x ==> P x) /\ (?z. P2 z /\ Q z) /\ (!x. P x /\ ~(P2 x) ==> ~(Q x)) ==>
 206     P2 y`, MESON_TAC[]);;
 207
 208
 209 let hminus_interval = prove(`interval_arith hminus (#1.2317544220903043901, #1.2317544220903047)`,
 210    SUBGOAL_THEN `!x lo hi. interval_arith x (lo,hi) = (\x. interval_arith x (lo, hi)) x` MP_TAC THENL [
 211      ASM_REWRITE_TAC[];
 212      ALL_TAC
 213    ] THEN
 214     DISCH_THEN (fun th -> PURE_ONCE_REWRITE_TAC[th]) THEN
 215      MATCH_MP_TAC root_lemma THEN REWRITE_TAC[interval_arith] THEN
 216      EXISTS_TAC `\x. #1.2 <= x /\ x < #1.3` THEN
 217      EXISTS_TAC `\x. marchal_quartic x = lmfun x` THEN
 218      ASM_REWRITE_TAC[Sphere.hminus; CONJ_ASSOC] THEN
 219      REWRITE_TAC[root_th; ineq_th] THEN
 220      REAL_ARITH_TAC);;
 221
 222
 223 add_constant_interval hminus_interval;;
 224
 225 (* end;; *)