(* Title: HOL/ex/Locales.thy ID: $Id$ Author: Markus Wenzel, LMU Muenchen License: GPL (GNU GENERAL PUBLIC LICENSE) *) header {* Locales and simple mathematical structures *} theory Locales = Main: text_raw {* \newcommand{\isasyminv}{\isasyminverse} \newcommand{\isasymone}{\isamath{1}} *} subsection {* Groups *} text {* Locales version of the inevitable group example. *} locale group = fixes prod :: "'a \ 'a \ 'a" (infixl "\" 70) and inv :: "'a \ 'a" ("(_\)" [1000] 999) and one :: 'a ("\") assumes assoc: "(x \ y) \ z = x \ (y \ z)" and left_inv: "x\ \ x = \" and left_one: "\ \ x = x" locale abelian_group = group + assumes commute: "x \ y = y \ x" theorem (in group) right_inv: "x \ x\ = \" proof - have "x \ x\ = \ \ (x \ x\)" by (simp only: left_one) also have "\ = \ \ x \ x\" by (simp only: assoc) also have "\ = (x\)\ \ x\ \ x \ x\" by (simp only: left_inv) also have "\ = (x\)\ \ (x\ \ x) \ x\" by (simp only: assoc) also have "\ = (x\)\ \ \ \ x\" by (simp only: left_inv) also have "\ = (x\)\ \ (\ \ x\)" by (simp only: assoc) also have "\ = (x\)\ \ x\" by (simp only: left_one) also have "\ = \" by (simp only: left_inv) finally show ?thesis . qed theorem (in group) right_one: "x \ \ = x" proof - have "x \ \ = x \ (x\ \ x)" by (simp only: left_inv) also have "\ = x \ x\ \ x" by (simp only: assoc) also have "\ = \ \ x" by (simp only: right_inv) also have "\ = x" by (simp only: left_one) finally show ?thesis . qed theorem (in group) (assumes eq: "e \ x = x") one_equality: "\ = e" proof - have "\ = x \ x\" by (simp only: right_inv) also have "\ = (e \ x) \ x\" by (simp only: eq) also have "\ = e \ (x \ x\)" by (simp only: assoc) also have "\ = e \ \" by (simp only: right_inv) also have "\ = e" by (simp only: right_one) finally show ?thesis . qed theorem (in group) (assumes eq: "x' \ x = \") inv_equality: "x\ = x'" proof - have "x\ = \ \ x\" by (simp only: left_one) also have "\ = (x' \ x) \ x\" by (simp only: eq) also have "\ = x' \ (x \ x\)" by (simp only: assoc) also have "\ = x' \ \" by (simp only: right_inv) also have "\ = x'" by (simp only: right_one) finally show ?thesis . qed theorem (in group) inv_prod: "(x \ y)\ = y\ \ x\" proof (rule inv_equality) show "(y\ \ x\) \ (x \ y) = \" proof - have "(y\ \ x\) \ (x \ y) = (y\ \ (x\ \ x)) \ y" by (simp only: assoc) also have "\ = (y\ \ \) \ y" by (simp only: left_inv) also have "\ = y\ \ y" by (simp only: right_one) also have "\ = \" by (simp only: left_inv) finally show ?thesis . qed qed theorem (in abelian_group) inv_prod': "(x \ y)\ = x\ \ y\" proof - have "(x \ y)\ = y\ \ x\" by (rule inv_prod) also have "\ = x\ \ y\" by (rule commute) finally show ?thesis . qed theorem (in group) inv_inv: "(x\)\ = x" proof (rule inv_equality) show "x \ x\ = \" by (simp only: right_inv) qed theorem (in group) (assumes eq: "x\ = y\") inv_inject: "x = y" proof - have "x = x \ \" by (simp only: right_one) also have "\ = x \ (y\ \ y)" by (simp only: left_inv) also have "\ = x \ (x\ \ y)" by (simp only: eq) also have "\ = (x \ x\) \ y" by (simp only: assoc) also have "\ = \ \ y" by (simp only: right_inv) also have "\ = y" by (simp only: left_one) finally show ?thesis . qed end