21 |
21 |
22 text {* Datatype definition of combinators @{text S} and @{text K}. *} |
22 text {* Datatype definition of combinators @{text S} and @{text K}. *} |
23 |
23 |
24 datatype comb = K |
24 datatype comb = K |
25 | S |
25 | S |
26 | "##" comb comb (infixl 90) |
26 | Ap comb comb (infixl "##" 90) |
|
27 |
|
28 const_syntax (xsymbols) |
|
29 Ap (infixl "\<bullet>" 90) |
|
30 |
27 |
31 |
28 text {* |
32 text {* |
29 Inductive definition of contractions, @{text "-1->"} and |
33 Inductive definition of contractions, @{text "-1->"} and |
30 (multi-step) reductions, @{text "--->"}. |
34 (multi-step) reductions, @{text "--->"}. |
31 *} |
35 *} |
32 |
36 |
33 consts |
37 consts |
34 contract :: "(comb*comb) set" |
38 contract :: "(comb*comb) set" |
35 "-1->" :: "[comb,comb] => bool" (infixl 50) |
39 |
36 "--->" :: "[comb,comb] => bool" (infixl 50) |
40 abbreviation |
37 |
41 contract_rel1 :: "[comb,comb] => bool" (infixl "-1->" 50) |
38 translations |
42 "x -1-> y == (x,y) \<in> contract" |
39 "x -1-> y" == "(x,y) \<in> contract" |
43 contract_rel :: "[comb,comb] => bool" (infixl "--->" 50) |
40 "x ---> y" == "(x,y) \<in> contract^*" |
44 "x ---> y == (x,y) \<in> contract^*" |
41 |
|
42 syntax (xsymbols) |
|
43 "op ##" :: "[comb,comb] => comb" (infixl "\<bullet>" 90) |
|
44 |
45 |
45 inductive contract |
46 inductive contract |
46 intros |
47 intros |
47 K: "K##x##y -1-> x" |
48 K: "K##x##y -1-> x" |
48 S: "S##x##y##z -1-> (x##z)##(y##z)" |
49 S: "S##x##y##z -1-> (x##z)##(y##z)" |
54 (multi-step) parallel reductions, @{text "===>"}. |
55 (multi-step) parallel reductions, @{text "===>"}. |
55 *} |
56 *} |
56 |
57 |
57 consts |
58 consts |
58 parcontract :: "(comb*comb) set" |
59 parcontract :: "(comb*comb) set" |
59 "=1=>" :: "[comb,comb] => bool" (infixl 50) |
60 |
60 "===>" :: "[comb,comb] => bool" (infixl 50) |
61 abbreviation |
61 |
62 parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50) |
62 translations |
63 "x =1=> y == (x,y) \<in> parcontract" |
63 "x =1=> y" == "(x,y) \<in> parcontract" |
64 parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50) |
64 "x ===> y" == "(x,y) \<in> parcontract^*" |
65 "x ===> y == (x,y) \<in> parcontract^*" |
65 |
66 |
66 inductive parcontract |
67 inductive parcontract |
67 intros |
68 intros |
68 refl: "x =1=> x" |
69 refl: "x =1=> x" |
69 K: "K##x##y =1=> x" |
70 K: "K##x##y =1=> x" |
72 |
73 |
73 text {* |
74 text {* |
74 Misc definitions. |
75 Misc definitions. |
75 *} |
76 *} |
76 |
77 |
77 constdefs |
78 definition |
78 I :: comb |
79 I :: comb |
79 "I == S##K##K" |
80 "I = S##K##K" |
80 |
81 |
81 diamond :: "('a * 'a)set => bool" |
82 diamond :: "('a * 'a)set => bool" |
82 --{*confluence; Lambda/Commutation treats this more abstractly*} |
83 --{*confluence; Lambda/Commutation treats this more abstractly*} |
83 "diamond(r) == \<forall>x y. (x,y) \<in> r --> |
84 "diamond(r) = (\<forall>x y. (x,y) \<in> r --> |
84 (\<forall>y'. (x,y') \<in> r --> |
85 (\<forall>y'. (x,y') \<in> r --> |
85 (\<exists>z. (y,z) \<in> r & (y',z) \<in> r))" |
86 (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))" |
86 |
87 |
87 |
88 |
88 subsection {*Reflexive/Transitive closure preserves Church-Rosser property*} |
89 subsection {*Reflexive/Transitive closure preserves Church-Rosser property*} |
89 |
90 |
90 text{*So does the Transitive closure, with a similar proof*} |
91 text{*So does the Transitive closure, with a similar proof*} |