src/ZF/Resid/Conversion.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Resid/Conversion.thy	Thu Apr 13 15:38:07 1995 +0200
@@ -0,0 +1,36 @@
+(*  Title: 	Conversion.thy
+    ID:         $Id$
+    Author: 	Ole Rasmussen
+    Copyright   1995  University of Cambridge
+    Logic Image: ZF
+
+*)
+
+Conversion = Confluence+
+
+consts
+  Sconv1	:: "i"
+  "<-1->"	:: "[i,i]=>o" (infixl 50)
+  Sconv		:: "i"
+  "<--->"	:: "[i,i]=>o" (infixl 50)
+
+translations
+  "a<-1->b"    == "<a,b>:Sconv1"
+  "a<--->b"    == "<a,b>:Sconv"
+  
+inductive
+  domains       "Sconv1" <= "lambda*lambda"
+  intrs
+    red1	"m -1-> n ==> m<-1->n"
+    expl  	"n -1-> m ==> m<-1->n"
+  type_intrs	"[red1D1,red1D2]@lambda.intrs@bool_typechecks"
+
+inductive
+  domains       "Sconv" <= "lambda*lambda"
+  intrs
+    one_step	"m<-1->n  ==> m<--->n"
+    refl  	"m:lambda ==> m<--->m"
+    trans	"[|m<--->n; n<--->p|] ==> m<--->p"
+  type_intrs	"[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
+end
+