author | wenzelm |
Sat, 17 Oct 2009 14:43:18 +0200 | |
changeset 32960 | 69916a850301 |
parent 24894 | 163c82d039cf |
child 35068 | 544867142ea4 |
permissions | -rw-r--r-- |
12560 | 1 |
(* Title: ZF/Induct/Comb.thy |
12088 | 2 |
Author: Lawrence C Paulson |
3 |
Copyright 1994 University of Cambridge |
|
4 |
*) |
|
5 |
||
12610 | 6 |
header {* Combinatory Logic example: the Church-Rosser Theorem *} |
12088 | 7 |
|
16417 | 8 |
theory Comb imports Main begin |
12088 | 9 |
|
12610 | 10 |
text {* |
11 |
Curiously, combinators do not include free variables. |
|
12 |
||
13 |
Example taken from \cite{camilleri-melham}. |
|
14 |
*} |
|
15 |
||
16 |
subsection {* Definitions *} |
|
17 |
||
18 |
text {* Datatype definition of combinators @{text S} and @{text K}. *} |
|
12088 | 19 |
|
12610 | 20 |
consts comb :: i |
21 |
datatype comb = |
|
22 |
K |
|
23 |
| S |
|
15775 | 24 |
| app ("p \<in> comb", "q \<in> comb") (infixl "@@" 90) |
12610 | 25 |
|
26 |
text {* |
|
27 |
Inductive definition of contractions, @{text "-1->"} and |
|
28 |
(multi-step) reductions, @{text "--->"}. |
|
29 |
*} |
|
30 |
||
12088 | 31 |
consts |
12610 | 32 |
contract :: i |
33 |
syntax |
|
15775 | 34 |
"_contract" :: "[i,i] => o" (infixl "-1->" 50) |
12610 | 35 |
"_contract_multi" :: "[i,i] => o" (infixl "--->" 50) |
12088 | 36 |
translations |
12560 | 37 |
"p -1-> q" == "<p,q> \<in> contract" |
38 |
"p ---> q" == "<p,q> \<in> contract^*" |
|
12088 | 39 |
|
15775 | 40 |
syntax (xsymbols) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24894
diff
changeset
|
41 |
"comb.app" :: "[i, i] => i" (infixl "\<bullet>" 90) |
15775 | 42 |
|
12088 | 43 |
inductive |
12610 | 44 |
domains "contract" \<subseteq> "comb \<times> comb" |
12560 | 45 |
intros |
15775 | 46 |
K: "[| p \<in> comb; q \<in> comb |] ==> K\<bullet>p\<bullet>q -1-> p" |
47 |
S: "[| p \<in> comb; q \<in> comb; r \<in> comb |] ==> S\<bullet>p\<bullet>q\<bullet>r -1-> (p\<bullet>r)\<bullet>(q\<bullet>r)" |
|
48 |
Ap1: "[| p-1->q; r \<in> comb |] ==> p\<bullet>r -1-> q\<bullet>r" |
|
49 |
Ap2: "[| p-1->q; r \<in> comb |] ==> r\<bullet>p -1-> r\<bullet>q" |
|
12610 | 50 |
type_intros comb.intros |
12088 | 51 |
|
12610 | 52 |
text {* |
53 |
Inductive definition of parallel contractions, @{text "=1=>"} and |
|
54 |
(multi-step) parallel reductions, @{text "===>"}. |
|
55 |
*} |
|
56 |
||
12088 | 57 |
consts |
12610 | 58 |
parcontract :: i |
59 |
syntax |
|
60 |
"_parcontract" :: "[i,i] => o" (infixl "=1=>" 50) |
|
61 |
"_parcontract_multi" :: "[i,i] => o" (infixl "===>" 50) |
|
12088 | 62 |
translations |
12560 | 63 |
"p =1=> q" == "<p,q> \<in> parcontract" |
64 |
"p ===> q" == "<p,q> \<in> parcontract^+" |
|
12088 | 65 |
|
66 |
inductive |
|
12610 | 67 |
domains "parcontract" \<subseteq> "comb \<times> comb" |
12560 | 68 |
intros |
12610 | 69 |
refl: "[| p \<in> comb |] ==> p =1=> p" |
15775 | 70 |
K: "[| p \<in> comb; q \<in> comb |] ==> K\<bullet>p\<bullet>q =1=> p" |
71 |
S: "[| p \<in> comb; q \<in> comb; r \<in> comb |] ==> S\<bullet>p\<bullet>q\<bullet>r =1=> (p\<bullet>r)\<bullet>(q\<bullet>r)" |
|
72 |
Ap: "[| p=1=>q; r=1=>s |] ==> p\<bullet>r =1=> q\<bullet>s" |
|
12610 | 73 |
type_intros comb.intros |
12088 | 74 |
|
12610 | 75 |
text {* |
76 |
Misc definitions. |
|
77 |
*} |
|
12088 | 78 |
|
24894 | 79 |
definition |
80 |
I :: i where |
|
15775 | 81 |
"I == S\<bullet>K\<bullet>K" |
12088 | 82 |
|
24894 | 83 |
definition |
84 |
diamond :: "i => o" where |
|
12610 | 85 |
"diamond(r) == |
86 |
\<forall>x y. <x,y>\<in>r --> (\<forall>y'. <x,y'>\<in>r --> (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))" |
|
12560 | 87 |
|
88 |
||
12610 | 89 |
subsection {* Transitive closure preserves the Church-Rosser property *} |
12560 | 90 |
|
91 |
lemma diamond_strip_lemmaD [rule_format]: |
|
12610 | 92 |
"[| diamond(r); <x,y>:r^+ |] ==> |
93 |
\<forall>y'. <x,y'>:r --> (\<exists>z. <y',z>: r^+ & <y,z>: r)" |
|
94 |
apply (unfold diamond_def) |
|
95 |
apply (erule trancl_induct) |
|
96 |
apply (blast intro: r_into_trancl) |
|
97 |
apply clarify |
|
98 |
apply (drule spec [THEN mp], assumption) |
|
99 |
apply (blast intro: r_into_trancl trans_trancl [THEN transD]) |
|
100 |
done |
|
12560 | 101 |
|
102 |
lemma diamond_trancl: "diamond(r) ==> diamond(r^+)" |
|
12610 | 103 |
apply (simp (no_asm_simp) add: diamond_def) |
104 |
apply (rule impI [THEN allI, THEN allI]) |
|
105 |
apply (erule trancl_induct) |
|
106 |
apply auto |
|
107 |
apply (best intro: r_into_trancl trans_trancl [THEN transD] |
|
108 |
dest: diamond_strip_lemmaD)+ |
|
109 |
done |
|
12560 | 110 |
|
15775 | 111 |
inductive_cases Ap_E [elim!]: "p\<bullet>q \<in> comb" |
12560 | 112 |
|
113 |
declare comb.intros [intro!] |
|
114 |
||
115 |
||
12610 | 116 |
subsection {* Results about Contraction *} |
12560 | 117 |
|
12610 | 118 |
text {* |
119 |
For type checking: replaces @{term "a -1-> b"} by @{text "a, b \<in> |
|
120 |
comb"}. |
|
121 |
*} |
|
122 |
||
12560 | 123 |
lemmas contract_combE2 = contract.dom_subset [THEN subsetD, THEN SigmaE2] |
12610 | 124 |
and contract_combD1 = contract.dom_subset [THEN subsetD, THEN SigmaD1] |
125 |
and contract_combD2 = contract.dom_subset [THEN subsetD, THEN SigmaD2] |
|
12560 | 126 |
|
127 |
lemma field_contract_eq: "field(contract) = comb" |
|
12610 | 128 |
by (blast intro: contract.K elim!: contract_combE2) |
12560 | 129 |
|
12610 | 130 |
lemmas reduction_refl = |
131 |
field_contract_eq [THEN equalityD2, THEN subsetD, THEN rtrancl_refl] |
|
12560 | 132 |
|
12610 | 133 |
lemmas rtrancl_into_rtrancl2 = |
134 |
r_into_rtrancl [THEN trans_rtrancl [THEN transD]] |
|
12560 | 135 |
|
136 |
declare reduction_refl [intro!] contract.K [intro!] contract.S [intro!] |
|
137 |
||
12610 | 138 |
lemmas reduction_rls = |
139 |
contract.K [THEN rtrancl_into_rtrancl2] |
|
140 |
contract.S [THEN rtrancl_into_rtrancl2] |
|
141 |
contract.Ap1 [THEN rtrancl_into_rtrancl2] |
|
142 |
contract.Ap2 [THEN rtrancl_into_rtrancl2] |
|
12560 | 143 |
|
15775 | 144 |
lemma "p \<in> comb ==> I\<bullet>p ---> p" |
12610 | 145 |
-- {* Example only: not used *} |
146 |
by (unfold I_def) (blast intro: reduction_rls) |
|
12560 | 147 |
|
148 |
lemma comb_I: "I \<in> comb" |
|
12610 | 149 |
by (unfold I_def) blast |
12560 | 150 |
|
12610 | 151 |
|
152 |
subsection {* Non-contraction results *} |
|
12560 | 153 |
|
12610 | 154 |
text {* Derive a case for each combinator constructor. *} |
155 |
||
156 |
inductive_cases |
|
157 |
K_contractE [elim!]: "K -1-> r" |
|
158 |
and S_contractE [elim!]: "S -1-> r" |
|
15775 | 159 |
and Ap_contractE [elim!]: "p\<bullet>q -1-> r" |
12560 | 160 |
|
161 |
lemma I_contract_E: "I -1-> r ==> P" |
|
12610 | 162 |
by (auto simp add: I_def) |
12560 | 163 |
|
15775 | 164 |
lemma K1_contractD: "K\<bullet>p -1-> r ==> (\<exists>q. r = K\<bullet>q & p -1-> q)" |
12610 | 165 |
by auto |
12560 | 166 |
|
15775 | 167 |
lemma Ap_reduce1: "[| p ---> q; r \<in> comb |] ==> p\<bullet>r ---> q\<bullet>r" |
12610 | 168 |
apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1]) |
169 |
apply (drule field_contract_eq [THEN equalityD1, THEN subsetD]) |
|
170 |
apply (erule rtrancl_induct) |
|
171 |
apply (blast intro: reduction_rls) |
|
172 |
apply (erule trans_rtrancl [THEN transD]) |
|
173 |
apply (blast intro: contract_combD2 reduction_rls) |
|
174 |
done |
|
12560 | 175 |
|
15775 | 176 |
lemma Ap_reduce2: "[| p ---> q; r \<in> comb |] ==> r\<bullet>p ---> r\<bullet>q" |
12610 | 177 |
apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1]) |
178 |
apply (drule field_contract_eq [THEN equalityD1, THEN subsetD]) |
|
179 |
apply (erule rtrancl_induct) |
|
180 |
apply (blast intro: reduction_rls) |
|
13573 | 181 |
apply (blast intro: trans_rtrancl [THEN transD] |
182 |
contract_combD2 reduction_rls) |
|
12610 | 183 |
done |
12560 | 184 |
|
12610 | 185 |
text {* Counterexample to the diamond property for @{text "-1->"}. *} |
12560 | 186 |
|
15775 | 187 |
lemma KIII_contract1: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> I" |
12610 | 188 |
by (blast intro: comb.intros contract.K comb_I) |
12560 | 189 |
|
15775 | 190 |
lemma KIII_contract2: "K\<bullet>I\<bullet>(I\<bullet>I) -1-> K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I))" |
12610 | 191 |
by (unfold I_def) (blast intro: comb.intros contract.intros) |
12560 | 192 |
|
15775 | 193 |
lemma KIII_contract3: "K\<bullet>I\<bullet>((K\<bullet>I)\<bullet>(K\<bullet>I)) -1-> I" |
12610 | 194 |
by (blast intro: comb.intros contract.K comb_I) |
12560 | 195 |
|
12610 | 196 |
lemma not_diamond_contract: "\<not> diamond(contract)" |
197 |
apply (unfold diamond_def) |
|
198 |
apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3 |
|
199 |
elim!: I_contract_E) |
|
200 |
done |
|
12560 | 201 |
|
202 |
||
12610 | 203 |
subsection {* Results about Parallel Contraction *} |
12560 | 204 |
|
12610 | 205 |
text {* For type checking: replaces @{text "a =1=> b"} by @{text "a, b |
206 |
\<in> comb"} *} |
|
12560 | 207 |
lemmas parcontract_combE2 = parcontract.dom_subset [THEN subsetD, THEN SigmaE2] |
12610 | 208 |
and parcontract_combD1 = parcontract.dom_subset [THEN subsetD, THEN SigmaD1] |
209 |
and parcontract_combD2 = parcontract.dom_subset [THEN subsetD, THEN SigmaD2] |
|
12560 | 210 |
|
211 |
lemma field_parcontract_eq: "field(parcontract) = comb" |
|
12610 | 212 |
by (blast intro: parcontract.K elim!: parcontract_combE2) |
12560 | 213 |
|
12610 | 214 |
text {* Derive a case for each combinator constructor. *} |
215 |
inductive_cases |
|
216 |
K_parcontractE [elim!]: "K =1=> r" |
|
217 |
and S_parcontractE [elim!]: "S =1=> r" |
|
15775 | 218 |
and Ap_parcontractE [elim!]: "p\<bullet>q =1=> r" |
12560 | 219 |
|
220 |
declare parcontract.intros [intro] |
|
221 |
||
222 |
||
12610 | 223 |
subsection {* Basic properties of parallel contraction *} |
12560 | 224 |
|
12610 | 225 |
lemma K1_parcontractD [dest!]: |
15775 | 226 |
"K\<bullet>p =1=> r ==> (\<exists>p'. r = K\<bullet>p' & p =1=> p')" |
12610 | 227 |
by auto |
12560 | 228 |
|
12610 | 229 |
lemma S1_parcontractD [dest!]: |
15775 | 230 |
"S\<bullet>p =1=> r ==> (\<exists>p'. r = S\<bullet>p' & p =1=> p')" |
12610 | 231 |
by auto |
12560 | 232 |
|
233 |
lemma S2_parcontractD [dest!]: |
|
15775 | 234 |
"S\<bullet>p\<bullet>q =1=> r ==> (\<exists>p' q'. r = S\<bullet>p'\<bullet>q' & p =1=> p' & q =1=> q')" |
12610 | 235 |
by auto |
12560 | 236 |
|
237 |
lemma diamond_parcontract: "diamond(parcontract)" |
|
12610 | 238 |
-- {* Church-Rosser property for parallel contraction *} |
239 |
apply (unfold diamond_def) |
|
240 |
apply (rule impI [THEN allI, THEN allI]) |
|
241 |
apply (erule parcontract.induct) |
|
242 |
apply (blast elim!: comb.free_elims intro: parcontract_combD2)+ |
|
243 |
done |
|
12560 | 244 |
|
12610 | 245 |
text {* |
246 |
\medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}. |
|
247 |
*} |
|
12560 | 248 |
|
249 |
lemma contract_imp_parcontract: "p-1->q ==> p=1=>q" |
|
18415 | 250 |
by (induct set: contract) auto |
12560 | 251 |
|
252 |
lemma reduce_imp_parreduce: "p--->q ==> p===>q" |
|
12610 | 253 |
apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1]) |
254 |
apply (drule field_contract_eq [THEN equalityD1, THEN subsetD]) |
|
255 |
apply (erule rtrancl_induct) |
|
256 |
apply (blast intro: r_into_trancl) |
|
257 |
apply (blast intro: contract_imp_parcontract r_into_trancl |
|
258 |
trans_trancl [THEN transD]) |
|
259 |
done |
|
12560 | 260 |
|
261 |
lemma parcontract_imp_reduce: "p=1=>q ==> p--->q" |
|
18415 | 262 |
apply (induct set: parcontract) |
12610 | 263 |
apply (blast intro: reduction_rls) |
264 |
apply (blast intro: reduction_rls) |
|
12560 | 265 |
apply (blast intro: reduction_rls) |
12610 | 266 |
apply (blast intro: trans_rtrancl [THEN transD] |
267 |
Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2) |
|
268 |
done |
|
12560 | 269 |
|
270 |
lemma parreduce_imp_reduce: "p===>q ==> p--->q" |
|
12610 | 271 |
apply (frule trancl_type [THEN subsetD, THEN SigmaD1]) |
272 |
apply (drule field_parcontract_eq [THEN equalityD1, THEN subsetD]) |
|
273 |
apply (erule trancl_induct, erule parcontract_imp_reduce) |
|
274 |
apply (erule trans_rtrancl [THEN transD]) |
|
275 |
apply (erule parcontract_imp_reduce) |
|
276 |
done |
|
12560 | 277 |
|
278 |
lemma parreduce_iff_reduce: "p===>q <-> p--->q" |
|
12610 | 279 |
by (blast intro: parreduce_imp_reduce reduce_imp_parreduce) |
12088 | 280 |
|
281 |
end |