src/HOL/Induct/Perm.thy
changeset 3120 c58423c20740
child 8354 c02e3c131eca
equal deleted inserted replaced
3119:bb2ee88aa43f 3120:c58423c20740
       
     1 (*  Title:      HOL/ex/Perm.thy
       
     2     ID:         $Id$
       
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
       
     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"   
       
    12 syntax "@perm"  :: ['a list, 'a list] => bool ("_ <~~> _"  [50,50] 50)
       
    13 
       
    14 translations
       
    15     "x <~~> y" == "(x,y) : perm"
       
    16 
       
    17 inductive perm
       
    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