|
13562
|
1 |
theory Calc = Main:
|
|
|
2 |
|
|
|
3 |
axclass
|
|
|
4 |
group < zero, plus, minus
|
|
|
5 |
assoc: "(x + y) + z = x + (y + z)"
|
|
|
6 |
left_0: "0 + x = x"
|
|
|
7 |
left_minus: "-x + x = 0"
|
|
|
8 |
|
|
|
9 |
theorem right_minus: "x + -x = (0::'a::group)"
|
|
|
10 |
proof -
|
|
|
11 |
have "x + -x = (-(-x) + -x) + (x + -x)"
|
|
|
12 |
by (simp only: left_0 left_minus)
|
|
|
13 |
also have "... = -(-x) + ((-x + x) + -x)"
|
|
|
14 |
by (simp only: group.assoc)
|
|
|
15 |
also have "... = 0"
|
|
|
16 |
by (simp only: left_0 left_minus)
|
|
|
17 |
finally show ?thesis .
|
|
|
18 |
qed
|
|
|
19 |
|
|
|
20 |
|
|
|
21 |
lemma assumes R: "(a,b) \<in> R" "(b,c) \<in> R" "(c,d) \<in> R"
|
|
|
22 |
shows "(a,d) \<in> R\<^sup>*"
|
|
|
23 |
proof -
|
|
|
24 |
have "(a,b) \<in> R\<^sup>*" ..
|
|
|
25 |
also have "(b,c) \<in> R\<^sup>*" ..
|
|
|
26 |
also have "(c,d) \<in> R\<^sup>*" ..
|
|
|
27 |
finally show ?thesis .
|
|
|
28 |
qed
|
|
|
29 |
|
|
|
30 |
end |