src/HOL/Semiring_Normalization.thy
 author wenzelm Thu Sep 10 16:44:17 2015 +0200 (2015-09-10) changeset 61153 3d5e01b427cb parent 60758 d8d85a8172b5 child 66836 4eb431c3f974 permissions -rw-r--r--
more standard local_theory operations;
eliminated slightly odd @{cpat};
 haftmann@36751 ` 1` ```(* Title: HOL/Semiring_Normalization.thy ``` wenzelm@23252 ` 2` ``` Author: Amine Chaieb, TU Muenchen ``` wenzelm@23252 ` 3` ```*) ``` wenzelm@23252 ` 4` wenzelm@60758 ` 5` ```section \Semiring normalization\ ``` haftmann@28402 ` 6` haftmann@36751 ` 7` ```theory Semiring_Normalization ``` haftmann@36699 ` 8` ```imports Numeral_Simprocs Nat_Transfer ``` wenzelm@23252 ` 9` ```begin ``` wenzelm@23252 ` 10` wenzelm@60758 ` 11` ```text \Prelude\ ``` haftmann@36873 ` 12` haftmann@36873 ` 13` ```class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel + ``` haftmann@36873 ` 14` ``` assumes crossproduct_eq: "w * y + x * z = w * z + x * y \ w = x \ y = z" ``` haftmann@36873 ` 15` ```begin ``` haftmann@36873 ` 16` haftmann@36873 ` 17` ```lemma crossproduct_noteq: ``` haftmann@36873 ` 18` ``` "a \ b \ c \ d \ a * c + b * d \ a * d + b * c" ``` haftmann@36873 ` 19` ``` by (simp add: crossproduct_eq) ``` haftmann@36756 ` 20` haftmann@36873 ` 21` ```lemma add_scale_eq_noteq: ``` haftmann@36873 ` 22` ``` "r \ 0 \ a = b \ c \ d \ a + r * c \ b + r * d" ``` haftmann@36873 ` 23` ```proof (rule notI) ``` haftmann@36873 ` 24` ``` assume nz: "r\ 0" and cnd: "a = b \ c\d" ``` haftmann@36873 ` 25` ``` and eq: "a + (r * c) = b + (r * d)" ``` haftmann@36873 ` 26` ``` have "(0 * d) + (r * c) = (0 * c) + (r * d)" ``` haftmann@59557 ` 27` ``` using add_left_imp_eq eq mult_zero_left by (simp add: cnd) ``` haftmann@36873 ` 28` ``` then show False using crossproduct_eq [of 0 d] nz cnd by simp ``` haftmann@36873 ` 29` ```qed ``` haftmann@36756 ` 30` haftmann@36873 ` 31` ```lemma add_0_iff: ``` haftmann@36873 ` 32` ``` "b = b + a \ a = 0" ``` haftmann@59557 ` 33` ``` using add_left_imp_eq [of b a 0] by auto ``` haftmann@36873 ` 34` haftmann@36873 ` 35` ```end ``` haftmann@36873 ` 36` haftmann@37946 ` 37` ```subclass (in idom) comm_semiring_1_cancel_crossproduct ``` haftmann@36756 ` 38` ```proof ``` haftmann@36756 ` 39` ``` fix w x y z ``` haftmann@36756 ` 40` ``` show "w * y + x * z = w * z + x * y \ w = x \ y = z" ``` haftmann@36756 ` 41` ``` proof ``` haftmann@36756 ` 42` ``` assume "w * y + x * z = w * z + x * y" ``` haftmann@36756 ` 43` ``` then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps) ``` haftmann@36756 ` 44` ``` then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) ``` haftmann@36756 ` 45` ``` then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps) ``` haftmann@36756 ` 46` ``` then have "y - z = 0 \ w - x = 0" by (rule divisors_zero) ``` haftmann@36756 ` 47` ``` then show "w = x \ y = z" by auto ``` haftmann@57514 ` 48` ``` qed (auto simp add: ac_simps) ``` haftmann@36756 ` 49` ```qed ``` haftmann@36756 ` 50` haftmann@36873 ` 51` ```instance nat :: comm_semiring_1_cancel_crossproduct ``` haftmann@36756 ` 52` ```proof ``` haftmann@36756 ` 53` ``` fix w x y z :: nat ``` haftmann@36873 ` 54` ``` have aux: "\y z. y < z \ w * y + x * z = w * z + x * y \ w = x" ``` haftmann@36873 ` 55` ``` proof - ``` haftmann@36873 ` 56` ``` fix y z :: nat ``` haftmann@36873 ` 57` ``` assume "y < z" then have "\k. z = y + k \ k \ 0" by (intro exI [of _ "z - y"]) auto ``` haftmann@36873 ` 58` ``` then obtain k where "z = y + k" and "k \ 0" by blast ``` haftmann@36873 ` 59` ``` assume "w * y + x * z = w * z + x * y" ``` wenzelm@60758 ` 60` ``` then have "(w * y + x * y) + x * k = (w * y + x * y) + w * k" by (simp add: \z = y + k\ algebra_simps) ``` haftmann@36873 ` 61` ``` then have "x * k = w * k" by simp ``` wenzelm@60758 ` 62` ``` then show "w = x" using \k \ 0\ by simp ``` haftmann@36873 ` 63` ``` qed ``` haftmann@36873 ` 64` ``` show "w * y + x * z = w * z + x * y \ w = x \ y = z" ``` haftmann@36873 ` 65` ``` by (auto simp add: neq_iff dest!: aux) ``` haftmann@36756 ` 66` ```qed ``` haftmann@36756 ` 67` wenzelm@60758 ` 68` ```text \Semiring normalization proper\ ``` haftmann@36871 ` 69` wenzelm@58826 ` 70` ```ML_file "Tools/semiring_normalizer.ML" ``` wenzelm@23252 ` 71` haftmann@36871 ` 72` ```context comm_semiring_1 ``` haftmann@36871 ` 73` ```begin ``` haftmann@36871 ` 74` wenzelm@61153 ` 75` ```lemma semiring_normalization_rules: ``` wenzelm@61153 ` 76` ``` "(a * m) + (b * m) = (a + b) * m" ``` wenzelm@61153 ` 77` ``` "(a * m) + m = (a + 1) * m" ``` wenzelm@61153 ` 78` ``` "m + (a * m) = (a + 1) * m" ``` wenzelm@61153 ` 79` ``` "m + m = (1 + 1) * m" ``` wenzelm@61153 ` 80` ``` "0 + a = a" ``` wenzelm@61153 ` 81` ``` "a + 0 = a" ``` wenzelm@61153 ` 82` ``` "a * b = b * a" ``` wenzelm@61153 ` 83` ``` "(a + b) * c = (a * c) + (b * c)" ``` wenzelm@61153 ` 84` ``` "0 * a = 0" ``` wenzelm@61153 ` 85` ``` "a * 0 = 0" ``` wenzelm@61153 ` 86` ``` "1 * a = a" ``` wenzelm@61153 ` 87` ``` "a * 1 = a" ``` wenzelm@61153 ` 88` ``` "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" ``` wenzelm@61153 ` 89` ``` "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" ``` wenzelm@61153 ` 90` ``` "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" ``` wenzelm@61153 ` 91` ``` "(lx * ly) * rx = (lx * rx) * ly" ``` wenzelm@61153 ` 92` ``` "(lx * ly) * rx = lx * (ly * rx)" ``` wenzelm@61153 ` 93` ``` "lx * (rx * ry) = (lx * rx) * ry" ``` wenzelm@61153 ` 94` ``` "lx * (rx * ry) = rx * (lx * ry)" ``` wenzelm@61153 ` 95` ``` "(a + b) + (c + d) = (a + c) + (b + d)" ``` wenzelm@61153 ` 96` ``` "(a + b) + c = a + (b + c)" ``` wenzelm@61153 ` 97` ``` "a + (c + d) = c + (a + d)" ``` wenzelm@61153 ` 98` ``` "(a + b) + c = (a + c) + b" ``` wenzelm@61153 ` 99` ``` "a + c = c + a" ``` wenzelm@61153 ` 100` ``` "a + (c + d) = (a + c) + d" ``` wenzelm@61153 ` 101` ``` "(x ^ p) * (x ^ q) = x ^ (p + q)" ``` wenzelm@61153 ` 102` ``` "x * (x ^ q) = x ^ (Suc q)" ``` wenzelm@61153 ` 103` ``` "(x ^ q) * x = x ^ (Suc q)" ``` wenzelm@61153 ` 104` ``` "x * x = x\<^sup>2" ``` wenzelm@61153 ` 105` ``` "(x * y) ^ q = (x ^ q) * (y ^ q)" ``` wenzelm@61153 ` 106` ``` "(x ^ p) ^ q = x ^ (p * q)" ``` wenzelm@61153 ` 107` ``` "x ^ 0 = 1" ``` wenzelm@61153 ` 108` ``` "x ^ 1 = x" ``` wenzelm@61153 ` 109` ``` "x * (y + z) = (x * y) + (x * z)" ``` wenzelm@61153 ` 110` ``` "x ^ (Suc q) = x * (x ^ q)" ``` wenzelm@61153 ` 111` ``` "x ^ (2*n) = (x ^ n) * (x ^ n)" ``` wenzelm@61153 ` 112` ``` by (simp_all add: algebra_simps power_add power2_eq_square ``` wenzelm@61153 ` 113` ``` power_mult_distrib power_mult del: one_add_one) ``` wenzelm@61153 ` 114` wenzelm@61153 ` 115` ```local_setup \ ``` haftmann@59554 ` 116` ``` Semiring_Normalizer.declare @{thm comm_semiring_1_axioms} ``` wenzelm@61153 ` 117` ``` {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], ``` wenzelm@61153 ` 118` ``` @{thms semiring_normalization_rules}), ``` wenzelm@61153 ` 119` ``` ring = ([], []), ``` wenzelm@61153 ` 120` ``` field = ([], []), ``` wenzelm@61153 ` 121` ``` idom = [], ``` wenzelm@61153 ` 122` ``` ideal = []} ``` wenzelm@61153 ` 123` ```\ ``` haftmann@36756 ` 124` haftmann@36871 ` 125` ```end ``` wenzelm@23252 ` 126` haftmann@36871 ` 127` ```context comm_ring_1 ``` haftmann@36871 ` 128` ```begin ``` haftmann@36871 ` 129` wenzelm@61153 ` 130` ```lemma ring_normalization_rules: ``` wenzelm@61153 ` 131` ``` "- x = (- 1) * x" ``` wenzelm@61153 ` 132` ``` "x - y = x + (- y)" ``` wenzelm@61153 ` 133` ``` by simp_all ``` wenzelm@61153 ` 134` wenzelm@61153 ` 135` ```local_setup \ ``` haftmann@59554 ` 136` ``` Semiring_Normalizer.declare @{thm comm_ring_1_axioms} ``` wenzelm@61153 ` 137` ``` {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], ``` wenzelm@61153 ` 138` ``` @{thms semiring_normalization_rules}), ``` wenzelm@61153 ` 139` ``` ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), ``` wenzelm@61153 ` 140` ``` field = ([], []), ``` wenzelm@61153 ` 141` ``` idom = [], ``` wenzelm@61153 ` 142` ``` ideal = []} ``` wenzelm@61153 ` 143` ```\ ``` chaieb@30866 ` 144` haftmann@36871 ` 145` ```end ``` haftmann@36871 ` 146` haftmann@36873 ` 147` ```context comm_semiring_1_cancel_crossproduct ``` haftmann@36871 ` 148` ```begin ``` haftmann@36871 ` 149` wenzelm@61153 ` 150` ```local_setup \ ``` wenzelm@61153 ` 151` ``` Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms} ``` wenzelm@61153 ` 152` ``` {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], ``` wenzelm@61153 ` 153` ``` @{thms semiring_normalization_rules}), ``` wenzelm@61153 ` 154` ``` ring = ([], []), ``` wenzelm@61153 ` 155` ``` field = ([], []), ``` wenzelm@61153 ` 156` ``` idom = @{thms crossproduct_noteq add_scale_eq_noteq}, ``` wenzelm@61153 ` 157` ``` ideal = []} ``` wenzelm@61153 ` 158` ```\ ``` wenzelm@23252 ` 159` haftmann@36871 ` 160` ```end ``` wenzelm@23252 ` 161` haftmann@36871 ` 162` ```context idom ``` haftmann@36871 ` 163` ```begin ``` haftmann@36871 ` 164` wenzelm@61153 ` 165` ```local_setup \ ``` wenzelm@61153 ` 166` ``` Semiring_Normalizer.declare @{thm idom_axioms} ``` wenzelm@61153 ` 167` ``` {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], ``` wenzelm@61153 ` 168` ``` @{thms semiring_normalization_rules}), ``` wenzelm@61153 ` 169` ``` ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), ``` wenzelm@61153 ` 170` ``` field = ([], []), ``` wenzelm@61153 ` 171` ``` idom = @{thms crossproduct_noteq add_scale_eq_noteq}, ``` wenzelm@61153 ` 172` ``` ideal = @{thms right_minus_eq add_0_iff}} ``` wenzelm@61153 ` 173` ```\ ``` wenzelm@23252 ` 174` haftmann@36871 ` 175` ```end ``` haftmann@36871 ` 176` haftmann@36871 ` 177` ```context field ``` haftmann@36871 ` 178` ```begin ``` haftmann@36871 ` 179` wenzelm@61153 ` 180` ```local_setup \ ``` wenzelm@61153 ` 181` ``` Semiring_Normalizer.declare @{thm field_axioms} ``` wenzelm@61153 ` 182` ``` {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], ``` wenzelm@61153 ` 183` ``` @{thms semiring_normalization_rules}), ``` wenzelm@61153 ` 184` ``` ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), ``` wenzelm@61153 ` 185` ``` field = ([@{term "x / y"}, @{term "inverse x"}], @{thms divide_inverse inverse_eq_divide}), ``` wenzelm@61153 ` 186` ``` idom = @{thms crossproduct_noteq add_scale_eq_noteq}, ``` wenzelm@61153 ` 187` ``` ideal = @{thms right_minus_eq add_0_iff}} ``` wenzelm@61153 ` 188` ```\ ``` haftmann@36756 ` 189` haftmann@36871 ` 190` ```end ``` haftmann@36871 ` 191` haftmann@52435 ` 192` ```code_identifier ``` haftmann@52435 ` 193` ``` code_module Semiring_Normalization \ (SML) Arith and (OCaml) Arith and (Haskell) Arith ``` huffman@47108 ` 194` haftmann@28402 ` 195` ```end ```