47295

1 
(* Title: HOL/Isar_Examples/Group_Notepad.thy


2 
Author: Makarius


3 
*)


4 


5 
header {* Some algebraic identities derived from group axioms  proof notepad version *}


6 


7 
theory Group_Notepad


8 
imports Main


9 
begin


10 


11 
notepad


12 
begin


13 
txt {* hypothetical group axiomatization *}


14 


15 
fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)


16 
and one :: "'a"


17 
and inverse :: "'a => 'a"


18 
assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"


19 
and left_one: "\<And>x. one ** x = x"


20 
and left_inverse: "\<And>x. inverse x ** x = one"


21 


22 
txt {* some consequences *}


23 


24 
have right_inverse: "\<And>x. x ** inverse x = one"


25 
proof 


26 
fix x


27 
have "x ** inverse x = one ** (x ** inverse x)"


28 
by (simp only: left_one)


29 
also have "\<dots> = one ** x ** inverse x"


30 
by (simp only: assoc)


31 
also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"


32 
by (simp only: left_inverse)


33 
also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"


34 
by (simp only: assoc)


35 
also have "\<dots> = inverse (inverse x) ** one ** inverse x"


36 
by (simp only: left_inverse)


37 
also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"


38 
by (simp only: assoc)


39 
also have "\<dots> = inverse (inverse x) ** inverse x"


40 
by (simp only: left_one)


41 
also have "\<dots> = one"


42 
by (simp only: left_inverse)


43 
finally show "x ** inverse x = one" .


44 
qed


45 


46 
have right_one: "\<And>x. x ** one = x"


47 
proof 


48 
fix x


49 
have "x ** one = x ** (inverse x ** x)"


50 
by (simp only: left_inverse)


51 
also have "\<dots> = x ** inverse x ** x"


52 
by (simp only: assoc)


53 
also have "\<dots> = one ** x"


54 
by (simp only: right_inverse)


55 
also have "\<dots> = x"


56 
by (simp only: left_one)


57 
finally show "x ** one = x" .


58 
qed


59 


60 
have one_equality: "\<And>e x. e ** x = x \<Longrightarrow> one = e"


61 
proof 


62 
fix e x


63 
assume eq: "e ** x = x"


64 
have "one = x ** inverse x"


65 
by (simp only: right_inverse)


66 
also have "\<dots> = (e ** x) ** inverse x"


67 
by (simp only: eq)


68 
also have "\<dots> = e ** (x ** inverse x)"


69 
by (simp only: assoc)


70 
also have "\<dots> = e ** one"


71 
by (simp only: right_inverse)


72 
also have "\<dots> = e"


73 
by (simp only: right_one)


74 
finally show "one = e" .


75 
qed


76 


77 
have inverse_equality: "\<And>x x'. x' ** x = one \<Longrightarrow> inverse x = x'"


78 
proof 


79 
fix x x'


80 
assume eq: "x' ** x = one"


81 
have "inverse x = one ** inverse x"


82 
by (simp only: left_one)


83 
also have "\<dots> = (x' ** x) ** inverse x"


84 
by (simp only: eq)


85 
also have "\<dots> = x' ** (x ** inverse x)"


86 
by (simp only: assoc)


87 
also have "\<dots> = x' ** one"


88 
by (simp only: right_inverse)


89 
also have "\<dots> = x'"


90 
by (simp only: right_one)


91 
finally show "inverse x = x'" .


92 
qed


93 


94 
end


95 


96 
end
