Skip to content

Commit

Permalink
Eliminated a number of duplicated theorems (often exact duplicates,
Browse files Browse the repository at this point in the history 
otherwise differing at most in their outer universal quantifiers or
bound variable names):

        BOREL_INDUCT_OPEN_UNIONS_INTERS -> BOREL_INDUCT_UNIONS_INTERS
        CLOSED_SIMPLEX -> SIMPLEX_IMP_CLOSED
        COMPACT_IN_SUBTOPOLOGY_EQ -> COMPACT_IN_SUBTOPOLOGY
        COMPACT_SIMPLEX -> SIMPLEX_IMP_COMPACT
        COMPLEX_DIFFERENTIABLE_COMPOSE -> COMPLEX_DIFFERENTIABLE_COMPOSE_AT
        CONVEX_SIMPLEX -> SIMPLEX_IMP_CONVEX
        DIAGONAL_MATRIX_MUL_EXPLICIT -> MATRIX_MUL_DIAGONAL
        DOT_NORM_NEG -> DOT_NORM_SUB
        FINITE_EMPTY_INTERIOR -> EMPTY_INTERIOR_FINITE
        HAS_VECTOR_DERIVATIVE_UNIQUE_AT -> VECTOR_DERIVATIVE_AT
        HAUSDIST_TRANS -> HAUSDIST_TRIANGLE
        INT_LE_NEG -> INT_LE_NEG2
        INT_LT_NEG -> INT_LT_NEG2
        INT_NEGNEG -> INT_NEG_NEG
        INT_OF_REAL_OF_INT -> int_abstr
        LAMBDA_UNPAIR_THM -> LAMBDA_PAIR
        LIM_NULL_COMPLEX_BOUND -> LIM_NULL_COMPARISON_COMPLEX
        MATRIX_LEFT_INVERTIBLE_NULLSPACE -> MATRIX_LEFT_INVERTIBLE_KER
        MBOUNDED_IFF_FINITE_DIAMETER -> MBOUNDED_ALT
        PSUBSET_MEMBER -> PSUBSET_ALT
        REALLIM_TRANSFORM_BOUND -> REALLIM_NULL_COMPARISON
        REAL_LE_NEG -> REAL_LE_NEG2
        REAL_LT_NEG -> REAL_LT_NEG2
        REAL_NEGNEG -> REAL_NEG_NEG
        REAL_POS_NZ -> REAL_LT_IMP_NZ
        RELATIVE_FRONTIER_CONVEX_HULL_CASES -> RELATIVE_FRONTIER_OF_CONVEX_HULL
        SETDIST_LIPSCHITZ -> SETDIST_SING_TRIANGLE
        num_RECURSION_STD -> num_RECURSION

Also changed the following to be the genuinely distinct theorems that were
presumably intended:

  ABS_DROP (was same as NORM_1)
  ANGLE_EQ_PI_RIGHT (was same as ANGLE_EQ_PI_LEFT)
  CLOSURE_RATIONALS_IN_OPEN_SET (was same as CLOSURE_DYADIC_RATIONALS_IN_OPEN_SET)
  CONNECTED_CONVEX_1_GEN (was same as CONVEX_CONNECTED_1_GEN)

Also added quite a few more new theorems about Baire functions:

        BAIRE_COMPOSE
        BAIRE_CONTINUOUS_COMPOSE
        BAIRE_FSIGMA_PREIMAGE_GEN
        BAIRE_INDICATOR_LOCALLY
        FSIGMA_DISJOINT_GEN
        FSIGMA_GDELTA_DISJOINT
        FSIGMA_GDELTA_GEN
        FSIGMA_LOCALLY_EQ
        FSIGMA_LOCALLY_GEN
        FSIGMA_LOCALLY_TRANS
        GDELTA_FSIGMA_GEN
        GDELTA_LOCALLY_EQ
        GDELTA_LOCALLY_GEN
        GDELTA_LOCALLY_TRANS
        HOMEOMORPHIC_BAIRE_INDICATOR
        HOMEOMORPHIC_COUNTABLE_INTERSECTION_OF_BAIRE_INDICATOR
        HOMEOMORPHIC_COUNTABLE_UNION_OF_BAIRE_INDICATOR
        LOCALLY_BAIRE
        LOCALLY_BAIRE_ALT
        LOCALLY_BAIRE_EXPLICIT
  • Loading branch information
