src/ZF/Resid/Residuals.thy
 author clasohm Sat Dec 09 13:36:11 1995 +0100 (1995-12-09 ago) changeset 1401 0c439768f45c parent 1155 928a16e02f9f child 1478 2b8c2a7547ab permissions -rw-r--r--
removed quotes from consts and syntax sections
```     1 (*  Title: 	Residuals.thy
```
```     2     ID:         \$Id\$
```
```     3     Author: 	Ole Rasmussen
```
```     4     Copyright   1995  University of Cambridge
```
```     5     Logic Image: ZF
```
```     6
```
```     7 *)
```
```     8
```
```     9 Residuals = Substitution+
```
```    10
```
```    11 consts
```
```    12   Sres		:: i
```
```    13   residuals	:: [i,i,i]=>i
```
```    14   "|>"		:: [i,i]=>i     (infixl 70)
```
```    15
```
```    16 translations
```
```    17   "residuals(u,v,w)"  == "<u,v,w>:Sres"
```
```    18
```
```    19 inductive
```
```    20   domains       "Sres" <= "redexes*redexes*redexes"
```
```    21   intrs
```
```    22     Res_Var	"n:nat ==> residuals(Var(n),Var(n),Var(n))"
```
```    23     Res_Fun	"[|residuals(u,v,w)|]==>
```
```    24 		     residuals(Fun(u),Fun(v),Fun(w))"
```
```    25     Res_App	"[|residuals(u1,v1,w1);
```
```    26 		   residuals(u2,v2,w2); b:bool|]==>
```
```    27 		 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
```
```    28     Res_redex	"[|residuals(u1,v1,w1);
```
```    29 		   residuals(u2,v2,w2); b:bool|]==>
```
```    30 		 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
```
```    31   type_intrs	"[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
```
```    32
```
```    33 rules
```
```    34   res_func_def  "u |> v == THE w.residuals(u,v,w)"
```
```    35 end
```
```    36
```