14 | Fun ("t: redexes") |
14 | Fun ("t: redexes") |
15 | App ("b:bool" ,"f:redexes" , "a:redexes") |
15 | App ("b:bool" ,"f:redexes" , "a:redexes") |
16 type_intrs "[bool_into_univ]" |
16 type_intrs "[bool_into_univ]" |
17 |
17 |
18 |
18 |
|
19 |
19 consts |
20 consts |
20 redex_rec :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i |
21 Ssub,Scomp,Sreg :: i |
21 |
22 "<==","~" :: [i,i]=>o (infixl 70) |
|
23 un :: [i,i]=>i (infixl 70) |
|
24 union_aux :: i=>i |
|
25 regular :: i=>o |
|
26 |
|
27 primrec (*explicit lambda is required because both arguments of "un" vary*) |
|
28 "union_aux(Var(n)) = |
|
29 (lam t:redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))" |
|
30 |
|
31 "union_aux(Fun(u)) = |
|
32 (lam t:redexes. redexes_case(%j. 0, %y. Fun(u un y), |
|
33 %b y z. 0, t))" |
|
34 |
|
35 "union_aux(App(b,f,a)) = |
|
36 (lam t:redexes. |
|
37 redexes_case(%j. 0, %y. 0, |
|
38 %c z u. App(b or c, f un z, a un u), t))" |
|
39 |
22 defs |
40 defs |
23 redex_rec_def |
41 union_def "u un v == union_aux(u)`v" |
24 "redex_rec(p,b,c,d) == |
42 |
25 Vrec(p, %p g. redexes_case(b, %x. c(x,g`x), |
43 |
26 %n x y. d(n, x, y, g`x, g`y), p))" |
44 translations |
|
45 "a<==b" == "<a,b>:Ssub" |
|
46 "a ~ b" == "<a,b>:Scomp" |
|
47 "regular(a)" == "a:Sreg" |
|
48 |
|
49 inductive |
|
50 domains "Ssub" <= "redexes*redexes" |
|
51 intrs |
|
52 Sub_Var "n:nat ==> Var(n)<== Var(n)" |
|
53 Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)" |
|
54 Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==> |
|
55 App(0,u1,u2)<== App(b,v1,v2)" |
|
56 Sub_App2 "[|u1<== v1; u2<== v2|]==> |
|
57 App(1,u1,u2)<== App(1,v1,v2)" |
|
58 type_intrs "redexes.intrs@bool_typechecks" |
|
59 |
|
60 inductive |
|
61 domains "Scomp" <= "redexes*redexes" |
|
62 intrs |
|
63 Comp_Var "n:nat ==> Var(n) ~ Var(n)" |
|
64 Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)" |
|
65 Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==> |
|
66 App(b1,u1,u2) ~ App(b2,v1,v2)" |
|
67 type_intrs "redexes.intrs@bool_typechecks" |
|
68 |
|
69 inductive |
|
70 domains "Sreg" <= "redexes" |
|
71 intrs |
|
72 Reg_Var "n:nat ==> regular(Var(n))" |
|
73 Reg_Fun "[|regular(u)|]==> regular(Fun(u))" |
|
74 Reg_App1 "[|regular(Fun(u)); regular(v) |
|
75 |]==>regular(App(1,Fun(u),v))" |
|
76 Reg_App2 "[|regular(u); regular(v) |
|
77 |]==>regular(App(0,u,v))" |
|
78 type_intrs "redexes.intrs@bool_typechecks" |
|
79 |
|
80 |
27 end |
81 end |
28 |
82 |