normalizerScript.sml

1Theory normalizer[bare]
2Ancestors
3  arithmetic
4Libs
5  HolKernel Parse boolLib boolSimps simpLib tautLib mesonLib
6
7(* from numLib.sml, not defined yet when compiling this file *)
8val INDUCT_TAC = INDUCT_THEN numTheory.INDUCTION ASSUME_TAC
9
10fun is_comm t =
11    let val (l,r) = dest_eq $ #2 $ strip_forall t
12        val (f, xs) = strip_comb l
13        val _ = length xs = 2 orelse raise mk_HOL_ERR "" "" ""
14        val (g, ys) = strip_comb r
15        val _ = length ys = 2 orelse raise mk_HOL_ERR "" "" ""
16    in
17      f ~~ g andalso el 1 xs ~~ el 2 ys andalso el 2 xs ~~ el 1 ys
18    end handle HOL_ERR _ => false
19
20Theorem SEMIRING_PTHS:
21  (!(x:'a) y z. add x (add y z) = add (add x y) z) /\
22  (!x y. add x y = add y x) /\
23  (!x. add r0 x = x) /\
24  (!x y z. mul x (mul y z) = mul (mul x y) z) /\
25  (!x y. mul x y = mul y x) /\
26  (!x. mul r1 x = x) /\
27  (!x. mul r0 x = r0) /\
28  (!x y z. mul x (add y z) = add (mul x y) (mul x z)) /\
29  (!x. pwr x 0 = r1) /\
30  (!x n. pwr x (SUC n) = mul x (pwr x n))
31  ==> (mul r1 x = x) /\
32      (add (mul a m) (mul b m) = mul (add a b) m) /\
33      (add (mul a m) m = mul (add a r1) m) /\
34      (add m (mul a m) = mul (add a r1) m) /\
35      (add m m = mul (add r1 r1) m) /\
36      (mul r0 m = r0) /\
37      (add r0 a = a) /\
38      (add a r0 = a) /\
39      (mul a b = mul b a) /\
40      (mul (add a b) c = add (mul a c) (mul b c)) /\
41      (mul r0 a = r0) /\
42      (mul a r0 = r0) /\
43      (mul r1 a = a) /\
44      (mul a r1 = a) /\
45      (mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)) /\
46      (mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))) /\
47      (mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)) /\
48      (mul (mul lx ly) rx = mul (mul lx rx) ly) /\
49      (mul (mul lx ly) rx = mul lx (mul ly rx)) /\
50      (mul lx rx = mul rx lx) /\
51      (mul lx (mul rx ry) = mul (mul lx rx) ry) /\
52      (mul lx (mul rx ry) = mul rx (mul lx ry)) /\
53      (add (add a b) (add c d) = add (add a c) (add b d)) /\
54      (add (add a b) c = add a (add b c)) /\
55      (add a (add c d) = add c (add a d)) /\
56      (add (add a b) c = add (add a c) b) /\
57      (add a c = add c a) /\
58      (add a (add c d) = add (add a c) d) /\
59      (mul (pwr x p) (pwr x q) = pwr x (p + q)) /\
60      (mul x (pwr x q) = pwr x (SUC q)) /\
61      (mul (pwr x q) x = pwr x (SUC q)) /\
62      (mul x x = pwr x 2) /\
63      (pwr (mul x y) q = mul (pwr x q) (pwr y q)) /\
64      (pwr (pwr x p) q = pwr x (p * q)) /\
65      (pwr x 0 = r1) /\
66      (pwr x 1 = x) /\
67      (mul x (add y z) = add (mul x y) (mul x z)) /\
68      (pwr x (SUC q) = mul x (pwr x q))
69Proof
70  STRIP_TAC THEN
71  SUBGOAL_THEN
72    “(!m:'a n. add m n = add n m) /\
73    (!m n p. add (add m n) p = add m (add n p)) /\
74    (!m n p. add m (add n p) = add n (add m p)) /\
75    (!x. add x r0 = x) /\
76    (!m n. mul m n = mul n m) /\
77    (!m n p. mul (mul m n) p = mul m (mul n p)) /\
78    (!m n p. mul m (mul n p) = mul n (mul m p)) /\
79    (!m n p. mul (add m n) p = add (mul m p) (mul n p)) /\
80    (!x. mul x r1 = x) /\
81    (!x. mul x r0 = r0)”
82  MP_TAC
83  >- (rpt strip_tac >>
84      TRY (FIRST_ASSUM MATCH_ACCEPT_TAC) >>
85      FILTER_ASM_REWRITE_TAC (not o is_comm) [] >>
86      rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >>
87      TRY (FIRST_ASSUM MATCH_ACCEPT_TAC) >>
88      ONCE_ASM_REWRITE_TAC[] >>
89      FILTER_ASM_REWRITE_TAC(not o is_comm)[] >>
90      UNDISCH_THEN “!x:'a y. add x y :'a = add y x”
91        (fn th => CONV_TAC (LAND_CONV (REWR_CONV th))) >>
92      UNDISCH_THEN “!x:'a y. mul x y :'a = mul y x”
93        (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th]))) >>
94      REWRITE_TAC[]) >>
95  MAP_EVERY (fn t => UNDISCH_THEN t (K ALL_TAC)) [
96    “!(x:'a) y z. add x (add y z) = add (add x y) z”,
97    “!(x:'a) y. add x y :'a = add y x”,
98    “!(x:'a) y z. mul x (mul y z) = mul (mul x y) z”,
99    “!(x:'a) y. mul x y :'a = mul y x”] THEN STRIP_TAC THEN
100  ASM_SIMP_TAC bool_ss [ONE, TWO] THEN
101  SUBGOAL_THEN “!m (n:num) (x:'a). pwr x (m + n) :'a = mul (pwr x m) (pwr x n)”
102  ASSUME_TAC
103  >- (GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC bool_ss [ADD_CLAUSES]) \\
104  SUBGOAL_THEN
105    “!(x:'a) (y:'a) (n:num). pwr (mul x y) n = mul (pwr x n) (pwr y n)”
106    ASSUME_TAC
107  >- (GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC bool_ss []) \\
108  FILTER_ASM_REWRITE_TAC (not o is_comm) [] >>
109  ID_SPEC_TAC “q:num” THEN INDUCT_TAC THEN ASM_SIMP_TAC bool_ss[MULT_CLAUSES]
110QED
111
112Theorem NUM_NORMALIZE_CONV_sth[local]:
113  (!x y z:num. x + (y + z) = (x + y) + z) /\
114  (!x y:num. x + y = y + x) /\
115  (!x:num. 0 + x = x) /\
116  (!x y z:num. x * (y * z) = (x * y) * z) /\
117  (!x y:num. x * y = y * x) /\
118  (!x:num. 1 * x = x) /\
119  (!x:num. 0 * x = 0) /\
120  (!x y z:num. x * (y + z) = x * y + x * z) /\
121  (!x. x EXP 0 = 1) /\
122  (!x n. x EXP (SUC n) = x * x EXP n)
123Proof
124  REWRITE_TAC[EXP, MULT_CLAUSES, ADD_CLAUSES, LEFT_ADD_DISTRIB] THEN
125  SIMP_TAC bool_ss [AC ADD_SYM ADD_ASSOC, AC MULT_SYM MULT_ASSOC]
126QED
127
128Theorem NUM_NORMALIZE_CONV_sth =
129  MATCH_MP SEMIRING_PTHS NUM_NORMALIZE_CONV_sth;
130
131Theorem RING_FINAL_pth = TAUT `(p ==> F) ==> (~q <=> p) ==> q`;
132Theorem NOT_EVEN = GSYM ODD_EVEN;
133Theorem NOT_ODD  = GSYM EVEN_ODD;
134Theorem PRE_ELIM_THM'' =
135  CONV_RULE (RAND_CONV normalForms.NNFD_CONV) PRE_ELIM_THM'; (* forall *)
136Theorem SUB_ELIM_THM'' =
137  CONV_RULE (RAND_CONV normalForms.NNFD_CONV) SUB_ELIM_THM'; (* forall *)
138Theorem DIVMOD_ELIM_THM'' =
139  CONV_RULE (RAND_CONV normalForms.NNFD_CONV) (SPEC_ALL DIVMOD_ELIM_THM);
140
141Theorem RING_pth_step:
142  !(add:'a->'a->'a) (mul:'a->'a->'a) (n0:'a).
143    (!x. mul n0 x = n0) /\
144    (!x y z. (add x y = add x z) <=> (y = z)) /\
145    (!w x y z. (add (mul w y) (mul x z) = add (mul w z) (mul x y)) <=>
146      (w = x) \/ (y = z))
147    ==>
148    (!a b c d. ~(a = b) /\ ~(c = d) <=>
149      ~(add (mul a c) (mul b d) =
150        add (mul a d) (mul b c))) /\
151    (!n a b c d. ~(n = n0)
152      ==> (a = b) /\ ~(c = d)
153      ==> ~(add a (mul n c) = add b (mul n d)))
154Proof
155  REPEAT GEN_TAC THEN STRIP_TAC THEN
156  ASM_REWRITE_TAC[GSYM DE_MORGAN_THM] THEN
157  REPEAT GEN_TAC THEN DISCH_TAC THEN STRIP_TAC THEN
158  FIRST_X_ASSUM(MP_TAC o SPECL [“n0:'a”, “n:'a”, “d:'a”, “c:'a”]) THEN
159  ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN ASM_SIMP_TAC bool_ss []
160QED
161
162Theorem NUM_SIMPLIFY_CONV_pth_evenodd:
163  (EVEN(x) <=> (!y. ~(x = SUC(2 * y)))) /\
164  (ODD(x) <=> (!y. ~(x = 2 * y))) /\
165  (~EVEN(x) <=> (!y. ~(x = 2 * y))) /\
166  (~ODD(x) <=> (!y. ~(x = SUC(2 * y))))
167Proof
168  rpt strip_tac >| [
169    REWRITE_TAC[EVEN_ODD, ODD_EXISTS],
170    REWRITE_TAC[ODD_EVEN, EVEN_EXISTS],
171    REWRITE_TAC[EVEN_EXISTS],
172    REWRITE_TAC[ODD_EXISTS]
173  ] >> CONV_TAC (LAND_CONV NOT_EXISTS_CONV) >> REWRITE_TAC[]
174QED
175
176Theorem NUM_INTEGRAL_LEMMA:
177  ((w :num) = x + d) /\ (y = z + e)
178  ==> ((w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))
179Proof
180  DISCH_THEN(fn th => REWRITE_TAC[th]) THEN
181  REWRITE_TAC[LEFT_ADD_DISTRIB, RIGHT_ADD_DISTRIB] THEN
182  ONCE_REWRITE_TAC [SIMP_PROVE bool_ss [AC ADD_SYM ADD_ASSOC]
183    “(a :num) + b + (c + d) + e = a + c + (e + (b + d))”] THEN
184  REWRITE_TAC[EQ_ADD_LCANCEL, ADD_INV_0_EQ, MULT_EQ_0]
185QED
186
187Theorem NUM_INTEGRAL:
188  (!(x :num). 0 * x = 0) /\
189  (!(x :num) y z. (x + y = x + z) <=> (y = z)) /\
190  (!(w :num) x y z. (w * y + x * z = w * z + x * y) <=> (w = x) \/ (y = z))
191Proof
192  REWRITE_TAC[MULT_CLAUSES, EQ_ADD_LCANCEL] THEN
193  REPEAT GEN_TAC THEN
194  DISJ_CASES_TAC (SPECL [“w:num”, “x:num”] LE_CASES) THEN
195  DISJ_CASES_TAC (SPECL [“y:num”, “z:num”] LE_CASES) THEN
196  REPEAT (FIRST_X_ASSUM
197    (CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS])) THEN
198  ASM_MESON_TAC [NUM_INTEGRAL_LEMMA, ADD_SYM, MULT_SYM]
199QED
200