@jrh13
jrh13 committed Aug 28, 2017
1 parent 7b6df60 commit 1bedc13
Show file tree
Hide file tree
Showing 46 changed files with 1,098 additions and 639 deletions.
2 changes: 1 addition & 1 deletion 100/inclusion_exclusion.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -279,7 +279,7 @@ let CARD_SUBSUPERSETS_EVEN_ODD = prove
CARD {t | s SUBSET t /\ t SUBSET u /\ ODD(CARD t)}`,
ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN
REPEAT GEN_TAC THEN WF_INDUCT_TAC `CARD(u:A->bool)` THEN
REWRITE_TAC[PSUBSET_MEMBER] THEN
REWRITE_TAC[PSUBSET_ALT] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
DISCH_THEN(X_CHOOSE_THEN `x:A` STRIP_ASSUME_TAC) THEN
FIRST_X_ASSUM(SUBST_ALL_TAC o MATCH_MP (SET_RULE
Expand Down
10 changes: 5 additions & 5 deletions 100/pnt.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2060,7 +2060,7 @@ let NEWMAN_INGHAM_THEOREM = prove
PATH_IMAGE_NEGATEPATH] THEN
REWRITE_TAC[IN_IMAGE; COMPLEX_RING `Cx(&0) = --x <=> x = Cx(&0)`] THEN
ASM_REWRITE_TAC[UNWIND_THM2] THEN
SIMP_TAC[COMPLEX_EQ; RE_NEG; IM_NEG; RE; IM; REAL_NEG_0; REAL_NEGNEG];
SIMP_TAC[COMPLEX_EQ; RE_NEG; IM_NEG; RE; IM; REAL_NEG_0; REAL_NEG_NEG];
ALL_TAC] THEN
SUBGOAL_THEN
`valid_path(A ++ A') /\
Expand Down Expand Up @@ -3739,7 +3739,7 @@ let REALLIM_LOG1_OVER_LOG = prove
ALL_TAC] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM REAL_ADD_RID] THEN
MATCH_MP_TAC REALLIM_ADD THEN REWRITE_TAC[REALLIM_CONST] THEN
MATCH_MP_TAC REALLIM_TRANSFORM_BOUND THEN
MATCH_MP_TAC REALLIM_NULL_COMPARISON THEN
EXISTS_TAC `\n. inv(&n)` THEN REWRITE_TAC[REALLIM_1_OVER_N] THEN
REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN EXISTS_TAC `16` THEN
X_GEN_TAC `n:num` THEN DISCH_TAC THEN
Expand Down Expand Up @@ -4185,7 +4185,7 @@ let PNT = prove
DISCH_TAC THEN
REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_RDISTRIB] THEN
REWRITE_TAC[GSYM real_div] THEN REWRITE_TAC[GSYM SUM_SUB_NUMSEG] THEN
MATCH_MP_TAC REALLIM_TRANSFORM_BOUND THEN
MATCH_MP_TAC REALLIM_NULL_COMPARISON THEN
EXISTS_TAC `\n. sum(1..n) (\k. &1 / log(&k + &1) pow 2 +
&2 / (&k * log(&k + &1))) /
((&n + &1) / log(&n + &1))` THEN
Expand Down Expand Up @@ -4219,7 +4219,7 @@ let PNT = prove
MATCH_MP_TAC LOG_POS THEN
REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE] THEN ASM_ARITH_TAC;
ALL_TAC] THEN
MATCH_MP_TAC REALLIM_TRANSFORM_BOUND THEN
MATCH_MP_TAC REALLIM_NULL_COMPARISON THEN
EXISTS_TAC `\n. sum(1..n) (\k. &3 / log(&k + &1) pow 2) /
((&n + &1) / log(&n + &1))` THEN
REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN CONJ_TAC THENL
Expand Down Expand Up @@ -4278,7 +4278,7 @@ let PNT = prove
MP_TAC(SPEC `1` (MATCH_MP REAL_SEQ_OFFSET REALLIM_LOG_OVER_N)) THEN
REWRITE_TAC[REAL_INV_DIV; GSYM REAL_OF_NUM_ADD];
ALL_TAC] THEN
MATCH_MP_TAC REALLIM_TRANSFORM_BOUND THEN
MATCH_MP_TAC REALLIM_NULL_COMPARISON THEN
EXISTS_TAC `\n. &2 / log(&n + &1)` THEN CONJ_TAC THENL
[ALL_TAC;
REWRITE_TAC[real_div] THEN MATCH_MP_TAC REALLIM_NULL_LMUL THEN
Expand Down
69 changes: 56 additions & 13 deletions CHANGES
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,30 +8,73 @@
* page: https://github.com/jrh13/hol-light/commits/master *
* *****************************************************************

Thu 24th Aug 2017 passim

Eliminated a number of duplicated theorems (often exact duplicates,
otherwise differing at most in their outer universal quantifiers or
bound variable names):

BOREL_INDUCT_OPEN_UNIONS_INTERS -> BOREL_INDUCT_UNIONS_INTERS
CLOSED_SIMPLEX -> SIMPLEX_IMP_CLOSED
COMPACT_IN_SUBTOPOLOGY_EQ -> COMPACT_IN_SUBTOPOLOGY
COMPACT_SIMPLEX -> SIMPLEX_IMP_COMPACT
COMPLEX_DIFFERENTIABLE_COMPOSE -> COMPLEX_DIFFERENTIABLE_COMPOSE_AT
CONVEX_SIMPLEX -> SIMPLEX_IMP_CONVEX
DIAGONAL_MATRIX_MUL_EXPLICIT -> MATRIX_MUL_DIAGONAL
DOT_NORM_NEG -> DOT_NORM_SUB
FINITE_EMPTY_INTERIOR -> EMPTY_INTERIOR_FINITE
HAS_VECTOR_DERIVATIVE_UNIQUE_AT -> VECTOR_DERIVATIVE_AT
HAUSDIST_TRANS -> HAUSDIST_TRIANGLE
INT_LE_NEG -> INT_LE_NEG2
INT_LT_NEG -> INT_LT_NEG2
INT_NEGNEG -> INT_NEG_NEG
INT_OF_REAL_OF_INT -> int_abstr
LAMBDA_UNPAIR_THM -> LAMBDA_PAIR
LIM_NULL_COMPLEX_BOUND -> LIM_NULL_COMPARISON_COMPLEX
MATRIX_LEFT_INVERTIBLE_NULLSPACE -> MATRIX_LEFT_INVERTIBLE_KER
MBOUNDED_IFF_FINITE_DIAMETER -> MBOUNDED_ALT
PSUBSET_MEMBER -> PSUBSET_ALT
REALLIM_TRANSFORM_BOUND -> REALLIM_NULL_COMPARISON
REAL_LE_NEG -> REAL_LE_NEG2
REAL_LT_NEG -> REAL_LT_NEG2
REAL_NEGNEG -> REAL_NEG_NEG
REAL_POS_NZ -> REAL_LT_IMP_NZ
RELATIVE_FRONTIER_CONVEX_HULL_CASES -> RELATIVE_FRONTIER_OF_CONVEX_HULL
SETDIST_LIPSCHITZ -> SETDIST_SING_TRIANGLE
num_RECURSION_STD -> num_RECURSION

Also changed the following to be the genuinely distinct theorems that were
presumably intended:

ABS_DROP (was same as NORM_1)
ANGLE_EQ_PI_RIGHT (was same as ANGLE_EQ_PI_LEFT)
CLOSURE_RATIONALS_IN_OPEN_SET (was same as CLOSURE_DYADIC_RATIONALS_IN_OPEN_SET)
CONNECTED_CONVEX_1_GEN (was same as CONVEX_CONNECTED_1_GEN)

Fri 18th Aug 2017 real.ml

Added quite a few new and fairly basic real number theorems (some of the convex
bounds ones were moved out of Multivariate/misc.ml).

REAL_ABS_LE_SQRT =
|- !x y. abs (sqrt x - sqrt y) <= sqrt (&2 * abs (x - y))

REAL_ABS_LE_SQRT_POS =
|- !x y. &0 <= x /\ &0 <= y ==> abs (sqrt x - sqrt y) <= sqrt (abs (x - y))

REAL_ABS_SQRT =
|- !x. abs (sqrt x) = sqrt (abs x)

REAL_CONVEX_BOUND2_LE =
|- !x y a u v.
x <= a /\ y <= b /\ &0 <= u /\ &0 <= v /\ u + v = &1
==> u * x + v * y <= u * a + v * b

REAL_CONVEX_BOUND2_LT =
|- !x y a u v.
x < a /\ y < b /\ &0 <= u /\ &0 <= v /\ u + v = &1
==> u * x + v * y < u * a + v * b

REAL_CONVEX_BOUNDS_LE =
|- !x y a b u v.
a <= x /\
Expand All @@ -42,35 +85,35 @@ bounds ones were moved out of Multivariate/misc.ml).
&0 <= v /\
u + v = &1
==> a <= u * x + v * y /\ u * x + v * y <= b

