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