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

author | wenzelm |

Mon, 05 Feb 2001 20:34:05 +0100 | |

changeset 11072 | 8f47967ecc80 |

parent 11071 | 4e542a09b582 |

child 11073 | e45b136716f5 |

tuned

--- a/src/HOL/AxClasses/Group.thy Mon Feb 05 20:33:50 2001 +0100 +++ b/src/HOL/AxClasses/Group.thy Mon Feb 05 20:34:05 2001 +0100 @@ -10,7 +10,7 @@ consts times :: "'a => 'a => 'a" (infixl "[*]" 70) - inverse :: "'a => 'a" + invers :: "'a => 'a" one :: 'a @@ -24,7 +24,7 @@ axclass group < semigroup left_unit: "one [*] x = x" - left_inverse: "inverse x [*] x = one" + left_inverse: "invers x [*] x = one" axclass agroup < group commute: "x [*] y = y [*] x" @@ -32,21 +32,21 @@ subsection {* Abstract reasoning *} -theorem group_right_inverse: "x [*] inverse x = (one::'a::group)" +theorem group_right_inverse: "x [*] invers x = (one::'a::group)" proof - - have "x [*] inverse x = one [*] (x [*] inverse x)" + have "x [*] invers x = one [*] (x [*] invers x)" by (simp only: group.left_unit) - also have "... = one [*] x [*] inverse x" + also have "... = one [*] x [*] invers x" by (simp only: semigroup.assoc) - also have "... = inverse (inverse x) [*] inverse x [*] x [*] inverse x" + also have "... = invers (invers x) [*] invers x [*] x [*] invers x" by (simp only: group.left_inverse) - also have "... = inverse (inverse x) [*] (inverse x [*] x) [*] inverse x" + also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x" by (simp only: semigroup.assoc) - also have "... = inverse (inverse x) [*] one [*] inverse x" + also have "... = invers (invers x) [*] one [*] invers x" by (simp only: group.left_inverse) - also have "... = inverse (inverse x) [*] (one [*] inverse x)" + also have "... = invers (invers x) [*] (one [*] invers x)" by (simp only: semigroup.assoc) - also have "... = inverse (inverse x) [*] inverse x" + also have "... = invers (invers x) [*] invers x" by (simp only: group.left_unit) also have "... = one" by (simp only: group.left_inverse) @@ -55,9 +55,9 @@ theorem group_right_unit: "x [*] one = (x::'a::group)" proof - - have "x [*] one = x [*] (inverse x [*] x)" + have "x [*] one = x [*] (invers x [*] x)" by (simp only: group.left_inverse) - also have "... = x [*] inverse x [*] x" + also have "... = x [*] invers x [*] x" by (simp only: semigroup.assoc) also have "... = one [*] x" by (simp only: group_right_inverse) @@ -92,7 +92,7 @@ defs (overloaded) times_bool_def: "x [*] y == x ~= (y::bool)" - inverse_bool_def: "inverse x == x::bool" + inverse_bool_def: "invers x == x::bool" unit_bool_def: "one == False" instance bool :: agroup

--- a/src/HOL/Unix/Unix.thy Mon Feb 05 20:33:50 2001 +0100 +++ b/src/HOL/Unix/Unix.thy Mon Feb 05 20:34:05 2001 +0100 @@ -259,7 +259,7 @@ proof - assume "path' \<parallel> path" then obtain y z xs ys zs where - "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs" + "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs" by (blast dest: parallel_decomp) hence "lookup (update path' opt root) path = lookup root path" by (blast intro: lookup_update_other)

--- a/src/HOL/Unix/document/root.bib Mon Feb 05 20:33:50 2001 +0100 +++ b/src/HOL/Unix/document/root.bib Mon Feb 05 20:34:05 2001 +0100 @@ -1,6 +1,7 @@ @Unpublished{Bauer-et-al:2001:HOL-Library, - author = {Gertrud Bauer and Tobias Nipkow and Lawrence C Paulson and Markus Wenzel}, + author = {Gertrud Bauer and Tobias Nipkow and Lawrence C Paulson and + Thomas M Rasmussen and Markus Wenzel}, title = {The Supplemental {Isabelle/HOL} Library}, note = {\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, year = 2001