author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9747  043098ba5098 
child 10558  09a91221ced1 
permissions  rwrr 
3335  1 
(* Title: HOL/ex/Primrec 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

6 
Primitive Recursive Functions 

7 

8 
Proof adopted from 

9 
Nora Szasz, 

10 
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive, 

11 
In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317338. 

12 

13 
See also E. Mendelson, Introduction to Mathematical Logic. 

14 
(Van Nostrand, 1964), page 250, exercise 11. 

15 
*) 

16 

17 

18 
(** Useful special cases of evaluation ***) 

19 

5069  20 
Goalw [SC_def] "SC (x#l) = Suc x"; 
3335  21 
by (Asm_simp_tac 1); 
22 
qed "SC"; 

23 

5069  24 
Goalw [CONST_def] "CONST k l = k"; 
3335  25 
by (Asm_simp_tac 1); 
26 
qed "CONST"; 

27 

5069  28 
Goalw [PROJ_def] "PROJ(0) (x#l) = x"; 
3335  29 
by (Asm_simp_tac 1); 
30 
qed "PROJ_0"; 

31 

5069  32 
Goalw [COMP_def] "COMP g [f] l = g [f l]"; 
3335  33 
by (Asm_simp_tac 1); 
34 
qed "COMP_1"; 

35 

5069  36 
Goalw [PREC_def] "PREC f g (0#l) = f l"; 
3335  37 
by (Asm_simp_tac 1); 
38 
qed "PREC_0"; 

39 

5069  40 
Goalw [PREC_def] "PREC f g (Suc x # l) = g (PREC f g (x#l) # x # l)"; 
3335  41 
by (Asm_simp_tac 1); 
42 
qed "PREC_Suc"; 

43 

44 
Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc]; 

45 

46 

47 
(*PROPERTY A 4*) 

5069  48 
Goal "j < ack(i,j)"; 
9747  49 
by (induct_thm_tac ack.induct "i j" 1); 
3335  50 
by (ALLGOALS Asm_simp_tac); 
51 
qed "less_ack2"; 

52 

53 
AddIffs [less_ack2]; 

54 

55 
(*PROPERTY A 5, the singlestep lemma*) 

5069  56 
Goal "ack(i,j) < ack(i, Suc(j))"; 
9747  57 
by (induct_thm_tac ack.induct "i j" 1); 
3335  58 
by (ALLGOALS Asm_simp_tac); 
59 
qed "ack_less_ack_Suc2"; 

60 

61 
AddIffs [ack_less_ack_Suc2]; 

62 

63 
(*PROPERTY A 5, monotonicity for < *) 

5069  64 
Goal "j<k > ack(i,j) < ack(i,k)"; 
9747  65 
by (induct_thm_tac ack.induct "i k" 1); 
3335  66 
by (ALLGOALS Asm_simp_tac); 
4089  67 
by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1); 
3335  68 
qed_spec_mp "ack_less_mono2"; 
69 

70 
(*PROPERTY A 5', monotonicity for<=*) 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

71 
Goal "j<=k ==> ack(i,j)<=ack(i,k)"; 
5599  72 
by (full_simp_tac (simpset() addsimps [order_le_less]) 1); 
4089  73 
by (blast_tac (claset() addIs [ack_less_mono2]) 1); 
3335  74 
qed "ack_le_mono2"; 
75 

76 
(*PROPERTY A 6*) 

5069  77 
Goal "ack(i, Suc(j)) <= ack(Suc(i), j)"; 
3335  78 
by (induct_tac "j" 1); 
79 
by (ALLGOALS Asm_simp_tac); 

4089  80 
by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI, 
3335  81 
le_trans]) 1); 
82 
qed "ack2_le_ack1"; 

83 

84 
AddIffs [ack2_le_ack1]; 

85 

86 
(*PROPERTY A 7, the singlestep lemma*) 

5069  87 
Goal "ack(i,j) < ack(Suc(i),j)"; 
4089  88 
by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1); 
3335  89 
qed "ack_less_ack_Suc1"; 
90 

91 
AddIffs [ack_less_ack_Suc1]; 

92 

93 
(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*) 

5069  94 
Goal "i < ack(i,j)"; 
3335  95 
by (induct_tac "i" 1); 
96 
by (ALLGOALS Asm_simp_tac); 

4089  97 
by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1); 
3335  98 
qed "less_ack1"; 
99 
AddIffs [less_ack1]; 

100 

101 
(*PROPERTY A 8*) 

