src/ZF/Resid/Residuals.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 3840 e0baea4d485a
permissions -rw-r--r--
expanded tabs
     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