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 
Addsimps ack.rules;


48 


49 
(*PROPERTY A 4*)

5069

50 
Goal "j < ack(i,j)";

3335

51 
by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);


52 
by (ALLGOALS Asm_simp_tac);


53 
by (ALLGOALS trans_tac);


54 
qed "less_ack2";


55 


56 
AddIffs [less_ack2];


57 


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

5069

59 
Goal "ack(i,j) < ack(i, Suc(j))";

3335

60 
by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);


61 
by (ALLGOALS Asm_simp_tac);


62 
qed "ack_less_ack_Suc2";


63 


64 
AddIffs [ack_less_ack_Suc2];


65 


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

5069

67 
Goal "j<k > ack(i,j) < ack(i,k)";

3335

68 
by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);


69 
by (ALLGOALS Asm_simp_tac);

4089

70 
by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1);

3335

71 
qed_spec_mp "ack_less_mono2";


72 


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

5069

74 
Goal "!!i j k. j<=k ==> ack(i,j)<=ack(i,k)";

4089

75 
by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);


76 
by (blast_tac (claset() addIs [ack_less_mono2]) 1);

3335

77 
qed "ack_le_mono2";


78 


79 
(*PROPERTY A 6*)

5069

80 
Goal "ack(i, Suc(j)) <= ack(Suc(i), j)";

3335

81 
by (induct_tac "j" 1);


82 
by (ALLGOALS Asm_simp_tac);

4089

83 
by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI,

3335

84 
le_trans]) 1);


85 
qed "ack2_le_ack1";


86 


87 
AddIffs [ack2_le_ack1];


88 


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

5069

90 
Goal "ack(i,j) < ack(Suc(i),j)";

4089

91 
by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1);

3335

92 
qed "ack_less_ack_Suc1";


93 


94 
AddIffs [ack_less_ack_Suc1];


95 


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

5069

97 
Goal "i < ack(i,j)";

3335

98 
by (induct_tac "i" 1);


99 
by (ALLGOALS Asm_simp_tac);

4089

100 
by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1);

3335

101 
qed "less_ack1";


102 
AddIffs [less_ack1];


103 


104 
(*PROPERTY A 8*)

5069

105 
Goal "ack(1,j) = Suc(Suc(j))";

3335

106 
by (induct_tac "j" 1);


107 
by (ALLGOALS Asm_simp_tac);


108 
qed "ack_1";


109 
Addsimps [ack_1];


110 


111 
(*PROPERTY A 9*)

5069

112 
Goal "ack(Suc(1),j) = Suc(Suc(Suc(j+j)))";

3335

113 
by (induct_tac "j" 1);


114 
by (ALLGOALS Asm_simp_tac);


115 
qed "ack_2";


116 
Addsimps [ack_2];


117 


118 


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

5069

120 
Goal "ack(i,k) < ack(Suc(i+i'),k)";

3335

121 
by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);


122 
by (ALLGOALS Asm_full_simp_tac);

4089

123 
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2);

3335

124 
by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1);


125 
by (ALLGOALS Asm_simp_tac);

4089

126 
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1);


127 
by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);

3335

128 
val lemma = result();


129 

5069

130 
Goal "!!i j k. i<j ==> ack(i,k) < ack(j,k)";

3457

131 
by (etac less_natE 1);

4089

132 
by (blast_tac (claset() addSIs [lemma]) 1);

3335

133 
qed "ack_less_mono1";


134 


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

5069

136 
Goal "!!i j k. i<=j ==> ack(i,k)<=ack(j,k)";

4089

137 
by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);


138 
by (blast_tac (claset() addIs [ack_less_mono1]) 1);

3335

139 
qed "ack_le_mono1";


140 


141 
(*PROPERTY A 10*)

5069

142 
Goal "ack(i1, ack(i2,j)) < ack(Suc(Suc(i1+i2)), j)";

3335

143 
by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1);


144 
by (Asm_simp_tac 1);


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


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

4089

147 
by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1);

3335

148 
qed "ack_nest_bound";


149 


150 
(*PROPERTY A 11*)

5069

151 
Goal "ack(i1,j) + ack(i2,j) < ack(Suc(Suc(Suc(Suc(i1+i2)))), j)";

3335

152 
by (res_inst_tac [("j", "ack(Suc(1), ack(i1 + i2, j))")] less_trans 1);


153 
by (Asm_simp_tac 1);


154 
by (rtac (ack_nest_bound RS less_le_trans) 2);


155 
by (Asm_simp_tac 2);

4089

156 
by (blast_tac (claset() addSIs [le_add1, le_add2]

3335

157 
addIs [le_imp_less_Suc, ack_le_mono1, le_SucI,


158 
add_le_mono]) 1);


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... *)

5069

163 
Goal "!!i j k. i < ack(k,j) ==> i+j < ack(Suc(Suc(Suc(Suc(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);


189 
by (exhaust_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 

5069

198 
Goal

3335

199 
"!!fs. fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \


200 
\ ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)";


201 
by (etac lists.induct 1);


202 
by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1);

4153

203 
by Safe_tac;

3335

204 
by (Asm_simp_tac 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]

3335

209 
"!!g. [ ALL l. g l < ack(kg, list_add l); \


210 
\ fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \


211 
\ ] ==> EX k. ALL l. COMP g fs l < ack(k, list_add l)";


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]

3335

224 
"!!f g. [ ALL l. f l + list_add l < ack(kf, list_add l); \


225 
\ ALL l. g l + list_add l < ack(kg, list_add l) \


226 
\ ] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";


227 
by (exhaust_tac "l" 1);


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 

5069

247 
Goal

3335

248 
"!!f g. [ ALL l. f l < ack(kf, list_add l); \


249 
\ ALL l. g l < ack(kg, list_add l) \


250 
\ ] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";

3457

251 
by (rtac exI 1);


252 
by (rtac allI 1);

3335

253 
by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1);

4089

254 
by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1));

3335

255 
qed "PREC_case";


256 

5069

257 
Goal "!!f. f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)";

3335

258 
by (etac PRIMREC.induct 1);


259 
by (ALLGOALS

4089

260 
(blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case,

3335

261 
PREC_case])));


262 
qed "ack_bounds_PRIMREC";


263 

5069

264 
Goal "(%l. case l of [] => 0  x#l' => ack(x,x)) ~: PRIMREC";

3335

265 
by (rtac notI 1);


266 
by (etac (ack_bounds_PRIMREC RS exE) 1);


267 
by (rtac less_irrefl 1);


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


269 
by (Asm_full_simp_tac 1);


270 
qed "ack_not_PRIMREC";


271 
