# 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 \<open>Groups and calculational reasoning\<close> 
 
-text \<open>Groups over signature \<open>(\<times> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, one :: \<alpha>, inverse :: \<alpha> \<Rightarrow> \<alpha>)\<close>
+text \<open>Groups over signature \<open>(* :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, 1 :: \<alpha>, inverse :: \<alpha> \<Rightarrow> \<alpha>)\<close>
   are defined as an axiomatic type class as follows. Note that the parent
-  class \<open>\<times>\<close> is provided by the basic HOL theory.\<close>
+  class \<open>times\<close> is provided by the basic HOL theory.\<close>
 
 class group = times + one + inverse +
   assumes group_assoc: "(x * y) * z = x * (y * z)"
@@ -122,7 +122,7 @@
 
 subsection \<open>Groups as monoids\<close>
 
-text \<open>Monoids over signature \<open>(\<times> :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, one :: \<alpha>)\<close> are defined like
+text \<open>Monoids over signature \<open>(* :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, 1 :: \<alpha>)\<close> are defined like
   this.\<close>
 
 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 \<open>hypothetical group axiomatization\<close>
 
 context
-  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
+  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<odot>" 70)
     and one :: "'a"
     and inverse :: "'a \<Rightarrow> '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 \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
+    and left_one: "one \<odot> x = x"
+    and left_inverse: "inverse x \<odot> x = one"
 begin
 
 text \<open>some consequences\<close>
 
-lemma right_inverse: "x ** inverse x = one"
+lemma right_inverse: "x \<odot> inverse x = one"
 proof -
-  have "x ** inverse x = one ** (x ** inverse x)"
+  have "x \<odot> inverse x = one \<odot> (x \<odot> inverse x)"
     by (simp only: left_one)
-  also have "\<dots> = one ** x ** inverse x"
+  also have "\<dots> = one \<odot> x \<odot> inverse x"
     by (simp only: assoc)
-  also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
+  also have "\<dots> = inverse (inverse x) \<odot> inverse x \<odot> x \<odot> inverse x"
     by (simp only: left_inverse)
-  also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
+  also have "\<dots> = inverse (inverse x) \<odot> (inverse x \<odot> x) \<odot> inverse x"
     by (simp only: assoc)
-  also have "\<dots> = inverse (inverse x) ** one ** inverse x"
+  also have "\<dots> = inverse (inverse x) \<odot> one \<odot> inverse x"
     by (simp only: left_inverse)
-  also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
+  also have "\<dots> = inverse (inverse x) \<odot> (one \<odot> inverse x)"
     by (simp only: assoc)
-  also have "\<dots> = inverse (inverse x) ** inverse x"
+  also have "\<dots> = inverse (inverse x) \<odot> inverse x"
     by (simp only: left_one)
   also have "\<dots> = 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 \<odot> one = x"
 proof -
-  have "x ** one = x ** (inverse x ** x)"
+  have "x \<odot> one = x \<odot> (inverse x \<odot> x)"
     by (simp only: left_inverse)
-  also have "\<dots> = x ** inverse x ** x"
+  also have "\<dots> = x \<odot> inverse x \<odot> x"
     by (simp only: assoc)
-  also have "\<dots> = one ** x"
+  also have "\<dots> = one \<odot> x"
     by (simp only: right_inverse)
   also have "\<dots> = 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 \<odot> x = x"
   shows "one = e"
 proof -
-  have "one = x ** inverse x"
+  have "one = x \<odot> inverse x"
     by (simp only: right_inverse)
-  also have "\<dots> = (e ** x) ** inverse x"
+  also have "\<dots> = (e \<odot> x) \<odot> inverse x"
     by (simp only: eq)
-  also have "\<dots> = e ** (x ** inverse x)"
+  also have "\<dots> = e \<odot> (x \<odot> inverse x)"
     by (simp only: assoc)
-  also have "\<dots> = e ** one"
+  also have "\<dots> = e \<odot> one"
     by (simp only: right_inverse)
   also have "\<dots> = 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' \<odot> x = one"
   shows "inverse x = x'"
 proof -
-  have "inverse x = one ** inverse x"
+  have "inverse x = one \<odot> inverse x"
     by (simp only: left_one)
-  also have "\<dots> = (x' ** x) ** inverse x"
+  also have "\<dots> = (x' \<odot> x) \<odot> inverse x"
     by (simp only: eq)
-  also have "\<dots> = x' ** (x ** inverse x)"
+  also have "\<dots> = x' \<odot> (x \<odot> inverse x)"
     by (simp only: assoc)
-  also have "\<dots> = x' ** one"
+  also have "\<dots> = x' \<odot> one"
     by (simp only: right_inverse)
   also have "\<dots> = 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 \<open>hypothetical group axiomatization\<close>
 
