equal
deleted
inserted
replaced
62 |
62 |
63 |
63 |
64 subsubsection {* Declaring the abstract theory *} |
64 subsubsection {* Declaring the abstract theory *} |
65 |
65 |
66 lemma semiring_ops: |
66 lemma semiring_ops: |
67 fixes meta_term :: "'a => prop" ("TERM _") |
|
68 shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)" |
67 shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)" |
69 and "TERM r0" and "TERM r1" |
68 and "TERM r0" and "TERM r1" . |
70 by rule+ |
|
71 |
69 |
72 lemma semiring_rules: |
70 lemma semiring_rules: |
73 "add (mul a m) (mul b m) = mul (add a b) m" |
71 "add (mul a m) (mul b m) = mul (add a b) m" |
74 "add (mul a m) m = mul (add a r1) m" |
72 "add (mul a m) m = mul (add a r1) m" |
75 "add m (mul a m) = mul (add a r1) m" |
73 "add m (mul a m) = mul (add a r1) m" |
224 and neg :: "'a \<Rightarrow> 'a" |
222 and neg :: "'a \<Rightarrow> 'a" |
225 assumes neg_mul: "neg x = mul (neg r1) x" |
223 assumes neg_mul: "neg x = mul (neg r1) x" |
226 and sub_add: "sub x y = add x (neg y)" |
224 and sub_add: "sub x y = add x (neg y)" |
227 begin |
225 begin |
228 |
226 |
229 lemma ring_ops: |
227 lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" . |
230 fixes meta_term :: "'a => prop" ("TERM _") |
|
231 shows "TERM (sub x y)" and "TERM (neg x)" . |
|
232 |
228 |
233 lemmas ring_rules = neg_mul sub_add |
229 lemmas ring_rules = neg_mul sub_add |
234 |
230 |
235 lemmas gb_ring_axioms' = |
231 lemmas gb_ring_axioms' = |
236 gb_ring_axioms [normalizer |
232 gb_ring_axioms [normalizer |