1 files changed, 36 insertions, 0 deletions
diff --git a/hol-light/TacticRecording/examples3_output.txt b/hol-light/TacticRecording/examples3_output.txt
new file mode 100644
index 00000000..18d4901f
--- /dev/null
+++ b/hol-light/TacticRecording/examples3_output.txt
@@ -0,0 +1,36 @@
+# let LEMMA_1 = prove
+ (`!x n. x pow (n + 1) - (&n + &1) * x + &n =
+         (x - &1) pow 2 * sum(1..n) (\k. &k * x pow (n - k))`,
+  CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN INDUCT_TAC THEN
+  REWRITE_TAC[SUM_CLAUSES_NUMSEG; ARITH_EQ; ADD_CLAUSES] THENL
+   [REAL_ARITH_TAC; REWRITE_TAC[ARITH_RULE `1 <= SUC n`]] THEN
+  SIMP_TAC[ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; SUB_REFL] THEN
+  REWRITE_TAC[real_pow; REAL_MUL_RID] THEN
+  REWRITE_TAC[REAL_ARITH `k * x * x pow n = (k * x pow n) * x`] THEN
+  ASM_REWRITE_TAC[SUM_RMUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN
+  REWRITE_TAC[GSYM REAL_OF_NUM_SUC; REAL_POW_ADD] THEN REAL_ARITH_TAC);;
+val ( LEMMA_1 ) : thm =
+  |- !x n.
+         x pow (n + 1) - (&n + &1) * x + &n =
+         (x - &1) pow 2 * sum (1..n) (\k. &k * x pow (n - k))
+
+# print_executed_proof ();;
+e ((CONV_TAC (ONCE_DEPTH_CONV SYM_CONV)) THEN GEN_TAC THEN INDUCT_TAC THEN (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]) THENL [REAL_ARITH_TAC; REWRITE_TAC [ARITH_RULE `1 <= SUC n`]] THEN (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]) THEN (REWRITE_TAC [real_pow;REAL_MUL_RID]) THEN (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]) THEN (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]) THEN (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]) THEN REAL_ARITH_TAC);;
+
+val it : unit = () 
+# print_flat_proof ();;
+e (CONV_TAC (ONCE_DEPTH_CONV SYM_CONV));;
+e (GEN_TAC);;
+e (INDUCT_TAC);;
+e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
+e (REAL_ARITH_TAC);;
+e (REWRITE_TAC [SUM_CLAUSES_NUMSEG;ARITH_EQ;ADD_CLAUSES]);;
+e (REWRITE_TAC [ARITH_RULE `1 <= SUC n`]);;
+e (SIMP_TAC [ARITH_RULE `k <= n ==> SUC n - k = SUC (n - k)`; SUB_REFL]);;
+e (REWRITE_TAC [real_pow;REAL_MUL_RID]);;
+e (REWRITE_TAC [REAL_ARITH `k * x * x pow n = (k * x pow n) * x`]);;
+e (ASM_REWRITE_TAC [SUM_RMUL;REAL_MUL_ASSOC;REAL_ADD_LDISTRIB]);;
+e (REWRITE_TAC [GSYM REAL_OF_NUM_SUC; REAL_POW_ADD]);;
+e (REAL_ARITH_TAC);;
+
+