Last active
December 1, 2016 04:21
-
-
Save mbrcknl/b7dea796895b209d6cfcd7097f5c8cec to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| theory Scratch imports Main begin | |
| locale Magma = | |
| fixes m :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" | |
| locale SemiGroup = Magma + | |
| assumes assoc: "\<And>x y z. m (m x y) z = m x (m y z)" | |
| locale Commutative = Magma + | |
| assumes comm: "\<And>x y. m x y = m y x" | |
| locale Monoid = SemiGroup + | |
| fixes e :: "'a" | |
| assumes lunit: "\<And>x. m e x = x" | |
| assumes runit: "\<And>x. m x e = x" | |
| locale Group = Monoid + | |
| fixes i :: "'a \<Rightarrow> 'a" | |
| assumes linv: "\<And>x. m (i x) x = e" | |
| assumes rinv: "\<And>x. m x (i x) = e" | |
| locale AbelianGroup = Commutative + Group | |
| locale BooleanGroup = Monoid + | |
| assumes selfi: "\<And>x. m x x = e" | |
| context BooleanGroup begin | |
| sublocale Commutative | |
| proof | |
| fix x y | |
| have "m (m y x) (m y x) = e" | |
| by (rule selfi) | |
| hence "m y (m (m (m y x) (m y x)) x) = m y x" | |
| by (simp add: lunit) | |
| hence "m (m y y) (m (m x y) (m x x)) = m y x" | |
| by (simp add: assoc) | |
| thus "m x y = m y x" | |
| by (simp add: selfi lunit runit) | |
| qed | |
| sublocale AbelianGroup _ _ id | |
| unfolding id_def by unfold_locales (rule selfi)+ | |
| end | |
| end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment