From 6b8beea8acf40d09b5cbce25c4b8ccaeb29b7c90 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Fri, 7 Jun 2024 11:10:10 +1000 Subject: [PATCH 1/3] Extended domain of rpow (powr) --- src/real/analysis/derivativeScript.sml | 1 + src/real/analysis/limScript.sml | 26 +- src/real/analysis/real_topologyScript.sml | 52 +++- src/real/analysis/transcScript.sml | 280 ++++++++++++++-------- 4 files changed, 232 insertions(+), 127 deletions(-) diff --git a/src/real/analysis/derivativeScript.sml b/src/real/analysis/derivativeScript.sml index 7e32ec0e0d..eba387f786 100644 --- a/src/real/analysis/derivativeScript.sml +++ b/src/real/analysis/derivativeScript.sml @@ -1704,6 +1704,7 @@ QED (* CONTINUOUS_ON_EXP *) (* ------------------------------------------------------------------------- *) +(* See limTheory.HAS_DERIVATIVE_POW' for a better version without sum *) val HAS_DERIVATIVE_POW = store_thm ("HAS_DERIVATIVE_POW", ``!q0 n. ((\q. q pow n) has_derivative diff --git a/src/real/analysis/limScript.sml b/src/real/analysis/limScript.sml index f701f5fcd6..6e0265a5b5 100644 --- a/src/real/analysis/limScript.sml +++ b/src/real/analysis/limScript.sml @@ -5,8 +5,8 @@ open HolKernel Parse bossLib boolLib; open numLib reduceLib pairLib pairTheory arithmeticTheory numTheory jrhUtils - prim_recTheory realTheory realLib metricTheory netsTheory combinTheory; -open pred_setTheory mesonLib; + prim_recTheory realTheory realLib metricTheory netsTheory combinTheory + pred_setTheory mesonLib hurdUtils; open topologyTheory real_topologyTheory derivativeTheory seqTheory; @@ -15,17 +15,9 @@ val _ = ParseExtras.temp_loose_equality() val _ = Parse.reveal "B"; -(* mini hurdUtils *) -val Know = Q_TAC KNOW_TAC; -val Suff = Q_TAC SUFF_TAC; -fun wrap a = [a]; -val Rewr = DISCH_THEN (REWRITE_TAC o wrap); -val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); -val POP_ORW = POP_ASSUM (ONCE_REWRITE_TAC o wrap); -val art = ASM_REWRITE_TAC; - val tendsto = netsTheory.tendsto; (* conflict with real_topologyTheory.tendsto *) val GEN_ALL = hol88Lib.GEN_ALL; (* this gives old (reverted) variable orders *) +val EXACT_CONV = jrhUtils.EXACT_CONV; (* there's one also in hurdUtils *) (*---------------------------------------------------------------------------*) (* Specialize nets theorems to the pointwise limit of real->real functions *) @@ -700,6 +692,18 @@ val DIFF_POW = store_thm("DIFF_POW", REWRITE_TAC[ONE, pow] THEN REWRITE_TAC[SYM ONE, REAL_MUL_RID]]); +val lemma = REWRITE_RULE [diffl_has_derivative, Once REAL_MUL_COMM] DIFF_POW; + +Theorem HAS_DERIVATIVE_POW' : + !n x. ((\x. x pow n) has_derivative (\y. &n * x pow (n - 1) * y)) (at x) +Proof + REWRITE_TAC [lemma] +QED + +(* !n x. ((\x. x pow n) has_vector_derivative &n * x pow (n - 1)) (at x) *) +Theorem HAS_VECTOR_DERIVATIVE_POW = + REWRITE_RULE [diffl_has_vector_derivative] DIFF_POW + (*---------------------------------------------------------------------------*) (* Now power of -1 (then differentiation of inverses follows from chain rule)*) (*---------------------------------------------------------------------------*) diff --git a/src/real/analysis/real_topologyScript.sml b/src/real/analysis/real_topologyScript.sml index e4995ba524..49bd5eb737 100644 --- a/src/real/analysis/real_topologyScript.sml +++ b/src/real/analysis/real_topologyScript.sml @@ -22,7 +22,7 @@ open numTheory numLib unwindLib tautLib prim_recTheory combinTheory quotientTheory arithmeticTheory realTheory real_sigmaTheory jrhUtils pairTheory boolTheory pred_setTheory optionTheory sumTheory InductiveDefinition listTheory mesonLib - RealArith realSimps topologyTheory metricTheory netsTheory; + realLib topologyTheory metricTheory netsTheory; open wellorderTheory cardinalTheory permutesTheory iterateTheory hurdUtils; @@ -6229,22 +6229,39 @@ val LIM_TRANSFORM_WITHIN_SET_IMP = store_thm ("LIM_TRANSFORM_WITHIN_SET_IMP", (* Common case assuming being away from some crucial point like 0. *) (* ------------------------------------------------------------------------- *) -val LIM_TRANSFORM_AWAY_WITHIN = store_thm ("LIM_TRANSFORM_AWAY_WITHIN", - ``!f:real->real g a b s. ~(a = b) /\ +Theorem LIM_TRANSFORM_AWAY_WITHIN_lemma[local] : + !f:real->real g a b s. ~(a = b) /\ (!x. x IN s /\ ~(x = a) /\ ~(x = b) ==> (f(x) = g(x))) /\ - (f --> l) (at a within s) ==> (g --> l) (at a within s)``, + (f --> l) (at a within s) ==> (g --> l) (at a within s) +Proof REPEAT STRIP_TAC THEN MATCH_MP_TAC LIM_TRANSFORM_WITHIN THEN MAP_EVERY EXISTS_TAC [``f:real->real``, ``dist(a:real,b)``] THEN ASM_REWRITE_TAC[GSYM DIST_NZ] THEN X_GEN_TAC ``y:real`` THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN - ASM_MESON_TAC[DIST_SYM, REAL_LT_REFL]); + ASM_MESON_TAC[DIST_SYM, REAL_LT_REFL] +QED -val LIM_TRANSFORM_AWAY_AT = store_thm ("LIM_TRANSFORM_AWAY_AT", - ``!f:real->real g a b. ~(a = b) /\ - (!x. ~(x = a) /\ ~(x = b) ==> (f(x) = g(x))) /\ - (f --> l) (at a) ==> (g --> l) (at a)``, +(* NOTE: removed the unused quantifier ‘b’ *) +Theorem LIM_TRANSFORM_AWAY_WITHIN : + !f:real->real g a s l. + (!x. x IN s /\ ~(x = a) ==> (f(x) = g(x))) /\ + (f --> l) (at a within s) ==> (g --> l) (at a within s) +Proof + rpt STRIP_TAC + >> MATCH_MP_TAC LIM_TRANSFORM_AWAY_WITHIN_lemma + >> qexistsl_tac [‘f’, ‘a + 1’] >> rw [] + >> REAL_ARITH_TAC +QED + +(* NOTE: removed the unused quantifier ‘b’ *) +Theorem LIM_TRANSFORM_AWAY_AT : + !f:real->real g a l. + (!x. ~(x = a) ==> (f(x) = g(x))) /\ + (f --> l) (at a) ==> (g --> l) (at a) +Proof ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN - MESON_TAC[LIM_TRANSFORM_AWAY_WITHIN]); + MESON_TAC[LIM_TRANSFORM_AWAY_WITHIN] +QED (* ------------------------------------------------------------------------- *) (* Alternatively, within an open set. *) @@ -6261,6 +6278,21 @@ val LIM_TRANSFORM_WITHIN_OPEN = store_thm ("LIM_TRANSFORM_WITHIN_OPEN", STRIP_TAC THEN EXISTS_TAC ``e:real`` THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SUBSET_DEF, IN_BALL] THEN ASM_MESON_TAC[DIST_NZ, DIST_SYM]); +Theorem LIM_TRANSFORM_WITHIN_OPEN_EQ : + !f g:real->real s a l. + open s /\ a IN s /\ (!x. x IN s /\ ~(x = a) ==> (f x = g x)) ==> + ((f --> l) (at a) <=> (g --> l) (at a)) +Proof + rpt STRIP_TAC + >> EQ_TAC >> DISCH_TAC + >| [ (* goal 1 (of 2) *) + MATCH_MP_TAC LIM_TRANSFORM_WITHIN_OPEN \\ + qexistsl_tac [‘f’, ‘s’] >> rw [], + (* goal 2 (of 2) *) + MATCH_MP_TAC LIM_TRANSFORM_WITHIN_OPEN \\ + qexistsl_tac [‘g’, ‘s’] >> rw [] ] +QED + val LIM_TRANSFORM_WITHIN_OPEN_IN = store_thm ("LIM_TRANSFORM_WITHIN_OPEN_IN", ``!f g:real->real s t a l. open_in (subtopology euclidean t) s /\ a IN s /\ diff --git a/src/real/analysis/transcScript.sml b/src/real/analysis/transcScript.sml index c38a804b46..76ac931c3f 100644 --- a/src/real/analysis/transcScript.sml +++ b/src/real/analysis/transcScript.sml @@ -25,7 +25,7 @@ open reduceLib numTheory prim_recTheory arithmeticTheory - realTheory realSimps realLib + realTheory realLib metricTheory netsTheory real_sigmaTheory @@ -33,7 +33,7 @@ open reduceLib jrhUtils Diff pred_setTheory - mesonLib; + mesonLib hurdUtils; open iterateTheory real_topologyTheory derivativeTheory; open seqTheory limTheory powserTheory; @@ -41,14 +41,6 @@ open seqTheory limTheory powserTheory; val _ = new_theory "transc"; val _ = Parse.reveal "B"; -(* Mini hurdUtils *) -val Suff = Q_TAC SUFF_TAC; -val Know = Q_TAC KNOW_TAC; -fun wrap a = [a]; -val Rewr' = DISCH_THEN (ONCE_REWRITE_TAC o wrap); -val POP_ORW = POP_ASSUM (ONCE_REWRITE_TAC o wrap); -val art = ASM_REWRITE_TAC; - val MVT = limTheory.MVT; val ROLLE = limTheory.ROLLE; val summable = seqTheory.summable; @@ -2664,30 +2656,64 @@ Theorem DIFF_LN_COMPOSITE'[difftool] = SPEC_ALL DIFF_LN_COMPOSITE (* Exponentiation with real exponents (rpow) *) (* ------------------------------------------------------------------------- *) -fun K_TAC _ = ALL_TAC; +Theorem powr_lemma[local] : + !n a. 0 < a ==> exp (ln a * &n) = a pow n +Proof + Induct_on ‘n’ + >- RW_TAC real_ss [pow, POW_1, GSYM EXP_0] + >> RW_TAC std_ss [pow, REAL, REAL_LDISTRIB, EXP_ADD, REAL_MUL_RID] + >> ‘exp (ln a) = a’ by PROVE_TAC [EXP_LN] + >> POP_ORW + >> REWRITE_TAC [Once REAL_MUL_COMM] +QED + +(* New definition of powr (rpow) *) +local + val thm = Q.prove ( + ‘?f :real -> real -> real. + (!a b. 0 < a ==> f a b = exp (b * ln a)) /\ + (!b. 0 < b ==> f 0 b = 0) /\ + (!a n. f a &n = a pow n /\ f a (-&SUC n) = inv (a pow (SUC n)))’, + (* proof *) + Q.EXISTS_TAC ‘\a b. if 0 < a then exp (b * ln a) else + if a = 0 /\ 0 < b then 0 else + if ?n. b = &n then a pow (flr b) else + if ?n. -b = &n then inv (a pow (flr (-b))) else 0’ + >> rw [NUM_FLOOR_EQNS] (* 2 subgoals *) + >| [ (* goal 1 (of 2) *) + MATCH_MP_TAC powr_lemma >> art [], + (* goal 2 (of 2) *) + RW_TAC std_ss [REAL_MUL_LNEG, EXP_NEG] \\ + AP_TERM_TAC \\ + MATCH_MP_TAC powr_lemma >> art [] ]); +in + (* |- (!a b. 0 < a ==> a powr b = exp (b * ln a)) /\ + (!b. 0 < b ==> 0 powr b = 0) /\ + !a n. a powr &n = a pow n /\ + a powr -&SUC n = inv (a pow SUC n) + *) + val powr_def = new_specification ("powr_def", ["powr"], thm); +end; + +(* Infix syntax: ‘a powr b’ *) +val _ = set_fixity "powr" (Infixr 700); -(* Definition *) +(* NOTE: the name "rpow" is for backward compatibility purposes *) +Overload rpow[inferior] = “$powr” val _ = set_fixity "rpow" (Infixr 700); -val rpow = Define `a rpow b = exp (b * ln a)`; - -(* Properties *) +(* |- !a b. 0 < a ==> powr a b = exp (b * ln a) *) +Theorem rpow_def = cj 1 powr_def -val GEN_RPOW = store_thm - ("GEN_RPOW", - ``! a n. 0 < a ==> (a pow n = a rpow &n)``, - Induct_on `n` THENL [ - RW_TAC real_ss [pow,POW_1, rpow, GSYM EXP_0], +val rpow = rpow_def; -GEN_TAC THEN - RW_TAC std_ss[rpow,pow,REAL,REAL_RDISTRIB,EXP_ADD,REAL_MUL_LID] THEN +(* Properties of ‘powr’ / ‘rpow’ *) - KNOW_TAC ``exp(ln a)= a`` THEN1 - PROVE_TAC[EXP_LN] THEN - DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN - KNOW_TAC ``a* exp (&n * ln a) = exp (&n * ln a)*a`` THEN1 - RW_TAC std_ss[REAL_MUL_COMM] THEN - DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC]); +Theorem GEN_RPOW : + !a n. 0 < a ==> (a pow n = a rpow &n) +Proof + rw [rpow, powr_lemma] +QED val RPOW_SUC_N = store_thm ("RPOW_SUC_N", @@ -2698,64 +2724,78 @@ val RPOW_SUC_N = store_thm DISCH_TAC THEN ONCE_ASM_REWRITE_TAC[] THEN RW_TAC std_ss [GEN_RPOW]) ; -val RPOW_0= store_thm - ("RPOW_0", - ``! a. (0 < a)==> (a rpow &0 = &1)``, - RW_TAC std_ss [rpow]THEN - RW_TAC std_ss [REAL_MUL_LZERO]THEN - RW_TAC std_ss [EXP_0]); +(* NOTE: removed ‘0 < a’ under the new definition *) +Theorem RPOW_0 : + !a. a rpow &0 = &1 +Proof + rw [powr_def] +QED -val RPOW_1= store_thm - ("RPOW_1", - ``! a. (0 < a)==> ( a rpow &1 = a)``, - RW_TAC std_ss [GSYM GEN_RPOW,POW_1]); +(* NOTE: removed ‘0 < a’ under the new definition *) +Theorem RPOW_1 : + !a. a rpow &1 = a +Proof + rw [powr_def] +QED -val ONE_RPOW= store_thm - ("ONE_RPOW", - ``! a. (0 < a)==> (1 rpow a = 1)``, -RW_TAC real_ss [rpow,LN_1,EXP_0]); +(* NOTE: removed ‘0 < a’ (even under the old definition) *) +Theorem ONE_RPOW : + !a. 1 rpow a = 1 +Proof + rw [rpow, LN_1, EXP_0] +QED val RPOW_POS_LT= store_thm ("RPOW_POS_LT", ``! a b. (0 < a)==> (0 < a rpow b)``, RW_TAC std_ss [rpow, EXP_POS_LT]); -val RPOW_NZ= store_thm - ("RPOW_NZ", - ``! a b. (0 <> a)==> ( a rpow b <>0)``, -RW_TAC std_ss [rpow,EXP_NZ]); - +(* NOTE: the antecedent has changed from ‘0 <> a’ to ‘0 < a’ *) +Theorem RPOW_NZ : + !a b. 0 < a ==> a rpow b <> 0 +Proof + RW_TAC std_ss [rpow, EXP_NZ] +QED val LN_RPOW= store_thm ("LN_RPOW", ``! a b. (0 < a)==> (ln (a rpow b)= (b*ln a))``, RW_TAC std_ss [rpow,LN_EXP]); -val RPOW_ADD= store_thm - ("RPOW_ADD", - ``! a b c. a rpow (b + c)= (a rpow b)*(a rpow c)``, - RW_TAC std_ss [rpow, EXP_ADD, REAL_RDISTRIB] ); +(* NOTE: added antecedent ‘0 < a’ under the new definition *) +Theorem RPOW_ADD : + !a b c. 0 < a ==> a rpow (b + c)= (a rpow b)*(a rpow c) +Proof + RW_TAC std_ss [rpow, EXP_ADD, REAL_RDISTRIB] +QED -val RPOW_ADD_MUL= store_thm - ("RPOW_ADD_MUL", - ``! a b c. a rpow (b + c)* a rpow (-b)= (a rpow c)``, +(* NOTE: added antecedent ‘0 < a’ under the new definition *) +Theorem RPOW_ADD_MUL : + !a b c. 0 < a ==> a rpow (b + c)* a rpow (-b)= (a rpow c) +Proof RW_TAC std_ss [rpow, REAL_RDISTRIB, GSYM EXP_ADD]THEN KNOW_TAC`` ((b * ln a + c * ln a + -b * ln a)=(b * ln a -b * ln a + c*ln a)) ``THEN1 REAL_ARITH_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM K_TAC THEN KNOW_TAC``((b * ln a - b * ln a + c * ln a) = (c*ln a )) ``THEN1 REAL_ARITH_TAC THEN - RW_TAC real_ss []); + RW_TAC real_ss [] +QED -val RPOW_SUB= store_thm - ("RPOW_SUB", - ``! a b c. a rpow (b - c)= (a rpow b)/(a rpow c)``, -RW_TAC std_ss [rpow, REAL_SUB_RDISTRIB, EXP_SUB]); +(* NOTE: added antecedent ‘0 < a’ under the new definition *) +Theorem RPOW_SUB : + !a b c. 0 < a ==> a rpow (b - c) = (a rpow b)/(a rpow c) +Proof + RW_TAC std_ss [rpow, REAL_SUB_RDISTRIB, EXP_SUB] +QED -val RPOW_DIV= store_thm - ("RPOW_DIV", - ``! a b c. (0 < a)/\ (0 ((a/b) rpow c= (a rpow c)/(b rpow c))``, - RW_TAC std_ss [rpow ,LN_DIV, REAL_SUB_LDISTRIB, EXP_SUB]); +Theorem RPOW_DIV : + !a b c. 0 < a /\ 0 < b ==> ((a/b) rpow c = (a rpow c)/(b rpow c)) +Proof + rpt STRIP_TAC + >> ‘0 < a / b’ by PROVE_TAC [REAL_LT_DIV] + >> RW_TAC std_ss [rpow, LN_DIV, REAL_SUB_LDISTRIB, EXP_SUB] +QED val RPOW_INV= store_thm ("RPOW_INV", @@ -2763,24 +2803,31 @@ val RPOW_INV= store_thm RW_TAC real_ss [rpow, REAL_INV_1OVER, LN_DIV, REAL_SUB_LDISTRIB, EXP_SUB, LN_1, EXP_0]); +Theorem RPOW_MUL : + !a b c. 0 < a /\ 0 < b ==> (((a*b) rpow c) = (a rpow c)*(b rpow c)) +Proof + rpt STRIP_TAC + >> ‘0 < a * b’ by PROVE_TAC [REAL_LT_MUL] + >> RW_TAC std_ss [rpow, LN_MUL, REAL_LDISTRIB, EXP_ADD] +QED -val RPOW_MUL= store_thm - ("RPOW_MUL", - ``! a b c. (0 (((a*b) rpow c)=(a rpow c)*(b rpow c))``, -RW_TAC std_ss [rpow, LN_MUL, REAL_LDISTRIB, EXP_ADD]); - -val RPOW_RPOW= store_thm - ("RPOW_RPOW", - ``! a b c. (0 ((a rpow b) rpow c = a rpow (b*c))``, - RW_TAC real_ss [rpow, LN_EXP, REAL_MUL_ASSOC] THEN - PROVE_TAC[ REAL_MUL_COMM] ); +Theorem RPOW_RPOW : + !a b c. 0 < a ==> ((a rpow b) rpow c = a rpow (b*c)) +Proof + rpt STRIP_TAC + >> ‘0 < a powr b’ by PROVE_TAC [RPOW_POS_LT] + >> RW_TAC real_ss [rpow, LN_EXP, REAL_MUL_ASSOC] + >> PROVE_TAC [REAL_MUL_COMM] +QED Theorem RPOW_LT : !(a:real) (b:real) (c:real). 1 < a ==> (a rpow b < a rpow c <=> b < c) Proof - RW_TAC std_ss [rpow] THEN - KNOW_TAC`` exp (b * ln a) < exp (c * ln a) <=> (b*ln a < c*ln a)`` THEN1 - RW_TAC real_ss [EXP_MONO_LT] THEN + rpt STRIP_TAC + >> ‘0 < a’ by PROVE_TAC [REAL_LT_TRANS, REAL_LT_01] + >> RW_TAC std_ss [rpow] + >> KNOW_TAC ``exp (b * ln a) < exp (c * ln a) <=> (b*ln a < c*ln a)`` + >- RW_TAC real_ss [EXP_MONO_LT] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM K_TAC THEN KNOW_TAC``((b:real)*ln a < (c:real)*ln a) <=> (b < c)`` THENL [ MATCH_MP_TAC REAL_LT_RMUL THEN @@ -2802,9 +2849,11 @@ Proof QED Theorem RPOW_LE : - !a b c. 1 < a ==> (a rpow b <= a rpow c <=> b <= c) + !a b c. 1 < a ==> (a rpow b <= a rpow c <=> b <= c) Proof - RW_TAC std_ss [rpow] THEN + rpt STRIP_TAC + >> ‘0 < a’ by PROVE_TAC [REAL_LT_TRANS, REAL_LT_01] + >> RW_TAC std_ss [rpow] THEN KNOW_TAC ``exp ((b:real) * ln a) <= exp ((c:real) * ln a) <=> ((b:real)*ln a <= (c:real)*ln a)`` THEN1 RW_TAC real_ss [EXP_MONO_LE] THEN @@ -2855,9 +2904,10 @@ QED Theorem RPOW_UNIQ_BASE : !a b c. 0 < a /\ 0 < c /\ 0 <> b /\ (a rpow b = c rpow b) ==> (a = c) Proof - RW_TAC std_ss [rpow, GSYM LN_INJ] THEN - POP_ASSUM MP_TAC THEN - KNOW_TAC ``(exp (b * ln a) = exp (b * ln c)) <=> + rpt STRIP_TAC + >> rfs [rpow, GSYM LN_INJ] + >> POP_ASSUM MP_TAC + >> KNOW_TAC ``(exp (b * ln a) = exp (b * ln c)) <=> (ln (exp (b * ln a)) = ln (exp (b * ln c)))``THEN1 PROVE_TAC[LN_EXP]THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM K_TAC THEN @@ -2868,9 +2918,11 @@ QED Theorem RPOW_UNIQ_EXP : !a b c. 1 < a /\ 0 < c /\ 0 < b /\ (a rpow b = a rpow c) ==> (b = c) Proof - RW_TAC std_ss [rpow, GSYM LN_INJ] THEN - POP_ASSUM MP_TAC THEN - KNOW_TAC ``(exp (b * ln a) = exp (c * ln a)) <=> + rpt STRIP_TAC + >> ‘0 < a’ by PROVE_TAC [REAL_LT_TRANS, REAL_LT_01] + >> fs [rpow, GSYM LN_INJ] + >> Q.PAT_X_ASSUM ‘exp (b * ln a) = exp (c * ln a)’ MP_TAC + >> KNOW_TAC ``(exp (b * ln a) = exp (c * ln a)) <=> (ln (exp (b * ln a)) = ln (exp (c * ln a)))`` THEN1 PROVE_TAC[LN_EXP] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM K_TAC THEN @@ -2933,25 +2985,44 @@ Proof QED Theorem DIFF_RPOW : - !x y. 0 < x ==> ((\x. (x rpow y)) diffl (y * (x rpow (y - 1)))) x -Proof -RW_TAC real_ss [rpow,GSYM RPOW_DIV_BASE] THEN -RW_TAC real_ss [REAL_MUL_ASSOC,real_div,REAL_MUL_COMM]THEN -RW_TAC real_ss [GSYM real_div] THEN -KNOW_TAC ``!x'. exp ((y * ln x')) = exp ((\x'. y *ln x') x')`` THEN1 - RW_TAC real_ss [] THEN -DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN -KNOW_TAC `` ((y / x) * exp ((\x'. y * ln x') x))= ( exp ((\x'. y * ln x') x)*(y/x) ) `` THEN1 - RW_TAC std_ss [REAL_MUL_COMM] THEN -DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN -MATCH_MP_TAC DIFF_COMPOSITE_EXP THEN -KNOW_TAC ``((\x. y * ln x) diffl (y/x)) x = ((\x. y * (\x.ln x) x) diffl (y/x)) x`` THEN1 - RW_TAC real_ss [] THEN -DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN -RW_TAC real_ss [real_div] THEN -MATCH_MP_TAC DIFF_CMUL THEN -MATCH_MP_TAC DIFF_LN THEN -RW_TAC real_ss [] + !x y. 0 < x ==> ((\x. x rpow y) diffl (y * (x rpow (y - 1)))) x +Proof + RW_TAC real_ss [rpow, GSYM RPOW_DIV_BASE] + (* eliminate ‘rpow’ by LIM_TRANSFORM_WITHIN_OPEN_EQ *) + >> qabbrev_tac ‘l = y * (exp (y * ln x) / x)’ + >> Know ‘((\x. x powr y) diffl l) x <=> ((\x. exp (y * ln x)) diffl l) x’ + >- (REWRITE_TAC [diffl, GSYM LIM_AT_LIM] \\ + Q.ABBREV_TAC ‘f = \z. (z powr y - x powr y) / (z - x)’ \\ + ‘(\h. ((x + h) powr y - x powr y) / h) = (\h. f (x + h))’ + by simp [FUN_EQ_THM, Abbr ‘f’, REAL_ADD_SUB] >> POP_ORW \\ + Q.ABBREV_TAC ‘g = \z. (exp (y * ln z) - exp (y * ln x)) / (z - x)’ \\ + ‘(\h. (exp (y * ln (x + h)) - exp (y * ln x)) / h) = (\h. g (x + h))’ + by simp [FUN_EQ_THM, Abbr ‘g’, REAL_ADD_SUB] >> POP_ORW \\ + MATCH_MP_TAC LIM_TRANSFORM_WITHIN_OPEN_EQ >> simp [] \\ + Q.EXISTS_TAC ‘{y | -x < y}’ >> simp [OPEN_INTERVAL_RIGHT] \\ + Q.X_GEN_TAC ‘z’ >> rw [] \\ + ‘0 < x + z’ by (Q.PAT_X_ASSUM ‘-x < z’ MP_TAC >> REAL_ARITH_TAC) \\ + rw [Abbr ‘f’, Abbr ‘g’, REAL_ADD_SUB] \\ + rw [rpow_def]) + >> Rewr' + >> qunabbrev_tac ‘l’ + (* below is the old proof *) + >> RW_TAC real_ss [REAL_MUL_ASSOC,real_div,REAL_MUL_COMM] + >> RW_TAC real_ss [GSYM real_div] + >> Know ‘!x'. exp ((y * ln x')) = exp ((\x'. y * ln x') x')’ + >- RW_TAC real_ss [] + >> Rewr' + >> Know ‘(y/x) * exp ((\x'. y * ln x') x) = exp ((\x'. y * ln x') x) * (y/x)’ + >- RW_TAC std_ss [REAL_MUL_COMM] + >> Rewr' + >> MATCH_MP_TAC DIFF_COMPOSITE_EXP + >> Know ‘((\x. y * ln x) diffl (y/x)) x = ((\x. y * (\x.ln x) x) diffl (y/x)) x’ + >- RW_TAC real_ss [] + >> Rewr' + >> RW_TAC real_ss [real_div] + >> MATCH_MP_TAC DIFF_CMUL + >> MATCH_MP_TAC DIFF_LN + >> RW_TAC real_ss [] QED Theorem lem[local] : @@ -3631,9 +3702,6 @@ QED (* Real-valued power, log, and log base 2 functions (from util_probTheory) *) (* ------------------------------------------------------------------------- *) -val _ = set_fixity "powr" (Infixr 700); -val _ = overload_on ("powr", ``$rpow``); - Definition logr_def : logr a x = ln x / ln a End From c4a3bb9c6a4f7c6cd80cddd59f9af68eb5226618 Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Fri, 7 Jun 2024 13:38:41 +1000 Subject: [PATCH 2/3] FTBFS due to changes of rpow_def --- src/probability/martingaleScript.sml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/probability/martingaleScript.sml b/src/probability/martingaleScript.sml index 7c6bb4af7c..b8366ee148 100644 --- a/src/probability/martingaleScript.sml +++ b/src/probability/martingaleScript.sml @@ -1898,6 +1898,12 @@ Proof >> PROVE_TAC [FCP_CONCAT_THM] QED +Theorem pair_operation_CONS : + pair_operation (\x y. [x; y]) (EL 0) (EL 1) +Proof + rw [pair_operation_def] +QED + val general_cross_def = Define ‘general_cross (cons :'a -> 'b -> 'c) A B = {cons a b | a IN A /\ b IN B}’; @@ -7696,6 +7702,7 @@ Proof >> rw [extreal_abs_def] >> ‘0 < abs (a + b) /\ 0 < abs a /\ 0 < abs b’ by rw [] >> rw [normal_powr, extreal_of_num_def, extreal_add_def, extreal_mul_def, extreal_le_eq] + >> ONCE_REWRITE_TAC [REAL_MUL_COMM] (* below is real-only *) >> MATCH_MP_TAC REAL_LE_TRANS >> Q.EXISTS_TAC ‘(max (abs a powr r) (abs b powr r)) * 2 powr r’ From a80e888561e5b882c3ac75b17cd57b0c77ee8dbd Mon Sep 17 00:00:00 2001 From: "Chun Tian (binghe)" Date: Sat, 8 Jun 2024 03:54:57 +1000 Subject: [PATCH 3/3] Minor updates to powr_def (more friendly as rewriting rules) --- src/real/analysis/transcScript.sml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/real/analysis/transcScript.sml b/src/real/analysis/transcScript.sml index 76ac931c3f..7a23918723 100644 --- a/src/real/analysis/transcScript.sml +++ b/src/real/analysis/transcScript.sml @@ -2673,7 +2673,8 @@ local ‘?f :real -> real -> real. (!a b. 0 < a ==> f a b = exp (b * ln a)) /\ (!b. 0 < b ==> f 0 b = 0) /\ - (!a n. f a &n = a pow n /\ f a (-&SUC n) = inv (a pow (SUC n)))’, + (!a n. f a &n = a pow n) /\ + (!a n. f a (-&n) = inv (a pow n))’, (* proof *) Q.EXISTS_TAC ‘\a b. if 0 < a then exp (b * ln a) else if a = 0 /\ 0 < b then 0 else @@ -2689,8 +2690,8 @@ local in (* |- (!a b. 0 < a ==> a powr b = exp (b * ln a)) /\ (!b. 0 < b ==> 0 powr b = 0) /\ - !a n. a powr &n = a pow n /\ - a powr -&SUC n = inv (a pow SUC n) + (!a n. a powr &n = a pow n) /\ + !a n. a powr -&n = inv (a pow n) *) val powr_def = new_specification ("powr_def", ["powr"], thm); end;