I was able to turn a miz3 proof into a HOL Light tactics proof. As I barely
understand tactics, maybe someone can make a suggestion. First, three CLAUSES
results from iterate.ml have odd-looking statements, which I changed without
understanding any of the tactics. I just made the final else clauses
{} / neutral op / 0.
instead of
m..n / iterate op (m..n) f / nsum(m..n) f.
Then I improved my earlier miz3 proof a bit, and turned it into a tactics proof
by trial-and-erroring with the tactics proof of ITERATE_CLAUS_NUMSEG. I feel
that there should be a tactics proof that doesn't use my long ASM_MESON_TAC
tactic, which of course I took right out of my miz3 proof.
--
Best,
Bill
let NUMSEG_CLAUS = prove
(`(!m. m..0 = if m = 0 then {0} else {}) /\
(!m n. m..SUC n = if m <= SUC n then (SUC n) INSERT (m..n) else {})`,
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
GEN_REWRITE_TAC I [EXTENSION] THEN
REWRITE_TAC[IN_NUMSEG; NOT_IN_EMPTY; IN_INSERT] THEN
POP_ASSUM MP_TAC THEN ARITH_TAC);;
let ITERATE_CLAUS_NUMSEG = prove
(`!op. monoidal op
==> (!m. iterate op (m..0) f = if m = 0 then f(0) else neutral op) /\
(!m n. iterate op (m..SUC n) f =
if m <= SUC n then op (iterate op (m..n) f) (f(SUC n))
else neutral op)`,
REWRITE_TAC[NUMSEG_CLAUS] THEN REPEAT STRIP_TAC THEN
COND_CASES_TAC THEN
ASM_SIMP_TAC[ITERATE_CLAUSES; FINITE_NUMSEG; IN_NUMSEG; FINITE_EMPTY] THEN
REWRITE_TAC[ARITH_RULE `~(SUC n <= n)`; NOT_IN_EMPTY] THEN
ASM_MESON_TAC[monoidal; ITERATE_CLAUSES_GEN]);;
let NSUM_CLAUS_NUMSEG = prove
(`(!m. nsum(m..0) f = if m = 0 then f(0) else 0) /\
(!m n. nsum(m..SUC n) f = if m <= SUC n then nsum(m..n) f + f(SUC n)
else 0)`,
MP_TAC(MATCH_MP ITERATE_CLAUS_NUMSEG MONOIDAL_ADD) THEN
REWRITE_TAC[NEUTRAL_ADD; nsum]);;
horizon := 0;;
timeout := 50;;
let NSUM_CLAUS1_NUMSEG = thm `;
let f be num->num;
thus (! m. nsum (m..0) f = if m = 0 then f 0 else 0) /\
! m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n) else 0
proof
! m. nsum (m..0) f = (if m = 0 then f 0 else 0) [mf0]
by NUMSEG_CLAUS, NSUM_SING, NSUM_CLAUSES;
! m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n)
else 0
proof
let m n be num;
FINITE (m..n) [mnFinite] by FINITE_NUMSEG;
~(SUC n <= n) by ARITH_RULE;
~(SUC n IN (m..n)) [TooBig] by -, IN_NUMSEG;
nsum (m..SUC n) f = if m <= SUC n then nsum (SUC n INSERT (m..n)) f else
nsum {} f by NUMSEG_CLAUS;
qed by mnFinite, TooBig, NUMSEG_CLAUS, -, NSUM_CLAUSES, ADD_SYM;
qed by mf0, -;
`;;
let NSUM_CLAUS2_NUMSEG = prove
(`(!m. nsum (m..0) f = if m = 0 then f 0 else 0) /\
!m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n) else
0`,
REWRITE_TAC[NUMSEG_CLAUS] THEN REPEAT STRIP_TAC THEN COND_CASES_TAC THEN
ASM_SIMP_TAC[NSUM_SING] THEN ASM_SIMP_TAC[NSUM_CLAUSES] THEN
ASM_SIMP_TAC[FINITE_NUMSEG] THEN
ASM_MESON_TAC[FINITE_NUMSEG; ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG;
NUMSEG_CLAUS; NSUM_CLAUSES; ADD_SYM]);;
------------------------------------------------------------------------------
Keep yourself connected to Go Parallel:
DESIGN Expert tips on starting your parallel project right.
http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
