src/HOL/Semiring_Normalization.thy
 changeset 36845 d778c64fc35d parent 36756 c1ae8a0b4265 child 36871 3763c349c8c1
```     1.1 --- a/src/HOL/Semiring_Normalization.thy	Tue May 11 19:21:05 2010 +0200
1.2 +++ b/src/HOL/Semiring_Normalization.thy	Tue May 11 19:21:39 2010 +0200
1.3 @@ -52,286 +52,155 @@
1.4
1.5  setup Semiring_Normalizer.setup
1.6
1.7 -locale normalizing_semiring =
1.8 -  fixes add mul pwr r0 r1
1.10 -    and add_c: "add x y = add y x" and add_0:"add r0 x = x"
1.11 -    and mul_a:"mul x (mul y z) = mul (mul x y) z" and mul_c:"mul x y = mul y x"
1.12 -    and mul_1:"mul r1 x = x" and  mul_0:"mul r0 x = r0"
1.13 -    and mul_d:"mul x (add y z) = add (mul x y) (mul x z)"
1.14 -    and pwr_0:"pwr x 0 = r1" and pwr_Suc:"pwr x (Suc n) = mul x (pwr x n)"
1.15 -begin
1.16 -
1.17 -lemma mul_pwr:"mul (pwr x p) (pwr x q) = pwr x (p + q)"
1.18 -proof (induct p)
1.19 -  case 0
1.20 -  then show ?case by (auto simp add: pwr_0 mul_1)
1.21 -next
1.22 -  case Suc
1.23 -  from this [symmetric] show ?case
1.24 -    by (auto simp add: pwr_Suc mul_1 mul_a)
1.25 -qed
1.26 -
1.27 -lemma pwr_mul: "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
1.28 -proof (induct q arbitrary: x y, auto simp add:pwr_0 pwr_Suc mul_1)
1.29 -  fix q x y
1.30 -  assume "\<And>x y. pwr (mul x y) q = mul (pwr x q) (pwr y q)"
1.31 -  have "mul (mul x y) (mul (pwr x q) (pwr y q)) = mul x (mul y (mul (pwr x q) (pwr y q)))"
1.32 -    by (simp add: mul_a)
1.33 -  also have "\<dots> = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c)
1.34 -  also have "\<dots> = (mul (mul y (pwr y q)) (mul (pwr x q) x))" by (simp add: mul_a)
1.35 -  finally show "mul (mul x y) (mul (pwr x q) (pwr y q)) =
1.36 -    mul (mul x (pwr x q)) (mul y (pwr y q))" by (simp add: mul_c)
1.37 -qed
1.38 -
1.39 -lemma pwr_pwr: "pwr (pwr x p) q = pwr x (p * q)"
1.40 -proof (induct p arbitrary: q)
1.41 -  case 0
1.42 -  show ?case using pwr_Suc mul_1 pwr_0 by (induct q) auto
1.43 -next
1.44 -  case Suc
1.45 -  thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc)
1.46 -qed
1.47 -
1.48 -lemma semiring_ops:
1.49 -  shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
1.50 -    and "TERM r0" and "TERM r1" .
1.51 +lemma (in comm_semiring_1) semiring_ops:
1.52 +  shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)"
1.53 +    and "TERM 0" and "TERM 1" .
1.54
1.55 -lemma semiring_rules:
1.56 -  "add (mul a m) (mul b m) = mul (add a b) m"
1.57 -  "add (mul a m) m = mul (add a r1) m"
1.58 -  "add m (mul a m) = mul (add a r1) m"
1.59 -  "add m m = mul (add r1 r1) m"
1.60 -  "add r0 a = a"
1.61 -  "add a r0 = a"
1.62 -  "mul a b = mul b a"
1.63 -  "mul (add a b) c = add (mul a c) (mul b c)"
1.64 -  "mul r0 a = r0"
1.65 -  "mul a r0 = r0"
1.66 -  "mul r1 a = a"
1.67 -  "mul a r1 = a"
1.68 -  "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
1.69 -  "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
1.70 -  "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
1.71 -  "mul (mul lx ly) rx = mul (mul lx rx) ly"
1.72 -  "mul (mul lx ly) rx = mul lx (mul ly rx)"
1.73 -  "mul lx (mul rx ry) = mul (mul lx rx) ry"
1.74 -  "mul lx (mul rx ry) = mul rx (mul lx ry)"
1.79 -  "add a c = add c a"
1.81 -  "mul (pwr x p) (pwr x q) = pwr x (p + q)"
1.82 -  "mul x (pwr x q) = pwr x (Suc q)"
1.83 -  "mul (pwr x q) x = pwr x (Suc q)"
1.84 -  "mul x x = pwr x 2"
1.85 -  "pwr (mul x y) q = mul (pwr x q) (pwr y q)"
1.86 -  "pwr (pwr x p) q = pwr x (p * q)"
1.87 -  "pwr x 0 = r1"
1.88 -  "pwr x 1 = x"
1.89 -  "mul x (add y z) = add (mul x y) (mul x z)"
1.90 -  "pwr x (Suc q) = mul x (pwr x q)"
1.91 -  "pwr x (2*n) = mul (pwr x n) (pwr x n)"
1.92 -  "pwr x (Suc (2*n)) = mul x (mul (pwr x n) (pwr x n))"
1.93 -proof -
1.94 -  show "add (mul a m) (mul b m) = mul (add a b) m" using mul_d mul_c by simp
1.95 -next show"add (mul a m) m = mul (add a r1) m" using mul_d mul_c mul_1 by simp
1.96 -next show "add m (mul a m) = mul (add a r1) m" using mul_c mul_d mul_1 add_c by simp
1.97 -next show "add m m = mul (add r1 r1) m" using mul_c mul_d mul_1 by simp
1.98 -next show "add r0 a = a" using add_0 by simp
1.99 -next show "add a r0 = a" using add_0 add_c by simp
1.100 -next show "mul a b = mul b a" using mul_c by simp
1.101 -next show "mul (add a b) c = add (mul a c) (mul b c)" using mul_c mul_d by simp
1.102 -next show "mul r0 a = r0" using mul_0 by simp
1.103 -next show "mul a r0 = r0" using mul_0 mul_c by simp
1.104 -next show "mul r1 a = a" using mul_1 by simp
1.105 -next show "mul a r1 = a" using mul_1 mul_c by simp
1.106 -next show "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)"
1.107 -    using mul_c mul_a by simp
1.108 -next show "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))"
1.109 -    using mul_a by simp
1.110 -next
1.111 -  have "mul (mul lx ly) (mul rx ry) = mul (mul rx ry) (mul lx ly)" by (rule mul_c)
1.112 -  also have "\<dots> = mul rx (mul ry (mul lx ly))" using mul_a by simp
1.113 -  finally
1.114 -  show "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)"
1.115 -    using mul_c by simp
1.116 -next show "mul (mul lx ly) rx = mul (mul lx rx) ly" using mul_c mul_a by simp
1.117 -next
1.118 -  show "mul (mul lx ly) rx = mul lx (mul ly rx)" by (simp add: mul_a)
1.119 -next show "mul lx (mul rx ry) = mul (mul lx rx) ry" by (simp add: mul_a )
1.120 -next show "mul lx (mul rx ry) = mul rx (mul lx ry)" by (simp add: mul_a,simp add: mul_c)
1.122 -    using add_c add_a by simp
1.123 -next show "add (add a b) c = add a (add b c)" using add_a by simp
1.124 -next show "add a (add c d) = add c (add a d)"
1.125 -    apply (simp add: add_a) by (simp only: add_c)
1.127 -next show "add a c = add c a" by (rule add_c)
1.128 -next show "add a (add c d) = add (add a c) d" using add_a by simp
1.129 -next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr)
1.130 -next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp
1.131 -next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp
1.132 -next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
1.133 -next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
1.134 -next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
1.135 -next show "pwr x 0 = r1" using pwr_0 .
1.136 -next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
1.137 -next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
1.138 -next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
1.139 -next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr)
1.140 -next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))"
1.141 -    by (simp add: nat_number' pwr_Suc mul_pwr)
1.142 -qed
1.143 -
1.144 -end
1.145 -
1.146 -sublocale comm_semiring_1
1.147 -  < normalizing!: normalizing_semiring plus times power zero one
1.148 -proof
1.149 -qed (simp_all add: algebra_simps)
1.150 +lemma (in comm_semiring_1) semiring_rules:
1.151 +  "(a * m) + (b * m) = (a + b) * m"
1.152 +  "(a * m) + m = (a + 1) * m"
1.153 +  "m + (a * m) = (a + 1) * m"
1.154 +  "m + m = (1 + 1) * m"
1.155 +  "0 + a = a"
1.156 +  "a + 0 = a"
1.157 +  "a * b = b * a"
1.158 +  "(a + b) * c = (a * c) + (b * c)"
1.159 +  "0 * a = 0"
1.160 +  "a * 0 = 0"
1.161 +  "1 * a = a"
1.162 +  "a * 1 = a"
1.163 +  "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)"
1.164 +  "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))"
1.165 +  "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)"
1.166 +  "(lx * ly) * rx = (lx * rx) * ly"
1.167 +  "(lx * ly) * rx = lx * (ly * rx)"
1.168 +  "lx * (rx * ry) = (lx * rx) * ry"
1.169 +  "lx * (rx * ry) = rx * (lx * ry)"
1.170 +  "(a + b) + (c + d) = (a + c) + (b + d)"
1.171 +  "(a + b) + c = a + (b + c)"
1.172 +  "a + (c + d) = c + (a + d)"
1.173 +  "(a + b) + c = (a + c) + b"
1.174 +  "a + c = c + a"
1.175 +  "a + (c + d) = (a + c) + d"
1.176 +  "(x ^ p) * (x ^ q) = x ^ (p + q)"
1.177 +  "x * (x ^ q) = x ^ (Suc q)"
1.178 +  "(x ^ q) * x = x ^ (Suc q)"
1.179 +  "x * x = x ^ 2"
1.180 +  "(x * y) ^ q = (x ^ q) * (y ^ q)"
1.181 +  "(x ^ p) ^ q = x ^ (p * q)"
1.182 +  "x ^ 0 = 1"
1.183 +  "x ^ 1 = x"
1.184 +  "x * (y + z) = (x * y) + (x * z)"
1.185 +  "x ^ (Suc q) = x * (x ^ q)"
1.186 +  "x ^ (2*n) = (x ^ n) * (x ^ n)"
1.187 +  "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))"
1.188 +  by (simp_all add: algebra_simps power_add power2_eq_square power_mult_distrib power_mult)
1.189
1.190  lemmas (in comm_semiring_1) normalizing_comm_semiring_1_axioms =
1.191    comm_semiring_1_axioms [normalizer
1.192 -    semiring ops: normalizing.semiring_ops
1.193 -    semiring rules: normalizing.semiring_rules]
1.194 +    semiring ops: semiring_ops
1.195 +    semiring rules: semiring_rules]
1.196
1.197  declaration (in comm_semiring_1)
1.198    {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *}
1.199
1.200 -locale normalizing_ring = normalizing_semiring +
1.201 -  fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.202 -    and neg :: "'a \<Rightarrow> 'a"
1.203 -  assumes neg_mul: "neg x = mul (neg r1) x"
1.204 -    and sub_add: "sub x y = add x (neg y)"
1.205 -begin
1.206 -
1.207 -lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" .
1.208 +lemma (in comm_ring_1) ring_ops: shows "TERM (x- y)" and "TERM (- x)" .
1.209
1.210 -lemmas ring_rules = neg_mul sub_add
1.211 -
1.212 -end
1.213 -
1.214 -sublocale comm_ring_1
1.215 -  < normalizing!: normalizing_ring plus times power zero one minus uminus
1.216 -proof
1.217 -qed (simp_all add: diff_minus)
1.218 +lemma (in comm_ring_1) ring_rules:
1.219 +  "- x = (- 1) * x"
1.220 +  "x - y = x + (- y)"
1.221 +  by (simp_all add: diff_minus)
1.222
1.223  lemmas (in comm_ring_1) normalizing_comm_ring_1_axioms =
1.224    comm_ring_1_axioms [normalizer
1.225 -    semiring ops: normalizing.semiring_ops
1.226 -    semiring rules: normalizing.semiring_rules
1.227 -    ring ops: normalizing.ring_ops
1.228 -    ring rules: normalizing.ring_rules]
1.229 +    semiring ops: semiring_ops
1.230 +    semiring rules: semiring_rules
1.231 +    ring ops: ring_ops
1.232 +    ring rules: ring_rules]
1.233
1.234  declaration (in comm_ring_1)
1.235    {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *}
1.236
1.237 -locale normalizing_semiring_cancel = normalizing_semiring +
1.238 -  assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z"
1.239 -  and add_mul_solve: "add (mul w y) (mul x z) =
1.240 -    add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z"
1.241 -begin
1.242 -
1.243 -lemma noteq_reduce: "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
1.244 +lemma (in comm_semiring_1_cancel_norm) noteq_reduce:
1.245 +  "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
1.246  proof-
1.247    have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp
1.248 -  also have "\<dots> \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
1.249 -    using add_mul_solve by blast
1.250 -  finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)"
1.251 +  also have "\<dots> \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
1.252 +    using add_mult_solve by blast
1.253 +  finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
1.254      by simp
1.255  qed
1.256
1.257 -lemma add_scale_eq_noteq: "\<lbrakk>r \<noteq> r0 ; (a = b) \<and> ~(c = d)\<rbrakk>
1.258 -  \<Longrightarrow> add a (mul r c) \<noteq> add b (mul r d)"
1.259 +lemma (in comm_semiring_1_cancel_norm) add_scale_eq_noteq:
1.260 +  "\<lbrakk>r \<noteq> 0 ; a = b \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> a + (r * c) \<noteq> b + (r * d)"
1.261  proof(clarify)
1.262 -  assume nz: "r\<noteq> r0" and cnd: "c\<noteq>d"
1.263 -    and eq: "add b (mul r c) = add b (mul r d)"
1.264 -  hence "mul r c = mul r d" using cnd add_cancel by simp
1.265 -  hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)"
1.266 -    using mul_0 add_cancel by simp
1.267 -  thus "False" using add_mul_solve nz cnd by simp
1.268 +  assume nz: "r\<noteq> 0" and cnd: "c\<noteq>d"
1.269 +    and eq: "b + (r * c) = b + (r * d)"
1.270 +  have "(0 * d) + (r * c) = (0 * c) + (r * d)"
1.271 +    using add_imp_eq eq mult_zero_left by simp
1.272 +  thus "False" using add_mult_solve[of 0 d] nz cnd by simp
1.273  qed
1.274
1.275 -lemma add_r0_iff: " x = add x a \<longleftrightarrow> a = r0"
1.276 +lemma (in comm_semiring_1_cancel_norm) add_0_iff:
1.277 +  "x = x + a \<longleftrightarrow> a = 0"
1.278  proof-
1.279 -  have "a = r0 \<longleftrightarrow> add x a = add x r0" by (simp add: add_cancel)
1.280 -  thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0)
1.281 +  have "a = 0 \<longleftrightarrow> x + a = x + 0" using add_imp_eq[of x a 0] by auto
1.282 +  thus "x = x + a \<longleftrightarrow> a = 0" by (auto simp add: add_commute)
1.283  qed
1.284
1.285 -end
1.286 -
1.287 -sublocale comm_semiring_1_cancel_norm
1.288 -  < normalizing!: normalizing_semiring_cancel plus times power zero one
1.289 -proof
1.291 -
1.292  declare (in comm_semiring_1_cancel_norm)
1.293    normalizing_comm_semiring_1_axioms [normalizer del]
1.294
1.295  lemmas (in comm_semiring_1_cancel_norm)
1.296    normalizing_comm_semiring_1_cancel_norm_axioms =
1.297    comm_semiring_1_cancel_norm_axioms [normalizer
1.298 -    semiring ops: normalizing.semiring_ops
1.299 -    semiring rules: normalizing.semiring_rules
1.300 -    idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq]
1.301 +    semiring ops: semiring_ops
1.302 +    semiring rules: semiring_rules
1.303 +    idom rules: noteq_reduce add_scale_eq_noteq]
1.304
1.305  declaration (in comm_semiring_1_cancel_norm)
1.306    {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *}
1.307
1.308 -locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring +
1.309 -  assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y"
1.310 -
1.311 -sublocale idom
1.312 -  < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus
1.313 -proof
1.314 -qed simp
1.315 -
1.316  declare (in idom) normalizing_comm_ring_1_axioms [normalizer del]
1.317
1.318  lemmas (in idom) normalizing_idom_axioms = idom_axioms [normalizer
1.319 -  semiring ops: normalizing.semiring_ops
1.320 -  semiring rules: normalizing.semiring_rules
1.321 -  ring ops: normalizing.ring_ops
1.322 -  ring rules: normalizing.ring_rules
1.323 -  idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq
1.324 -  ideal rules: normalizing.subr0_iff normalizing.add_r0_iff]
1.325 +  semiring ops: semiring_ops
1.326 +  semiring rules: semiring_rules
1.327 +  ring ops: ring_ops
1.328 +  ring rules: ring_rules
1.329 +  idom rules: noteq_reduce add_scale_eq_noteq
1.330 +  ideal rules: right_minus_eq add_0_iff]
1.331
1.332  declaration (in idom)
1.333    {* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *}
1.334
1.335 -locale normalizing_field = normalizing_ring_cancel +
1.336 -  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.337 -    and inverse:: "'a \<Rightarrow> 'a"
1.338 -  assumes divide_inverse: "divide x y = mul x (inverse y)"
1.339 -     and inverse_divide: "inverse x = divide r1 x"
1.340 -begin
1.341 -
1.342 -lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" .
1.343 +lemma (in field) field_ops:
1.344 +  shows "TERM (x / y)" and "TERM (inverse x)" .
1.345
1.346 -lemmas field_rules = divide_inverse inverse_divide
1.347 -
1.348 -end
1.349 -
1.350 -sublocale field
1.351 -  < normalizing!: normalizing_field plus times power zero one minus uminus divide inverse
1.352 -proof
1.353 -qed (simp_all add: divide_inverse)
1.354 +lemmas (in field) field_rules = divide_inverse inverse_eq_divide
1.355
1.356  lemmas (in field) normalizing_field_axioms =
1.357    field_axioms [normalizer
1.358 -    semiring ops: normalizing.semiring_ops
1.359 -    semiring rules: normalizing.semiring_rules
1.360 -    ring ops: normalizing.ring_ops
1.361 -    ring rules: normalizing.ring_rules
1.362 -    field ops: normalizing.field_ops
1.363 -    field rules: normalizing.field_rules
1.364 -    idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq
1.365 -    ideal rules: normalizing.subr0_iff normalizing.add_r0_iff]
1.366 +    semiring ops: semiring_ops
1.367 +    semiring rules: semiring_rules
1.368 +    ring ops: ring_ops
1.369 +    ring rules: ring_rules
1.370 +    field ops: field_ops
1.371 +    field rules: field_rules
1.372 +    idom rules: noteq_reduce add_scale_eq_noteq
1.373 +    ideal rules: right_minus_eq add_0_iff]
1.374
1.375  declaration (in field)
1.376    {* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *}
1.377
1.378 +hide_fact (open) normalizing_comm_semiring_1_axioms
1.379 +  normalizing_comm_semiring_1_cancel_norm_axioms semiring_ops semiring_rules
1.380 +
1.381 +hide_fact (open) normalizing_comm_ring_1_axioms
1.382 +  normalizing_idom_axioms ring_ops ring_rules
1.383 +
1.384 +hide_fact (open)  normalizing_field_axioms field_ops field_rules
1.385 +
1.386 +hide_fact (open) add_scale_eq_noteq noteq_reduce
1.387 +
1.388  end
```