1279377Simp(* Title: HOL/Semiring_Normalization.thy 2279377Simp Author: Amine Chaieb, TU Muenchen 3279377Simp*) 4279377Simp 5279377Simpsection \<open>Semiring normalization\<close> 6279377Simp 7279377Simptheory Semiring_Normalization 8279377Simpimports Numeral_Simprocs 9279377Simpbegin 10279377Simp 11279377Simptext \<open>Prelude\<close> 12279377Simp 13279377Simpclass comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel + 14279377Simp assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" 15279377Simpbegin 16279377Simp 17279377Simplemma crossproduct_noteq: 18279377Simp "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> a * c + b * d \<noteq> a * d + b * c" 19279377Simp by (simp add: crossproduct_eq) 20279377Simp 21279377Simplemma add_scale_eq_noteq: 22279377Simp "r \<noteq> 0 \<Longrightarrow> a = b \<and> c \<noteq> d \<Longrightarrow> a + r * c \<noteq> b + r * d" 23279377Simpproof (rule notI) 24279377Simp assume nz: "r\<noteq> 0" and cnd: "a = b \<and> c\<noteq>d" 25279377Simp and eq: "a + (r * c) = b + (r * d)" 26279377Simp have "(0 * d) + (r * c) = (0 * c) + (r * d)" 27279377Simp using add_left_imp_eq eq mult_zero_left by (simp add: cnd) 28279377Simp then show False using crossproduct_eq [of 0 d] nz cnd by simp 29279377Simpqed 30279377Simp 31279377Simplemma add_0_iff: 32279377Simp "b = b + a \<longleftrightarrow> a = 0" 33279377Simp using add_left_imp_eq [of b a 0] by auto 34279377Simp 35279377Simpend 36279377Simp 37279377Simpsubclass (in idom) comm_semiring_1_cancel_crossproduct 38279377Simpproof 39279377Simp fix w x y z 40279377Simp show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" 41279377Simp proof 42279377Simp assume "w * y + x * z = w * z + x * y" 43279377Simp then have "w * y + x * z - w * z - x * y = 0" by (simp add: algebra_simps) 44279377Simp then have "w * (y - z) - x * (y - z) = 0" by (simp add: algebra_simps) 45279377Simp then have "(y - z) * (w - x) = 0" by (simp add: algebra_simps) 46279377Simp then have "y - z = 0 \<or> w - x = 0" by (rule divisors_zero) 47279377Simp then show "w = x \<or> y = z" by auto 48279377Simp qed (auto simp add: ac_simps) 49279377Simpqed 50279377Simp 51279377Simpinstance nat :: comm_semiring_1_cancel_crossproduct 52279377Simpproof 53279377Simp fix w x y z :: nat 54279377Simp have aux: "\<And>y z. y < z \<Longrightarrow> w * y + x * z = w * z + x * y \<Longrightarrow> w = x" 55279377Simp proof - 56279377Simp fix y z :: nat 57279377Simp assume "y < z" then have "\<exists>k. z = y + k \<and> k \<noteq> 0" by (intro exI [of _ "z - y"]) auto 58279377Simp then obtain k where "z = y + k" and "k \<noteq> 0" by blast 59279377Simp assume "w * y + x * z = w * z + x * y" 60279377Simp then have "(w * y + x * y) + x * k = (w * y + x * y) + w * k" by (simp add: \<open>z = y + k\<close> algebra_simps) 61279377Simp then have "x * k = w * k" by simp 62279377Simp then show "w = x" using \<open>k \<noteq> 0\<close> by simp 63279377Simp qed 64279377Simp show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" 65279377Simp by (auto simp add: neq_iff dest!: aux) 66279377Simpqed 67279377Simp 68279377Simptext \<open>Semiring normalization proper\<close> 69279377Simp 70ML_file "Tools/semiring_normalizer.ML" 71 72context comm_semiring_1 73begin 74 75lemma semiring_normalization_rules: 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 "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], 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: 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 "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], 138 @{thms semiring_normalization_rules}), 139 ring = ([@{term "x - y"}, @{term "- x"}], @{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 "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], 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 "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], 168 @{thms semiring_normalization_rules}), 169 ring = ([@{term "x - y"}, @{term "- x"}], @{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 "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], 183 @{thms semiring_normalization_rules}), 184 ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), 185 field = ([@{term "x / y"}, @{term "inverse x"}], @{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