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