reduceScript.sml

1Theory reduce[bare]
2Ancestors
3  arithmetic
4Libs
5  HolKernel Parse boolLib computeLib
6
7Theorem num_case_compute_lazy =
8  lazyfy_thm arithmeticTheory.num_case_compute;
9
10Theorem div_thm:
11  !x y q r. x DIV y = if (x = q * y + r) /\ (r < y) then q else x DIV y
12Proof
13  REPEAT STRIP_TAC THEN COND_CASES_TAC THEN REWRITE_TAC [] THEN
14  MATCH_MP_TAC DIV_UNIQUE THEN EXISTS_TAC (Term `r:num`) THEN
15  ASM_REWRITE_TAC []
16QED
17
18Theorem mod_thm:
19  !x y q r. x MOD y = if (x = q * y + r) /\ r<y then r else x MOD y
20Proof
21  REPEAT STRIP_TAC THEN COND_CASES_TAC THEN REWRITE_TAC [] THEN
22  MATCH_MP_TAC MOD_UNIQUE THEN EXISTS_TAC (Term `q:num`) THEN
23  ASM_REWRITE_TAC []
24QED
25