summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 07 Dec 2015 10:19:30 +0100 | |

changeset 61797 | 458b4e3720ab |

parent 61796 | 341103068504 |

child 61798 | 27f3c10b0b50 |

tuned;

--- 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 +

--- 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

--- 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