--- a/src/HOL/Library/Permutation.thy Wed Jul 11 11:27:46 2007 +0200
+++ b/src/HOL/Library/Permutation.thy Wed Jul 11 11:28:13 2007 +0200
@@ -8,19 +8,13 @@
imports Multiset
begin
-consts
- perm :: "('a list * 'a list) set"
-
-abbreviation
- perm_rel :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50) where
- "x <~~> y == (x, y) \<in> perm"
-
-inductive perm
- intros
+inductive
+ perm :: "'a list => 'a list => bool" ("_ <~~> _" [50, 50] 50)
+ where
Nil [intro!]: "[] <~~> []"
- swap [intro!]: "y # x # l <~~> x # y # l"
- Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
- trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
+ | swap [intro!]: "y # x # l <~~> x # y # l"
+ | Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
+ | trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
lemma perm_refl [iff]: "l <~~> l"
by (induct l) auto