equal
deleted
inserted
replaced
1 theory Specifications_with_bundle_mixins |
1 theory Specifications_with_bundle_mixins |
2 imports "HOL-Library.Perm" |
2 imports "HOL-Library.Perm" |
3 begin |
3 begin |
4 |
4 |
5 locale involutory = |
5 locale involutory = opening permutation_syntax + |
6 includes permutation_syntax |
|
7 fixes f :: \<open>'a perm\<close> |
6 fixes f :: \<open>'a perm\<close> |
8 assumes involutory: \<open>\<And>x. f \<langle>$\<rangle> (f \<langle>$\<rangle> x) = x\<close> |
7 assumes involutory: \<open>\<And>x. f \<langle>$\<rangle> (f \<langle>$\<rangle> x) = x\<close> |
9 begin |
8 begin |
10 |
9 |
11 lemma |
10 lemma |
21 thm involutory (*syntax from permutation_syntax only present in locale specification and initial block*) |
20 thm involutory (*syntax from permutation_syntax only present in locale specification and initial block*) |
22 |
21 |
23 end |
22 end |
24 |
23 |
25 |
24 |
26 class at_most_two_elems = |
25 class at_most_two_elems = opening permutation_syntax + |
27 includes permutation_syntax |
|
28 assumes swap_distinct: \<open>a \<noteq> b \<Longrightarrow> \<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c \<noteq> c\<close> |
26 assumes swap_distinct: \<open>a \<noteq> b \<Longrightarrow> \<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c \<noteq> c\<close> |
29 begin |
27 begin |
30 |
28 |
31 lemma |
29 lemma |
32 \<open>card (UNIV :: 'a set) \<le> 2\<close> |
30 \<open>card (UNIV :: 'a set) \<le> 2\<close> |