From 74560a4095e4ed5d50e784c5b82df6d929fe214a Mon Sep 17 00:00:00 2001 From: John Harrison Date: Tue, 2 Nov 2021 17:27:19 -0700 Subject: [PATCH] Added a few theorems including some systematic gaps in integer theorems where the analog was present for reals, and a few more word theorems. INT_ABS_BOUNDS INT_EQ_LCANCEL_IMP INT_EQ_RCANCEL_IMP INT_EVENPOW_ABS INT_LE_LCANCEL_IMP INT_LE_POW_2 INT_LE_RCANCEL_IMP INT_LE_RMUL_EQ INT_LT_LADD_IMP INT_LT_LCANCEL_IMP INT_LT_LMUL INT_LT_LNEG INT_LT_POW_2 INT_LT_RCANCEL_IMP INT_LT_RMUL INT_LT_RNEG INT_LT_SQUARE INT_OF_NUM_SUB_CASES INT_POS_EQ_SQUARE INT_POW_EQ_1 INT_POW_EQ_1_IMP INT_POW_EQ_EQ INT_POW_EQ_ODD INT_POW_EQ_ODD_EQ INT_POW_LBOUND INT_POW_LE2_ODD_EQ INT_POW_LT2_ODD INT_POW_LT2_ODD_EQ REAL_EVENPOW_ABS VAL_WORD_AND_LE VAL_WORD_AND_LE_MIN VAL_WORD_AND_WORD_LE VAL_WORD_OR_LE_MAX WORD_JOIN_NOT WORD_SUBWORD_NOT Also added missing conversions WORD_JROL_CONV and WORD_JROR_CONV (for word-word rotate operations) and included them in WORD_RED_CONV and hence WORD_REDUCE_CONV. --- CHANGES | 156 +++++++++++++++++++++++++++++++++++++++++++++-- Library/words.ml | 60 ++++++++++++++++++ database.ml | 29 +++++++++ int.ml | 38 ++++++++++-- parser.ml | 2 +- real.ml | 4 ++ 6 files changed, 277 insertions(+), 12 deletions(-) diff --git a/CHANGES b/CHANGES index ef68f0b4..b20121a7 100644 --- a/CHANGES +++ b/CHANGES @@ -8,7 +8,151 @@ * page: https://github.com/jrh13/hol-light/commits/master * * ***************************************************************** -Wed 9th Oct 2021 int.ml +Tue 2nd Nov 2021 Library/words.ml + +Added missing conversions WORD_JROL_CONV and WORD_JROR_CONV (for +word-word rotate operations) and included them in WORD_RED_CONV +and hence WORD_REDUCE_CONV. + +Mon 1st Nov 2021 parser.ml + +Fixed a trivial typo in the error message "closing square bracket +of list expected". + +Tue 12th Oct 2021 Library/words.ml + +Added a couple more word lemmas about pushing logical complements through +other constructs; the side-conditions make them a bit ugly but they can be +useful: + + WORD_JOIN_NOT = + |- !v w. + dimindex(:P) <= dimindex(:M) + dimindex(:N) + ==> word_join (word_not v) (word_not w) = word_not (word_join v w) + + WORD_SUBWORD_NOT = + |- !x pos len. + dimindex(:N) <= len /\ pos + len <= dimindex(:M) + ==> word_subword (word_not x) (pos,len) = + word_not (word_subword x (pos,len)) + +Sat 9th Oct 2021 Library/words.ml + +Added a few more elementary word lemmas like a simple upper bound on +a concrete masking of a word: + + VAL_WORD_AND_LE = + |- (!x y. val (word_and x y) <= val x) /\ + (!x y. val (word_and x y) <= val y) + + VAL_WORD_AND_LE_MIN = + |- !x y. val (word_and x y) <= MIN (val x) (val y) + + VAL_WORD_AND_WORD_LE = + |- (!x n. val (word_and x (word n)) <= n) /\ + (!x n. val (word_and (word n) x) <= n) + + VAL_WORD_OR_LE_MAX = + |- !x y. MAX (val x) (val y) <= val (word_or x y) + +Fri 8th Oct 2021 int.ml + +Added a systematic set of missing analogs of real theorems for ints: + + INT_ABS_BOUNDS : thm = + |- !x k. abs x <= k <=> --k <= x /\ x <= k + + INT_EQ_LCANCEL_IMP : thm = + |- !x y z. ~(z = &0) /\ z * x = z * y ==> x = y + + INT_EQ_RCANCEL_IMP : thm = + |- !x y z. ~(z = &0) /\ x * z = y * z ==> x = y + + INT_LE_LCANCEL_IMP : thm = + |- !x y z. &0 < x /\ x * y <= x * z ==> y <= z + + INT_LE_POW_2 : thm = + |- !x. &0 <= x pow 2 + + INT_LE_RCANCEL_IMP : thm = + |- !x y z. &0 < z /\ x * z <= y * z ==> x <= y + + INT_LE_RMUL_EQ : thm = + |- !x y z. &0 < z ==> (x * z <= y * z <=> x <= y) + + INT_LT_LADD_IMP : thm = + |- !x y z. y < z ==> x + y < x + z + + INT_LT_LCANCEL_IMP : thm = + |- !x y z. &0 < x /\ x * y < x * z ==> y < z + + INT_LT_LMUL : thm = + |- !x y z. &0 < x /\ y < z ==> x * y < x * z + + INT_LT_LNEG : thm = + |- !x y. --x < y <=> &0 < x + y + + INT_LT_POW_2 : thm = + |- !x. &0 < x pow 2 <=> ~(x = &0) + + INT_LT_RCANCEL_IMP : thm = + |- !x y z. &0 < z /\ x * z < y * z ==> x < y + + INT_LT_RMUL : thm = + |- !x y z. x < y /\ &0 < z ==> x * z < y * z + + INT_LT_RNEG : thm = + |- !x y. x < --y <=> x + y < &0 + + INT_LT_SQUARE : thm = + |- !x. &0 < x * x <=> ~(x = &0) + + INT_OF_NUM_SUB_CASES : thm = + |- !m n. &m - &n = (if n <= m then &(m - n) else -- &(n - m)) + + INT_POS_EQ_SQUARE : thm = + |- !x. &0 <= x <=> (?y. y pow 2 = real_of_int x) + + INT_POW_EQ_1 : thm = + |- !x n. x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) \/ n = 0 + + INT_POW_EQ_1_IMP : thm = + |- !x n. ~(n = 0) /\ x pow n = &1 ==> abs x = &1 + + INT_POW_EQ_EQ : thm = + |- !n x y. + x pow n = y pow n <=> + (if EVEN n then n = 0 \/ abs x = abs y else x = y) + + INT_POW_EQ_ODD : thm = + |- !n x y. ODD n /\ x pow n = y pow n ==> x = y + + INT_POW_EQ_ODD_EQ : thm = + |- !n x y. ODD n ==> (x pow n = y pow n <=> x = y) + + INT_POW_LBOUND : thm = + |- !x n. &0 <= x ==> &1 + &n * x <= (&1 + x) pow n + + INT_POW_LE2_ODD_EQ : thm = + |- !n x y. ODD n ==> (x pow n <= y pow n <=> x <= y) + + INT_POW_LT2_ODD : thm = + |- !n x y. x < y /\ ODD n ==> x pow n < y pow n + + INT_POW_LT2_ODD_EQ : thm = + |- !n x y. ODD n ==> (x pow n < y pow n <=> x < y) + +Fri 8th Oct 2021 real.ml, int.ml + +Added integer and real forms of this simple lemma: + + INT_EVENPOW_ABS = + |- !x n. EVEN n ==> abs x pow n = x pow n + + REAL_EVENPOW_ABS = + |- !x n. EVEN n ==> abs x pow n = x pow n + +Wed 6th Oct 2021 int.ml Added a natural integer analog of MOD_UNIQUE: @@ -17,7 +161,7 @@ Added a natural integer analog of MOD_UNIQUE: m rem n = p <=> (n = &0 /\ m = p \/ &0 <= p /\ p < abs n) /\ (m == p) (mod n) -Tue 8th Oct 2021 Library/words.ml +Tue 5th Oct 2021 Library/words.ml Added a few trivial theorems about unsigned word max/min: @@ -65,11 +209,11 @@ proved automatically by WORD_ARITH_TAC. WORD_ADC_LE_EXACT = |- (!x y. val(word_add (word_add x y) (word 1)) <= val x <=> - val(word_add (word_add x y) (word 1)) + 2 EXP dimindex (:N) = + val(word_add (word_add x y) (word 1)) + 2 EXP dimindex(:N) = val x + val y + 1) /\ (!x y. val(word_add (word_add x y) (word 1)) <= val y <=> - val(word_add (word_add x y) (word 1)) + 2 EXP dimindex (:N) = + val(word_add (word_add x y) (word 1)) + 2 EXP dimindex(:N) = val x + val y + 1) WORD_ADC_LE_INEXACT = @@ -83,10 +227,10 @@ proved automatically by WORD_ARITH_TAC. WORD_ADD_LT_EXACT = |- (!x y. val(word_add x y) < val x <=> - val(word_add x y) + 2 EXP dimindex (:N) = val x + val y) /\ + val(word_add x y) + 2 EXP dimindex(:N) = val x + val y) /\ (!x y. val(word_add x y) < val y <=> - val(word_add x y) + 2 EXP dimindex (:N) = val x + val y) + val(word_add x y) + 2 EXP dimindex(:N) = val x + val y) WORD_ADD_LT_INEXACT = |- (!x y. diff --git a/Library/words.ml b/Library/words.ml index f2627326..27bd0195 100644 --- a/Library/words.ml +++ b/Library/words.ml @@ -1544,6 +1544,23 @@ let VAL_WORD_AND_POW2 = prove COND_CASES_TAC THEN REWRITE_TAC[MULT_CLAUSES; LT_EXP; EXP_LT_0] THEN CONV_TAC NUM_REDUCE_CONV THEN ASM_MESON_TAC[BIT_TRIVIAL; NOT_LE]);; +let VAL_WORD_AND_LE = prove + (`(!x y:N word. val(word_and x y) <= val x) /\ + (!x y:N word. val(word_and x y) <= val y)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[val_def] THEN MATCH_MP_TAC NSUM_LE THEN + REWRITE_TAC[FINITE_NUMSEG_LT] THEN X_GEN_TAC `i:num` THEN + SIMP_TAC[IN_ELIM_THM; BIT_WORD_AND; LE_MULT_LCANCEL; LE_BITVAL]);; + +let VAL_WORD_AND_LE_MIN = prove + (`!x y:N word. val(word_and x y) <= MIN (val x) (val y)`, + REWRITE_TAC[ARITH_RULE `x <= MIN y z <=> x <= y /\ x <= z`] THEN + REWRITE_TAC[VAL_WORD_AND_LE]);; + +let VAL_WORD_AND_WORD_LE = prove + (`(!(x:N word) n. val(word_and x (word n)) <= n) /\ + (!(x:N word) n. val(word_and (word n) x) <= n)`, + MESON_TAC[VAL_WORD_AND_LE; LE_TRANS; LE_REFL; VAL_WORD_LE]);; + let word_or = new_definition `word_or = bitwise2 (\/)`;; @@ -1576,6 +1593,11 @@ let VAL_WORD_OR_LE = prove REPEAT STRIP_TAC THEN MATCH_MP_TAC VAL_LE_BITS THEN SIMP_TAC[BIT_WORD_OR]);; +let VAL_WORD_OR_LE_MAX = prove + (`(!x y:N word. MAX (val x) (val y) <= val(word_or x y))`, + REWRITE_TAC[ARITH_RULE `MAX y z <= x <=> y <= x /\ z <= x`] THEN + REWRITE_TAC[VAL_WORD_OR_LE]);; + let word_xor = new_definition `word_xor = bitwise2 (\x y. ~(x <=> y))`;; @@ -2957,6 +2979,16 @@ let VAL_WORD_JOIN_SIMPLE = prove REWRITE_TAC[LE_MULT_LCANCEL; ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN REWRITE_TAC[EXP_EQ_0; ARITH_EQ]]);; +let WORD_JOIN_NOT = prove + (`!v w. dimindex(:P) <= dimindex(:M) + dimindex(:N) + ==> (word_join:(M)word->(N)word->(P)word) (word_not v) (word_not w) = + word_not(word_join v w)`, + REPEAT STRIP_TAC THEN REWRITE_TAC[WORD_EQ_BITS_ALT] THEN + SIMP_TAC[BIT_WORD_JOIN; BIT_WORD_NOT; COND_SWAP] THEN + REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN + ONCE_REWRITE_TAC[BIT_GUARD] THEN EQ_TAC THEN SIMP_TAC[] THEN + ASM_ARITH_TAC);; + (* ------------------------------------------------------------------------- *) (* Subwords, where the (pos,len) argument is (lsb_position,length) *) (* ------------------------------------------------------------------------- *) @@ -3149,6 +3181,16 @@ let WORD_SUBWORD_XOR = prove REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; BIT_WORD_XOR] THEN ONCE_REWRITE_TAC[BIT_GUARD] THEN CONV_TAC TAUT);; +let WORD_SUBWORD_NOT = prove + (`!(x:M word) pos len. + dimindex(:N) <= len /\ pos + len <= dimindex(:M) + ==> word_subword (word_not x) (pos,len):N word = + word_not (word_subword x (pos,len))`, + REWRITE_TAC[WORD_EQ_BITS_ALT; BIT_WORD_SUBWORD; BIT_WORD_NOT] THEN + SIMP_TAC[ARITH_RULE `i < MIN m n <=> i < m /\ i < n`] THEN + REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[DE_MORGAN_THM] THEN + STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC);; + (* ------------------------------------------------------------------------- *) (* Bit recursion equations for "linear" operations. *) (* ------------------------------------------------------------------------- *) @@ -5901,6 +5943,22 @@ let WORD_JUSHR_CONV = NUM_MOD_CONV) THENC WORD_USHR_CONV;; +let WORD_JROL_CONV = + let pth = prove + (`word_jrol (word(NUMERAL m):N word) (word(NUMERAL n):N word) = + word_rol (word(NUMERAL m):N word) (val(word(NUMERAL n):N word))`, + REWRITE_TAC[word_jrol]) in + GEN_REWRITE_CONV I [pth] THENC RAND_CONV WORD_VAL_CONV THENC + WORD_ROL_CONV;; + +let WORD_JROR_CONV = + let pth = prove + (`word_jror (word(NUMERAL m):N word) (word(NUMERAL n):N word) = + word_ror (word(NUMERAL m):N word) (val(word(NUMERAL n):N word))`, + REWRITE_TAC[word_jror]) in + GEN_REWRITE_CONV I [pth] THENC RAND_CONV WORD_VAL_CONV THENC + WORD_ROR_CONV;; + let WORD_JDIV_CONV = let pth = prove (`word_jdiv (word(NUMERAL m):N word) (word(NUMERAL n)) = @@ -5979,6 +6037,8 @@ let WORD_RED_CONV = `word_jshl (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JSHL_CONV; `word_jshr (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JSHR_CONV; `word_jushr (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JUSHR_CONV; + `word_jrol (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JROL_CONV; + `word_jror (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JROR_CONV; `word_jdiv (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JDIV_CONV; `word_jrem (word(NUMERAL m):N word) (word(NUMERAL n))`,WORD_JREM_CONV] (basic_net()) in diff --git a/database.ml b/database.ml index 1b815ea1..c7de954f 100644 --- a/database.ml +++ b/database.ml @@ -904,6 +904,7 @@ theorems := "INT_ABS_BETWEEN1",INT_ABS_BETWEEN1; "INT_ABS_BETWEEN2",INT_ABS_BETWEEN2; "INT_ABS_BOUND",INT_ABS_BOUND; +"INT_ABS_BOUNDS",INT_ABS_BOUNDS; "INT_ABS_CASES",INT_ABS_CASES; "INT_ABS_CIRCLE",INT_ABS_CIRCLE; "INT_ABS_LE",INT_ABS_LE; @@ -984,13 +985,16 @@ theorems := "INT_EQ_ADD_RCANCEL",INT_EQ_ADD_RCANCEL; "INT_EQ_ADD_RCANCEL_0",INT_EQ_ADD_RCANCEL_0; "INT_EQ_IMP_LE",INT_EQ_IMP_LE; +"INT_EQ_LCANCEL_IMP",INT_EQ_LCANCEL_IMP; "INT_EQ_MUL_LCANCEL",INT_EQ_MUL_LCANCEL; "INT_EQ_MUL_RCANCEL",INT_EQ_MUL_RCANCEL; "INT_EQ_NEG2",INT_EQ_NEG2; +"INT_EQ_RCANCEL_IMP",INT_EQ_RCANCEL_IMP; "INT_EQ_SGN_ABS",INT_EQ_SGN_ABS; "INT_EQ_SQUARE_ABS",INT_EQ_SQUARE_ABS; "INT_EQ_SUB_LADD",INT_EQ_SUB_LADD; "INT_EQ_SUB_RADD",INT_EQ_SUB_RADD; +"INT_EVENPOW_ABS",INT_EVENPOW_ABS; "INT_EXISTS_ABS",INT_EXISTS_ABS; "INT_EXISTS_POS",INT_EXISTS_POS; "INT_FORALL_ABS",INT_FORALL_ABS; @@ -1021,6 +1025,7 @@ theorems := "INT_LE_DOUBLE",INT_LE_DOUBLE; "INT_LE_LADD",INT_LE_LADD; "INT_LE_LADD_IMP",INT_LE_LADD_IMP; +"INT_LE_LCANCEL_IMP",INT_LE_LCANCEL_IMP; "INT_LE_LMUL",INT_LE_LMUL; "INT_LE_LMUL_EQ",INT_LE_LMUL_EQ; "INT_LE_LNEG",INT_LE_LNEG; @@ -1035,9 +1040,12 @@ theorems := "INT_LE_NEGR",INT_LE_NEGR; "INT_LE_NEGTOTAL",INT_LE_NEGTOTAL; "INT_LE_POW2",INT_LE_POW2; +"INT_LE_POW_2",INT_LE_POW_2; "INT_LE_RADD",INT_LE_RADD; +"INT_LE_RCANCEL_IMP",INT_LE_RCANCEL_IMP; "INT_LE_REFL",INT_LE_REFL; "INT_LE_RMUL",INT_LE_RMUL; +"INT_LE_RMUL_EQ",INT_LE_RMUL_EQ; "INT_LE_RNEG",INT_LE_RNEG; "INT_LE_SQUARE",INT_LE_SQUARE; "INT_LE_SQUARE_ABS",INT_LE_SQUARE_ABS; @@ -1071,8 +1079,12 @@ theorems := "INT_LT_IMP_LE",INT_LT_IMP_LE; "INT_LT_IMP_NE",INT_LT_IMP_NE; "INT_LT_LADD",INT_LT_LADD; +"INT_LT_LADD_IMP",INT_LT_LADD_IMP; +"INT_LT_LCANCEL_IMP",INT_LT_LCANCEL_IMP; "INT_LT_LE",INT_LT_LE; +"INT_LT_LMUL",INT_LT_LMUL; "INT_LT_LMUL_EQ",INT_LT_LMUL_EQ; +"INT_LT_LNEG",INT_LT_LNEG; "INT_LT_MAX",INT_LT_MAX; "INT_LT_MIN",INT_LT_MIN; "INT_LT_MUL",INT_LT_MUL; @@ -1081,11 +1093,16 @@ theorems := "INT_LT_NEG2",INT_LT_NEG2; "INT_LT_NEGTOTAL",INT_LT_NEGTOTAL; "INT_LT_POW2",INT_LT_POW2; +"INT_LT_POW_2",INT_LT_POW_2; "INT_LT_RADD",INT_LT_RADD; +"INT_LT_RCANCEL_IMP",INT_LT_RCANCEL_IMP; "INT_LT_REFL",INT_LT_REFL; "INT_LT_REM",INT_LT_REM; "INT_LT_REM_EQ",INT_LT_REM_EQ; +"INT_LT_RMUL",INT_LT_RMUL; "INT_LT_RMUL_EQ",INT_LT_RMUL_EQ; +"INT_LT_RNEG",INT_LT_RNEG; +"INT_LT_SQUARE",INT_LT_SQUARE; "INT_LT_SQUARE_ABS",INT_LT_SQUARE_ABS; "INT_LT_SUB_LADD",INT_LT_SUB_LADD; "INT_LT_SUB_RADD",INT_LT_SUB_RADD; @@ -1159,8 +1176,10 @@ theorems := "INT_OF_NUM_POW",INT_OF_NUM_POW; "INT_OF_NUM_REM",INT_OF_NUM_REM; "INT_OF_NUM_SUB",INT_OF_NUM_SUB; +"INT_OF_NUM_SUB_CASES",INT_OF_NUM_SUB_CASES; "INT_OF_NUM_SUC",INT_OF_NUM_SUC; "INT_POS",INT_POS; +"INT_POS_EQ_SQUARE",INT_POS_EQ_SQUARE; "INT_POS_NZ",INT_POS_NZ; "INT_POW",INT_POW; "INT_POW2_ABS",INT_POW2_ABS; @@ -1171,14 +1190,23 @@ theorems := "INT_POW_ADD",INT_POW_ADD; "INT_POW_EQ",INT_POW_EQ; "INT_POW_EQ_0",INT_POW_EQ_0; +"INT_POW_EQ_1",INT_POW_EQ_1; +"INT_POW_EQ_1_IMP",INT_POW_EQ_1_IMP; "INT_POW_EQ_ABS",INT_POW_EQ_ABS; +"INT_POW_EQ_EQ",INT_POW_EQ_EQ; +"INT_POW_EQ_ODD",INT_POW_EQ_ODD; +"INT_POW_EQ_ODD_EQ",INT_POW_EQ_ODD_EQ; +"INT_POW_LBOUND",INT_POW_LBOUND; "INT_POW_LE",INT_POW_LE; "INT_POW_LE2",INT_POW_LE2; "INT_POW_LE2_ODD",INT_POW_LE2_ODD; +"INT_POW_LE2_ODD_EQ",INT_POW_LE2_ODD_EQ; "INT_POW_LE2_REV",INT_POW_LE2_REV; "INT_POW_LE_1",INT_POW_LE_1; "INT_POW_LT",INT_POW_LT; "INT_POW_LT2",INT_POW_LT2; +"INT_POW_LT2_ODD",INT_POW_LT2_ODD; +"INT_POW_LT2_ODD_EQ",INT_POW_LT2_ODD_EQ; "INT_POW_LT2_REV",INT_POW_LT2_REV; "INT_POW_LT_1",INT_POW_LT_1; "INT_POW_MONO",INT_POW_MONO; @@ -1960,6 +1988,7 @@ theorems := "REAL_EQ_SQUARE_ABS",REAL_EQ_SQUARE_ABS; "REAL_EQ_SUB_LADD",REAL_EQ_SUB_LADD; "REAL_EQ_SUB_RADD",REAL_EQ_SUB_RADD; +"REAL_EVENPOW_ABS",REAL_EVENPOW_ABS; "REAL_GROW_SHRINK",REAL_GROW_SHRINK; "REAL_HREAL_LEMMA1",REAL_HREAL_LEMMA1; "REAL_HREAL_LEMMA2",REAL_HREAL_LEMMA2; diff --git a/int.ml b/int.ml index a930475c..17ba2a8d 100644 --- a/int.ml +++ b/int.ml @@ -304,6 +304,7 @@ let INT_ABS_BETWEEN = INT_OF_REAL_THM REAL_ABS_BETWEEN;; let INT_ABS_BETWEEN1 = INT_OF_REAL_THM REAL_ABS_BETWEEN1;; let INT_ABS_BETWEEN2 = INT_OF_REAL_THM REAL_ABS_BETWEEN2;; let INT_ABS_BOUND = INT_OF_REAL_THM REAL_ABS_BOUND;; +let INT_ABS_BOUNDS = INT_OF_REAL_THM REAL_ABS_BOUNDS;; let INT_ABS_CASES = INT_OF_REAL_THM REAL_ABS_CASES;; let INT_ABS_CIRCLE = INT_OF_REAL_THM REAL_ABS_CIRCLE;; let INT_ABS_LE = INT_OF_REAL_THM REAL_ABS_LE;; @@ -343,13 +344,16 @@ let INT_EQ_ADD_LCANCEL_0 = INT_OF_REAL_THM REAL_EQ_ADD_LCANCEL_0;; let INT_EQ_ADD_RCANCEL = INT_OF_REAL_THM REAL_EQ_ADD_RCANCEL;; let INT_EQ_ADD_RCANCEL_0 = INT_OF_REAL_THM REAL_EQ_ADD_RCANCEL_0;; let INT_EQ_IMP_LE = INT_OF_REAL_THM REAL_EQ_IMP_LE;; +let INT_EQ_LCANCEL_IMP = INT_OF_REAL_THM REAL_EQ_LCANCEL_IMP;; let INT_EQ_MUL_LCANCEL = INT_OF_REAL_THM REAL_EQ_MUL_LCANCEL;; let INT_EQ_MUL_RCANCEL = INT_OF_REAL_THM REAL_EQ_MUL_RCANCEL;; let INT_EQ_NEG2 = INT_OF_REAL_THM REAL_EQ_NEG2;; +let INT_EQ_RCANCEL_IMP = INT_OF_REAL_THM REAL_EQ_RCANCEL_IMP;; let INT_EQ_SGN_ABS = INT_OF_REAL_THM REAL_EQ_SGN_ABS;; let INT_EQ_SQUARE_ABS = INT_OF_REAL_THM REAL_EQ_SQUARE_ABS;; let INT_EQ_SUB_LADD = INT_OF_REAL_THM REAL_EQ_SUB_LADD;; let INT_EQ_SUB_RADD = INT_OF_REAL_THM REAL_EQ_SUB_RADD;; +let INT_EVENPOW_ABS = INT_OF_REAL_THM REAL_EVENPOW_ABS;; let INT_LET_ADD = INT_OF_REAL_THM REAL_LET_ADD;; let INT_LET_ADD2 = INT_OF_REAL_THM REAL_LET_ADD2;; let INT_LET_ANTISYM = INT_OF_REAL_THM REAL_LET_ANTISYM;; @@ -364,6 +368,7 @@ let INT_LE_ANTISYM = INT_OF_REAL_THM REAL_LE_ANTISYM;; let INT_LE_DOUBLE = INT_OF_REAL_THM REAL_LE_DOUBLE;; let INT_LE_LADD = INT_OF_REAL_THM REAL_LE_LADD;; let INT_LE_LADD_IMP = INT_OF_REAL_THM REAL_LE_LADD_IMP;; +let INT_LE_LCANCEL_IMP = INT_OF_REAL_THM REAL_LE_LCANCEL_IMP;; let INT_LE_LMUL = INT_OF_REAL_THM REAL_LE_LMUL;; let INT_LE_LMUL_EQ = INT_OF_REAL_THM REAL_LE_LMUL_EQ;; let INT_LE_LNEG = INT_OF_REAL_THM REAL_LE_LNEG;; @@ -371,16 +376,19 @@ let INT_LE_LT = INT_OF_REAL_THM REAL_LE_LT;; let INT_LE_MAX = INT_OF_REAL_THM REAL_LE_MAX;; let INT_LE_MIN = INT_OF_REAL_THM REAL_LE_MIN;; let INT_LE_MUL = INT_OF_REAL_THM REAL_LE_MUL;; -let INT_LE_MUL_EQ = INT_OF_REAL_THM REAL_LE_MUL_EQ;; let INT_LE_MUL2 = INT_OF_REAL_THM REAL_LE_MUL2;; +let INT_LE_MUL_EQ = INT_OF_REAL_THM REAL_LE_MUL_EQ;; let INT_LE_NEG2 = INT_OF_REAL_THM REAL_LE_NEG2;; let INT_LE_NEGL = INT_OF_REAL_THM REAL_LE_NEGL;; let INT_LE_NEGR = INT_OF_REAL_THM REAL_LE_NEGR;; let INT_LE_NEGTOTAL = INT_OF_REAL_THM REAL_LE_NEGTOTAL;; let INT_LE_POW2 = INT_OF_REAL_THM REAL_LE_POW2;; +let INT_LE_POW_2 = INT_OF_REAL_THM REAL_LE_POW_2;; let INT_LE_RADD = INT_OF_REAL_THM REAL_LE_RADD;; +let INT_LE_RCANCEL_IMP = INT_OF_REAL_THM REAL_LE_RCANCEL_IMP;; let INT_LE_REFL = INT_OF_REAL_THM REAL_LE_REFL;; let INT_LE_RMUL = INT_OF_REAL_THM REAL_LE_RMUL;; +let INT_LE_RMUL_EQ = INT_OF_REAL_THM REAL_LE_RMUL_EQ;; let INT_LE_RNEG = INT_OF_REAL_THM REAL_LE_RNEG;; let INT_LE_SQUARE = INT_OF_REAL_THM REAL_LE_SQUARE;; let INT_LE_SQUARE_ABS = INT_OF_REAL_THM REAL_LE_SQUARE_ABS;; @@ -408,19 +416,28 @@ let INT_LT_GT = INT_OF_REAL_THM REAL_LT_GT;; let INT_LT_IMP_LE = INT_OF_REAL_THM REAL_LT_IMP_LE;; let INT_LT_IMP_NE = INT_OF_REAL_THM REAL_LT_IMP_NE;; let INT_LT_LADD = INT_OF_REAL_THM REAL_LT_LADD;; +let INT_LT_LADD_IMP = INT_OF_REAL_THM REAL_LT_LADD_IMP;; +let INT_LT_LCANCEL_IMP = INT_OF_REAL_THM REAL_LT_LCANCEL_IMP;; let INT_LT_LE = INT_OF_REAL_THM REAL_LT_LE;; +let INT_LT_LMUL = INT_OF_REAL_THM REAL_LT_LMUL;; let INT_LT_LMUL_EQ = INT_OF_REAL_THM REAL_LT_LMUL_EQ;; +let INT_LT_LNEG = INT_OF_REAL_THM REAL_LT_LNEG;; let INT_LT_MAX = INT_OF_REAL_THM REAL_LT_MAX;; let INT_LT_MIN = INT_OF_REAL_THM REAL_LT_MIN;; let INT_LT_MUL = INT_OF_REAL_THM REAL_LT_MUL;; -let INT_LT_MUL_EQ = INT_OF_REAL_THM REAL_LT_MUL_EQ;; let INT_LT_MUL2 = INT_OF_REAL_THM REAL_LT_MUL2;; +let INT_LT_MUL_EQ = INT_OF_REAL_THM REAL_LT_MUL_EQ;; let INT_LT_NEG2 = INT_OF_REAL_THM REAL_LT_NEG2;; let INT_LT_NEGTOTAL = INT_OF_REAL_THM REAL_LT_NEGTOTAL;; let INT_LT_POW2 = INT_OF_REAL_THM REAL_LT_POW2;; +let INT_LT_POW_2 = INT_OF_REAL_THM REAL_LT_POW_2;; let INT_LT_RADD = INT_OF_REAL_THM REAL_LT_RADD;; +let INT_LT_RCANCEL_IMP = INT_OF_REAL_THM REAL_LT_RCANCEL_IMP;; let INT_LT_REFL = INT_OF_REAL_THM REAL_LT_REFL;; +let INT_LT_RMUL = INT_OF_REAL_THM REAL_LT_RMUL;; let INT_LT_RMUL_EQ = INT_OF_REAL_THM REAL_LT_RMUL_EQ;; +let INT_LT_RNEG = INT_OF_REAL_THM REAL_LT_RNEG;; +let INT_LT_SQUARE = INT_OF_REAL_THM REAL_LT_SQUARE;; let INT_LT_SQUARE_ABS = INT_OF_REAL_THM REAL_LT_SQUARE_ABS;; let INT_LT_SUB_LADD = INT_OF_REAL_THM REAL_LT_SUB_LADD;; let INT_LT_SUB_RADD = INT_OF_REAL_THM REAL_LT_SUB_RADD;; @@ -482,8 +499,10 @@ let INT_OF_NUM_MOD = INT_OF_REAL_THM REAL_OF_NUM_MOD;; let INT_OF_NUM_MUL = INT_OF_REAL_THM REAL_OF_NUM_MUL;; let INT_OF_NUM_POW = INT_OF_REAL_THM REAL_OF_NUM_POW;; let INT_OF_NUM_SUB = INT_OF_REAL_THM REAL_OF_NUM_SUB;; +let INT_OF_NUM_SUB_CASES = INT_OF_REAL_THM REAL_OF_NUM_SUB_CASES;; let INT_OF_NUM_SUC = INT_OF_REAL_THM REAL_OF_NUM_SUC;; let INT_POS = INT_OF_REAL_THM REAL_POS;; +let INT_POS_EQ_SQUARE = INT_OF_REAL_THM REAL_POS_EQ_SQUARE;; let INT_POS_NZ = INT_OF_REAL_THM REAL_LT_IMP_NZ;; let INT_POW2_ABS = INT_OF_REAL_THM REAL_POW2_ABS;; let INT_POW_1 = INT_OF_REAL_THM REAL_POW_1;; @@ -493,14 +512,23 @@ let INT_POW_2 = INT_OF_REAL_THM REAL_POW_2;; let INT_POW_ADD = INT_OF_REAL_THM REAL_POW_ADD;; let INT_POW_EQ = INT_OF_REAL_THM REAL_POW_EQ;; let INT_POW_EQ_0 = INT_OF_REAL_THM REAL_POW_EQ_0;; +let INT_POW_EQ_1 = INT_OF_REAL_THM REAL_POW_EQ_1;; +let INT_POW_EQ_1_IMP = INT_OF_REAL_THM REAL_POW_EQ_1_IMP;; let INT_POW_EQ_ABS = INT_OF_REAL_THM REAL_POW_EQ_ABS;; +let INT_POW_EQ_EQ = INT_OF_REAL_THM REAL_POW_EQ_EQ;; +let INT_POW_EQ_ODD = INT_OF_REAL_THM REAL_POW_EQ_ODD;; +let INT_POW_EQ_ODD_EQ = INT_OF_REAL_THM REAL_POW_EQ_ODD_EQ;; +let INT_POW_LBOUND = INT_OF_REAL_THM REAL_POW_LBOUND;; let INT_POW_LE = INT_OF_REAL_THM REAL_POW_LE;; let INT_POW_LE2 = INT_OF_REAL_THM REAL_POW_LE2;; let INT_POW_LE2_ODD = INT_OF_REAL_THM REAL_POW_LE2_ODD;; +let INT_POW_LE2_ODD_EQ = INT_OF_REAL_THM REAL_POW_LE2_ODD_EQ;; let INT_POW_LE2_REV = INT_OF_REAL_THM REAL_POW_LE2_REV;; let INT_POW_LE_1 = INT_OF_REAL_THM REAL_POW_LE_1;; let INT_POW_LT = INT_OF_REAL_THM REAL_POW_LT;; let INT_POW_LT2 = INT_OF_REAL_THM REAL_POW_LT2;; +let INT_POW_LT2_ODD = INT_OF_REAL_THM REAL_POW_LT2_ODD;; +let INT_POW_LT2_ODD_EQ = INT_OF_REAL_THM REAL_POW_LT2_ODD_EQ;; let INT_POW_LT2_REV = INT_OF_REAL_THM REAL_POW_LT2_REV;; let INT_POW_LT_1 = INT_OF_REAL_THM REAL_POW_LT_1;; let INT_POW_MONO = INT_OF_REAL_THM REAL_POW_MONO;; @@ -513,6 +541,8 @@ let INT_POW_POW = INT_OF_REAL_THM REAL_POW_POW;; let INT_POW_ZERO = INT_OF_REAL_THM REAL_POW_ZERO;; let INT_RNEG_UNIQ = INT_OF_REAL_THM REAL_RNEG_UNIQ;; let INT_SGN = INT_OF_REAL_THM real_sgn;; +let INT_SGNS_EQ = INT_OF_REAL_THM REAL_SGNS_EQ;; +let INT_SGNS_EQ_ALT = INT_OF_REAL_THM REAL_SGNS_EQ_ALT;; let INT_SGN_0 = INT_OF_REAL_THM REAL_SGN_0;; let INT_SGN_ABS = INT_OF_REAL_THM REAL_SGN_ABS;; let INT_SGN_ABS_ALT = INT_OF_REAL_THM REAL_SGN_ABS_ALT;; @@ -520,13 +550,11 @@ let INT_SGN_CASES = INT_OF_REAL_THM REAL_SGN_CASES;; let INT_SGN_EQ = INT_OF_REAL_THM REAL_SGN_EQ;; let INT_SGN_EQ_INEQ = INT_OF_REAL_THM REAL_SGN_EQ_INEQ;; let INT_SGN_INEQS = INT_OF_REAL_THM REAL_SGN_INEQS;; +let INT_SGN_INT_SGN = INT_OF_REAL_THM REAL_SGN_REAL_SGN;; let INT_SGN_MUL = INT_OF_REAL_THM REAL_SGN_MUL;; let INT_SGN_NEG = INT_OF_REAL_THM REAL_SGN_NEG;; let INT_SGN_POW = INT_OF_REAL_THM REAL_SGN_POW;; let INT_SGN_POW_2 = INT_OF_REAL_THM REAL_SGN_POW_2;; -let INT_SGN_INT_SGN = INT_OF_REAL_THM REAL_SGN_REAL_SGN;; -let INT_SGNS_EQ = INT_OF_REAL_THM REAL_SGNS_EQ;; -let INT_SGNS_EQ_ALT = INT_OF_REAL_THM REAL_SGNS_EQ_ALT;; let INT_SOS_EQ_0 = INT_OF_REAL_THM REAL_SOS_EQ_0;; let INT_SUB_0 = INT_OF_REAL_THM REAL_SUB_0;; let INT_SUB_ABS = INT_OF_REAL_THM REAL_SUB_ABS;; diff --git a/parser.ml b/parser.ml index d856f6e9..b98a4a4e 100644 --- a/parser.ml +++ b/parser.ml @@ -479,7 +479,7 @@ let parse_preterm = >> (pmk_list o snd o fst)) ||| (a (Resword "[") ++ elistof preterm (a (Resword ";")) "semicolon separated list of terms" - >> (fun _ -> failwith "closing square bracket on list expected")) + >> (fun _ -> failwith "closing square bracket of list expected")) ||| (a (Resword "{") ++ (elistof nocommapreterm (a (Ident ",")) "comma separated list of terms" ++ a (Resword "}") >> lmk_setenum diff --git a/real.ml b/real.ml index 8e3e14da..8aa03fe5 100644 --- a/real.ml +++ b/real.ml @@ -1373,6 +1373,10 @@ let REAL_POW_EQ_EQ = prove FIRST_X_ASSUM(X_CHOOSE_THEN `m:num` SUBST1_TAC o REWRITE_RULE[EVEN_EXISTS]) THEN ASM_REWRITE_TAC[GSYM REAL_POW_POW]);; +let REAL_EVENPOW_ABS = prove + (`!x n. EVEN n ==> abs x pow n = x pow n`, + SIMP_TAC[REAL_POW_EQ_EQ; REAL_ABS_ABS]);; + (* ------------------------------------------------------------------------- *) (* Bounds on convex combinations. *) (* ------------------------------------------------------------------------- *)