18 (** Datatype definition of combinators S and K, with infixed application **) |
18 (** Datatype definition of combinators S and K, with infixed application **) |
19 consts comb :: i |
19 consts comb :: i |
20 datatype |
20 datatype |
21 "comb" = K |
21 "comb" = K |
22 | S |
22 | S |
23 | "#" ("p: comb", "q: comb") (infixl 90) |
23 | "#" ("p \\<in> comb", "q \\<in> comb") (infixl 90) |
24 |
24 |
25 (** Inductive definition of contractions, -1-> |
25 (** Inductive definition of contractions, -1-> |
26 and (multi-step) reductions, ---> |
26 and (multi-step) reductions, ---> |
27 **) |
27 **) |
28 consts |
28 consts |
29 contract :: i |
29 contract :: i |
30 "-1->" :: [i,i] => o (infixl 50) |
30 "-1->" :: [i,i] => o (infixl 50) |
31 "--->" :: [i,i] => o (infixl 50) |
31 "--->" :: [i,i] => o (infixl 50) |
32 |
32 |
33 translations |
33 translations |
34 "p -1-> q" == "<p,q> : contract" |
34 "p -1-> q" == "<p,q> \\<in> contract" |
35 "p ---> q" == "<p,q> : contract^*" |
35 "p ---> q" == "<p,q> \\<in> contract^*" |
36 |
36 |
37 inductive |
37 inductive |
38 domains "contract" <= "comb*comb" |
38 domains "contract" <= "comb*comb" |
39 intrs |
39 intrs |
40 K "[| p:comb; q:comb |] ==> K#p#q -1-> p" |
40 K "[| p \\<in> comb; q \\<in> comb |] ==> K#p#q -1-> p" |
41 S "[| p:comb; q:comb; r:comb |] ==> S#p#q#r -1-> (p#r)#(q#r)" |
41 S "[| p \\<in> comb; q \\<in> comb; r \\<in> comb |] ==> S#p#q#r -1-> (p#r)#(q#r)" |
42 Ap1 "[| p-1->q; r:comb |] ==> p#r -1-> q#r" |
42 Ap1 "[| p-1->q; r \\<in> comb |] ==> p#r -1-> q#r" |
43 Ap2 "[| p-1->q; r:comb |] ==> r#p -1-> r#q" |
43 Ap2 "[| p-1->q; r \\<in> comb |] ==> r#p -1-> r#q" |
44 type_intrs "comb.intrs" |
44 type_intrs "comb.intrs" |
45 |
45 |
46 |
46 |
47 (** Inductive definition of parallel contractions, =1=> |
47 (** Inductive definition of parallel contractions, =1=> |
48 and (multi-step) parallel reductions, ===> |
48 and (multi-step) parallel reductions, ===> |
51 parcontract :: i |
51 parcontract :: i |
52 "=1=>" :: [i,i] => o (infixl 50) |
52 "=1=>" :: [i,i] => o (infixl 50) |
53 "===>" :: [i,i] => o (infixl 50) |
53 "===>" :: [i,i] => o (infixl 50) |
54 |
54 |
55 translations |
55 translations |
56 "p =1=> q" == "<p,q> : parcontract" |
56 "p =1=> q" == "<p,q> \\<in> parcontract" |
57 "p ===> q" == "<p,q> : parcontract^+" |
57 "p ===> q" == "<p,q> \\<in> parcontract^+" |
58 |
58 |
59 inductive |
59 inductive |
60 domains "parcontract" <= "comb*comb" |
60 domains "parcontract" <= "comb*comb" |
61 intrs |
61 intrs |
62 refl "[| p:comb |] ==> p =1=> p" |
62 refl "[| p \\<in> comb |] ==> p =1=> p" |
63 K "[| p:comb; q:comb |] ==> K#p#q =1=> p" |
63 K "[| p \\<in> comb; q \\<in> comb |] ==> K#p#q =1=> p" |
64 S "[| p:comb; q:comb; r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)" |
64 S "[| p \\<in> comb; q \\<in> comb; r \\<in> comb |] ==> S#p#q#r =1=> (p#r)#(q#r)" |
65 Ap "[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s" |
65 Ap "[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s" |
66 type_intrs "comb.intrs" |
66 type_intrs "comb.intrs" |
67 |
67 |
68 |
68 |
69 (*Misc definitions*) |
69 (*Misc definitions*) |
70 constdefs |
70 constdefs |
71 I :: i |
71 I :: i |
72 "I == S#K#K" |
72 "I == S#K#K" |
73 |
73 |
74 diamond :: i => o |
74 diamond :: i => o |
75 "diamond(r) == ALL x y. <x,y>:r --> |
75 "diamond(r) == \\<forall>x y. <x,y>:r --> |
76 (ALL y'. <x,y'>:r --> |
76 (\\<forall>y'. <x,y'>:r --> |
77 (EX z. <y,z>:r & <y',z> : r))" |
77 (\\<exists>z. <y,z>:r & <y',z> \\<in> r))" |
78 |
78 |
79 end |
79 end |