# HG changeset patch # User wenzelm # Date 1449479970 -3600 # Node ID 458b4e3720abb07c70d13994ea01cfdd3aeaf380 # Parent 341103068504bf846741c214673084dc216d98b1 tuned; diff -r 341103068504 -r 458b4e3720ab src/HOL/Isar_Examples/Group.thy --- a/src/HOL/Isar_Examples/Group.thy Sun Dec 06 23:48:25 2015 +0100 +++ b/src/HOL/Isar_Examples/Group.thy Mon Dec 07 10:19:30 2015 +0100 @@ -10,9 +10,9 @@ subsection \Groups and calculational reasoning\ -text \Groups over signature \(\ :: \ \ \ \ \, one :: \, inverse :: \ \ \)\ +text \Groups over signature \(* :: \ \ \ \ \, 1 :: \, inverse :: \ \ \)\ are defined as an axiomatic type class as follows. Note that the parent - class \\\ is provided by the basic HOL theory.\ + class \times\ is provided by the basic HOL theory.\ class group = times + one + inverse + assumes group_assoc: "(x * y) * z = x * (y * z)" @@ -122,7 +122,7 @@ subsection \Groups as monoids\ -text \Monoids over signature \(\ :: \ \ \ \ \, one :: \)\ are defined like +text \Monoids over signature \(* :: \ \ \ \ \, 1 :: \)\ are defined like this.\ class monoid = times + one + diff -r 341103068504 -r 458b4e3720ab src/HOL/Isar_Examples/Group_Context.thy --- a/src/HOL/Isar_Examples/Group_Context.thy Sun Dec 06 23:48:25 2015 +0100 +++ b/src/HOL/Isar_Examples/Group_Context.thy Mon Dec 07 10:19:30 2015 +0100 @@ -11,82 +11,82 @@ text \hypothetical group axiomatization\ context - fixes prod :: "'a \ 'a \ 'a" (infixl "**" 70) + fixes prod :: "'a \ 'a \ '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" + 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" +lemma right_inverse: "x \ inverse x = one" proof - - have "x ** inverse x = one ** (x ** inverse x)" + have "x \ inverse x = one \ (x \ inverse x)" by (simp only: left_one) - also have "\ = one ** x ** inverse x" + also have "\ = one \ x \ inverse x" by (simp only: assoc) - also have "\ = inverse (inverse x) ** inverse x ** x ** inverse x" + 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" + also have "\ = inverse (inverse x) \ (inverse x \ x) \ inverse x" by (simp only: assoc) - also have "\ = inverse (inverse x) ** one ** inverse x" + also have "\ = inverse (inverse x) \ one \ inverse x" by (simp only: left_inverse) - also have "\ = inverse (inverse x) ** (one ** inverse x)" + also have "\ = inverse (inverse x) \ (one \ inverse x)" by (simp only: assoc) - also have "\ = inverse (inverse x) ** inverse x" + also have "\ = inverse (inverse x) \ inverse x" by (simp only: left_one) also have "\ = one" by (simp only: left_inverse) - finally show "x ** inverse x = one" . + finally show ?thesis . qed -lemma right_one: "x ** one = x" +lemma right_one: "x \ one = x" proof - - have "x ** one = x ** (inverse x ** x)" + have "x \ one = x \ (inverse x \ x)" by (simp only: left_inverse) - also have "\ = x ** inverse x ** x" + also have "\ = x \ inverse x \ x" by (simp only: assoc) - also have "\ = one ** x" + also have "\ = one \ x" by (simp only: right_inverse) also have "\ = x" by (simp only: left_one) - finally show "x ** one = x" . + finally show ?thesis . qed lemma one_equality: - assumes eq: "e ** x = x" + assumes eq: "e \ x = x" shows "one = e" proof - - have "one = x ** inverse x" + have "one = x \ inverse x" by (simp only: right_inverse) - also have "\ = (e ** x) ** inverse x" + also have "\ = (e \ x) \ inverse x" by (simp only: eq) - also have "\ = e ** (x ** inverse x)" + also have "\ = e \ (x \ inverse x)" by (simp only: assoc) - also have "\ = e ** one" + also have "\ = e \ one" by (simp only: right_inverse) also have "\ = e" by (simp only: right_one) - finally show "one = e" . + finally show ?thesis . qed lemma inverse_equality: - assumes eq: "x' ** x = one" + assumes eq: "x' \ x = one" shows "inverse x = x'" proof - - have "inverse x = one ** inverse x" + have "inverse x = one \ inverse x" by (simp only: left_one) - also have "\ = (x' ** x) ** inverse x" + also have "\ = (x' \ x) \ inverse x" by (simp only: eq) - also have "\ = x' ** (x ** inverse x)" + also have "\ = x' \ (x \ inverse x)" by (simp only: assoc) - also have "\ = x' ** one" + also have "\ = x' \ one" by (simp only: right_inverse) also have "\ = x'" by (simp only: right_one) - finally show "inverse x = x'" . + finally show ?thesis . qed end diff -r 341103068504 -r 458b4e3720ab src/HOL/Isar_Examples/Group_Notepad.thy --- a/src/HOL/Isar_Examples/Group_Notepad.thy Sun Dec 06 23:48:25 2015 +0100 +++ b/src/HOL/Isar_Examples/Group_Notepad.thy Mon Dec 07 10:19:30 2015 +0100 @@ -12,83 +12,78 @@ begin txt \hypothetical group axiomatization\ - fix prod :: "'a \ 'a \ 'a" (infixl "**" 70) + fix prod :: "'a \ 'a \ 'a" (infixl "\" 70) and one :: "'a" and inverse :: "'a \ 'a" - assume assoc: "\x y z. (x ** y) ** z = x ** (y ** z)" - and left_one: "\x. one ** x = x" - and left_inverse: "\x. inverse x ** x = one" + 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 \some consequences\ - have right_inverse: "\x. x ** inverse x = one" + have right_inverse: "x \ inverse x = one" for x proof - - fix x - have "x ** inverse x = one ** (x ** inverse x)" + have "x \ inverse x = one \ (x \ inverse x)" by (simp only: left_one) - also have "\ = one ** x ** inverse x" + also have "\ = one \ x \ inverse x" by (simp only: assoc) - also have "\ = inverse (inverse x) ** inverse x ** x ** inverse x" + 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" + also have "\ = inverse (inverse x) \ (inverse x \ x) \ inverse x" by (simp only: assoc) - also have "\ = inverse (inverse x) ** one ** inverse x" + also have "\ = inverse (inverse x) \ one \ inverse x" by (simp only: left_inverse) - also have "\ = inverse (inverse x) ** (one ** inverse x)" + also have "\ = inverse (inverse x) \ (one \ inverse x)" by (simp only: assoc) - also have "\ = inverse (inverse x) ** inverse x" + also have "\ = inverse (inverse x) \ inverse x" by (simp only: left_one) also have "\ = one" by (simp only: left_inverse) - finally show "x ** inverse x = one" . + finally show ?thesis . qed - have right_one: "\x. x ** one = x" + have right_one: "x \ one = x" for x proof - - fix x - have "x ** one = x ** (inverse x ** x)" + have "x \ one = x \ (inverse x \ x)" by (simp only: left_inverse) - also have "\ = x ** inverse x ** x" + also have "\ = x \ inverse x \ x" by (simp only: assoc) - also have "\ = one ** x" + also have "\ = one \ x" by (simp only: right_inverse) also have "\ = x" by (simp only: left_one) - finally show "x ** one = x" . + finally show ?thesis . qed - have one_equality: "\e x. e ** x = x \ one = e" + have one_equality: "one = e" if eq: "e \ x = x" for e x proof - - fix e x - assume eq: "e ** x = x" - have "one = x ** inverse x" + have "one = x \ inverse x" by (simp only: right_inverse) - also have "\ = (e ** x) ** inverse x" + also have "\ = (e \ x) \ inverse x" by (simp only: eq) - also have "\ = e ** (x ** inverse x)" + also have "\ = e \ (x \ inverse x)" by (simp only: assoc) - also have "\ = e ** one" + also have "\ = e \ one" by (simp only: right_inverse) also have "\ = e" by (simp only: right_one) - finally show "one = e" . + finally show ?thesis . qed - have inverse_equality: "\x x'. x' ** x = one \ inverse x = x'" + have inverse_equality: "inverse x = x'" if eq: "x' \ x = one" for x x' proof - - fix x x' - assume eq: "x' ** x = one" - have "inverse x = one ** inverse x" + have "inverse x = one \ inverse x" by (simp only: left_one) - also have "\ = (x' ** x) ** inverse x" + also have "\ = (x' \ x) \ inverse x" by (simp only: eq) - also have "\ = x' ** (x ** inverse x)" + also have "\ = x' \ (x \ inverse x)" by (simp only: assoc) - also have "\ = x' ** one" + also have "\ = x' \ one" by (simp only: right_inverse) also have "\ = x'" by (simp only: right_one) - finally show "inverse x = x'" . + finally show ?thesis . qed end