An key part of mathematics is proofs, on this site I would like to include proofs in a consistant way across all the topics, I am therefore using a program called Isabelle which is a proof assistant. More about this program on this page.
So far, we don't have any of the imporant proofs on this page, just the initial constructions.
This is taken from Isabelle code (from this site) but I have not put the complete code here, just an outline.
Semigroup
We start with a semigroup, as an associative binary operation. There is also an abelian group which add a commutitive axiom. |
locale semigroup =
fixes f :: "'a => 'a => 'a" (infixl "*" 70)
assumes assoc [ac_simps]: "a * b * c = a * (b * c)"
locale abel_semigroup = semigroup +
assumes commute [ac_simps]: "a * b = b * a"
begin
lemma left_commute [ac_simps]:
"b * (a * c) = a * (b * c)"
proof -
have "(b * a) * c = (a * b) * c"
by (simp only: commute)
then show ?thesis
by (simp only: assoc)
qed
end |
Monoids
| We also add a monoid and commutative monoid which are the semigroups above with an identity element '1'. | locale monoid = semigroup +
fixes z :: 'a ("1")
assumes left_neutral [simp]: "1 * a = a"
assumes right_neutral [simp]: "a * 1 = a"
locale comm_monoid = abel_semigroup +
fixes z :: 'a ("1")
assumes comm_neutral: "a * 1 = a"
sublocale comm_monoid < monoid proof
qed (simp_all add: commute comm_neutral)
|
Groups
Then, when groups are introduced in the Isabelle library code for groups, things seem to get a bit messy, there seems to be a switch over from '*' as the group operation to '+' even for non-abelian group.
| Since we are using '+' for the binary operation then the inverse operation is a unary minus (-). We can also add a binary minus operation (although not part of the axioms) as shown here. | class group_add = minus + uminus + monoid_add + assumes left_minus [simp]: "- a + a = 0" assumes diff_minus: "a - b = a + (- b)" begin lemma minus_unique: assumes "a + b = 0" shows "- a = b" proof - have "- a = - a + (a + b)" using assms by simp also have "… = b" by (simp add: add_assoc [symmetric]) finally show ?thesis . qed lemma minus_zero [simp]: "- 0 = 0" proof - have "0 + 0 = 0" by (rule add_0_right) thus "- 0 = 0" by (rule minus_unique) qed lemma minus_minus [simp]: "- (- a) = a" proof - have "- a + a = 0" by (rule left_minus) thus "- (- a) = a" by (rule minus_unique) qed lemma right_minus [simp]: "a + - a = 0" proof - have "a + - a = - (- a) + - a" by simp also have "… = 0" by (rule left_minus) finally show ?thesis . qed |
