src/HOL/Library/Permutation.thy
changeset 23755 1c4672d130b1
parent 21404 eb85850d3eb7
child 25277 95128fcdd7e8
     1.1 --- a/src/HOL/Library/Permutation.thy	Wed Jul 11 11:27:46 2007 +0200
     1.2 +++ b/src/HOL/Library/Permutation.thy	Wed Jul 11 11:28:13 2007 +0200
     1.3 @@ -8,19 +8,13 @@
     1.4  imports Multiset
     1.5  begin
     1.6  
     1.7 -consts
     1.8 -  perm :: "('a list * 'a list) set"
     1.9 -
    1.10 -abbreviation
    1.11 -  perm_rel :: "'a list => 'a list => bool"  ("_ <~~> _"  [50, 50] 50) where
    1.12 -  "x <~~> y == (x, y) \<in> perm"
    1.13 -
    1.14 -inductive perm
    1.15 -  intros
    1.16 +inductive
    1.17 +  perm :: "'a list => 'a list => bool"  ("_ <~~> _"  [50, 50] 50)
    1.18 +  where
    1.19      Nil  [intro!]: "[] <~~> []"
    1.20 -    swap [intro!]: "y # x # l <~~> x # y # l"
    1.21 -    Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
    1.22 -    trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
    1.23 +  | swap [intro!]: "y # x # l <~~> x # y # l"
    1.24 +  | Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
    1.25 +  | trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
    1.26  
    1.27  lemma perm_refl [iff]: "l <~~> l"
    1.28    by (induct l) auto