
paulson@3120: (*  Title:      HOL/ex/Perm.thy
paulson@3120:     ID:         $Id$
paulson@3120:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120:     Copyright   1995  University of Cambridge
paulson@3120: 
paulson@3120: Permutations: example of an inductive definition
paulson@3120: *)
paulson@3120: 
paulson@3120: Perm = List +
paulson@3120: 
paulson@3120: consts  perm    :: "('a list * 'a list) set"   
paulson@3120: syntax "@perm"  :: ['a list, 'a list] => bool ("_ <~~> _"  [50,50] 50)
paulson@3120: 
paulson@3120: translations
paulson@3120:     "x <~~> y" == "(x,y) : perm"
paulson@3120: 
paulson@3120: inductive perm
paulson@3120:   intrs
paulson@3120:     Nil   "[] <~~> []"
paulson@3120:     swap  "y#x#l <~~> x#y#l"
paulson@3120:     Cons  "xs <~~> ys ==> z#xs <~~> z#ys"
paulson@3120:     trans "[| xs <~~> ys;  ys <~~> zs |] ==> xs <~~> zs"
paulson@3120: 
paulson@3120: end




