Add rules directly to the corresponding class locales instead.
authorhoelzl
Tue May 11 19:21:39 2010 +0200 (2010-05-11)
changeset 36845d778c64fc35d
parent 36844 5f9385ecc1a7
child 36846 0f67561ed5a6
Add rules directly to the corresponding class locales instead.
src/HOL/Semiring_Normalization.thy
     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.9 -  assumes add_a:"(add x (add y z) = add (add x y) z)"
    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.75 -  "add (add a b) (add c d) = add (add a c) (add b d)"
    1.76 -  "add (add a b) c = add a (add b c)"
    1.77 -  "add a (add c d) = add c (add a d)"
    1.78 -  "add (add a b) c = add (add a c) b"
    1.79 -  "add a c = add c a"
    1.80 -  "add a (add c d) = add (add a c) d"
    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.121 -next show "add (add a b) (add c d) = add (add a c) (add b d)"
   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.126 -next show "add (add a b) c = add (add a c) b" using add_a add_c by simp
   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.290 -qed (simp_all add: add_mult_solve)
   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