--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/contract0.thy Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,36 @@
+(* Title: ZF/ex/contract.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Lawrence C Paulson
+ Copyright 1993 University of Cambridge
+
+Inductive definition of (1-step) contractions and (mult-step) reductions
+*)
+
+Contract0 = Comb +
+consts
+ diamond :: "i => o"
+ I :: "i"
+
+ contract :: "i"
+ "-1->" :: "[i,i] => o" (infixl 50)
+ "--->" :: "[i,i] => o" (infixl 50)
+
+ parcontract :: "i"
+ "=1=>" :: "[i,i] => o" (infixl 50)
+ "===>" :: "[i,i] => o" (infixl 50)
+
+translations
+ "p -1-> q" == "<p,q> : contract"
+ "p ---> q" == "<p,q> : contract^*"
+ "p =1=> q" == "<p,q> : parcontract"
+ "p ===> q" == "<p,q> : parcontract^+"
+
+rules
+
+ diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
+\ (ALL y'. <x,y'>:r --> \
+\ (EX z. <y,z>:r & <y',z> : r))"
+
+ I_def "I == S#K#K"
+
+end