src/HOLCF/explicit_domains/Dnat.thy

--- a/src/HOLCF/explicit_domains/Dnat.thy	Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dnat.thy	Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	HOLCF/Dnat.thy
+(*  Title:      HOLCF/Dnat.thy
     ID:         $Id$
-    Author: 	Franz Regensburger
+    Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
 Theory for the domain of natural numbers  dnat = one ++ dnat
@@ -31,22 +31,22 @@
 (* ----------------------------------------------------------------------- *)
 (* essential constants                                                     *)
 
-dnat_rep	:: " dnat -> (one ++ dnat)"
-dnat_abs	:: "(one ++ dnat) -> dnat"
+dnat_rep        :: " dnat -> (one ++ dnat)"
+dnat_abs        :: "(one ++ dnat) -> dnat"
 
 (* ----------------------------------------------------------------------- *)
 (* abstract constants and auxiliary constants                              *)
 
-dnat_copy	:: "(dnat -> dnat) -> dnat -> dnat"
+dnat_copy       :: "(dnat -> dnat) -> dnat -> dnat"
 
-dzero		:: "dnat"
-dsucc		:: "dnat -> dnat"
-dnat_when	:: "'b -> (dnat -> 'b) -> dnat -> 'b"
-is_dzero	:: "dnat -> tr"
-is_dsucc	:: "dnat -> tr"
-dpred		:: "dnat -> dnat"
-dnat_take	:: "nat => dnat -> dnat"
-dnat_bisim	:: "(dnat => dnat => bool) => bool"
+dzero           :: "dnat"
+dsucc           :: "dnat -> dnat"
+dnat_when       :: "'b -> (dnat -> 'b) -> dnat -> 'b"
+is_dzero        :: "dnat -> tr"
+is_dsucc        :: "dnat -> tr"
+dpred           :: "dnat -> dnat"
+dnat_take       :: "nat => dnat -> dnat"
+dnat_bisim      :: "(dnat => dnat => bool) => bool"
 
 rules
 
@@ -61,11 +61,11 @@
 (* dnat_abs is an isomorphism with inverse dnat_rep                        *)
 (* identity is the least endomorphism on dnat                              *)
 
-dnat_abs_iso	"dnat_rep`(dnat_abs`x) = x"
-dnat_rep_iso	"dnat_abs`(dnat_rep`x) = x"
-dnat_copy_def	"dnat_copy == (LAM f. dnat_abs oo 
-		 (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
-dnat_reach	"(fix`dnat_copy)`x=x"
+dnat_abs_iso    "dnat_rep`(dnat_abs`x) = x"
+dnat_rep_iso    "dnat_abs`(dnat_rep`x) = x"
+dnat_copy_def   "dnat_copy == (LAM f. dnat_abs oo 
+                 (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
+dnat_reach      "(fix`dnat_copy)`x=x"
 
 
 defs
@@ -74,21 +74,21 @@
 (* ----------------------------------------------------------------------- *)
 (* constructors                                                            *)
 
-dzero_def	"dzero == dnat_abs`(sinl`one)"
-dsucc_def	"dsucc == (LAM n. dnat_abs`(sinr`n))"
+dzero_def       "dzero == dnat_abs`(sinl`one)"
+dsucc_def       "dsucc == (LAM n. dnat_abs`(sinr`n))"
 
 (* ----------------------------------------------------------------------- *)
 (* discriminator functional                                                *)
 
-dnat_when_def	"dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
+dnat_when_def   "dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
 
 
 (* ----------------------------------------------------------------------- *)
 (* discriminators and selectors                                            *)
 
-is_dzero_def	"is_dzero == dnat_when`TT`(LAM x.FF)"
-is_dsucc_def	"is_dsucc == dnat_when`FF`(LAM x.TT)"
-dpred_def	"dpred == dnat_when`UU`(LAM x.x)"
+is_dzero_def    "is_dzero == dnat_when`TT`(LAM x.FF)"
+is_dsucc_def    "is_dsucc == dnat_when`FF`(LAM x.TT)"
+dpred_def       "dpred == dnat_when`UU`(LAM x.x)"
 
 
 (* ----------------------------------------------------------------------- *)
@@ -102,9 +102,9 @@
 
 dnat_bisim_def "dnat_bisim ==
 (%R.!s1 s2.
- 	R s1 s2 -->
+        R s1 s2 -->
   ((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |
   (? s11 s21. s11~=UU & s21~=UU & s1=dsucc`s11 &
-		 s2 = dsucc`s21 & R s11 s21)))"
+                 s2 = dsucc`s21 & R s11 s21)))"
 
 end