15 *) |
15 *) |
16 |
16 |
17 |
17 |
18 (** Useful special cases of evaluation ***) |
18 (** Useful special cases of evaluation ***) |
19 |
19 |
20 goalw thy [SC_def] "SC (x#l) = Suc x"; |
20 Goalw [SC_def] "SC (x#l) = Suc x"; |
21 by (Asm_simp_tac 1); |
21 by (Asm_simp_tac 1); |
22 qed "SC"; |
22 qed "SC"; |
23 |
23 |
24 goalw thy [CONST_def] "CONST k l = k"; |
24 Goalw [CONST_def] "CONST k l = k"; |
25 by (Asm_simp_tac 1); |
25 by (Asm_simp_tac 1); |
26 qed "CONST"; |
26 qed "CONST"; |
27 |
27 |
28 goalw thy [PROJ_def] "PROJ(0) (x#l) = x"; |
28 Goalw [PROJ_def] "PROJ(0) (x#l) = x"; |
29 by (Asm_simp_tac 1); |
29 by (Asm_simp_tac 1); |
30 qed "PROJ_0"; |
30 qed "PROJ_0"; |
31 |
31 |
32 goalw thy [COMP_def] "COMP g [f] l = g [f l]"; |
32 Goalw [COMP_def] "COMP g [f] l = g [f l]"; |
33 by (Asm_simp_tac 1); |
33 by (Asm_simp_tac 1); |
34 qed "COMP_1"; |
34 qed "COMP_1"; |
35 |
35 |
36 goalw thy [PREC_def] "PREC f g (0#l) = f l"; |
36 Goalw [PREC_def] "PREC f g (0#l) = f l"; |
37 by (Asm_simp_tac 1); |
37 by (Asm_simp_tac 1); |
38 qed "PREC_0"; |
38 qed "PREC_0"; |
39 |
39 |
40 goalw thy [PREC_def] "PREC f g (Suc x # l) = g (PREC f g (x#l) # x # l)"; |
40 Goalw [PREC_def] "PREC f g (Suc x # l) = g (PREC f g (x#l) # x # l)"; |
41 by (Asm_simp_tac 1); |
41 by (Asm_simp_tac 1); |
42 qed "PREC_Suc"; |
42 qed "PREC_Suc"; |
43 |
43 |
44 Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc]; |
44 Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc]; |
45 |
45 |
46 |
46 |
47 Addsimps ack.rules; |
47 Addsimps ack.rules; |
48 |
48 |
49 (*PROPERTY A 4*) |
49 (*PROPERTY A 4*) |
50 goal thy "j < ack(i,j)"; |
50 Goal "j < ack(i,j)"; |
51 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1); |
51 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1); |
52 by (ALLGOALS Asm_simp_tac); |
52 by (ALLGOALS Asm_simp_tac); |
53 by (ALLGOALS trans_tac); |
53 by (ALLGOALS trans_tac); |
54 qed "less_ack2"; |
54 qed "less_ack2"; |
55 |
55 |
56 AddIffs [less_ack2]; |
56 AddIffs [less_ack2]; |
57 |
57 |
58 (*PROPERTY A 5-, the single-step lemma*) |
58 (*PROPERTY A 5-, the single-step lemma*) |
59 goal thy "ack(i,j) < ack(i, Suc(j))"; |
59 Goal "ack(i,j) < ack(i, Suc(j))"; |
60 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1); |
60 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1); |
61 by (ALLGOALS Asm_simp_tac); |
61 by (ALLGOALS Asm_simp_tac); |
62 qed "ack_less_ack_Suc2"; |
62 qed "ack_less_ack_Suc2"; |
63 |
63 |
64 AddIffs [ack_less_ack_Suc2]; |
64 AddIffs [ack_less_ack_Suc2]; |
65 |
65 |
66 (*PROPERTY A 5, monotonicity for < *) |
66 (*PROPERTY A 5, monotonicity for < *) |
67 goal thy "j<k --> ack(i,j) < ack(i,k)"; |
67 Goal "j<k --> ack(i,j) < ack(i,k)"; |
68 by (res_inst_tac [("u","i"),("v","k")] ack.induct 1); |
68 by (res_inst_tac [("u","i"),("v","k")] ack.induct 1); |
69 by (ALLGOALS Asm_simp_tac); |
69 by (ALLGOALS Asm_simp_tac); |
70 by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1); |
70 by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1); |
71 qed_spec_mp "ack_less_mono2"; |
71 qed_spec_mp "ack_less_mono2"; |
72 |
72 |
73 (*PROPERTY A 5', monotonicity for<=*) |
73 (*PROPERTY A 5', monotonicity for<=*) |
74 goal thy "!!i j k. j<=k ==> ack(i,j)<=ack(i,k)"; |
74 Goal "!!i j k. j<=k ==> ack(i,j)<=ack(i,k)"; |
75 by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); |
75 by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); |
76 by (blast_tac (claset() addIs [ack_less_mono2]) 1); |
76 by (blast_tac (claset() addIs [ack_less_mono2]) 1); |
77 qed "ack_le_mono2"; |
77 qed "ack_le_mono2"; |
78 |
78 |
79 (*PROPERTY A 6*) |
79 (*PROPERTY A 6*) |
80 goal thy "ack(i, Suc(j)) <= ack(Suc(i), j)"; |
80 Goal "ack(i, Suc(j)) <= ack(Suc(i), j)"; |
81 by (induct_tac "j" 1); |
81 by (induct_tac "j" 1); |
82 by (ALLGOALS Asm_simp_tac); |
82 by (ALLGOALS Asm_simp_tac); |
83 by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI, |
83 by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI, |
84 le_trans]) 1); |
84 le_trans]) 1); |
85 qed "ack2_le_ack1"; |
85 qed "ack2_le_ack1"; |
86 |
86 |
87 AddIffs [ack2_le_ack1]; |
87 AddIffs [ack2_le_ack1]; |
88 |
88 |
89 (*PROPERTY A 7-, the single-step lemma*) |
89 (*PROPERTY A 7-, the single-step lemma*) |
90 goal thy "ack(i,j) < ack(Suc(i),j)"; |
90 Goal "ack(i,j) < ack(Suc(i),j)"; |
91 by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1); |
91 by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1); |
92 qed "ack_less_ack_Suc1"; |
92 qed "ack_less_ack_Suc1"; |
93 |
93 |
94 AddIffs [ack_less_ack_Suc1]; |
94 AddIffs [ack_less_ack_Suc1]; |
95 |
95 |
96 (*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*) |
96 (*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*) |
97 goal thy "i < ack(i,j)"; |
97 Goal "i < ack(i,j)"; |
98 by (induct_tac "i" 1); |
98 by (induct_tac "i" 1); |
99 by (ALLGOALS Asm_simp_tac); |
99 by (ALLGOALS Asm_simp_tac); |
100 by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1); |
100 by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1); |
101 qed "less_ack1"; |
101 qed "less_ack1"; |
102 AddIffs [less_ack1]; |
102 AddIffs [less_ack1]; |
103 |
103 |
104 (*PROPERTY A 8*) |
104 (*PROPERTY A 8*) |
105 goal thy "ack(1,j) = Suc(Suc(j))"; |
105 Goal "ack(1,j) = Suc(Suc(j))"; |
106 by (induct_tac "j" 1); |
106 by (induct_tac "j" 1); |
107 by (ALLGOALS Asm_simp_tac); |
107 by (ALLGOALS Asm_simp_tac); |
108 qed "ack_1"; |
108 qed "ack_1"; |
109 Addsimps [ack_1]; |
109 Addsimps [ack_1]; |
110 |
110 |
111 (*PROPERTY A 9*) |
111 (*PROPERTY A 9*) |
112 goal thy "ack(Suc(1),j) = Suc(Suc(Suc(j+j)))"; |
112 Goal "ack(Suc(1),j) = Suc(Suc(Suc(j+j)))"; |
113 by (induct_tac "j" 1); |
113 by (induct_tac "j" 1); |
114 by (ALLGOALS Asm_simp_tac); |
114 by (ALLGOALS Asm_simp_tac); |
115 qed "ack_2"; |
115 qed "ack_2"; |
116 Addsimps [ack_2]; |
116 Addsimps [ack_2]; |
117 |
117 |
118 |
118 |
119 (*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*) |
119 (*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*) |
120 goal thy "ack(i,k) < ack(Suc(i+i'),k)"; |
120 Goal "ack(i,k) < ack(Suc(i+i'),k)"; |
121 by (res_inst_tac [("u","i"),("v","k")] ack.induct 1); |
121 by (res_inst_tac [("u","i"),("v","k")] ack.induct 1); |
122 by (ALLGOALS Asm_full_simp_tac); |
122 by (ALLGOALS Asm_full_simp_tac); |
123 by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2); |
123 by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2); |
124 by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1); |
124 by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1); |
125 by (ALLGOALS Asm_simp_tac); |
125 by (ALLGOALS Asm_simp_tac); |
126 by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1); |
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); |
127 by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1); |
128 val lemma = result(); |
128 val lemma = result(); |
129 |
129 |
130 goal thy "!!i j k. i<j ==> ack(i,k) < ack(j,k)"; |
130 Goal "!!i j k. i<j ==> ack(i,k) < ack(j,k)"; |
131 by (etac less_natE 1); |
131 by (etac less_natE 1); |
132 by (blast_tac (claset() addSIs [lemma]) 1); |
132 by (blast_tac (claset() addSIs [lemma]) 1); |
133 qed "ack_less_mono1"; |
133 qed "ack_less_mono1"; |
134 |
134 |
135 (*PROPERTY A 7', monotonicity for<=*) |
135 (*PROPERTY A 7', monotonicity for<=*) |
136 goal thy "!!i j k. i<=j ==> ack(i,k)<=ack(j,k)"; |
136 Goal "!!i j k. i<=j ==> ack(i,k)<=ack(j,k)"; |
137 by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); |
137 by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); |
138 by (blast_tac (claset() addIs [ack_less_mono1]) 1); |
138 by (blast_tac (claset() addIs [ack_less_mono1]) 1); |
139 qed "ack_le_mono1"; |
139 qed "ack_le_mono1"; |
140 |
140 |
141 (*PROPERTY A 10*) |
141 (*PROPERTY A 10*) |
142 goal thy "ack(i1, ack(i2,j)) < ack(Suc(Suc(i1+i2)), j)"; |
142 Goal "ack(i1, ack(i2,j)) < ack(Suc(Suc(i1+i2)), j)"; |
143 by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1); |
143 by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1); |
144 by (Asm_simp_tac 1); |
144 by (Asm_simp_tac 1); |
145 by (rtac (le_add1 RS ack_le_mono1 RS le_less_trans) 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); |
146 by (rtac (ack_less_mono1 RS ack_less_mono2) 1); |
147 by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1); |
147 by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1); |
148 qed "ack_nest_bound"; |
148 qed "ack_nest_bound"; |
149 |
149 |
150 (*PROPERTY A 11*) |
150 (*PROPERTY A 11*) |
151 goal thy "ack(i1,j) + ack(i2,j) < ack(Suc(Suc(Suc(Suc(i1+i2)))), j)"; |
151 Goal "ack(i1,j) + ack(i2,j) < ack(Suc(Suc(Suc(Suc(i1+i2)))), j)"; |
152 by (res_inst_tac [("j", "ack(Suc(1), ack(i1 + i2, j))")] less_trans 1); |
152 by (res_inst_tac [("j", "ack(Suc(1), ack(i1 + i2, j))")] less_trans 1); |
153 by (Asm_simp_tac 1); |
153 by (Asm_simp_tac 1); |
154 by (rtac (ack_nest_bound RS less_le_trans) 2); |
154 by (rtac (ack_nest_bound RS less_le_trans) 2); |
155 by (Asm_simp_tac 2); |
155 by (Asm_simp_tac 2); |
156 by (blast_tac (claset() addSIs [le_add1, le_add2] |
156 by (blast_tac (claset() addSIs [le_add1, le_add2] |
242 by (Asm_simp_tac 1); |
242 by (Asm_simp_tac 1); |
243 by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1); |
243 by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1); |
244 by (etac ack_less_mono2 1); |
244 by (etac ack_less_mono2 1); |
245 qed "PREC_case_lemma"; |
245 qed "PREC_case_lemma"; |
246 |
246 |
247 goal thy |
247 Goal |
248 "!!f g. [| ALL l. f l < ack(kf, list_add l); \ |
248 "!!f g. [| ALL l. f l < ack(kf, list_add l); \ |
249 \ ALL l. g l < ack(kg, 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)"; |
250 \ |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)"; |
251 by (rtac exI 1); |
251 by (rtac exI 1); |
252 by (rtac allI 1); |
252 by (rtac allI 1); |
253 by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1); |
253 by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1); |
254 by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1)); |
254 by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1)); |
255 qed "PREC_case"; |
255 qed "PREC_case"; |
256 |
256 |
257 goal thy "!!f. f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)"; |
257 Goal "!!f. f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)"; |
258 by (etac PRIMREC.induct 1); |
258 by (etac PRIMREC.induct 1); |
259 by (ALLGOALS |
259 by (ALLGOALS |
260 (blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, |
260 (blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, |
261 PREC_case]))); |
261 PREC_case]))); |
262 qed "ack_bounds_PRIMREC"; |
262 qed "ack_bounds_PRIMREC"; |
263 |
263 |
264 goal thy "(%l. case l of [] => 0 | x#l' => ack(x,x)) ~: PRIMREC"; |
264 Goal "(%l. case l of [] => 0 | x#l' => ack(x,x)) ~: PRIMREC"; |
265 by (rtac notI 1); |
265 by (rtac notI 1); |
266 by (etac (ack_bounds_PRIMREC RS exE) 1); |
266 by (etac (ack_bounds_PRIMREC RS exE) 1); |
267 by (rtac less_irrefl 1); |
267 by (rtac less_irrefl 1); |
268 by (dres_inst_tac [("x", "[x]")] spec 1); |
268 by (dres_inst_tac [("x", "[x]")] spec 1); |
269 by (Asm_full_simp_tac 1); |
269 by (Asm_full_simp_tac 1); |