equal
deleted
inserted
replaced
26 end |
26 end |
27 |
27 |
28 class mult_zero = times + zero + |
28 class mult_zero = times + zero + |
29 assumes mult_zero_left [simp]: "0 * a = 0" |
29 assumes mult_zero_left [simp]: "0 * a = 0" |
30 assumes mult_zero_right [simp]: "a * 0 = 0" |
30 assumes mult_zero_right [simp]: "a * 0 = 0" |
31 |
|
32 class semiring_0 = semiring + comm_monoid_add + mult_zero |
|
33 begin |
31 begin |
34 |
32 |
35 lemma mult_not_zero: |
33 lemma mult_not_zero: |
36 "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0" |
34 "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0" |
37 by auto |
35 by auto |
38 |
36 |
39 end |
37 end |
|
38 |
|
39 class semiring_0 = semiring + comm_monoid_add + mult_zero |
40 |
40 |
41 class semiring_0_cancel = semiring + cancel_comm_monoid_add |
41 class semiring_0_cancel = semiring + cancel_comm_monoid_add |
42 begin |
42 begin |
43 |
43 |
44 subclass semiring_0 |
44 subclass semiring_0 |