1 (* Gives an interval approximation of hminus *)
2 (* hminus ~ 1.2317544220903043901 *)
4 (* load_path := "/mnt/Repository/formal_ineqs" :: !load_path;; *)
6 (* tested with base = 100 *)
7 needs "verifier/m_verifier_main.hl";;
9 (* module Hminus = struct *)
11 open M_verifier_main;;
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);;
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
22 let eq_tm = `marchal_quartic x - lmfun x`;;
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;;
28 let eq_tm1 = (rand o concl) eq_th1 and
29 eq_tm2 = (rand o concl) eq_th2;;
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);;
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`;;
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);;
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;;
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
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;
59 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) 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
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
76 let marchal_quartic_continuous_at = prove(`!x. marchal_quartic real_continuous atreal x`,
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];
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];
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];
100 MATCH_MP_TAC REAL_CONTINUOUS_LMUL THEN
101 REWRITE_TAC[REAL_CONTINUOUS_AT_ID]);;
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])`
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));
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`
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));
149 (* Lemma lmfun_continuous *)
150 let lmfun_continuous = section_proof []
151 `lmfun real_continuous_on UNIV`
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));
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 [
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];
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 [
182 MP_TAC ((SPEC `#1.2317544220903043901` o GEN_ALL o DISCH_ALL) eq_th1) THEN
184 REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC;
187 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
191 MP_TAC (SPEC `#1.2317544220903047` ineq2_th) THEN ANTS_TAC THENL [
195 MP_TAC ((SPEC `#1.2317544220903047` o GEN_ALL o DISCH_ALL) eq_th1) THEN
197 REWRITE_TAC[Sphere.h0] THEN REAL_ARITH_TAC;
200 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
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[]);;
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 [
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
223 add_constant_interval hminus_interval;;