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.46 -    by (simp_all add: algebra_simps power_add power2_eq_square
    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.86 +  by (simp_all add: algebra_simps power_add power2_eq_square
    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