|
(* Title: HOL/Isar_Examples/Group_Notepad.thy
Author: Makarius
*)
section \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
theory Group_Notepad
imports Main
begin
notepad
begin
txt \<open>hypothetical group axiomatization\<close>
fix prod :: "'a \ 'a \ 'a" (infixl "\" 70)
and one :: "'a"
and inverse :: "'a \ 'a"
assume assoc: "(x \ y) \ z = x \ (y \ z)"
and left_one: "one \ x = x"
and left_inverse: "inverse x \ x = one"
for x y z
txt \<open>some consequences\<close>
have right_inverse: "x \ inverse x = one" for x
proof -
have "x \ inverse x = one \ (x \ inverse x)"
by (simp only: left_one)
also have "\ = one \ x \ inverse x"
by (simp only: assoc)
also have "\ = inverse (inverse x) \ inverse x \ x \ inverse x"
by (simp only: left_inverse)
also have "\ = inverse (inverse x) \ (inverse x \ x) \ inverse x"
by (simp only: assoc)
also have "\ = inverse (inverse x) \ one \ inverse x"
by (simp only: left_inverse)
also have "\ = inverse (inverse x) \ (one \ inverse x)"
by (simp only: assoc)
also have "\ = inverse (inverse x) \ inverse x"
by (simp only: left_one)
also have "\ = one"
by (simp only: left_inverse)
finally show ?thesis .
qed
have right_one: "x \ one = x" for x
proof -
have "x \ one = x \ (inverse x \ x)"
by (simp only: left_inverse)
also have "\ = x \ inverse x \ x"
by (simp only: assoc)
also have "\ = one \ x"
by (simp only: right_inverse)
also have "\ = x"
by (simp only: left_one)
finally show ?thesis .
qed
have one_equality: "one = e" if eq: "e \ x = x" for e x
proof -
have "one = x \ inverse x"
by (simp only: right_inverse)
also have "\ = (e \ x) \ inverse x"
by (simp only: eq)
also have "\ = e \ (x \ inverse x)"
by (simp only: assoc)
also have "\ = e \ one"
by (simp only: right_inverse)
also have "\ = e"
by (simp only: right_one)
finally show ?thesis .
qed
have inverse_equality: "inverse x = x'" if eq: "x' \ x = one" for x x'
proof -
have "inverse x = one \ inverse x"
by (simp only: left_one)
also have "\ = (x' \ x) \ inverse x"
by (simp only: eq)
also have "\ = x' \ (x \ inverse x)"
by (simp only: assoc)
also have "\ = x' \ one"
by (simp only: right_inverse)
also have "\ = x'"
by (simp only: right_one)
finally show ?thesis .
qed
end
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
