23 \<close> |
20 \<close> |
24 |
21 |
25 |
22 |
26 subsection\<open>Ackermann's Function\<close> |
23 subsection\<open>Ackermann's Function\<close> |
27 |
24 |
28 fun ack :: "nat => nat => nat" where |
25 fun ack :: "[nat,nat] \<Rightarrow> nat" where |
29 "ack 0 n = Suc n" | |
26 "ack 0 n = Suc n" |
30 "ack (Suc m) 0 = ack m 1" | |
27 | "ack (Suc m) 0 = ack m 1" |
31 "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)" |
28 | "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)" |
32 |
29 |
33 |
30 |
34 text \<open>PROPERTY A 4\<close> |
31 text \<open>PROPERTY A 4\<close> |
35 |
32 |
36 lemma less_ack2 [iff]: "j < ack i j" |
33 lemma less_ack2 [iff]: "j < ack i j" |
37 by (induct i j rule: ack.induct) simp_all |
34 by (induct i j rule: ack.induct) simp_all |
38 |
35 |
39 |
36 |
40 text \<open>PROPERTY A 5-, the single-step lemma\<close> |
37 text \<open>PROPERTY A 5-, the single-step lemma\<close> |
41 |
38 |
42 lemma ack_less_ack_Suc2 [iff]: "ack i j < ack i (Suc j)" |
39 lemma ack_less_ack_Suc2 [iff]: "ack i j < ack i (Suc j)" |
43 by (induct i j rule: ack.induct) simp_all |
40 by (induct i j rule: ack.induct) simp_all |
44 |
41 |
45 |
42 |
46 text \<open>PROPERTY A 5, monotonicity for \<open><\<close>\<close> |
43 text \<open>PROPERTY A 5, monotonicity for \<open><\<close>\<close> |
47 |
44 |
48 lemma ack_less_mono2: "j < k ==> ack i j < ack i k" |
45 lemma ack_less_mono2: "j < k \<Longrightarrow> ack i j < ack i k" |
49 using lift_Suc_mono_less[where f = "ack i"] |
46 by (simp add: lift_Suc_mono_less) |
50 by (metis ack_less_ack_Suc2) |
|
51 |
47 |
52 |
48 |
53 text \<open>PROPERTY A 5', monotonicity for \<open>\<le>\<close>\<close> |
49 text \<open>PROPERTY A 5', monotonicity for \<open>\<le>\<close>\<close> |
54 |
50 |
55 lemma ack_le_mono2: "j \<le> k ==> ack i j \<le> ack i k" |
51 lemma ack_le_mono2: "j \<le> k \<Longrightarrow> ack i j \<le> ack i k" |
56 apply (simp add: order_le_less) |
52 by (simp add: ack_less_mono2 less_mono_imp_le_mono) |
57 apply (blast intro: ack_less_mono2) |
|
58 done |
|
59 |
53 |
60 |
54 |
61 text \<open>PROPERTY A 6\<close> |
55 text \<open>PROPERTY A 6\<close> |
62 |
56 |
63 lemma ack2_le_ack1 [iff]: "ack i (Suc j) \<le> ack (Suc i) j" |
57 lemma ack2_le_ack1 [iff]: "ack i (Suc j) \<le> ack (Suc i) j" |
64 proof (induct j) |
58 proof (induct j) |
65 case 0 show ?case by simp |
59 case 0 show ?case by simp |
66 next |
60 next |
67 case (Suc j) show ?case |
61 case (Suc j) show ?case |
68 by (auto intro!: ack_le_mono2) |
62 by (metis Suc ack.simps(3) ack_le_mono2 le_trans less_ack2 less_eq_Suc_le) |
69 (metis Suc Suc_leI Suc_lessI less_ack2 linorder_not_less) |
|
70 qed |
63 qed |
71 |
64 |
72 |
65 |
73 text \<open>PROPERTY A 7-, the single-step lemma\<close> |
66 text \<open>PROPERTY A 7-, the single-step lemma\<close> |
74 |
67 |
75 lemma ack_less_ack_Suc1 [iff]: "ack i j < ack (Suc i) j" |
68 lemma ack_less_ack_Suc1 [iff]: "ack i j < ack (Suc i) j" |
76 by (blast intro: ack_less_mono2 less_le_trans) |
69 by (blast intro: ack_less_mono2 less_le_trans) |
77 |
70 |
78 |
71 |
79 text \<open>PROPERTY A 4'? Extra lemma needed for \<^term>\<open>CONSTANT\<close> case, constant functions\<close> |
72 text \<open>PROPERTY A 4'? Extra lemma needed for \<^term>\<open>CONSTANT\<close> case, constant functions\<close> |
80 |
73 |
81 lemma less_ack1 [iff]: "i < ack i j" |
74 lemma less_ack1 [iff]: "i < ack i j" |
82 apply (induct i) |
75 proof (induct i) |
83 apply simp_all |
76 case 0 |
84 apply (blast intro: Suc_leI le_less_trans) |
77 then show ?case |
85 done |
78 by simp |
|
79 next |
|
80 case (Suc i) |
|
81 then show ?case |
|
82 using less_trans_Suc by blast |
|
83 qed |
86 |
84 |
87 |
85 |
88 text \<open>PROPERTY A 8\<close> |
86 text \<open>PROPERTY A 8\<close> |
89 |
87 |
90 lemma ack_1 [simp]: "ack (Suc 0) j = j + 2" |
88 lemma ack_1 [simp]: "ack (Suc 0) j = j + 2" |
91 by (induct j) simp_all |
89 by (induct j) simp_all |
92 |
90 |
93 |
91 |
94 text \<open>PROPERTY A 9. The unary \<open>1\<close> and \<open>2\<close> in \<^term>\<open>ack\<close> is essential for the rewriting.\<close> |
92 text \<open>PROPERTY A 9. The unary \<open>1\<close> and \<open>2\<close> in \<^term>\<open>ack\<close> is essential for the rewriting.\<close> |
95 |
93 |
96 lemma ack_2 [simp]: "ack (Suc (Suc 0)) j = 2 * j + 3" |
94 lemma ack_2 [simp]: "ack (Suc (Suc 0)) j = 2 * j + 3" |
97 by (induct j) simp_all |
95 by (induct j) simp_all |
98 |
96 |
99 |
97 |
100 text \<open>PROPERTY A 7, monotonicity for \<open><\<close> [not clear why |
98 text \<open>PROPERTY A 7, monotonicity for \<open><\<close> [not clear why |
101 @{thm [source] ack_1} is now needed first!]\<close> |
99 @{thm [source] ack_1} is now needed first!]\<close> |
102 |
100 |
103 lemma ack_less_mono1_aux: "ack i k < ack (Suc (i +i')) k" |
101 lemma ack_less_mono1_aux: "ack i k < ack (Suc (i +i')) k" |
104 proof (induct i k rule: ack.induct) |
102 proof (induct i k rule: ack.induct) |
105 case (1 n) show ?case |
103 case (1 n) show ?case |
106 by (simp, metis ack_less_ack_Suc1 less_ack2 less_trans_Suc) |
104 using less_le_trans by auto |
107 next |
105 next |
108 case (2 m) thus ?case by simp |
106 case (2 m) thus ?case by simp |
109 next |
107 next |
110 case (3 m n) thus ?case |
108 case (3 m n) thus ?case |
111 by (simp, blast intro: less_trans ack_less_mono2) |
109 using ack_less_mono2 less_trans by fastforce |
112 qed |
110 qed |
113 |
111 |
114 lemma ack_less_mono1: "i < j ==> ack i k < ack j k" |
112 lemma ack_less_mono1: "i < j \<Longrightarrow> ack i k < ack j k" |
115 apply (drule less_imp_Suc_add) |
113 using ack_less_mono1_aux less_iff_Suc_add by auto |
116 apply (blast intro!: ack_less_mono1_aux) |
|
117 done |
|
118 |
114 |
119 |
115 |
120 text \<open>PROPERTY A 7', monotonicity for \<open>\<le>\<close>\<close> |
116 text \<open>PROPERTY A 7', monotonicity for \<open>\<le>\<close>\<close> |
121 |
117 |
122 lemma ack_le_mono1: "i \<le> j ==> ack i k \<le> ack j k" |
118 lemma ack_le_mono1: "i \<le> j \<Longrightarrow> ack i k \<le> ack j k" |
123 apply (simp add: order_le_less) |
119 using ack_less_mono1 le_eq_less_or_eq by auto |
124 apply (blast intro: ack_less_mono1) |
|
125 done |
|
126 |
120 |
127 |
121 |
128 text \<open>PROPERTY A 10\<close> |
122 text \<open>PROPERTY A 10\<close> |
129 |
123 |
130 lemma ack_nest_bound: "ack i1 (ack i2 j) < ack (2 + (i1 + i2)) j" |
124 lemma ack_nest_bound: "ack i1 (ack i2 j) < ack (2 + (i1 + i2)) j" |
131 apply simp |
125 proof - |
132 apply (rule ack2_le_ack1 [THEN [2] less_le_trans]) |
126 have "ack i1 (ack i2 j) < ack (i1 + i2) (ack (Suc (i1 + i2)) j)" |
133 apply simp |
127 by (meson ack_le_mono1 ack_less_mono1 ack_less_mono2 le_add1 le_trans less_add_Suc2 not_less) |
134 apply (rule le_add1 [THEN ack_le_mono1, THEN le_less_trans]) |
128 also have "... = ack (Suc (i1 + i2)) (Suc j)" |
135 apply (rule ack_less_mono1 [THEN ack_less_mono2]) |
129 by simp |
136 apply (simp add: le_imp_less_Suc le_add2) |
130 also have "... \<le> ack (2 + (i1 + i2)) j" |
137 done |
131 using ack2_le_ack1 add_2_eq_Suc by presburger |
|
132 finally show ?thesis . |
|
133 qed |
|
134 |
138 |
135 |
139 |
136 |
140 text \<open>PROPERTY A 11\<close> |
137 text \<open>PROPERTY A 11\<close> |
141 |
138 |
142 lemma ack_add_bound: "ack i1 j + ack i2 j < ack (4 + (i1 + i2)) j" |
139 lemma ack_add_bound: "ack i1 j + ack i2 j < ack (4 + (i1 + i2)) j" |
143 apply (rule less_trans [of _ "ack (Suc (Suc 0)) (ack (i1 + i2) j)"]) |
140 proof - |
144 prefer 2 |
141 have "ack i1 j \<le> ack (i1 + i2) j" "ack i2 j \<le> ack (i1 + i2) j" |
145 apply (rule ack_nest_bound [THEN less_le_trans]) |
142 by (simp_all add: ack_le_mono1) |
146 apply (simp add: Suc3_eq_add_3) |
143 then have "ack i1 j + ack i2 j < ack (Suc (Suc 0)) (ack (i1 + i2) j)" |
147 apply simp |
144 by simp |
148 apply (cut_tac i = i1 and m1 = i2 and k = j in le_add1 [THEN ack_le_mono1]) |
145 also have "... < ack (4 + (i1 + i2)) j" |
149 apply (cut_tac i = "i2" and m1 = i1 and k = j in le_add2 [THEN ack_le_mono1]) |
146 by (metis ack_nest_bound add.assoc numeral_2_eq_2 numeral_Bit0) |
150 apply auto |
147 finally show ?thesis . |
151 done |
148 qed |
152 |
149 |
153 |
150 |
154 text \<open>PROPERTY A 12. Article uses existential quantifier but the ALF proof |
151 text \<open>PROPERTY A 12. Article uses existential quantifier but the ALF proof |
155 used \<open>k + 4\<close>. Quantified version must be nested \<open>\<exists>k'. \<forall>i j. ...\<close>\<close> |
152 used \<open>k + 4\<close>. Quantified version must be nested \<open>\<exists>k'. \<forall>i j. ...\<close>\<close> |
156 |
153 |
157 lemma ack_add_bound2: "i < ack k j ==> i + j < ack (4 + k) j" |
154 lemma ack_add_bound2: |
158 apply (rule less_trans [of _ "ack k j + ack 0 j"]) |
155 assumes "i < ack k j" shows "i + j < ack (4 + k) j" |
159 apply (blast intro: add_less_mono) |
156 proof - |
160 apply (rule ack_add_bound [THEN less_le_trans]) |
157 have "i + j < ack k j + ack 0 j" |
161 apply simp |
158 using assms by auto |
162 done |
159 also have "... < ack (4 + k) j" |
|
160 by (metis ack_add_bound add.right_neutral) |
|
161 finally show ?thesis . |
|
162 qed |
163 |
163 |
164 |
164 |
165 subsection\<open>Primitive Recursive Functions\<close> |
165 subsection\<open>Primitive Recursive Functions\<close> |
166 |
166 |
167 primrec hd0 :: "nat list => nat" where |
167 primrec hd0 :: "nat list \<Rightarrow> nat" where |
168 "hd0 [] = 0" | |
168 "hd0 [] = 0" |
169 "hd0 (m # ms) = m" |
169 | "hd0 (m # ms) = m" |
170 |
170 |
171 |
171 |
172 text \<open>Inductive definition of the set of primitive recursive functions of type \<^typ>\<open>nat list => nat\<close>.\<close> |
172 text \<open>Inductive definition of the set of primitive recursive functions of type \<^typ>\<open>nat list \<Rightarrow> nat\<close>.\<close> |
173 |
173 |
174 definition SC :: "nat list => nat" where |
174 definition SC :: "nat list \<Rightarrow> nat" |
175 "SC l = Suc (hd0 l)" |
175 where "SC l = Suc (hd0 l)" |
176 |
176 |
177 definition CONSTANT :: "nat => nat list => nat" where |
177 definition CONSTANT :: "nat \<Rightarrow> nat list \<Rightarrow> nat" |
178 "CONSTANT k l = k" |
178 where "CONSTANT k l = k" |
179 |
179 |
180 definition PROJ :: "nat => nat list => nat" where |
180 definition PROJ :: "nat \<Rightarrow> nat list \<Rightarrow> nat" |
181 "PROJ i l = hd0 (drop i l)" |
181 where "PROJ i l = hd0 (drop i l)" |
182 |
182 |
183 definition |
183 definition COMP :: "[nat list \<Rightarrow> nat, (nat list \<Rightarrow> nat) list, nat list] \<Rightarrow> nat" |
184 COMP :: "(nat list => nat) => (nat list => nat) list => nat list => nat" |
184 where "COMP g fs l = g (map (\<lambda>f. f l) fs)" |
185 where "COMP g fs l = g (map (\<lambda>f. f l) fs)" |
185 |
186 |
186 fun PREC :: "[nat list \<Rightarrow> nat, nat list \<Rightarrow> nat, nat list] \<Rightarrow> nat" |
187 definition PREC :: "(nat list => nat) => (nat list => nat) => nat list => nat" |
187 where |
188 where |
188 "PREC f g [] = 0" |
189 "PREC f g l = |
189 | "PREC f g (x # l) = rec_nat (f l) (\<lambda>y r. g (r # y # l)) x" |
190 (case l of |
190 \<comment> \<open>Note that \<^term>\<open>g\<close> is applied first to \<^term>\<open>PREC f g y\<close> and then to \<^term>\<open>y\<close>!\<close> |
191 [] => 0 |
191 |
192 | x # l' => rec_nat (f l') (\<lambda>y r. g (r # y # l')) x)" |
192 inductive PRIMREC :: "(nat list \<Rightarrow> nat) \<Rightarrow> bool" where |
193 \<comment> \<open>Note that \<^term>\<open>g\<close> is applied first to \<^term>\<open>PREC f g y\<close> and then to \<^term>\<open>y\<close>!\<close> |
193 SC: "PRIMREC SC" |
194 |
194 | CONSTANT: "PRIMREC (CONSTANT k)" |
195 inductive PRIMREC :: "(nat list => nat) => bool" where |
195 | PROJ: "PRIMREC (PROJ i)" |
196 SC: "PRIMREC SC" | |
196 | COMP: "PRIMREC g \<Longrightarrow> \<forall>f \<in> set fs. PRIMREC f \<Longrightarrow> PRIMREC (COMP g fs)" |
197 CONSTANT: "PRIMREC (CONSTANT k)" | |
197 | PREC: "PRIMREC f \<Longrightarrow> PRIMREC g \<Longrightarrow> PRIMREC (PREC f g)" |
198 PROJ: "PRIMREC (PROJ i)" | |
|
199 COMP: "PRIMREC g ==> \<forall>f \<in> set fs. PRIMREC f ==> PRIMREC (COMP g fs)" | |
|
200 PREC: "PRIMREC f ==> PRIMREC g ==> PRIMREC (PREC f g)" |
|
201 |
198 |
202 |
199 |
203 text \<open>Useful special cases of evaluation\<close> |
200 text \<open>Useful special cases of evaluation\<close> |
204 |
201 |
205 lemma SC [simp]: "SC (x # l) = Suc x" |
202 lemma SC [simp]: "SC (x # l) = Suc x" |
206 by (simp add: SC_def) |
203 by (simp add: SC_def) |
207 |
|
208 lemma CONSTANT [simp]: "CONSTANT k l = k" |
|
209 by (simp add: CONSTANT_def) |
|
210 |
204 |
211 lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x" |
205 lemma PROJ_0 [simp]: "PROJ 0 (x # l) = x" |
212 by (simp add: PROJ_def) |
206 by (simp add: PROJ_def) |
213 |
207 |
214 lemma COMP_1 [simp]: "COMP g [f] l = g [f l]" |
208 lemma COMP_1 [simp]: "COMP g [f] l = g [f l]" |
215 by (simp add: COMP_def) |
209 by (simp add: COMP_def) |
216 |
210 |
217 lemma PREC_0 [simp]: "PREC f g (0 # l) = f l" |
211 lemma PREC_0: "PREC f g (0 # l) = f l" |
218 by (simp add: PREC_def) |
212 by simp |
219 |
213 |
220 lemma PREC_Suc [simp]: "PREC f g (Suc x # l) = g (PREC f g (x # l) # x # l)" |
214 lemma PREC_Suc [simp]: "PREC f g (Suc x # l) = g (PREC f g (x # l) # x # l)" |
221 by (simp add: PREC_def) |
215 by auto |
222 |
216 |
223 |
217 |
224 text \<open>MAIN RESULT\<close> |
218 subsection \<open>MAIN RESULT\<close> |
225 |
219 |
226 lemma SC_case: "SC l < ack 1 (sum_list l)" |
220 lemma SC_case: "SC l < ack 1 (sum_list l)" |
227 apply (unfold SC_def) |
221 unfolding SC_def |
228 apply (induct l) |
222 by (induct l) (simp_all add: le_add1 le_imp_less_Suc) |
229 apply (simp_all add: le_add1 le_imp_less_Suc) |
|
230 done |
|
231 |
223 |
232 lemma CONSTANT_case: "CONSTANT k l < ack k (sum_list l)" |
224 lemma CONSTANT_case: "CONSTANT k l < ack k (sum_list l)" |
233 by simp |
225 by (simp add: CONSTANT_def) |
234 |
226 |
235 lemma PROJ_case: "PROJ i l < ack 0 (sum_list l)" |
227 lemma PROJ_case: "PROJ i l < ack 0 (sum_list l)" |
236 apply (simp add: PROJ_def) |
228 unfolding PROJ_def |
237 apply (induct l arbitrary:i) |
229 proof (induct l arbitrary: i) |
238 apply (auto simp add: drop_Cons split: nat.split) |
230 case Nil |
239 apply (blast intro: less_le_trans le_add2) |
231 then show ?case |
240 done |
232 by simp |
|
233 next |
|
234 case (Cons a l) |
|
235 then show ?case |
|
236 by (metis ack.simps(1) add.commute drop_Cons' hd0.simps(2) leD leI lessI not_less_eq sum_list.Cons trans_le_add2) |
|
237 qed |
241 |
238 |
242 |
239 |
243 text \<open>\<^term>\<open>COMP\<close> case\<close> |
240 text \<open>\<^term>\<open>COMP\<close> case\<close> |
244 |
241 |
245 lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l)) |
242 lemma COMP_map_aux: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l)) |
246 ==> \<exists>k. \<forall>l. sum_list (map (\<lambda>f. f l) fs) < ack k (sum_list l)" |
243 \<Longrightarrow> \<exists>k. \<forall>l. sum_list (map (\<lambda>f. f l) fs) < ack k (sum_list l)" |
247 apply (induct fs) |
244 proof (induct fs) |
248 apply (rule_tac x = 0 in exI) |
245 case Nil |
249 apply simp |
246 then show ?case |
250 apply simp |
247 by auto |
251 apply (blast intro: add_less_mono ack_add_bound less_trans) |
248 next |
252 done |
249 case (Cons a fs) |
|
250 then show ?case |
|
251 by simp (blast intro: add_less_mono ack_add_bound less_trans) |
|
252 qed |
253 |
253 |
254 lemma COMP_case: |
254 lemma COMP_case: |
255 "\<forall>l. g l < ack kg (sum_list l) ==> |
255 assumes 1: "\<forall>l. g l < ack kg (sum_list l)" |
256 \<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l)) |
256 and 2: "\<forall>f \<in> set fs. PRIMREC f \<and> (\<exists>kf. \<forall>l. f l < ack kf (sum_list l))" |
257 ==> \<exists>k. \<forall>l. COMP g fs l < ack k (sum_list l)" |
257 shows "\<exists>k. \<forall>l. COMP g fs l < ack k (sum_list l)" |
258 apply (unfold COMP_def) |
258 unfolding COMP_def |
259 apply (drule COMP_map_aux) |
259 using 1 COMP_map_aux [OF 2] by (meson ack_less_mono2 ack_nest_bound less_trans) |
260 apply (meson ack_less_mono2 ack_nest_bound less_trans) |
|
261 done |
|
262 |
|
263 |
260 |
264 text \<open>\<^term>\<open>PREC\<close> case\<close> |
261 text \<open>\<^term>\<open>PREC\<close> case\<close> |
265 |
262 |
266 lemma PREC_case_aux: |
263 lemma PREC_case_aux: |
267 "\<forall>l. f l + sum_list l < ack kf (sum_list l) ==> |
264 assumes f: "\<And>l. f l + sum_list l < ack kf (sum_list l)" |
268 \<forall>l. g l + sum_list l < ack kg (sum_list l) ==> |
265 and g: "\<And>l. g l + sum_list l < ack kg (sum_list l)" |
269 PREC f g l + sum_list l < ack (Suc (kf + kg)) (sum_list l)" |
266 shows "PREC f g l + sum_list l < ack (Suc (kf + kg)) (sum_list l)" |
270 apply (unfold PREC_def) |
267 proof (cases l) |
271 apply (case_tac l) |
268 case Nil |
272 apply simp_all |
269 then show ?thesis |
273 apply (blast intro: less_trans) |
270 by (simp add: Suc_lessD) |
274 apply (erule ssubst) \<comment> \<open>get rid of the needless assumption\<close> |
271 next |
275 apply (induct_tac a) |
272 case (Cons m l) |
276 apply simp_all |
273 have "rec_nat (f l) (\<lambda>y r. g (r # y # l)) m + (m + sum_list l) < ack (Suc (kf + kg)) (m + sum_list l)" |
277 txt \<open>base case\<close> |
274 proof (induct m) |
278 apply (blast intro: le_add1 [THEN le_imp_less_Suc, THEN ack_less_mono1] less_trans) |
275 case 0 |
279 txt \<open>induction step\<close> |
276 then show ?case |
280 apply (rule Suc_leI [THEN le_less_trans]) |
277 using ack_less_mono1_aux f less_trans by fastforce |
281 apply (rule le_refl [THEN add_le_mono, THEN le_less_trans]) |
278 next |
282 prefer 2 |
279 case (Suc m) |
283 apply (erule spec) |
280 let ?r = "rec_nat (f l) (\<lambda>y r. g (r # y # l)) m" |
284 apply (simp add: le_add2) |
281 have "\<not> g (?r # m # l) + sum_list (?r # m # l) < g (?r # m # l) + (m + sum_list l)" |
285 txt \<open>final part of the simplification\<close> |
282 by force |
286 apply simp |
283 then have "g (?r # m # l) + (m + sum_list l) < ack kg (sum_list (?r # m # l))" |
287 apply (rule le_add2 [THEN ack_le_mono1, THEN le_less_trans]) |
284 by (meson assms(2) leI less_le_trans) |
288 apply (erule ack_less_mono2) |
285 moreover |
289 done |
286 have "... < ack (kf + kg) (ack (Suc (kf + kg)) (m + sum_list l))" |
290 |
287 using Suc.hyps by simp (meson ack_le_mono1 ack_less_mono2 le_add2 le_less_trans) |
291 lemma PREC_case: |
288 ultimately show ?case |
292 "\<forall>l. f l < ack kf (sum_list l) ==> |
289 by auto |
293 \<forall>l. g l < ack kg (sum_list l) ==> |
290 qed |
294 \<exists>k. \<forall>l. PREC f g l < ack k (sum_list l)" |
291 then show ?thesis |
295 by (metis le_less_trans [OF le_add1 PREC_case_aux] ack_add_bound2) |
292 by (simp add: local.Cons) |
296 |
293 qed |
297 lemma ack_bounds_PRIMREC: "PRIMREC f ==> \<exists>k. \<forall>l. f l < ack k (sum_list l)" |
294 |
298 apply (erule PRIMREC.induct) |
295 proposition PREC_case: |
299 apply (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+ |
296 "\<lbrakk>\<And>l. f l < ack kf (sum_list l); \<And>l. g l < ack kg (sum_list l)\<rbrakk> |
300 done |
297 \<Longrightarrow> \<exists>k. \<forall>l. PREC f g l < ack k (sum_list l)" |
|
298 by (metis le_less_trans [OF le_add1 PREC_case_aux] ack_add_bound2) |
|
299 |
|
300 lemma ack_bounds_PRIMREC: "PRIMREC f \<Longrightarrow> \<exists>k. \<forall>l. f l < ack k (sum_list l)" |
|
301 by (erule PRIMREC.induct) (blast intro: SC_case CONSTANT_case PROJ_case COMP_case PREC_case)+ |
301 |
302 |
302 theorem ack_not_PRIMREC: |
303 theorem ack_not_PRIMREC: |
303 "\<not> PRIMREC (\<lambda>l. case l of [] => 0 | x # l' => ack x x)" |
304 "\<not> PRIMREC (\<lambda>l. case l of [] \<Rightarrow> 0 | x # l' \<Rightarrow> ack x x)" |
304 apply (rule notI) |
305 proof |
305 apply (erule ack_bounds_PRIMREC [THEN exE]) |
306 assume *: "PRIMREC (\<lambda>l. case l of [] \<Rightarrow> 0 | x # l' \<Rightarrow> ack x x)" |
306 apply (rule less_irrefl [THEN notE]) |
307 then obtain m where m: "\<And>l. (case l of [] \<Rightarrow> 0 | x # l' \<Rightarrow> ack x x) < ack m (sum_list l)" |
307 apply (drule_tac x = "[x]" in spec) |
308 using ack_bounds_PRIMREC by metis |
308 apply simp |
309 show False |
309 done |
310 using m [of "[m]"] by simp |
|
311 qed |
310 |
312 |
311 end |
313 end |