|
1476
|
1 |
(* Title: HOL/ex/Perm.thy
|
|
1173
|
2 |
ID: $Id$
|
|
1476
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
1173
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Permutations: example of an inductive definition
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Perm = List +
|
|
|
10 |
|
|
|
11 |
consts perm :: "('a list * 'a list) set"
|
|
1376
|
12 |
syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50)
|
|
1173
|
13 |
|
|
|
14 |
translations
|
|
|
15 |
"x <~~> y" == "(x,y) : perm"
|
|
|
16 |
|
|
1789
|
17 |
inductive perm
|
|
1173
|
18 |
intrs
|
|
|
19 |
Nil "[] <~~> []"
|
|
|
20 |
swap "y#x#l <~~> x#y#l"
|
|
|
21 |
Cons "xs <~~> ys ==> z#xs <~~> z#ys"
|
|
|
22 |
trans "[| xs <~~> ys; ys <~~> zs |] ==> xs <~~> zs"
|
|
|
23 |
|
|
|
24 |
end
|