-  fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
+  fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<odot>" 70)
     and one :: "'a"
     and inverse :: "'a \<Rightarrow> 'a"
-  assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
-    and left_one: "\<And>x. one ** x = x"
-    and left_inverse: "\<And>x. inverse x ** x = one"
+  assume assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
+    and left_one: "one \<odot> x = x"
+    and left_inverse: "inverse x \<odot> x = one"
+    for x y z
 
   txt \<open>some consequences\<close>
 
-  have right_inverse: "\<And>x. x ** inverse x = one"
+  have right_inverse: "x \<odot> inverse x = one" for x
   proof -
-    fix x
-    have "x ** inverse x = one ** (x ** inverse x)"
+    have "x \<odot> inverse x = one \<odot> (x \<odot> inverse x)"
       by (simp only: left_one)
-    also have "\<dots> = one ** x ** inverse x"
+    also have "\<dots> = one \<odot> x \<odot> inverse x"
       by (simp only: assoc)
-    also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
+    also have "\<dots> = inverse (inverse x) \<odot> inverse x \<odot> x \<odot> inverse x"
       by (simp only: left_inverse)
-    also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
+    also have "\<dots> = inverse (inverse x) \<odot> (inverse x \<odot> x) \<odot> inverse x"
       by (simp only: assoc)
-    also have "\<dots> = inverse (inverse x) ** one ** inverse x"
+    also have "\<dots> = inverse (inverse x) \<odot> one \<odot> inverse x"
       by (simp only: left_inverse)
-    also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
+    also have "\<dots> = inverse (inverse x) \<odot> (one \<odot> inverse x)"
       by (simp only: assoc)
-    also have "\<dots> = inverse (inverse x) ** inverse x"
+    also have "\<dots> = inverse (inverse x) \<odot> inverse x"
       by (simp only: left_one)
     also have "\<dots> = one"
       by (simp only: left_inverse)
-    finally show "x ** inverse x = one" .
+    finally show ?thesis .
   qed
 
-  have right_one: "\<And>x. x ** one = x"
+  have right_one: "x \<odot> one = x" for x
   proof -
-    fix x
-    have "x ** one = x ** (inverse x ** x)"
+    have "x \<odot> one = x \<odot> (inverse x \<odot> x)"
       by (simp only: left_inverse)
-    also have "\<dots> = x ** inverse x ** x"
+    also have "\<dots> = x \<odot> inverse x \<odot> x"
       by (simp only: assoc)
-    also have "\<dots> = one ** x"
+    also have "\<dots> = one \<odot> x"
       by (simp only: right_inverse)
     also have "\<dots> = x"
       by (simp only: left_one)
-    finally show "x ** one = x" .
+    finally show ?thesis .
   qed
 
-  have one_equality: "\<And>e x. e ** x = x \<Longrightarrow> one = e"
+  have one_equality: "one = e" if eq: "e \<odot> x = x" for e x
   proof -
-    fix e x
-    assume eq: "e ** x = x"
-    have "one = x ** inverse x"
+    have "one = x \<odot> inverse x"
       by (simp only: right_inverse)
-    also have "\<dots> = (e ** x) ** inverse x"
+    also have "\<dots> = (e \<odot> x) \<odot> inverse x"
       by (simp only: eq)
-    also have "\<dots> = e ** (x ** inverse x)"
+    also have "\<dots> = e \<odot> (x \<odot> inverse x)"
       by (simp only: assoc)
-    also have "\<dots> = e ** one"
+    also have "\<dots> = e \<odot> one"
       by (simp only: right_inverse)
     also have "\<dots> = e"
       by (simp only: right_one)
-    finally show "one = e" .
+    finally show ?thesis .
   qed
 
-  have inverse_equality: "\<And>x x'. x' ** x = one \<Longrightarrow> inverse x = x'"
+  have inverse_equality: "inverse x = x'" if eq: "x' \<odot> x = one" for x x'
   proof -
-    fix x x'
-    assume eq: "x' ** x = one"
-    have "inverse x = one ** inverse x"
+    have "inverse x = one \<odot> inverse x"
       by (simp only: left_one)
-    also have "\<dots> = (x' ** x) ** inverse x"
+    also have "\<dots> = (x' \<odot> x) \<odot> inverse x"
       by (simp only: eq)
-    also have "\<dots> = x' ** (x ** inverse x)"
+    also have "\<dots> = x' \<odot> (x \<odot> inverse x)"
       by (simp only: assoc)
-    also have "\<dots> = x' ** one"
+    also have "\<dots> = x' \<odot> one"
       by (simp only: right_inverse)
     also have "\<dots> = x'"
       by (simp only: right_one)
-    finally show "inverse x = x'" .
+    finally show ?thesis .
   qed
 
 end