diff options
Diffstat (limited to 'hol-light/TacticRecording/examples5.ml')
| -rw-r--r-- | hol-light/TacticRecording/examples5.ml | 241 |
1 files changed, 172 insertions, 69 deletions
diff --git a/hol-light/TacticRecording/examples5.ml b/hol-light/TacticRecording/examples5.ml index 6e34aaee..1ded99cf 100644 --- a/hol-light/TacticRecording/examples5.ml +++ b/hol-light/TacticRecording/examples5.ml @@ -1,79 +1,182 @@ -from Library/binomial.ml +(* Taken from Library/prime.ml *) prioritize_num();; (* ------------------------------------------------------------------------- *) -(* Binomial coefficients. *) +(* HOL88 compatibility (since all this is a port of old HOL88 stuff). *) (* ------------------------------------------------------------------------- *) -let binom = define - `(!n. binom(n,0) = 1) /\ - (!k. binom(0,SUC(k)) = 0) /\ - (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;; - -let binom = theorem_wrap "binom" binom;; - -let BINOM_LT = prove - (`!n k. n < k ==> (binom(n,k) = 0)`, - INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom; ARITH; LT_SUC; LT] THEN - ASM_SIMP_TAC[ARITH_RULE `n < k ==> n < SUC(k)`; ARITH]);; -let BINOM_LT = theorem_wrap "BINOM_LT" BINOM_LT;; - -print_flat_proof true;; - -let BINOM_REFL = prove - (`!n. binom(n,n) = 1`, - INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);; -let BINOM_REFL = theorem_wrap "BINOM_REFL" BINOM_REFL;; - -let BINOM_1 = prove - (`!n. binom(n,1) = n`, - REWRITE_TAC[num_CONV `1`] THEN - INDUCT_TAC THEN ASM_REWRITE_TAC[binom] THEN ARITH_TAC);; -let BINOM_1 = theorem_wrap "BINOM_1" BINOM_1;; - -let BINOM_FACT = prove - (`!n k. FACT n * FACT k * binom(n+k,k) = FACT(n + k)`, - INDUCT_TAC THEN REWRITE_TAC[FACT; ADD_CLAUSES; MULT_CLAUSES; BINOM_REFL] THEN - INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT; MULT_CLAUSES; binom] THEN - FIRST_X_ASSUM(MP_TAC o SPEC `SUC k`) THEN POP_ASSUM MP_TAC THEN - REWRITE_TAC[ADD_CLAUSES; FACT; binom] THEN CONV_TAC NUM_RING);; -let BINOM_FACT = theorem_wrap "BINOM_FACT" BINOM_FACT;; - -let BINOM_EQ_0 = prove - (`!n k. binom(n,k) = 0 <=> n < k`, - REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[BINOM_LT]] THEN - ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN - REWRITE_TAC[NOT_LT; LE_EXISTS] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN - DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN - DISCH_TAC THEN MP_TAC(SYM(SPECL [`d:num`; `k:num`] BINOM_FACT)) THEN - ASM_REWRITE_TAC[GSYM LT_NZ; MULT_CLAUSES; FACT_LT]);; -let BINOM_EQ_0 = theorem_wrap "BINOM_EQ_0" BINOM_EQ_0;; - -let BINOM_PENULT = prove - (`!n. binom(SUC n,n) = SUC n`, - INDUCT_TAC THEN ASM_REWRITE_TAC [binom; ONE; BINOM_REFL] THEN - SUBGOAL_THEN `binom(n,SUC n)=0` SUBST1_TAC THENL - [REWRITE_TAC [BINOM_EQ_0; LT]; REWRITE_TAC [ADD; ADD_0; ADD_SUC; SUC_INJ]]);; -let BINOM_PENULT = theorem_wrap "BINOM_PENULT" BINOM_PENULT;; +let MULT_MONO_EQ = prove + (`!m i n. ((SUC n) * m = (SUC n) * i) <=> (m = i)`, + REWRITE_TAC[EQ_MULT_LCANCEL; NOT_SUC]);; +let LESS_ADD_1 = prove + (`!m n. n < m ==> (?p. m = n + (p + 1))`, + REWRITE_TAC[LT_EXISTS; ADD1; ADD_ASSOC]);; + +let LESS_ADD_SUC = ARITH_RULE `!m n. m < (m + (SUC n))`;; + +let LESS_0_CASES = ARITH_RULE `!m. (0 = m) \/ 0 < m`;; + +let LESS_MONO_ADD = ARITH_RULE `!m n p. m < n ==> (m + p) < (n + p)`;; + +let LESS_EQ_0 = prove + (`!n. n <= 0 <=> (n = 0)`, + REWRITE_TAC[LE]);; + +let LESS_LESS_CASES = ARITH_RULE `!m n. (m = n) \/ m < n \/ n < m`;; + +let LESS_ADD_NONZERO = ARITH_RULE `!m n. ~(n = 0) ==> m < (m + n)`;; + +let NOT_EXP_0 = prove + (`!m n. ~((SUC n) EXP m = 0)`, + REWRITE_TAC[EXP_EQ_0; NOT_SUC]);; + +let LESS_THM = ARITH_RULE `!m n. m < (SUC n) <=> (m = n) \/ m < n`;; + +let NOT_LESS_0 = ARITH_RULE `!n. ~(n < 0)`;; + +let ZERO_LESS_EXP = prove + (`!m n. 0 < ((SUC n) EXP m)`, + REWRITE_TAC[LT_NZ; NOT_EXP_0]);; + +(* ------------------------------------------------------------------------- *) +(* General arithmetic lemmas. *) (* ------------------------------------------------------------------------- *) -(* More potentially useful lemmas. *) + +let MULT_FIX = prove( + `!x y. (x * y = x) <=> (x = 0) \/ (y = 1)`, + REPEAT GEN_TAC THEN + STRUCT_CASES_TAC(SPEC `x:num` num_CASES) THEN + REWRITE_TAC[MULT_CLAUSES; NOT_SUC] THEN + REWRITE_TAC[GSYM(el 4 (CONJUNCTS (SPEC_ALL MULT_CLAUSES)))] THEN + GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) (* MMA: this is a problem !!!!) + [GSYM(el 3 (CONJUNCTS(SPEC_ALL MULT_CLAUSES)))] THEN + MATCH_ACCEPT_TAC MULT_MONO_EQ);; + +let LESS_EQ_MULT = prove( + `!m n p q. m <= n /\ p <= q ==> (m * p) <= (n * q)`, + REPEAT GEN_TAC THEN + DISCH_THEN(STRIP_ASSUME_TAC o REWRITE_RULE[LE_EXISTS]) THEN + ASM_REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; + GSYM ADD_ASSOC; LE_ADD]);; + +let LESS_MULT = prove( + `!m n p q. m < n /\ p < q ==> (m * p) < (n * q)`, + REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN + ((CHOOSE_THEN SUBST_ALL_TAC) o MATCH_MP LESS_ADD_1)) THEN + REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN + REWRITE_TAC[GSYM ADD1; MULT_CLAUSES; ADD_CLAUSES; GSYM ADD_ASSOC] THEN + ONCE_REWRITE_TAC[GSYM (el 3 (CONJUNCTS ADD_CLAUSES))] THEN + MATCH_ACCEPT_TAC LESS_ADD_SUC);; + +let MULT_LCANCEL = prove( + `!a b c. ~(a = 0) /\ (a * b = a * c) ==> (b = c)`, + REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC `a:num` num_CASES) THEN + REWRITE_TAC[NOT_SUC; MULT_MONO_EQ]);; + +let LT_POW2_REFL = prove + (`!n. n < 2 EXP n`, + INDUCT_TAC THEN REWRITE_TAC[EXP] THEN TRY(POP_ASSUM MP_TAC) THEN ARITH_TAC);; + (* ------------------------------------------------------------------------- *) +(* Properties of the exponential function. *) +(* ------------------------------------------------------------------------- *) + +let EXP_0 = prove + (`!n. 0 EXP (SUC n) = 0`, + REWRITE_TAC[EXP; MULT_CLAUSES]);; + +let EXP_MONO_LT_SUC = prove + (`!n x y. (x EXP (SUC n)) < (y EXP (SUC n)) <=> (x < y)`, + REWRITE_TAC[EXP_MONO_LT; NOT_SUC]);; + +let EXP_MONO_LE_SUC = prove + (`!x y n. (x EXP (SUC n)) <= (y EXP (SUC n)) <=> x <= y`, + REWRITE_TAC[EXP_MONO_LE; NOT_SUC]);; + +let EXP_MONO_EQ_SUC = prove + (`!x y n. (x EXP (SUC n) = y EXP (SUC n)) <=> (x = y)`, + REWRITE_TAC[EXP_MONO_EQ; NOT_SUC]);; + +let EXP_EXP = prove + (`!x m n. (x EXP m) EXP n = x EXP (m * n)`, + REWRITE_TAC[EXP_MULT]);; + +(* ------------------------------------------------------------------------- *) +(* More ad-hoc arithmetic lemmas unlikely to be useful elsewhere. *) +(* ------------------------------------------------------------------------- *) + +let DIFF_LEMMA = prove( + `!a b. a < b ==> (a = 0) \/ (a + (b - a)) < (a + b)`, + REPEAT GEN_TAC THEN + DISJ_CASES_TAC(SPEC `a:num` LESS_0_CASES) THEN ASM_REWRITE_TAC[] THEN + DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN + DISJ2_TAC THEN REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN + GEN_REWRITE_TAC LAND_CONV [GSYM (CONJUNCT1 ADD_CLAUSES)] THEN + REWRITE_TAC[ADD_ASSOC] THEN + REPEAT(MATCH_MP_TAC LESS_MONO_ADD) THEN POP_ASSUM ACCEPT_TAC);; + +let NOT_EVEN_EQ_ODD = prove( + `!m n. ~(2 * m = SUC(2 * n))`, + REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN + REWRITE_TAC[EVEN; EVEN_MULT; ARITH]);; + +let CANCEL_TIMES2 = prove( + `!x y. (2 * x = 2 * y) <=> (x = y)`, + REWRITE_TAC[num_CONV `2`; MULT_MONO_EQ]);; + +let EVEN_SQUARE = prove( + `!n. EVEN(n) ==> ?x. n EXP 2 = 4 * x`, + GEN_TAC THEN REWRITE_TAC[EVEN_EXISTS] THEN + DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN + EXISTS_TAC `m * m` THEN REWRITE_TAC[EXP_2] THEN + REWRITE_TAC[SYM(REWRITE_CONV[ARITH] `2 * 2`)] THEN + REWRITE_TAC[MULT_AC]);; + +let ODD_SQUARE = prove( + `!n. ODD(n) ==> ?x. n EXP 2 = (4 * x) + 1`, + GEN_TAC THEN REWRITE_TAC[ODD_EXISTS] THEN + DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST1_TAC) THEN + ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES; ADD_CLAUSES] THEN + REWRITE_TAC[GSYM ADD1; SUC_INJ] THEN + EXISTS_TAC `(m * m) + m` THEN + REWRITE_TAC(map num_CONV [`4`; `3`; `2`; `1`]) THEN + REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN + REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN + REWRITE_TAC[ADD_AC]);; + +let DIFF_SQUARE = prove( + `!x y. (x EXP 2) - (y EXP 2) = (x + y) * (x - y)`, + REPEAT GEN_TAC THEN + DISJ_CASES_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THENL + [SUBGOAL_THEN `(x * x) <= (y * y)` MP_TAC THENL + [MATCH_MP_TAC LESS_EQ_MULT THEN ASM_REWRITE_TAC[]; + POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM SUB_EQ_0] THEN + REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[EXP_2; MULT_CLAUSES]]; + POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN + REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN + REWRITE_TAC[EXP_2; LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN + REWRITE_TAC[GSYM ADD_ASSOC; ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN + AP_TERM_TAC THEN GEN_REWRITE_TAC LAND_CONV [ADD_SYM] THEN + AP_TERM_TAC THEN MATCH_ACCEPT_TAC MULT_SYM]);; + +let ADD_IMP_SUB = prove( + `!x y z. (x + y = z) ==> (x = z - y)`, + REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN + REWRITE_TAC[ADD_SUB]);; + +let ADD_SUM_DIFF = prove( + `!v w. v <= w ==> ((w + v) - (w - v) = 2 * v) /\ + ((w + v) + (w - v) = 2 * w)`, + REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN + DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN + REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB] THEN + REWRITE_TAC[MULT_2; GSYM ADD_ASSOC] THEN + ONCE_REWRITE_TAC[ADD_SYM] THEN + REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUB; GSYM ADD_ASSOC]);; -let BINOM_TOP_STEP = prove - (`!n k. ((n + 1) - k) * binom(n + 1,k) = (n + 1) * binom(n,k)`, - REPEAT GEN_TAC THEN ASM_CASES_TAC `n < k:num` THENL - [FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP - (ARITH_RULE `n < k ==> n + 1 = k \/ n + 1 < k`)) THEN - ASM_SIMP_TAC[BINOM_LT; SUB_REFL; MULT_CLAUSES]; - ALL_TAC] THEN - FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[NOT_LT; LE_EXISTS]) THEN - DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN - REWRITE_TAC[GSYM ADD_ASSOC; ADD_SUB; ADD_SUB2] THEN - MP_TAC(SPECL [`d + 1`; `k:num`] BINOM_FACT) THEN - MP_TAC(SPECL [`d:num`; `k:num`] BINOM_FACT) THEN - REWRITE_TAC[GSYM ADD1; ADD_CLAUSES; FACT; ADD_AC] THEN - MAP_EVERY (fun t -> MP_TAC(SPEC t FACT_LT)) [`d:num`; `k:num`] THEN - REWRITE_TAC[LT_NZ] THEN CONV_TAC NUM_RING);; -let BINOM_TOP_STEP = theorem_wrap "BINOM_TOP_STEP" BINOM_TOP_STEP;; +let EXP_4 = prove( + `!n. n EXP 4 = (n EXP 2) EXP 2`, + GEN_TAC THEN REWRITE_TAC[EXP_EXP] THEN + REWRITE_TAC[ARITH]);; |