8794  102 
Goal "ack(1,j) = j + #2"; 
3335  103 
by (induct_tac "j" 1); 
104 
by (ALLGOALS Asm_simp_tac); 

105 
qed "ack_1"; 

106 
Addsimps [ack_1]; 

107 

8794  108 
(*PROPERTY A 9. The unary 1 and 2 in ack is essential for the rewriting.*) 
109 
Goal "ack(2,j) = #2*j + #3"; 

3335  110 
by (induct_tac "j" 1); 
111 
by (ALLGOALS Asm_simp_tac); 

112 
qed "ack_2"; 

113 
Addsimps [ack_2]; 

114 

115 

116 
(*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*) 

5069  117 
Goal "ack(i,k) < ack(Suc(i+i'),k)"; 
9747  118 
by (induct_thm_tac ack.induct "i k" 1); 
3335  119 
by (ALLGOALS Asm_full_simp_tac); 
4089  120 
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2); 
9747  121 
by (induct_thm_tac ack.induct "i' n" 1); 
3335  122 
by (ALLGOALS Asm_simp_tac); 
4089  123 
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1); 
124 
by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1); 

3335  125 
val lemma = result(); 
126 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

127 
Goal "i<j ==> ack(i,k) < ack(j,k)"; 
5078  128 
by (dtac less_eq_Suc_add 1); 
4089  129 
by (blast_tac (claset() addSIs [lemma]) 1); 
3335  130 
qed "ack_less_mono1"; 
131 

132 
(*PROPERTY A 7', monotonicity for<=*) 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

133 
Goal "i<=j ==> ack(i,k)<=ack(j,k)"; 
5599  134 
by (full_simp_tac (simpset() addsimps [order_le_less]) 1); 
4089  135 
by (blast_tac (claset() addIs [ack_less_mono1]) 1); 
3335  136 
qed "ack_le_mono1"; 
137 

138 
(*PROPERTY A 10*) 

8794  139 
Goal "ack(i1, ack(i2,j)) < ack(#2 + (i1+i2), j)"; 
140 
by (simp_tac numeral_ss 1); 

3335  141 
by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1); 
142 
by (Asm_simp_tac 1); 

143 
by (rtac (le_add1 RS ack_le_mono1 RS le_less_trans) 1); 

144 
by (rtac (ack_less_mono1 RS ack_less_mono2) 1); 

4089  145 
by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1); 
3335  146 
qed "ack_nest_bound"; 
147 

148 
(*PROPERTY A 11*) 

8794  149 
Goal "ack(i1,j) + ack(i2,j) < ack(#4 + (i1 + i2), j)"; 
150 
by (res_inst_tac [("j", "ack(2, ack(i1 + i2, j))")] less_trans 1); 

3335  151 
by (Asm_simp_tac 1); 
152 
by (rtac (ack_nest_bound RS less_le_trans) 2); 

8878
7aec47e7d727
changed to cope with the rewriting of #2+n to Suc(Suc n)
paulson
parents:
8794
diff
changeset

153 
by (asm_simp_tac (simpset() addsimps [Suc3_eq_add_3]) 2); 
8781  154 
by (cut_inst_tac [("i","i1"), ("m1","i2"), ("k","j")] 
155 
(le_add1 RS ack_le_mono1) 1); 

156 
by (cut_inst_tac [("i","i2"), ("m1","i1"), ("k","j")] 

157 
(le_add2 RS ack_le_mono1) 1); 

158 
by Auto_tac; 

3335  159 
qed "ack_add_bound"; 
160 

161 
(*PROPERTY A 12. Article uses existential quantifier but the ALF proof 

162 
used k+4. Quantified version must be nested EX k'. ALL i,j... *) 

8794  163 
Goal "i < ack(k,j) ==> i+j < ack(#4 + k, j)"; 
3335  164 
by (res_inst_tac [("j", "ack(k,j) + ack(0,j)")] less_trans 1); 
165 
by (rtac (ack_add_bound RS less_le_trans) 2); 

166 
by (Asm_simp_tac 2); 

167 
by (REPEAT (ares_tac ([add_less_mono, less_ack2]) 1)); 

168 
qed "ack_add_bound2"; 

169 

170 

171 
(*** Inductive definition of the PR functions ***) 

172 

173 
(*** MAIN RESULT ***) 

174 

5069  175 
Goalw [SC_def] "SC l < ack(1, list_add l)"; 
3335  176 
by (induct_tac "l" 1); 
4089  177 
by (ALLGOALS (simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc]))); 
3335  178 
qed "SC_case"; 
179 

