summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 04 Jun 1999 16:16:31 +0200 | |

changeset 6763 | df12aef00932 |

parent 6762 | a9a515a43ae0 |

child 6764 | cbe506c8311e |

Some bits of group theory. Demonstrate calculational proofs.

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_examples/Group.thy Fri Jun 04 16:16:31 1999 +0200 @@ -0,0 +1,115 @@ +(* Title: HOL/Isar_examples/Group.thy + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +Some bits of group theory. Demonstrate calculational proofs. +*) + +theory Group = Main:; + + +subsection {* axiomatic type class of groups over signature (*, inv, one) *}; + +consts + inv :: "'a => 'a" + one :: "'a"; + +axclass + group < times + assoc: "(x * y) * z = x * (y * z)" + left_unit: "one * x = x" + left_inverse: "inverse x * x = one"; + + +subsection {* some basic theorems of group theory *}; + +text {* We simulate *}; + +theorem right_inverse: "x * inverse x = (one::'a::group)"; +proof same; + have "x * inverse x = one * (x * inverse x)"; + by (simp add: left_unit); + + note calculation = facts; + let "_ = ..." = ??facts; + + have "... = (one * x) * inverse x"; + by (simp add: assoc); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + + have "... = inverse (inverse x) * inverse x * x * inverse x"; + by (simp add: left_inverse); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + + have "... = inverse (inverse x) * (inverse x * x) * inverse x"; + by (simp add: assoc); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + + have "... = inverse (inverse x) * one * inverse x"; + by (simp add: left_inverse); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + + have "... = inverse (inverse x) * (one * inverse x)"; + by (simp add: assoc); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + + have "... = inverse (inverse x) * inverse x"; + by (simp add: left_unit); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + + have "... = one"; + by (simp add: left_inverse); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + from calculation; + + show ??thesis; .; +qed; + + +theorem right_inverse: "x * one = (x::'a::group)"; +proof same; + + have "x * one = x * (inverse x * x)"; + by (simp add: left_inverse); + + note calculation = facts; + let "_ = ..." = ??facts; + + have "... = x * inverse x * x"; + by (simp add: assoc); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + + have "... = one * x"; + by (simp add: right_inverse); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + + have "... = x"; + by (simp add: left_unit); + + note calculation = trans[APP calculation facts]; + let "_ = ..." = ??facts; + from calculation; + + show ??thesis; .; +qed; + + +end;