src/ZF/ex/Contract0.thy

+(*  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