5069  180 
Goal "CONST k l < ack(k, list_add l)"; 
3335  181 
by (Simp_tac 1); 
182 
qed "CONST_case"; 

183 

5069  184 
Goalw [PROJ_def] "ALL i. PROJ i l < ack(0, list_add l)"; 
3335  185 
by (Simp_tac 1); 
186 
by (induct_tac "l" 1); 

187 
by (ALLGOALS Asm_simp_tac); 

188 
by (rtac allI 1); 

8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

189 
by (case_tac "i" 1); 
4089  190 
by (asm_simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc]) 1); 
3335  191 
by (Asm_simp_tac 1); 
4089  192 
by (blast_tac (claset() addIs [less_le_trans] 
3335  193 
addSIs [le_add2]) 1); 
194 
qed_spec_mp "PROJ_case"; 

195 

196 
(** COMP case **) 

197 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

198 
Goal "fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ 
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

199 
\ ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)"; 
3335  200 
by (etac lists.induct 1); 
201 
by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1); 

4153  202 
by Safe_tac; 
3335  203 
by (Asm_simp_tac 1); 
5462  204 
by (rtac exI 1); 
4089  205 
by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1); 
3335  206 
qed "COMP_map_lemma"; 
207 

5069  208 
Goalw [COMP_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

209 
"[ ALL l. g l < ack(kg, list_add l); \ 
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

210 
\ fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \ 
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

211 
\ ] ==> EX k. ALL l. COMP g fs l < ack(k, list_add l)"; 
3335  212 
by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1); 
213 
by (etac (COMP_map_lemma RS exE) 1); 

214 
by (rtac exI 1); 

215 
by (rtac allI 1); 

216 
by (REPEAT (dtac spec 1)); 

217 
by (etac less_trans 1); 

4089  218 
by (blast_tac (claset() addIs [ack_less_mono2, ack_nest_bound, less_trans]) 1); 
3335  219 
qed "COMP_case"; 
220 

221 
(** PREC case **) 

222 

5069  223 
Goalw [PREC_def] 
5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

224 
"[ ALL l. f l + list_add l < ack(kf, list_add l); \ 
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

225 
\ ALL l. g l + list_add l < ack(kg, list_add l) \ 
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

226 
\ ] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

227 
by (case_tac "l" 1); 
3335  228 
by (ALLGOALS Asm_simp_tac); 
4089  229 
by (blast_tac (claset() addIs [less_trans]) 1); 
3335  230 
by (etac ssubst 1); (*get rid of the needless assumption*) 
231 
by (induct_tac "a" 1); 

232 
by (ALLGOALS Asm_simp_tac); 

233 
(*base case*) 

4089  234 
by (blast_tac (claset() addIs [le_add1 RS le_imp_less_Suc RS ack_less_mono1, 
3335  235 
less_trans]) 1); 
236 
(*induction step*) 

237 
by (rtac (Suc_leI RS le_less_trans) 1); 

238 
by (rtac (le_refl RS add_le_mono RS le_less_trans) 1); 

239 
by (etac spec 2); 

4089  240 
by (asm_simp_tac (simpset() addsimps [le_add2]) 1); 
3335  241 
(*final part of the simplification*) 
242 
by (Asm_simp_tac 1); 

243 
by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1); 

244 
by (etac ack_less_mono2 1); 

245 
qed "PREC_case_lemma"; 

246 

5148
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

247 
Goal "[ ALL l. f l < ack(kf, list_add l); \ 
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

248 
\ ALL l. g l < ack(kg, list_add l) \ 
74919e8f221c
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5143
diff
changeset

249 
\ ] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)"; 
3457  250 
by (rtac exI 1); 
251 
by (rtac allI 1); 

3335  252 
by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1); 
4089  253 
by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1)); 
3335  254 
qed "PREC_case"; 
255 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

256 
Goal "f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)"; 
3335  257 
by (etac PRIMREC.induct 1); 
258 
by (ALLGOALS 

4089  259 
(blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
3335  260 
PREC_case]))); 
261 
qed "ack_bounds_PRIMREC"; 

262 

5069  263 
Goal "(%l. case l of [] => 0  x#l' => ack(x,x)) ~: PRIMREC"; 
3335  264 
by (rtac notI 1); 
265 
by (etac (ack_bounds_PRIMREC RS exE) 1); 

266 
by (rtac less_irrefl 1); 

267 
by (dres_inst_tac [("x", "[x]")] spec 1); 

268 
by (Asm_full_simp_tac 1); 

269 
qed "ack_not_PRIMREC"; 

270 