src/HOL/Semiring_Normalization.thy
 author wenzelm Thu May 24 17:25:53 2012 +0200 (2012-05-24) changeset 47988 e4b69e10b990 parent 47108 2a1953f0d20d child 48891 c0eafbd55de3 permissions -rw-r--r--
tuned proofs;
 haftmann@36751 ` 1` ```(* Title: HOL/Semiring_Normalization.thy ``` wenzelm@23252 ` 2` ``` Author: Amine Chaieb, TU Muenchen ``` wenzelm@23252 ` 3` ```*) ``` wenzelm@23252 ` 4` haftmann@36751 ` 5` ```header {* Semiring normalization *} ``` haftmann@28402 ` 6` haftmann@36751 ` 7` ```theory Semiring_Normalization ``` haftmann@36699 ` 8` ```imports Numeral_Simprocs Nat_Transfer ``` wenzelm@23252 ` 9` ```uses ``` haftmann@36753 ` 10` ``` "Tools/semiring_normalizer.ML" ``` wenzelm@23252 ` 11` ```begin ``` wenzelm@23252 ` 12` haftmann@36873 ` 13` ```text {* Prelude *} ``` haftmann@36873 ` 14` haftmann@36873 ` 15` ```class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel + ``` haftmann@36873 ` 16` ``` assumes crossproduct_eq: "w * y + x * z = w * z + x * y \ w = x \ y = z" ``` haftmann@36873 ` 17` ```begin ``` haftmann@36873 ` 18` haftmann@36873 ` 19` ```lemma crossproduct_noteq: ``` haftmann@36873 ` 20` ``` "a \ b \ c \ d \ a * c + b * d \ a * d + b * c" ``` haftmann@36873 ` 21` ``` by (simp add: crossproduct_eq) ``` haftmann@36756 ` 22` haftmann@36873 ` 23` ```lemma add_scale_eq_noteq: ``` haftmann@36873 ` 24` ``` "r \ 0 \ a = b \ c \ d \ a + r * c \ b + r * d" ``` haftmann@36873 ` 25` ```proof (rule notI) ``` haftmann@36873 ` 26` ``` assume nz: "r\ 0" and cnd: "a = b \ c\d" ``` haftmann@36873 ` 27` ``` and eq: "a + (r * c) = b + (r * d)" ``` haftmann@36873 ` 28` ``` have "(0 * d) + (r * c) = (0 * c) + (r * d)" ``` haftmann@36873 ` 29` ``` using add_imp_eq eq mult_zero_left by (simp add: cnd) ``` haftmann@36873 ` 30` ``` then show False using crossproduct_eq [of 0 d] nz cnd by simp ``` haftmann@36873 ` 31` ```qed ``` haftmann@36756 ` 32` haftmann@36873 ` 33` ```lemma add_0_iff: ``` haftmann@36873 ` 34` ``` "b = b + a \ a = 0" ``` haftmann@36873 ` 35` ``` using add_imp_eq [of b a 0] by auto ``` haftmann@36873 ` 36` haftmann@36873 ` 37` ```end ``` haftmann@36873 ` 38` haftmann@37946 ` 39` ```subclass (in idom) comm_semiring_1_cancel_crossproduct ``` haftmann@36756 ` 40` ```proof ``` haftmann@36756 ` 41` ``` fix w x y z ``` haftmann@36756 ` 42` ``` show "w * y + x * z = w * z + x * y \ w = x \ y = z" ``` haftmann@36756 ` 43` ``` proof ``` haftmann@36756 ` 44` ``` assume "w * y + x * z = w * z + x * y" ``` haftmann@36756 ` 45` ``` then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps) ``` haftmann@36756 ` 46` ``` then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) ``` haftmann@36756 ` 47` ``` then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps) ``` haftmann@36756 ` 48` ``` then have "y - z = 0 \ w - x = 0" by (rule divisors_zero) ``` haftmann@36756 ` 49` ``` then show "w = x \ y = z" by auto ``` haftmann@36756 ` 50` ``` qed (auto simp add: add_ac) ``` haftmann@36756 ` 51` ```qed ``` haftmann@36756 ` 52` haftmann@36873 ` 53` ```instance nat :: comm_semiring_1_cancel_crossproduct ``` haftmann@36756 ` 54` ```proof ``` haftmann@36756 ` 55` ``` fix w x y z :: nat ``` haftmann@36873 ` 56` ``` have aux: "\y z. y < z \ w * y + x * z = w * z + x * y \ w = x" ``` haftmann@36873 ` 57` ``` proof - ``` haftmann@36873 ` 58` ``` fix y z :: nat ``` haftmann@36873 ` 59` ``` assume "y < z" then have "\k. z = y + k \ k \ 0" by (intro exI [of _ "z - y"]) auto ``` haftmann@36873 ` 60` ``` then obtain k where "z = y + k" and "k \ 0" by blast ``` haftmann@36873 ` 61` ``` assume "w * y + x * z = w * z + x * y" ``` haftmann@36873 ` 62` ``` then have "(w * y + x * y) + x * k = (w * y + x * y) + w * k" by (simp add: `z = y + k` algebra_simps) ``` haftmann@36873 ` 63` ``` then have "x * k = w * k" by simp ``` haftmann@36873 ` 64` ``` then show "w = x" using `k \ 0` by simp ``` haftmann@36873 ` 65` ``` qed ``` haftmann@36873 ` 66` ``` show "w * y + x * z = w * z + x * y \ w = x \ y = z" ``` haftmann@36873 ` 67` ``` by (auto simp add: neq_iff dest!: aux) ``` haftmann@36756 ` 68` ```qed ``` haftmann@36756 ` 69` haftmann@36873 ` 70` ```text {* Semiring normalization proper *} ``` haftmann@36871 ` 71` haftmann@36753 ` 72` ```setup Semiring_Normalizer.setup ``` wenzelm@23252 ` 73` haftmann@36871 ` 74` ```context comm_semiring_1 ``` haftmann@36871 ` 75` ```begin ``` haftmann@36871 ` 76` haftmann@36872 ` 77` ```lemma normalizing_semiring_ops: ``` hoelzl@36845 ` 78` ``` shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)" ``` hoelzl@36845 ` 79` ``` and "TERM 0" and "TERM 1" . ``` wenzelm@23252 ` 80` haftmann@36872 ` 81` ```lemma normalizing_semiring_rules: ``` hoelzl@36845 ` 82` ``` "(a * m) + (b * m) = (a + b) * m" ``` hoelzl@36845 ` 83` ``` "(a * m) + m = (a + 1) * m" ``` hoelzl@36845 ` 84` ``` "m + (a * m) = (a + 1) * m" ``` hoelzl@36845 ` 85` ``` "m + m = (1 + 1) * m" ``` hoelzl@36845 ` 86` ``` "0 + a = a" ``` hoelzl@36845 ` 87` ``` "a + 0 = a" ``` hoelzl@36845 ` 88` ``` "a * b = b * a" ``` hoelzl@36845 ` 89` ``` "(a + b) * c = (a * c) + (b * c)" ``` hoelzl@36845 ` 90` ``` "0 * a = 0" ``` hoelzl@36845 ` 91` ``` "a * 0 = 0" ``` hoelzl@36845 ` 92` ``` "1 * a = a" ``` hoelzl@36845 ` 93` ``` "a * 1 = a" ``` hoelzl@36845 ` 94` ``` "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" ``` hoelzl@36845 ` 95` ``` "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" ``` hoelzl@36845 ` 96` ``` "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" ``` hoelzl@36845 ` 97` ``` "(lx * ly) * rx = (lx * rx) * ly" ``` hoelzl@36845 ` 98` ``` "(lx * ly) * rx = lx * (ly * rx)" ``` hoelzl@36845 ` 99` ``` "lx * (rx * ry) = (lx * rx) * ry" ``` hoelzl@36845 ` 100` ``` "lx * (rx * ry) = rx * (lx * ry)" ``` hoelzl@36845 ` 101` ``` "(a + b) + (c + d) = (a + c) + (b + d)" ``` hoelzl@36845 ` 102` ``` "(a + b) + c = a + (b + c)" ``` hoelzl@36845 ` 103` ``` "a + (c + d) = c + (a + d)" ``` hoelzl@36845 ` 104` ``` "(a + b) + c = (a + c) + b" ``` hoelzl@36845 ` 105` ``` "a + c = c + a" ``` hoelzl@36845 ` 106` ``` "a + (c + d) = (a + c) + d" ``` hoelzl@36845 ` 107` ``` "(x ^ p) * (x ^ q) = x ^ (p + q)" ``` hoelzl@36845 ` 108` ``` "x * (x ^ q) = x ^ (Suc q)" ``` hoelzl@36845 ` 109` ``` "(x ^ q) * x = x ^ (Suc q)" ``` hoelzl@36845 ` 110` ``` "x * x = x ^ 2" ``` hoelzl@36845 ` 111` ``` "(x * y) ^ q = (x ^ q) * (y ^ q)" ``` hoelzl@36845 ` 112` ``` "(x ^ p) ^ q = x ^ (p * q)" ``` hoelzl@36845 ` 113` ``` "x ^ 0 = 1" ``` hoelzl@36845 ` 114` ``` "x ^ 1 = x" ``` hoelzl@36845 ` 115` ``` "x * (y + z) = (x * y) + (x * z)" ``` hoelzl@36845 ` 116` ``` "x ^ (Suc q) = x * (x ^ q)" ``` hoelzl@36845 ` 117` ``` "x ^ (2*n) = (x ^ n) * (x ^ n)" ``` hoelzl@36845 ` 118` ``` "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))" ``` huffman@47108 ` 119` ``` by (simp_all add: algebra_simps power_add power2_eq_square ``` huffman@47108 ` 120` ``` power_mult_distrib power_mult del: one_add_one) ``` wenzelm@23252 ` 121` haftmann@36871 ` 122` ```lemmas normalizing_comm_semiring_1_axioms = ``` haftmann@36756 ` 123` ``` comm_semiring_1_axioms [normalizer ``` haftmann@36872 ` 124` ``` semiring ops: normalizing_semiring_ops ``` haftmann@36872 ` 125` ``` semiring rules: normalizing_semiring_rules] ``` haftmann@36756 ` 126` haftmann@36871 ` 127` ```declaration ``` haftmann@36756 ` 128` ``` {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *} ``` wenzelm@23573 ` 129` haftmann@36871 ` 130` ```end ``` wenzelm@23252 ` 131` haftmann@36871 ` 132` ```context comm_ring_1 ``` haftmann@36871 ` 133` ```begin ``` haftmann@36871 ` 134` haftmann@36872 ` 135` ```lemma normalizing_ring_ops: shows "TERM (x- y)" and "TERM (- x)" . ``` haftmann@36871 ` 136` haftmann@36872 ` 137` ```lemma normalizing_ring_rules: ``` hoelzl@36845 ` 138` ``` "- x = (- 1) * x" ``` hoelzl@36845 ` 139` ``` "x - y = x + (- y)" ``` hoelzl@36845 ` 140` ``` by (simp_all add: diff_minus) ``` wenzelm@23252 ` 141` haftmann@36871 ` 142` ```lemmas normalizing_comm_ring_1_axioms = ``` haftmann@36756 ` 143` ``` comm_ring_1_axioms [normalizer ``` haftmann@36872 ` 144` ``` semiring ops: normalizing_semiring_ops ``` haftmann@36872 ` 145` ``` semiring rules: normalizing_semiring_rules ``` haftmann@36872 ` 146` ``` ring ops: normalizing_ring_ops ``` haftmann@36872 ` 147` ``` ring rules: normalizing_ring_rules] ``` chaieb@30866 ` 148` haftmann@36871 ` 149` ```declaration ``` haftmann@36756 ` 150` ``` {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *} ``` chaieb@23327 ` 151` haftmann@36871 ` 152` ```end ``` haftmann@36871 ` 153` haftmann@36873 ` 154` ```context comm_semiring_1_cancel_crossproduct ``` haftmann@36871 ` 155` ```begin ``` haftmann@36871 ` 156` haftmann@36871 ` 157` ```declare ``` haftmann@36756 ` 158` ``` normalizing_comm_semiring_1_axioms [normalizer del] ``` wenzelm@23252 ` 159` haftmann@36871 ` 160` ```lemmas ``` haftmann@36873 ` 161` ``` normalizing_comm_semiring_1_cancel_crossproduct_axioms = ``` haftmann@36873 ` 162` ``` comm_semiring_1_cancel_crossproduct_axioms [normalizer ``` haftmann@36872 ` 163` ``` semiring ops: normalizing_semiring_ops ``` haftmann@36872 ` 164` ``` semiring rules: normalizing_semiring_rules ``` haftmann@36873 ` 165` ``` idom rules: crossproduct_noteq add_scale_eq_noteq] ``` wenzelm@23252 ` 166` haftmann@36871 ` 167` ```declaration ``` haftmann@36873 ` 168` ``` {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_crossproduct_axioms} *} ``` wenzelm@23252 ` 169` haftmann@36871 ` 170` ```end ``` wenzelm@23252 ` 171` haftmann@36871 ` 172` ```context idom ``` haftmann@36871 ` 173` ```begin ``` haftmann@36871 ` 174` haftmann@36871 ` 175` ```declare normalizing_comm_ring_1_axioms [normalizer del] ``` haftmann@36871 ` 176` haftmann@36871 ` 177` ```lemmas normalizing_idom_axioms = idom_axioms [normalizer ``` haftmann@36872 ` 178` ``` semiring ops: normalizing_semiring_ops ``` haftmann@36872 ` 179` ``` semiring rules: normalizing_semiring_rules ``` haftmann@36872 ` 180` ``` ring ops: normalizing_ring_ops ``` haftmann@36872 ` 181` ``` ring rules: normalizing_ring_rules ``` haftmann@36873 ` 182` ``` idom rules: crossproduct_noteq add_scale_eq_noteq ``` hoelzl@36845 ` 183` ``` ideal rules: right_minus_eq add_0_iff] ``` wenzelm@23252 ` 184` haftmann@36871 ` 185` ```declaration ``` haftmann@36756 ` 186` ``` {* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *} ``` wenzelm@23252 ` 187` haftmann@36871 ` 188` ```end ``` haftmann@36871 ` 189` haftmann@36871 ` 190` ```context field ``` haftmann@36871 ` 191` ```begin ``` haftmann@36871 ` 192` haftmann@36872 ` 193` ```lemma normalizing_field_ops: ``` hoelzl@36845 ` 194` ``` shows "TERM (x / y)" and "TERM (inverse x)" . ``` chaieb@23327 ` 195` haftmann@36872 ` 196` ```lemmas normalizing_field_rules = divide_inverse inverse_eq_divide ``` haftmann@28402 ` 197` haftmann@36871 ` 198` ```lemmas normalizing_field_axioms = ``` haftmann@36756 ` 199` ``` field_axioms [normalizer ``` haftmann@36872 ` 200` ``` semiring ops: normalizing_semiring_ops ``` haftmann@36872 ` 201` ``` semiring rules: normalizing_semiring_rules ``` haftmann@36872 ` 202` ``` ring ops: normalizing_ring_ops ``` haftmann@36872 ` 203` ``` ring rules: normalizing_ring_rules ``` haftmann@36872 ` 204` ``` field ops: normalizing_field_ops ``` haftmann@36872 ` 205` ``` field rules: normalizing_field_rules ``` haftmann@36873 ` 206` ``` idom rules: crossproduct_noteq add_scale_eq_noteq ``` hoelzl@36845 ` 207` ``` ideal rules: right_minus_eq add_0_iff] ``` haftmann@36756 ` 208` haftmann@36871 ` 209` ```declaration ``` haftmann@36756 ` 210` ``` {* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *} ``` haftmann@28402 ` 211` haftmann@36871 ` 212` ```end ``` haftmann@36871 ` 213` hoelzl@36845 ` 214` ```hide_fact (open) normalizing_comm_semiring_1_axioms ``` haftmann@36873 ` 215` ``` normalizing_comm_semiring_1_cancel_crossproduct_axioms normalizing_semiring_ops normalizing_semiring_rules ``` hoelzl@36845 ` 216` hoelzl@36845 ` 217` ```hide_fact (open) normalizing_comm_ring_1_axioms ``` haftmann@36872 ` 218` ``` normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules ``` hoelzl@36845 ` 219` haftmann@36872 ` 220` ```hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules ``` hoelzl@36845 ` 221` huffman@47108 ` 222` ```code_modulename SML ``` huffman@47108 ` 223` ``` Semiring_Normalization Arith ``` huffman@47108 ` 224` huffman@47108 ` 225` ```code_modulename OCaml ``` huffman@47108 ` 226` ``` Semiring_Normalization Arith ``` huffman@47108 ` 227` huffman@47108 ` 228` ```code_modulename Haskell ``` huffman@47108 ` 229` ``` Semiring_Normalization Arith ``` huffman@47108 ` 230` haftmann@28402 ` 231` ```end ```