src/ZF/ex/contract0.thy
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 16 0b033d50ca1c
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/contract.thy
     2     ID:         $Id$
     3     Author: 	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