|
1048
|
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))"
|
|
1155
|
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)"
|
|
1048
|
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 |
|