# HG changeset patch # User wenzelm # Date 928607325 -7200 # Node ID 687ddcad858139ee00507ead0bc6071f11a2e509 # Parent 9cf9c17d9e35aa3a2dd71cc550612cf20dd1be1e proper calculation; diff -r 9cf9c17d9e35 -r 687ddcad8581 src/HOL/Isar_examples/Group.thy --- a/src/HOL/Isar_examples/Group.thy Sat Jun 05 20:27:53 1999 +0200 +++ b/src/HOL/Isar_examples/Group.thy Sat Jun 05 20:28:45 1999 +0200 @@ -1,114 +1,122 @@ (* Title: HOL/Isar_examples/Group.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen - -Some bits of group theory. Demonstrate calculational proofs. *) theory Group = Main:; +title {* Basic group theory -- demonstrating calculational proofs *}; -subsection {* axiomatic type class of groups over signature (*, inv, one) *}; +section {* Groups *}; + +text {* + We define an axiomatic type class of general groupes over signature + (op *, one, inv). +*}; consts - inv :: "'a => 'a" - one :: "'a"; + one :: "'a" + inv :: "'a => 'a"; axclass group < times assoc: "(x * y) * z = x * (y * z)" left_unit: "one * x = x" - left_inverse: "inverse x * x = one"; - + left_inverse: "inv x * x = one"; -subsection {* some basic theorems of group theory *}; - -text {* We simulate *}; +text {* + The group axioms only state the properties of left unit and inverse, the + right versions are derivable as follows. The calculational proof style below + closely follows a typical presentation given in any basic course on + algebra. +*}; -theorem right_inverse: "x * inverse x = (one::'a::group)"; +theorem right_inverse: "x * inv x = (one::'a::group)"; proof same; - have "x * inverse x = one * (x * inverse x)"; + have "x * inv x = one * (x * inv x)"; by (simp add: left_unit); - - note calculation = facts; - let "_ = ..." = ??facts; - - have "... = (one * x) * inverse x"; + also; have "... = (one * x) * inv x"; + by (simp add: assoc); + also; have "... = inv (inv x) * inv x * x * inv x"; + by (simp add: left_inverse); + also; have "... = inv (inv x) * (inv x * x) * inv x"; + by (simp add: assoc); + also; have "... = inv (inv x) * one * inv x"; + by (simp add: left_inverse); + also; have "... = inv (inv x) * (one * inv x)"; by (simp add: assoc); + also; have "... = inv (inv x) * inv x"; + by (simp add: left_unit); + also; have "... = one"; + by (simp add: left_inverse); + finally; show ??thesis; .; +qed; - note calculation = trans[APP calculation facts]; - let "_ = ..." = ??facts; - - have "... = inverse (inverse x) * inverse x * x * inverse x"; - by (simp add: left_inverse); +text {* + With right_inverse already at our disposel, right_unit is now + obtained much simpler. +*}; - note calculation = trans[APP calculation facts]; - let "_ = ..." = ??facts; - - have "... = inverse (inverse x) * (inverse x * x) * inverse x"; +theorem right_unit: "x * one = (x::'a::group)"; +proof same; + have "x * one = x * (inv x * x)"; + by (simp add: left_inverse); + also; have "... = x * inv x * x"; by (simp add: assoc); + also; have "... = one * x"; + by (simp add: right_inverse); + also; have "... = x"; + by (simp add: left_unit); + finally; show ??thesis; .; +qed; - note calculation = trans[APP calculation facts]; - let "_ = ..." = ??facts; +text {* + There are only two language elements 'also' (for initial or + intermediate calculational steps), and 'finally' (for picking up the + result of a calculation). These constructs are not hardwired into + Isabelle/Isar, but defined on top of the basic Isar/VM interpreter. + + Without referring to 'also' or 'finally', calculations may be + simulated as follows. This can be also understood as an expansion of these + two derived language elements. - have "... = inverse (inverse x) * one * inverse x"; + Also note that "..." is just a special term binding that happens to + be bound automatically to the argument of the last fact established by + assume or any local goal. Unlike ??thesis, "..." is bound after the + proof is finished. +*}; + +theorem right_unit': "x * one = (x::'a::group)"; +proof same; + + have "x * one = x * (inv x * x)"; by (simp add: left_inverse); - note calculation = trans[APP calculation facts]; - let "_ = ..." = ??facts; + note calculation = facts + -- {* first calculational step: init register *}; - have "... = inverse (inverse x) * (one * inverse x)"; + have "... = x * inv x * 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; + note calculation = trans[APP calculation facts] + -- {* general calculational step: compose with transitivity rule *}; have "... = one * x"; by (simp add: right_inverse); - note calculation = trans[APP calculation facts]; - let "_ = ..." = ??facts; + note calculation = trans[APP calculation facts] + -- {* general calculational step: compose with transitivity rule *}; have "... = x"; by (simp add: left_unit); - note calculation = trans[APP calculation facts]; - let "_ = ..." = ??facts; - from calculation; + note calculation = trans[APP calculation facts] + -- {* final calculational step: compose with transitivity rule ... *}; + from calculation + -- {* ... and pick up final result *}; show ??thesis; .; + qed;