1 (* Title: HOL/Induct/Comb.thy |
1 (* Title: HOL/Induct/Comb.thy |
2 Author: Lawrence C Paulson |
2 Author: Lawrence C Paulson |
3 Copyright 1996 University of Cambridge |
3 Copyright 1996 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section {* Combinatory Logic example: the Church-Rosser Theorem *} |
6 section \<open>Combinatory Logic example: the Church-Rosser Theorem\<close> |
7 |
7 |
8 theory Comb imports Main begin |
8 theory Comb imports Main begin |
9 |
9 |
10 text {* |
10 text \<open> |
11 Curiously, combinators do not include free variables. |
11 Curiously, combinators do not include free variables. |
12 |
12 |
13 Example taken from @{cite camilleri92}. |
13 Example taken from @{cite camilleri92}. |
14 |
14 |
15 HOL system proofs may be found in the HOL distribution at |
15 HOL system proofs may be found in the HOL distribution at |
16 .../contrib/rule-induction/cl.ml |
16 .../contrib/rule-induction/cl.ml |
17 *} |
17 \<close> |
18 |
18 |
19 subsection {* Definitions *} |
19 subsection \<open>Definitions\<close> |
20 |
20 |
21 text {* Datatype definition of combinators @{text S} and @{text K}. *} |
21 text \<open>Datatype definition of combinators @{text S} and @{text K}.\<close> |
22 |
22 |
23 datatype comb = K |
23 datatype comb = K |
24 | S |
24 | S |
25 | Ap comb comb (infixl "##" 90) |
25 | Ap comb comb (infixl "##" 90) |
26 |
26 |
27 notation (xsymbols) |
27 notation (xsymbols) |
28 Ap (infixl "\<bullet>" 90) |
28 Ap (infixl "\<bullet>" 90) |
29 |
29 |
30 |
30 |
31 text {* |
31 text \<open> |
32 Inductive definition of contractions, @{text "-1->"} and |
32 Inductive definition of contractions, @{text "-1->"} and |
33 (multi-step) reductions, @{text "--->"}. |
33 (multi-step) reductions, @{text "--->"}. |
34 *} |
34 \<close> |
35 |
35 |
36 inductive_set |
36 inductive_set |
37 contract :: "(comb*comb) set" |
37 contract :: "(comb*comb) set" |
38 and contract_rel1 :: "[comb,comb] => bool" (infixl "-1->" 50) |
38 and contract_rel1 :: "[comb,comb] => bool" (infixl "-1->" 50) |
39 where |
39 where |
45 |
45 |
46 abbreviation |
46 abbreviation |
47 contract_rel :: "[comb,comb] => bool" (infixl "--->" 50) where |
47 contract_rel :: "[comb,comb] => bool" (infixl "--->" 50) where |
48 "x ---> y == (x,y) \<in> contract^*" |
48 "x ---> y == (x,y) \<in> contract^*" |
49 |
49 |
50 text {* |
50 text \<open> |
51 Inductive definition of parallel contractions, @{text "=1=>"} and |
51 Inductive definition of parallel contractions, @{text "=1=>"} and |
52 (multi-step) parallel reductions, @{text "===>"}. |
52 (multi-step) parallel reductions, @{text "===>"}. |
53 *} |
53 \<close> |
54 |
54 |
55 inductive_set |
55 inductive_set |
56 parcontract :: "(comb*comb) set" |
56 parcontract :: "(comb*comb) set" |
57 and parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50) |
57 and parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50) |
58 where |
58 where |
64 |
64 |
65 abbreviation |
65 abbreviation |
66 parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50) where |
66 parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50) where |
67 "x ===> y == (x,y) \<in> parcontract^*" |
67 "x ===> y == (x,y) \<in> parcontract^*" |
68 |
68 |
69 text {* |
69 text \<open> |
70 Misc definitions. |
70 Misc definitions. |
71 *} |
71 \<close> |
72 |
72 |
73 definition |
73 definition |
74 I :: comb where |
74 I :: comb where |
75 "I = S##K##K" |
75 "I = S##K##K" |
76 |
76 |
77 definition |
77 definition |
78 diamond :: "('a * 'a)set => bool" where |
78 diamond :: "('a * 'a)set => bool" where |
79 --{*confluence; Lambda/Commutation treats this more abstractly*} |
79 --\<open>confluence; Lambda/Commutation treats this more abstractly\<close> |
80 "diamond(r) = (\<forall>x y. (x,y) \<in> r --> |
80 "diamond(r) = (\<forall>x y. (x,y) \<in> r --> |
81 (\<forall>y'. (x,y') \<in> r --> |
81 (\<forall>y'. (x,y') \<in> r --> |
82 (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))" |
82 (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))" |
83 |
83 |
84 |
84 |
85 subsection {*Reflexive/Transitive closure preserves Church-Rosser property*} |
85 subsection \<open>Reflexive/Transitive closure preserves Church-Rosser property\<close> |
86 |
86 |
87 text{*So does the Transitive closure, with a similar proof*} |
87 text\<open>So does the Transitive closure, with a similar proof\<close> |
88 |
88 |
89 text{*Strip lemma. |
89 text\<open>Strip lemma. |
90 The induction hypothesis covers all but the last diamond of the strip.*} |
90 The induction hypothesis covers all but the last diamond of the strip.\<close> |
91 lemma diamond_strip_lemmaE [rule_format]: |
91 lemma diamond_strip_lemmaE [rule_format]: |
92 "[| diamond(r); (x,y) \<in> r^* |] ==> |
92 "[| diamond(r); (x,y) \<in> r^* |] ==> |
93 \<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)" |
93 \<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)" |
94 apply (unfold diamond_def) |
94 apply (unfold diamond_def) |
95 apply (erule rtrancl_induct) |
95 apply (erule rtrancl_induct) |
103 apply (erule rtrancl_induct, blast) |
103 apply (erule rtrancl_induct, blast) |
104 apply (meson rtrancl_trans r_into_rtrancl diamond_strip_lemmaE) |
104 apply (meson rtrancl_trans r_into_rtrancl diamond_strip_lemmaE) |
105 done |
105 done |
106 |
106 |
107 |
107 |
108 subsection {* Non-contraction results *} |
108 subsection \<open>Non-contraction results\<close> |
109 |
109 |
110 text {* Derive a case for each combinator constructor. *} |
110 text \<open>Derive a case for each combinator constructor.\<close> |
111 |
111 |
112 inductive_cases |
112 inductive_cases |
113 K_contractE [elim!]: "K -1-> r" |
113 K_contractE [elim!]: "K -1-> r" |
114 and S_contractE [elim!]: "S -1-> r" |
114 and S_contractE [elim!]: "S -1-> r" |
115 and Ap_contractE [elim!]: "p##q -1-> r" |
115 and Ap_contractE [elim!]: "p##q -1-> r" |
131 lemma Ap_reduce2 [intro]: "x ---> y ==> z##x ---> z##y" |
131 lemma Ap_reduce2 [intro]: "x ---> y ==> z##x ---> z##y" |
132 apply (erule rtrancl_induct) |
132 apply (erule rtrancl_induct) |
133 apply (blast intro: rtrancl_trans)+ |
133 apply (blast intro: rtrancl_trans)+ |
134 done |
134 done |
135 |
135 |
136 text {*Counterexample to the diamond property for @{term "x -1-> y"}*} |
136 text \<open>Counterexample to the diamond property for @{term "x -1-> y"}\<close> |
137 |
137 |
138 lemma not_diamond_contract: "~ diamond(contract)" |
138 lemma not_diamond_contract: "~ diamond(contract)" |
139 by (unfold diamond_def, metis S_contractE contract.K) |
139 by (unfold diamond_def, metis S_contractE contract.K) |
140 |
140 |
141 |
141 |
142 subsection {* Results about Parallel Contraction *} |
142 subsection \<open>Results about Parallel Contraction\<close> |
143 |
143 |
144 text {* Derive a case for each combinator constructor. *} |
144 text \<open>Derive a case for each combinator constructor.\<close> |
145 |
145 |
146 inductive_cases |
146 inductive_cases |
147 K_parcontractE [elim!]: "K =1=> r" |
147 K_parcontractE [elim!]: "K =1=> r" |
148 and S_parcontractE [elim!]: "S =1=> r" |
148 and S_parcontractE [elim!]: "S =1=> r" |
149 and Ap_parcontractE [elim!]: "p##q =1=> r" |
149 and Ap_parcontractE [elim!]: "p##q =1=> r" |
150 |
150 |
151 declare parcontract.intros [intro] |
151 declare parcontract.intros [intro] |
152 |
152 |
153 (*** Basic properties of parallel contraction ***) |
153 (*** Basic properties of parallel contraction ***) |
154 |
154 |
155 subsection {* Basic properties of parallel contraction *} |
155 subsection \<open>Basic properties of parallel contraction\<close> |
156 |
156 |
157 lemma K1_parcontractD [dest!]: "K##x =1=> z ==> (\<exists>x'. z = K##x' & x =1=> x')" |
157 lemma K1_parcontractD [dest!]: "K##x =1=> z ==> (\<exists>x'. z = K##x' & x =1=> x')" |
158 by blast |
158 by blast |
159 |
159 |
160 lemma S1_parcontractD [dest!]: "S##x =1=> z ==> (\<exists>x'. z = S##x' & x =1=> x')" |
160 lemma S1_parcontractD [dest!]: "S##x =1=> z ==> (\<exists>x'. z = S##x' & x =1=> x')" |
162 |
162 |
163 lemma S2_parcontractD [dest!]: |
163 lemma S2_parcontractD [dest!]: |
164 "S##x##y =1=> z ==> (\<exists>x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')" |
164 "S##x##y =1=> z ==> (\<exists>x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')" |
165 by blast |
165 by blast |
166 |
166 |
167 text{*The rules above are not essential but make proofs much faster*} |
167 text\<open>The rules above are not essential but make proofs much faster\<close> |
168 |
168 |
169 text{*Church-Rosser property for parallel contraction*} |
169 text\<open>Church-Rosser property for parallel contraction\<close> |
170 lemma diamond_parcontract: "diamond parcontract" |
170 lemma diamond_parcontract: "diamond parcontract" |
171 apply (unfold diamond_def) |
171 apply (unfold diamond_def) |
172 apply (rule impI [THEN allI, THEN allI]) |
172 apply (rule impI [THEN allI, THEN allI]) |
173 apply (erule parcontract.induct, fast+) |
173 apply (erule parcontract.induct, fast+) |
174 done |
174 done |
175 |
175 |
176 text {* |
176 text \<open> |
177 \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}. |
177 \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}. |
178 *} |
178 \<close> |
179 |
179 |
180 lemma contract_subset_parcontract: "contract <= parcontract" |
180 lemma contract_subset_parcontract: "contract <= parcontract" |
181 by (auto, erule contract.induct, blast+) |
181 by (auto, erule contract.induct, blast+) |
182 |
182 |
183 text{*Reductions: simply throw together reflexivity, transitivity and |
183 text\<open>Reductions: simply throw together reflexivity, transitivity and |
184 the one-step reductions*} |
184 the one-step reductions\<close> |
185 |
185 |
186 declare r_into_rtrancl [intro] rtrancl_trans [intro] |
186 declare r_into_rtrancl [intro] rtrancl_trans [intro] |
187 |
187 |
188 (*Example only: not used*) |
188 (*Example only: not used*) |
189 lemma reduce_I: "I##x ---> x" |
189 lemma reduce_I: "I##x ---> x" |