REAL_CONVEX_BOUNDS_LT =
|- !x y a b u v.
a < x /\ x < b /\ a < y /\ y < b /\ &0 <= u /\ &0 <= v /\ u + v = &1
==> a < u * x + v * y /\ u * x + v * y < b

REAL_CONVEX_BOUND_GE =
|- !x y a u v.
a <= x /\ a <= y /\ &0 <= u /\ &0 <= v /\ u + v = &1
==> a <= u * x + v * y

REAL_CONVEX_BOUND_GT =
|- !x y a u v.
a < x /\ a < y /\ &0 <= u /\ &0 <= v /\ u + v = &1
==> a < u * x + v * y

REAL_CONVEX_BOUND_LE =
|- !x y a u v.
x <= a /\ y <= a /\ &0 <= u /\ &0 <= v /\ u + v = &1
==> u * x + v * y <= a

REAL_CONVEX_BOUND_LT =
|- !x y a u v.
x < a /\ y < a /\ &0 <= u /\ &0 <= v /\ u + v = &1
==> u * x + v * y < a

REAL_DIV_EQ_1 =
|- !x y. x / y = &1 <=> x = y /\ ~(x = &0) /\ ~(y = &0)

SQRT_EQ_1 =
|- !x. sqrt x = &1 <=> x = &1

