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