equal
deleted
inserted
replaced
17 types |
17 types |
18 'x prm = "('x \<times> 'x) list" |
18 'x prm = "('x \<times> 'x) list" |
19 |
19 |
20 (* polymorphic operations for permutation and swapping*) |
20 (* polymorphic operations for permutation and swapping*) |
21 consts |
21 consts |
22 perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet> _" [80,80] 80) |
22 perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<bullet>" 80) |
23 swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x" |
23 swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x" |
24 |
24 |
25 (* permutation on sets *) |
25 (* permutation on sets *) |
26 defs (overloaded) |
26 defs (overloaded) |
27 perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}" |
27 perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}" |