equal
deleted
inserted
replaced
90 by (ALLGOALS (asm_simp_tac pr_ss)); |
90 by (ALLGOALS (asm_simp_tac pr_ss)); |
91 val ACK_in_primrec = result(); |
91 val ACK_in_primrec = result(); |
92 |
92 |
93 val ack_typechecks = |
93 val ack_typechecks = |
94 [ACK_in_primrec, primrec_into_fun RS apply_type, |
94 [ACK_in_primrec, primrec_into_fun RS apply_type, |
95 add_type, list_add_type, naturals_are_ordinals] @ |
95 add_type, list_add_type, nat_into_Ord] @ |
96 nat_typechecks @ List.intrs @ Primrec.intrs; |
96 nat_typechecks @ List.intrs @ Primrec.intrs; |
97 |
97 |
98 (*strict typechecking for the Ackermann proof; instantiates no vars*) |
98 (*strict typechecking for the Ackermann proof; instantiates no vars*) |
99 fun tc_tac rls = |
99 fun tc_tac rls = |
100 REPEAT |
100 REPEAT |
125 by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1); |
125 by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1); |
126 val ack_succ_succ = result(); |
126 val ack_succ_succ = result(); |
127 |
127 |
128 val ack_ss = |
128 val ack_ss = |
129 pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ, |
129 pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ, |
130 ack_type, naturals_are_ordinals]; |
130 ack_type, nat_into_Ord]; |
131 |
131 |
132 (*PROPERTY A 4*) |
132 (*PROPERTY A 4*) |
133 goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j < ack(i,j)"; |
133 goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j < ack(i,j)"; |
134 by (etac nat_induct 1); |
134 by (etac nat_induct 1); |
135 by (asm_simp_tac ack_ss 1); |
135 by (asm_simp_tac ack_ss 1); |
159 |
159 |
160 (*PROPERTY A 5', monotonicity for le *) |
160 (*PROPERTY A 5', monotonicity for le *) |
161 goal Primrec.thy |
161 goal Primrec.thy |
162 "!!i j k. [| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)"; |
162 "!!i j k. [| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)"; |
163 by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1); |
163 by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1); |
164 by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS naturals_are_ordinals] 1)); |
164 by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1)); |
165 val ack_le_mono2 = result(); |
165 val ack_le_mono2 = result(); |
166 |
166 |
167 (*PROPERTY A 6*) |
167 (*PROPERTY A 6*) |
168 goal Primrec.thy |
168 goal Primrec.thy |
169 "!!i j. [| i:nat; j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)"; |
169 "!!i j. [| i:nat; j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)"; |
192 |
192 |
193 (*PROPERTY A 7', monotonicity for le *) |
193 (*PROPERTY A 7', monotonicity for le *) |
194 goal Primrec.thy |
194 goal Primrec.thy |
195 "!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)"; |
195 "!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)"; |
196 by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1); |
196 by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1); |
197 by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS naturals_are_ordinals] 1)); |
197 by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1)); |
198 val ack_le_mono1 = result(); |
198 val ack_le_mono1 = result(); |
199 |
199 |
200 (*PROPERTY A 8*) |
200 (*PROPERTY A 8*) |
201 goal Primrec.thy "!!j. j:nat ==> ack(1,j) = succ(succ(j))"; |
201 goal Primrec.thy "!!j. j:nat ==> ack(1,j) = succ(succ(j))"; |
202 by (etac nat_induct 1); |
202 by (etac nat_induct 1); |
245 val ack_add_bound2 = result(); |
245 val ack_add_bound2 = result(); |
246 |
246 |
247 (*** MAIN RESULT ***) |
247 (*** MAIN RESULT ***) |
248 |
248 |
249 val ack2_ss = |
249 val ack2_ss = |
250 ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, |
250 ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, nat_into_Ord]; |
251 naturals_are_ordinals]; |
|
252 |
251 |
253 goalw Primrec.thy [SC_def] |
252 goalw Primrec.thy [SC_def] |
254 "!!l. l: list(nat) ==> SC ` l < ack(1, list_add(l))"; |
253 "!!l. l: list(nat) ==> SC ` l < ack(1, list_add(l))"; |
255 by (etac List.elim 1); |
254 by (etac List.elim 1); |
256 by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1); |
255 by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1); |