src/HOL/Semiring_Normalization.thy
 changeset 61153 3d5e01b427cb parent 60758 d8d85a8172b5 child 66836 4eb431c3f974
```     1.1 --- a/src/HOL/Semiring_Normalization.thy	Thu Sep 10 16:42:01 2015 +0200
1.2 +++ b/src/HOL/Semiring_Normalization.thy	Thu Sep 10 16:44:17 2015 +0200
1.3 @@ -72,101 +72,120 @@
1.4  context comm_semiring_1
1.5  begin
1.6
1.7 -declaration \<open>
1.8 -let
1.9 -  val rules = @{lemma
1.10 -    "(a * m) + (b * m) = (a + b) * m"
1.11 -    "(a * m) + m = (a + 1) * m"
1.12 -    "m + (a * m) = (a + 1) * m"
1.13 -    "m + m = (1 + 1) * m"
1.14 -    "0 + a = a"
1.15 -    "a + 0 = a"
1.16 -    "a * b = b * a"
1.17 -    "(a + b) * c = (a * c) + (b * c)"
1.18 -    "0 * a = 0"
1.19 -    "a * 0 = 0"
1.20 -    "1 * a = a"
1.21 -    "a * 1 = a"
1.22 -    "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)"
1.23 -    "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))"
1.24 -    "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)"
1.25 -    "(lx * ly) * rx = (lx * rx) * ly"
1.26 -    "(lx * ly) * rx = lx * (ly * rx)"
1.27 -    "lx * (rx * ry) = (lx * rx) * ry"
1.28 -    "lx * (rx * ry) = rx * (lx * ry)"
1.29 -    "(a + b) + (c + d) = (a + c) + (b + d)"
1.30 -    "(a + b) + c = a + (b + c)"
1.31 -    "a + (c + d) = c + (a + d)"
1.32 -    "(a + b) + c = (a + c) + b"
1.33 -    "a + c = c + a"
1.34 -    "a + (c + d) = (a + c) + d"
1.35 -    "(x ^ p) * (x ^ q) = x ^ (p + q)"
1.36 -    "x * (x ^ q) = x ^ (Suc q)"
1.37 -    "(x ^ q) * x = x ^ (Suc q)"
1.38 -    "x * x = x\<^sup>2"
1.39 -    "(x * y) ^ q = (x ^ q) * (y ^ q)"
1.40 -    "(x ^ p) ^ q = x ^ (p * q)"
1.41 -    "x ^ 0 = 1"
1.42 -    "x ^ 1 = x"
1.43 -    "x * (y + z) = (x * y) + (x * z)"
1.44 -    "x ^ (Suc q) = x * (x ^ q)"
1.45 -    "x ^ (2*n) = (x ^ n) * (x ^ n)"
1.47 -      power_mult_distrib power_mult del: one_add_one)}
1.48 -in
1.49 +lemma semiring_normalization_rules:
1.50 +  "(a * m) + (b * m) = (a + b) * m"
1.51 +  "(a * m) + m = (a + 1) * m"
1.52 +  "m + (a * m) = (a + 1) * m"
1.53 +  "m + m = (1 + 1) * m"
1.54 +  "0 + a = a"
1.55 +  "a + 0 = a"
1.56 +  "a * b = b * a"
1.57 +  "(a + b) * c = (a * c) + (b * c)"
1.58 +  "0 * a = 0"
1.59 +  "a * 0 = 0"
1.60 +  "1 * a = a"
1.61 +  "a * 1 = a"
1.62 +  "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)"
1.63 +  "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))"
1.64 +  "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)"
1.65 +  "(lx * ly) * rx = (lx * rx) * ly"
1.66 +  "(lx * ly) * rx = lx * (ly * rx)"
1.67 +  "lx * (rx * ry) = (lx * rx) * ry"
1.68 +  "lx * (rx * ry) = rx * (lx * ry)"
1.69 +  "(a + b) + (c + d) = (a + c) + (b + d)"
1.70 +  "(a + b) + c = a + (b + c)"
1.71 +  "a + (c + d) = c + (a + d)"
1.72 +  "(a + b) + c = (a + c) + b"
1.73 +  "a + c = c + a"
1.74 +  "a + (c + d) = (a + c) + d"
1.75 +  "(x ^ p) * (x ^ q) = x ^ (p + q)"
1.76 +  "x * (x ^ q) = x ^ (Suc q)"
1.77 +  "(x ^ q) * x = x ^ (Suc q)"
1.78 +  "x * x = x\<^sup>2"
1.79 +  "(x * y) ^ q = (x ^ q) * (y ^ q)"
1.80 +  "(x ^ p) ^ q = x ^ (p * q)"
1.81 +  "x ^ 0 = 1"
1.82 +  "x ^ 1 = x"
1.83 +  "x * (y + z) = (x * y) + (x * z)"
1.84 +  "x ^ (Suc q) = x * (x ^ q)"
1.85 +  "x ^ (2*n) = (x ^ n) * (x ^ n)"
1.87 +    power_mult_distrib power_mult del: one_add_one)
1.88 +
1.89 +local_setup \<open>
1.90    Semiring_Normalizer.declare @{thm comm_semiring_1_axioms}
1.91 -    {semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}],
1.92 -      rules), ring = ([], []), field = ([], []), idom = [], ideal = []}
1.93 -end\<close>
1.94 +    {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}],
1.95 +      @{thms semiring_normalization_rules}),
1.96 +     ring = ([], []),
1.97 +     field = ([], []),
1.98 +     idom = [],
1.99 +     ideal = []}
1.100 +\<close>
1.101
1.102  end
1.103
1.104  context comm_ring_1
1.105  begin
1.106
1.107 -declaration \<open>
1.108 -let
1.109 -  val rules = @{lemma
1.110 -    "- x = (- 1) * x"
1.111 -    "x - y = x + (- y)"
1.112 -    by simp_all}
1.113 -in
1.114 +lemma ring_normalization_rules:
1.115 +  "- x = (- 1) * x"
1.116 +  "x - y = x + (- y)"
1.117 +  by simp_all
1.118 +
1.119 +local_setup \<open>
1.120    Semiring_Normalizer.declare @{thm comm_ring_1_axioms}
1.121 -    {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms},
1.122 -      ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], rules), field = ([], []), idom = [], ideal = []}
1.123 -end\<close>
1.124 +    {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}],
1.125 +      @{thms semiring_normalization_rules}),
1.126 +      ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}),
1.127 +      field = ([], []),
1.128 +      idom = [],
1.129 +      ideal = []}
1.130 +\<close>
1.131
1.132  end
1.133
1.134  context comm_semiring_1_cancel_crossproduct
1.135  begin
1.136
1.137 -declaration \<open>Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms}
1.138 -  {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms},
1.139 -    ring = ([], []), field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, ideal = []}\<close>
1.140 +local_setup \<open>
1.141 +  Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms}
1.142 +    {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}],
1.143 +      @{thms semiring_normalization_rules}),
1.144 +     ring = ([], []),
1.145 +     field = ([], []),
1.146 +     idom = @{thms crossproduct_noteq add_scale_eq_noteq},
1.147 +     ideal = []}
1.148 +\<close>
1.149
1.150  end
1.151
1.152  context idom
1.153  begin
1.154
1.155 -declaration \<open>Semiring_Normalizer.declare @{thm idom_axioms}
1.156 -  {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_ring_1_axioms},
1.157 -    ring = Semiring_Normalizer.the_ring @{context} @{thm comm_ring_1_axioms},
1.158 -    field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq},
1.159 -    ideal = @{thms right_minus_eq add_0_iff}}\<close>
1.160 +local_setup \<open>
1.161 +  Semiring_Normalizer.declare @{thm idom_axioms}
1.162 +   {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}],
1.163 +      @{thms semiring_normalization_rules}),
1.164 +    ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}),
1.165 +    field = ([], []),
1.166 +    idom = @{thms crossproduct_noteq add_scale_eq_noteq},
1.167 +    ideal = @{thms right_minus_eq add_0_iff}}
1.168 +\<close>
1.169
1.170  end
1.171
1.172  context field
1.173  begin
1.174
1.175 -declaration \<open>Semiring_Normalizer.declare @{thm field_axioms}
1.176 -  {semiring = Semiring_Normalizer.the_semiring @{context} @{thm idom_axioms},
1.177 -    ring = Semiring_Normalizer.the_ring @{context} @{thm idom_axioms},
1.178 -    field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms divide_inverse inverse_eq_divide}),
1.179 -    idom = Semiring_Normalizer.the_idom @{context} @{thm idom_axioms},
1.180 -    ideal = Semiring_Normalizer.the_ideal @{context} @{thm idom_axioms}}\<close>
1.181 +local_setup \<open>
1.182 +  Semiring_Normalizer.declare @{thm field_axioms}
1.183 +   {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}],
1.184 +      @{thms semiring_normalization_rules}),
1.185 +    ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}),
1.186 +    field = ([@{term "x / y"}, @{term "inverse x"}], @{thms divide_inverse inverse_eq_divide}),
1.187 +    idom = @{thms crossproduct_noteq add_scale_eq_noteq},
1.188 +    ideal = @{thms right_minus_eq add_0_iff}}
1.189 +\<close>
1.190
1.191  end
1.192
```