|
1 (* Title: SubUnion.thy |
|
2 ID: $Id$ |
|
3 Author: Ole Rasmussen |
|
4 Copyright 1995 University of Cambridge |
|
5 Logic Image: ZF |
|
6 *) |
|
7 |
|
8 SubUnion = Redex + |
|
9 |
|
10 consts |
|
11 Ssub,Scomp,Sreg :: "i" |
|
12 "<==","~" :: "[i,i]=>o" (infixl 70) |
|
13 un :: "[i,i]=>i" (infixl 70) |
|
14 regular :: "i=>o" |
|
15 |
|
16 translations |
|
17 "a<==b" == "<a,b>:Ssub" |
|
18 "a ~ b" == "<a,b>:Scomp" |
|
19 "regular(a)" == "a:Sreg" |
|
20 |
|
21 inductive |
|
22 domains "Ssub" <= "redexes*redexes" |
|
23 intrs |
|
24 Sub_Var "n:nat ==> Var(n)<== Var(n)" |
|
25 Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)" |
|
26 Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==> \ |
|
27 \ App(0,u1,u2)<== App(b,v1,v2)" |
|
28 Sub_App2 "[|u1<== v1; u2<== v2|]==> \ |
|
29 \ App(1,u1,u2)<== App(1,v1,v2)" |
|
30 type_intrs "redexes.intrs@bool_typechecks" |
|
31 |
|
32 inductive |
|
33 domains "Scomp" <= "redexes*redexes" |
|
34 intrs |
|
35 Comp_Var "n:nat ==> Var(n) ~ Var(n)" |
|
36 Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)" |
|
37 Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==> \ |
|
38 \ App(b1,u1,u2) ~ App(b2,v1,v2)" |
|
39 type_intrs "redexes.intrs@bool_typechecks" |
|
40 |
|
41 inductive |
|
42 domains "Sreg" <= "redexes" |
|
43 intrs |
|
44 Reg_Var "n:nat ==> regular(Var(n))" |
|
45 Reg_Fun "[|regular(u)|]==> regular(Fun(u))" |
|
46 Reg_App1 "[|regular(Fun(u)); regular(v) \ |
|
47 \ |]==>regular(App(1,Fun(u),v))" |
|
48 Reg_App2 "[|regular(u); regular(v) \ |
|
49 \ |]==>regular(App(0,u,v))" |
|
50 type_intrs "redexes.intrs@bool_typechecks" |
|
51 |
|
52 defs |
|
53 union_def "u un v == redex_rec(u, \ |
|
54 \ %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t), \ |
|
55 \ %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t), \ |
|
56 \%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0, \ |
|
57 \ %c z u. App(b or c, m`z, p`u), t))`v" |
|
58 end |
|
59 |