Expand Down
2 changes: 1 addition & 1 deletion Formal_ineqs/arith/float_theory.hl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ let FLOAT_F_bound = (GEN_ALL o prove)(`num_exp n1 e1 <= num_exp n2 e2

let FLOAT_T_bound = (GEN_ALL o prove)(`num_exp n1 e1 <= num_exp n2 e2
==> float_num T n2 e2 <= float_num T n1 e1`,
REWRITE_TAC[FLOAT_NEG_T; REAL_LE_NEG; FLOAT_F_bound]);;
REWRITE_TAC[FLOAT_NEG_T; REAL_LE_NEG2; FLOAT_F_bound]);;



Expand Down
2 changes: 1 addition & 1 deletion Formal_ineqs/jordan/real_ext.hl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -212,7 +212,7 @@ let REAL_PROP_POS_ATN = ATN_POS_LT;; (* |- &0 < atn x = &0 < x *)
(* ------------------------------------------------------------------ *)

(* renamed from REAL_MK_NZ_OF_POS *)
let REAL_MK_NZ_POS = REAL_POS_NZ (* |- !x. &0 < x ==> ~(x = &0) *);;
let REAL_MK_NZ_POS = REAL_LT_IMP_NZ (* |- !x. &0 < x ==> ~(x = &0) *);;
let REAL_MK_NZ_EXP = REAL_EXP_NZ;; (* |- !x. ~(exp x = &0) *)

(* ------------------------------------------------------------------ *)
Expand Down
6 changes: 3 additions & 3 deletions Formal_ineqs/taylor/theory/multivariate_taylor-compiled.hl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1506,7 +1506,7 @@ let m_taylor_lower_bound = section_proof ["domain";"y";"w";"f";"dd_bound";"lo";"
((((use_arg_then "REAL_LE_TRANS") (disch_tac [])) THEN (clear_assumption "REAL_LE_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`(f y + s) - dd_bound / &2`))) (term_tac exists_tac)) THEN ((((use_arg_then "ineq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andbT")(thm_tac (new_rewrite [] []))))));
(((fun arg_tac -> (fun arg_tac -> arg_tac (Arg_theorem (REWRITE_RULE[GSYM IMP_IMP] REAL_LE_TRANS))) (fun fst_arg -> (use_arg_then "total_bound") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN (DISCH_THEN apply_tac));
((repeat_tactic 1 9 (((use_arg_then "real_sub")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "REAL_NEG_ADD")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_ADD_ASSOC")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_LE_RADD")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_LE_ADD2")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "f_bound")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andTb")(thm_tac (new_rewrite [] [])))));
((THENL_LAST) ((((use_arg_then "REAL_LE_TRANS") (disch_tac [])) THEN (clear_assumption "REAL_LE_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`--abs s`))) (term_tac exists_tac)) THEN (((use_arg_then "REAL_LE_NEG")(thm_tac (new_rewrite [] [])))) THEN (split_tac)) ((arith_tac) THEN (done_tac)));
((THENL_LAST) ((((use_arg_then "REAL_LE_TRANS") (disch_tac [])) THEN (clear_assumption "REAL_LE_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`--abs s`))) (term_tac exists_tac)) THEN (((use_arg_then "REAL_LE_NEG2")(thm_tac (new_rewrite [] [])))) THEN (split_tac)) ((arith_tac) THEN (done_tac)));
(((((use_arg_then "s_def")(gsym_then (thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "SUM_ABS_LE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "FINITE_NUMSEG")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andTb")(thm_tac (new_rewrite [] []))))) THEN (move ["i"]) THEN (move ["i_ineq"]) THEN (simp_tac));
(((((use_arg_then "REAL_ABS_MUL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_LE_MUL2")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "REAL_ABS_POS")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "REAL_LE_REFL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "VECTOR_SUB_COMPONENT")(thm_tac (new_rewrite [] [])))) THEN (((fun arg_tac -> (use_arg_then "domain_width") (fun fst_arg -> (use_arg_then "domainH") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg)))(thm_tac (new_rewrite [] []))))) THEN (done_tac));
];;
Expand All @@ -1525,7 +1525,7 @@ let m_taylor_bounds = section_proof ["domain";"y";"w";"f";"dd_bound";"lo";"hi";"
(((((use_arg_then "m_bounded_on_int")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "interval_arith")(thm_tac (new_rewrite [] [])))))) THEN (move ["domainH"]) THEN (move ["df"]) THEN (move ["errorH"]) THEN (case THEN ((move ["f_lo"]) THEN (move ["f_hi"]))) THEN (move ["err"]) THEN (move ["lo_ineq"]) THEN (move ["hi_ineq"]) THEN (move ["p"]) THEN (move ["p_in"]));
(((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "m_taylor_lower_bound") (fun fst_arg -> (use_arg_then "domainH") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "df") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "errorH") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "f_lo") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "lo_bound") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))));
(((((use_arg_then "p_in")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andbT")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "REAL_LE_TRANS") (disch_tac [])) THEN (clear_assumption "REAL_LE_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`lo - err_bound`))) (term_tac exists_tac)));
(((((use_arg_then "lo_ineq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andTb")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "real_sub")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "REAL_LE_ADD2")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_LE_REFL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_LE_NEG")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(((((use_arg_then "lo_ineq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andTb")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 1 9 (((use_arg_then "real_sub")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "REAL_LE_ADD2")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_LE_REFL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_LE_NEG2")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
(((fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (fun arg_tac -> (use_arg_then "m_taylor_upper_bound") (fun fst_arg -> (use_arg_then "domainH") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "df") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "errorH") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "f_hi") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (fun fst_arg -> (use_arg_then "hi_bound") (fun snd_arg -> combine_args_then arg_tac fst_arg snd_arg))) (disch_tac [])) THEN BETA_TAC THEN (((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))) THEN ((TRY done_tac)));
(((((use_arg_then "p_in")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andbT")(thm_tac (new_rewrite [] []))))) THEN (((use_arg_then "REAL_LE_TRANS") (disch_tac [])) THEN (clear_assumption "REAL_LE_TRANS") THEN (DISCH_THEN apply_tac)) THEN ((fun arg_tac -> arg_tac (Arg_term (`hi + err_bound`))) (term_tac exists_tac)));
(((((use_arg_then "hi_ineq")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andbT")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_LE_LADD")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
Expand Down Expand Up @@ -2238,7 +2238,7 @@ let diff2c_sqrt_compose = section_proof ["f"]
((THENL_LAST) (split_tac) (((fun arg_tac -> arg_tac (Arg_term (`f x`))) (term_tac exists_tac)) THEN (done_tac)));
((THENL_ROT (-1)) ((((use_arg_then "REAL_CONTINUOUS_NEG")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_CONTINUOUS_INV_ATREAL")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "REAL_CONTINUOUS_LMUL")(thm_tac (new_rewrite [] []))))));
((THENL_FIRST) (((((use_arg_then "REAL_ENTIRE")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "negb_or")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "andTb")(thm_tac (new_rewrite [] []))))) THEN (split_tac)) ((arith_tac) THEN (done_tac)));
((((use_arg_then "SQRT_EQ_0_COMPAT")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "REAL_POW_NZ")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "REAL_POS_NZ")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "REAL_POW_LE")(thm_tac (new_rewrite [] [])))));
((((use_arg_then "SQRT_EQ_0_COMPAT")(thm_tac (new_rewrite [] [])))) THEN (repeat_tactic 0 10 (((use_arg_then "REAL_POW_NZ")(thm_tac (new_rewrite [] []))))) THEN (repeat_tactic 0 10 (((use_arg_then "REAL_LT_IMP_NZ")(thm_tac (new_rewrite [] []))))) THEN ((TRY done_tac)) THEN (((use_arg_then "REAL_POW_LE")(thm_tac (new_rewrite [] [])))));
((((use_arg_then "fn0") (disch_tac [])) THEN (clear_assumption "fn0") THEN BETA_TAC) THEN (arith_tac) THEN (done_tac));
((fun arg_tac -> arg_tac (Arg_term (`(\x. sqrt (x pow 3)) = (sqrt o (\x. x pow 3))`))) (term_tac (have_gen_tac [](((conv_thm_tac DISCH_THEN)(thm_tac (new_rewrite [] [])))))));
(((((use_arg_then "FUN_EQ_THM")(thm_tac (new_rewrite [] [])))) THEN (((use_arg_then "o_THM")(thm_tac (new_rewrite [] []))))) THEN (done_tac));
Expand Down
Loading

0 comments on commit 1bedc13

Please sign in to comment.