summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Isar_Examples/Group_Context.thy

author | wenzelm |

Sat, 07 Apr 2012 16:41:59 +0200 | |

changeset 47389 | e8552cba702d |

parent 47311 | 1addbe2a7458 |

child 47872 | 1f6f519cdb32 |

permissions | -rw-r--r-- |

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

(* Title: HOL/Isar_Examples/Group_Context.thy Author: Makarius *) header {* Some algebraic identities derived from group axioms -- theory context version *} theory Group_Context imports Main begin text {* hypothetical group axiomatization *} context fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70) and one :: "'a" and inverse :: "'a => 'a" assumes assoc: "(x ** y) ** z = x ** (y ** z)" and left_one: "one ** x = x" and left_inverse: "inverse x ** x = one" begin text {* some consequences *} lemma right_inverse: "x ** inverse x = one" proof - have "x ** inverse x = one ** (x ** inverse x)" by (simp only: left_one) also have "\<dots> = one ** x ** inverse x" by (simp only: assoc) also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x" by (simp only: left_inverse) also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x" by (simp only: assoc) also have "\<dots> = inverse (inverse x) ** one ** inverse x" by (simp only: left_inverse) also have "\<dots> = inverse (inverse x) ** (one ** inverse x)" by (simp only: assoc) also have "\<dots> = inverse (inverse x) ** inverse x" by (simp only: left_one) also have "\<dots> = one" by (simp only: left_inverse) finally show "x ** inverse x = one" . qed lemma right_one: "x ** one = x" proof - have "x ** one = x ** (inverse x ** x)" by (simp only: left_inverse) also have "\<dots> = x ** inverse x ** x" by (simp only: assoc) also have "\<dots> = one ** x" by (simp only: right_inverse) also have "\<dots> = x" by (simp only: left_one) finally show "x ** one = x" . qed lemma one_equality: "e ** x = x \<Longrightarrow> one = e" proof - fix e x assume eq: "e ** x = x" have "one = x ** inverse x" by (simp only: right_inverse) also have "\<dots> = (e ** x) ** inverse x" by (simp only: eq) also have "\<dots> = e ** (x ** inverse x)" by (simp only: assoc) also have "\<dots> = e ** one" by (simp only: right_inverse) also have "\<dots> = e" by (simp only: right_one) finally show "one = e" . qed lemma inverse_equality: "x' ** x = one \<Longrightarrow> inverse x = x'" proof - fix x x' assume eq: "x' ** x = one" have "inverse x = one ** inverse x" by (simp only: left_one) also have "\<dots> = (x' ** x) ** inverse x" by (simp only: eq) also have "\<dots> = x' ** (x ** inverse x)" by (simp only: assoc) also have "\<dots> = x' ** one" by (simp only: right_inverse) also have "\<dots> = x'" by (simp only: right_one) finally show "inverse x = x'" . qed end end