author  paulson 
Wed, 07 May 1997 12:50:26 +0200  
changeset 3120  c58423c20740 
child 8354  c02e3c131eca 
permissions  rwrr 
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

1 
(* Title: HOL/ex/Perm.thy 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

2 
ID: $Id$ 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

4 
Copyright 1995 University of Cambridge 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

5 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

6 
Permutations: example of an inductive definition 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

7 
*) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

8 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

9 
Perm = List + 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

10 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

11 
consts perm :: "('a list * 'a list) set" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

12 
syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50) 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

13 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

14 
translations 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

15 
"x <~~> y" == "(x,y) : perm" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

16 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

17 
inductive perm 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

18 
intrs 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

19 
Nil "[] <~~> []" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

20 
swap "y#x#l <~~> x#y#l" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

21 
Cons "xs <~~> ys ==> z#xs <~~> z#ys" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

22 
trans "[ xs <~~> ys; ys <~~> zs ] ==> xs <~~> zs" 
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

23 

c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset

24 
end 