src/ZF/ex/Contract0.thy
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 16 0b033d50ca1c
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	ZF/ex/contract.thy
     2     ID:         $Id$
     3     Author: 	Tobias Nipkow & Lawrence C Paulson
     4     Copyright   1993  University of Cambridge
     5 
     6 Inductive definition of (1-step) contractions and (mult-step) reductions
     7 *)
     8 
     9 Contract0 = Comb +
    10 consts
    11   diamond   :: "i => o"
    12   I         :: "i"
    13 
    14   contract  :: "i"
    15   "-1->"    :: "[i,i] => o"    			(infixl 50)
    16   "--->"    :: "[i,i] => o"    			(infixl 50)
    17 
    18   parcontract :: "i"
    19   "=1=>"    :: "[i,i] => o"    			(infixl 50)
    20   "===>"    :: "[i,i] => o"    			(infixl 50)
    21 
    22 translations
    23   "p -1-> q" == "<p,q> : contract"
    24   "p ---> q" == "<p,q> : contract^*"
    25   "p =1=> q" == "<p,q> : parcontract"
    26   "p ===> q" == "<p,q> : parcontract^+"
    27 
    28 rules
    29 
    30   diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
    31 \                            (ALL y'. <x,y'>:r --> \
    32 \                                 (EX z. <y,z>:r & <y',z> : r))"
    33 
    34   I_def       "I == S#K#K"
    35 
    36 end