src/HOL/Semiring_Normalization.thy
 changeset 47108 2a1953f0d20d parent 37946 be3c0df7bb90 child 48891 c0eafbd55de3
equal inserted replaced
47107:35807a5d8dc2 47108:2a1953f0d20d
`   114   "x ^ 1 = x"`
`   114   "x ^ 1 = x"`
`   115   "x * (y + z) = (x * y) + (x * z)"`
`   115   "x * (y + z) = (x * y) + (x * z)"`
`   116   "x ^ (Suc q) = x * (x ^ q)"`
`   116   "x ^ (Suc q) = x * (x ^ q)"`
`   117   "x ^ (2*n) = (x ^ n) * (x ^ n)"`
`   117   "x ^ (2*n) = (x ^ n) * (x ^ n)"`
`   118   "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))"`
`   118   "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))"`
`   119   by (simp_all add: algebra_simps power_add power2_eq_square power_mult_distrib power_mult)`
`   119   by (simp_all add: algebra_simps power_add power2_eq_square`
`       `
`   120     power_mult_distrib power_mult del: one_add_one)`
`   120 `
`   121 `
`   121 lemmas normalizing_comm_semiring_1_axioms =`
`   122 lemmas normalizing_comm_semiring_1_axioms =`
`   122   comm_semiring_1_axioms [normalizer`
`   123   comm_semiring_1_axioms [normalizer`
`   123     semiring ops: normalizing_semiring_ops`
`   124     semiring ops: normalizing_semiring_ops`
`   124     semiring rules: normalizing_semiring_rules]`
`   125     semiring rules: normalizing_semiring_rules]`
`   216 hide_fact (open) normalizing_comm_ring_1_axioms`
`   217 hide_fact (open) normalizing_comm_ring_1_axioms`
`   217   normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules`
`   218   normalizing_idom_axioms normalizing_ring_ops normalizing_ring_rules`
`   218 `
`   219 `
`   219 hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules`
`   220 hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules`
`   220 `
`   221 `
`   221 end`
`   222 code_modulename SML`
`       `
`   223   Semiring_Normalization Arith`
`       `
`   224 `
`       `
`   225 code_modulename OCaml`
`       `
`   226   Semiring_Normalization Arith`
`       `
`   227 `
`       `
`   228 code_modulename Haskell`
`       `
`   229   Semiring_Normalization Arith`
`       `
`   230 `
`       `
`   231 end`