src/ZF/ex/primrec0.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 279 7738aed3f84d
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
lcp@16
     1
(*  Title: 	ZF/ex/primrec
lcp@16
     2
    ID:         $Id$
lcp@16
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@16
     4
    Copyright   1993  University of Cambridge
lcp@16
     5
lcp@16
     6
Primitive Recursive Functions
lcp@16
     7
lcp@16
     8
Proof adopted from
lcp@16
     9
Nora Szasz, 
lcp@16
    10
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
lcp@16
    11
In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
lcp@71
    12
lcp@71
    13
See also E. Mendelson, Introduction to Mathematical Logic.
lcp@71
    14
(Van Nostrand, 1964), page 250, exercise 11.
lcp@16
    15
*)
lcp@16
    16
lcp@16
    17
open Primrec0;
lcp@16
    18
lcp@16
    19
val pr0_typechecks = 
lcp@16
    20
    nat_typechecks @ List.intrs @ 
lcp@16
    21
    [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type];
lcp@16
    22
lcp@16
    23
(** Useful special cases of evaluation ***)
lcp@16
    24
lcp@16
    25
val pr0_ss = arith_ss 
lcp@16
    26
    addsimps List.case_eqns
lcp@16
    27
    addsimps [list_rec_Nil, list_rec_Cons, 
lcp@16
    28
	      drop_0, drop_Nil, drop_succ_Cons,
lcp@16
    29
	      map_Nil, map_Cons]
lcp@16
    30
    setsolver (type_auto_tac pr0_typechecks);
lcp@16
    31
lcp@16
    32
goalw Primrec0.thy [SC_def]
lcp@16
    33
    "!!x l. [| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
lcp@16
    34
by (asm_simp_tac pr0_ss 1);
lcp@16
    35
val SC = result();
lcp@16
    36
lcp@16
    37
goalw Primrec0.thy [CONST_def]
lcp@16
    38
    "!!l. [| l: list(nat) |] ==> CONST(k) ` l = k";
lcp@16
    39
by (asm_simp_tac pr0_ss 1);
lcp@16
    40
val CONST = result();
lcp@16
    41
lcp@16
    42
goalw Primrec0.thy [PROJ_def]
lcp@16
    43
    "!!l. [| x: nat;  l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
lcp@16
    44
by (asm_simp_tac pr0_ss 1);
lcp@16
    45
val PROJ_0 = result();
lcp@16
    46
lcp@16
    47
goalw Primrec0.thy [COMP_def]
lcp@16
    48
    "!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
lcp@16
    49
by (asm_simp_tac pr0_ss 1);
lcp@16
    50
val COMP_1 = result();
lcp@16
    51
lcp@16
    52
goalw Primrec0.thy [PREC_def]
lcp@16
    53
    "!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
lcp@16
    54
by (asm_simp_tac pr0_ss 1);
lcp@16
    55
val PREC_0 = result();
lcp@16
    56
lcp@16
    57
goalw Primrec0.thy [PREC_def]
lcp@16
    58
    "!!l. [| x:nat;  l: list(nat) |] ==>  \
lcp@16
    59
\         PREC(f,g) ` (Cons(succ(x),l)) = \
lcp@16
    60
\         g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
lcp@16
    61
by (asm_simp_tac pr0_ss 1);
lcp@16
    62
val PREC_succ = result();
lcp@16
    63
lcp@16
    64
(*** Inductive definition of the PR functions ***)
lcp@16
    65
lcp@16
    66
structure Primrec = Inductive_Fun
lcp@279
    67
 (val thy        = Primrec0.thy
lcp@279
    68
  val rec_doms   = [("primrec", "list(nat)->nat")]
lcp@279
    69
  val sintrs     = 
lcp@16
    70
      ["SC : primrec",
lcp@16
    71
       "k: nat ==> CONST(k) : primrec",
lcp@16
    72
       "i: nat ==> PROJ(i) : primrec",
lcp@279
    73
       "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec",
lcp@279
    74
       "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"]
lcp@279
    75
  val monos      = [list_mono]
lcp@279
    76
  val con_defs   = [SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]
lcp@16
    77
  val type_intrs = pr0_typechecks
lcp@16
    78
  val type_elims = []);
lcp@16
    79
lcp@279
    80
lcp@16
    81
(* c: primrec ==> c: list(nat) -> nat *)
lcp@16
    82
val primrec_into_fun = Primrec.dom_subset RS subsetD;
lcp@16
    83
lcp@16
    84
val pr_ss = pr0_ss 
lcp@16
    85
    setsolver (type_auto_tac ([primrec_into_fun] @ 
lcp@16
    86
			      pr0_typechecks @ Primrec.intrs));
lcp@16
    87
lcp@16
    88
goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
lcp@16
    89
by (etac nat_induct 1);
lcp@16
    90
by (ALLGOALS (asm_simp_tac pr_ss));
lcp@16
    91
val ACK_in_primrec = result();
lcp@16
    92
lcp@16
    93
val ack_typechecks =
lcp@16
    94
    [ACK_in_primrec, primrec_into_fun RS apply_type,
lcp@16
    95
     add_type, list_add_type, naturals_are_ordinals] @ 
lcp@16
    96
    nat_typechecks @ List.intrs @ Primrec.intrs;
lcp@16
    97
lcp@16
    98
(*strict typechecking for the Ackermann proof; instantiates no vars*)
lcp@16
    99
fun tc_tac rls =
lcp@16
   100
    REPEAT
lcp@16
   101
      (SOMEGOAL (test_assume_tac ORELSE' match_tac (rls @ ack_typechecks)));
lcp@16
   102
lcp@16
   103
goal Primrec.thy "!!i j. [| i:nat;  j:nat |] ==>  ack(i,j): nat";
lcp@16
   104
by (tc_tac []);
lcp@16
   105
val ack_type = result();
lcp@16
   106
lcp@16
   107
(** Ackermann's function cases **)
lcp@16
   108
lcp@16
   109
(*PROPERTY A 1*)
lcp@16
   110
goalw Primrec0.thy [ACK_def] "!!j. j:nat ==> ack(0,j) = succ(j)";
lcp@16
   111
by (asm_simp_tac (pr0_ss addsimps [SC]) 1);
lcp@16
   112
val ack_0 = result();
lcp@16
   113
lcp@16
   114
(*PROPERTY A 2*)
lcp@16
   115
goalw Primrec0.thy [ACK_def] "ack(succ(i), 0) = ack(i,1)";
lcp@16
   116
by (asm_simp_tac (pr0_ss addsimps [CONST,PREC_0]) 1);
lcp@16
   117
val ack_succ_0 = result();
lcp@16
   118
lcp@16
   119
(*PROPERTY A 3*)
lcp@16
   120
(*Could be proved in Primrec0, like the previous two cases, but using
lcp@16
   121
  primrec_into_fun makes type-checking easier!*)
lcp@16
   122
goalw Primrec.thy [ACK_def]
lcp@16
   123
    "!!i j. [| i:nat;  j:nat |] ==> \
lcp@16
   124
\           ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
lcp@16
   125
by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
lcp@16
   126
val ack_succ_succ = result();
lcp@16
   127
lcp@16
   128
val ack_ss = 
lcp@16
   129
    pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ, 
lcp@16
   130
		    ack_type, naturals_are_ordinals];
lcp@16
   131
lcp@16
   132
(*PROPERTY A 4*)
lcp@29
   133
goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j < ack(i,j)";
lcp@16
   134
by (etac nat_induct 1);
lcp@16
   135
by (asm_simp_tac ack_ss 1);
lcp@16
   136
by (rtac ballI 1);
lcp@16
   137
by (eres_inst_tac [("n","j")] nat_induct 1);
lcp@29
   138
by (DO_GOAL [rtac (nat_0I RS nat_0_le RS lt_trans),
lcp@29
   139
	     asm_simp_tac ack_ss] 1);
lcp@29
   140
by (DO_GOAL [etac (succ_leI RS lt_trans1),
lcp@29
   141
	     asm_simp_tac ack_ss] 1);
lcp@29
   142
val lt_ack2_lemma = result();
lcp@29
   143
val lt_ack2 = standard (lt_ack2_lemma RS bspec);
lcp@16
   144
lcp@16
   145
(*PROPERTY A 5-, the single-step lemma*)
lcp@29
   146
goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
lcp@16
   147
by (etac nat_induct 1);
lcp@29
   148
by (ALLGOALS (asm_simp_tac (ack_ss addsimps [lt_ack2])));
lcp@29
   149
val ack_lt_ack_succ2 = result();
lcp@16
   150
lcp@16
   151
(*PROPERTY A 5, monotonicity for < *)
lcp@29
   152
goal Primrec.thy "!!i j k. [| j<k; i:nat; k:nat |] ==> ack(i,j) < ack(i,k)";
lcp@29
   153
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
lcp@29
   154
by (etac succ_lt_induct 1);
lcp@16
   155
by (assume_tac 1);
lcp@29
   156
by (rtac lt_trans 2);
lcp@29
   157
by (REPEAT (ares_tac ([ack_lt_ack_succ2, ack_type] @ pr0_typechecks) 1));
lcp@29
   158
val ack_lt_mono2 = result();
lcp@16
   159
lcp@56
   160
(*PROPERTY A 5', monotonicity for le *)
lcp@16
   161
goal Primrec.thy
lcp@29
   162
    "!!i j k. [| j le k;  i: nat;  k:nat |] ==> ack(i,j) le ack(i,k)";
lcp@29
   163
by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
lcp@29
   164
by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS naturals_are_ordinals] 1));
lcp@29
   165
val ack_le_mono2 = result();
lcp@16
   166
lcp@16
   167
(*PROPERTY A 6*)
lcp@16
   168
goal Primrec.thy
lcp@29
   169
    "!!i j. [| i:nat;  j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
lcp@16
   170
by (nat_ind_tac "j" [] 1);
lcp@29
   171
by (ALLGOALS (asm_simp_tac ack_ss));
lcp@29
   172
by (rtac ack_le_mono2 1);
lcp@29
   173
by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
lcp@29
   174
by (REPEAT (ares_tac (ack_typechecks) 1));
lcp@29
   175
val ack2_le_ack1 = result();
lcp@16
   176
lcp@16
   177
(*PROPERTY A 7-, the single-step lemma*)
lcp@29
   178
goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) < ack(succ(i),j)";
lcp@29
   179
by (rtac (ack_lt_mono2 RS lt_trans2) 1);
lcp@29
   180
by (rtac ack2_le_ack1 4);
lcp@29
   181
by (REPEAT (ares_tac ([nat_le_refl, ack_type] @ pr0_typechecks) 1));
lcp@29
   182
val ack_lt_ack_succ1 = result();
lcp@16
   183
lcp@16
   184
(*PROPERTY A 7, monotonicity for < *)
lcp@29
   185
goal Primrec.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> ack(i,k) < ack(j,k)";
lcp@29
   186
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
lcp@29
   187
by (etac succ_lt_induct 1);
lcp@16
   188
by (assume_tac 1);
lcp@29
   189
by (rtac lt_trans 2);
lcp@29
   190
by (REPEAT (ares_tac ([ack_lt_ack_succ1, ack_type] @ pr0_typechecks) 1));
lcp@29
   191
val ack_lt_mono1 = result();
lcp@16
   192
lcp@29
   193
(*PROPERTY A 7', monotonicity for le *)
lcp@16
   194
goal Primrec.thy
lcp@29
   195
    "!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)";
lcp@29
   196
by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
lcp@29
   197
by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS naturals_are_ordinals] 1));
lcp@29
   198
val ack_le_mono1 = result();
lcp@16
   199
lcp@16
   200
(*PROPERTY A 8*)
lcp@16
   201
goal Primrec.thy "!!j. j:nat ==> ack(1,j) = succ(succ(j))";
lcp@16
   202
by (etac nat_induct 1);
lcp@16
   203
by (ALLGOALS (asm_simp_tac ack_ss));
lcp@16
   204
val ack_1 = result();
lcp@16
   205
lcp@16
   206
(*PROPERTY A 9*)
lcp@16
   207
goal Primrec.thy "!!j. j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
lcp@16
   208
by (etac nat_induct 1);
lcp@16
   209
by (ALLGOALS (asm_simp_tac (ack_ss addsimps [ack_1, add_succ_right])));
lcp@16
   210
val ack_2 = result();
lcp@16
   211
lcp@16
   212
(*PROPERTY A 10*)
lcp@16
   213
goal Primrec.thy
lcp@16
   214
    "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
lcp@29
   215
\               ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)";
lcp@29
   216
by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1);
lcp@16
   217
by (asm_simp_tac ack_ss 1);
lcp@29
   218
by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
lcp@29
   219
by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 5);
lcp@16
   220
by (tc_tac []);
lcp@16
   221
val ack_nest_bound = result();
lcp@16
   222
lcp@16
   223
(*PROPERTY A 11*)
lcp@16
   224
goal Primrec.thy
lcp@29
   225
    "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
lcp@29
   226
\          ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)";
lcp@29
   227
by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1);
lcp@29
   228
by (asm_simp_tac (ack_ss addsimps [ack_2]) 1);
lcp@29
   229
by (rtac (ack_nest_bound RS lt_trans2) 2);
lcp@29
   230
by (asm_simp_tac ack_ss 5);
lcp@29
   231
by (rtac (add_le_mono RS leI RS leI) 1);
lcp@29
   232
by (REPEAT (ares_tac ([add_le_self, add_le_self2, ack_le_mono1] @
lcp@29
   233
                      ack_typechecks) 1));
lcp@16
   234
val ack_add_bound = result();
lcp@16
   235
lcp@29
   236
(*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
lcp@29
   237
  used k#+4.  Quantified version must be nested EX k'. ALL i,j... *)
lcp@16
   238
goal Primrec.thy
lcp@29
   239
    "!!i j k. [| i < ack(k,j);  j:nat;  k:nat |] ==> \
lcp@29
   240
\             i#+j < ack(succ(succ(succ(succ(k)))), j)";
lcp@29
   241
by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
lcp@29
   242
by (rtac (ack_add_bound RS lt_trans2) 2);
lcp@29
   243
by (asm_simp_tac (ack_ss addsimps [add_0_right]) 5);
lcp@29
   244
by (REPEAT (ares_tac ([add_lt_mono, lt_ack2] @ ack_typechecks) 1));
lcp@16
   245
val ack_add_bound2 = result();
lcp@16
   246
lcp@16
   247
(*** MAIN RESULT ***)
lcp@16
   248
lcp@16
   249
val ack2_ss =
lcp@16
   250
    ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, 
lcp@16
   251
		     naturals_are_ordinals];
lcp@16
   252
lcp@16
   253
goalw Primrec.thy [SC_def]
lcp@29
   254
    "!!l. l: list(nat) ==> SC ` l < ack(1, list_add(l))";
lcp@16
   255
by (etac List.elim 1);
lcp@16
   256
by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1);
lcp@29
   257
by (asm_simp_tac (ack2_ss addsimps [ack_1, add_le_self]) 1);
lcp@16
   258
val SC_case = result();
lcp@16
   259
lcp@29
   260
(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
lcp@29
   261
goal Primrec.thy "!!j. [| i:nat; j:nat |] ==> i < ack(i,j)";
lcp@16
   262
by (etac nat_induct 1);
lcp@29
   263
by (asm_simp_tac (ack_ss addsimps [nat_0_le]) 1);
lcp@29
   264
by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
lcp@16
   265
by (tc_tac []);
lcp@29
   266
val lt_ack1 = result();
lcp@16
   267
lcp@16
   268
goalw Primrec.thy [CONST_def]
lcp@29
   269
    "!!l. [| l: list(nat);  k: nat |] ==> CONST(k) ` l < ack(k, list_add(l))";
lcp@29
   270
by (asm_simp_tac (ack2_ss addsimps [lt_ack1]) 1);
lcp@16
   271
val CONST_case = result();
lcp@16
   272
lcp@16
   273
goalw Primrec.thy [PROJ_def]
lcp@29
   274
    "!!l. l: list(nat) ==> ALL i:nat. PROJ(i) ` l < ack(0, list_add(l))";
lcp@16
   275
by (asm_simp_tac ack2_ss 1);
lcp@16
   276
by (etac List.induct 1);
lcp@29
   277
by (asm_simp_tac (ack2_ss addsimps [nat_0_le]) 1);
lcp@16
   278
by (asm_simp_tac ack2_ss 1);
lcp@16
   279
by (rtac ballI 1);
lcp@16
   280
by (eres_inst_tac [("n","x")] natE 1);
lcp@29
   281
by (asm_simp_tac (ack2_ss addsimps [add_le_self]) 1);
lcp@16
   282
by (asm_simp_tac ack2_ss 1);
lcp@29
   283
by (etac (bspec RS lt_trans2) 1);
lcp@29
   284
by (rtac (add_le_self2 RS succ_leI) 2);
lcp@29
   285
by (tc_tac []);
lcp@16
   286
val PROJ_case_lemma = result();
lcp@16
   287
val PROJ_case = PROJ_case_lemma RS bspec;
lcp@16
   288
lcp@16
   289
(** COMP case **)
lcp@16
   290
lcp@16
   291
goal Primrec.thy
lcp@16
   292
 "!!fs. fs : list({f: primrec .					\
lcp@16
   293
\              	   EX kf:nat. ALL l:list(nat). 			\
lcp@29
   294
\		    	      f`l < ack(kf, list_add(l))})	\
lcp@16
   295
\      ==> EX k:nat. ALL l: list(nat). 				\
lcp@29
   296
\                list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
lcp@16
   297
by (etac List.induct 1);
lcp@16
   298
by (DO_GOAL [res_inst_tac [("x","0")] bexI,
lcp@29
   299
	     asm_simp_tac (ack2_ss addsimps [lt_ack1, nat_0_le]),
lcp@16
   300
	     resolve_tac nat_typechecks] 1);
lcp@16
   301
by (safe_tac ZF_cs);
lcp@16
   302
by (asm_simp_tac ack2_ss 1);
lcp@16
   303
by (rtac (ballI RS bexI) 1);
lcp@29
   304
by (rtac (add_lt_mono RS lt_trans) 1);
lcp@16
   305
by (REPEAT (FIRSTGOAL (etac bspec)));
lcp@29
   306
by (rtac ack_add_bound 5);
lcp@29
   307
by (tc_tac []);
lcp@16
   308
val COMP_map_lemma = result();
lcp@16
   309
lcp@16
   310
goalw Primrec.thy [COMP_def]
lcp@16
   311
 "!!g. [| g: primrec;  kg: nat;					\
lcp@29
   312
\         ALL l:list(nat). g`l < ack(kg, list_add(l));		\
lcp@16
   313
\         fs : list({f: primrec .				\
lcp@16
   314
\                    EX kf:nat. ALL l:list(nat). 		\
lcp@29
   315
\		    	f`l < ack(kf, list_add(l))}) 		\
lcp@29
   316
\      |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l < ack(k, list_add(l))";
lcp@16
   317
by (asm_simp_tac ZF_ss 1);
lcp@16
   318
by (forward_tac [list_CollectD] 1);
lcp@16
   319
by (etac (COMP_map_lemma RS bexE) 1);
lcp@16
   320
by (rtac (ballI RS bexI) 1);
lcp@29
   321
by (etac (bspec RS lt_trans) 1);
lcp@29
   322
by (rtac lt_trans 2);
lcp@16
   323
by (rtac ack_nest_bound 3);
lcp@29
   324
by (etac (bspec RS ack_lt_mono2) 2);
lcp@16
   325
by (tc_tac [map_type]);
lcp@16
   326
val COMP_case = result();
lcp@16
   327
lcp@16
   328
(** PREC case **)
lcp@16
   329
lcp@16
   330
goalw Primrec.thy [PREC_def]
lcp@29
   331
 "!!f g. [| ALL l:list(nat). f`l #+ list_add(l) < ack(kf, list_add(l));	\
lcp@29
   332
\           ALL l:list(nat). g`l #+ list_add(l) < ack(kg, list_add(l));	\
lcp@29
   333
\           f: primrec;  kf: nat;					\
lcp@16
   334
\           g: primrec;  kg: nat;					\
lcp@16
   335
\           l: list(nat)						\
lcp@29
   336
\        |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))";
lcp@16
   337
by (etac List.elim 1);
lcp@29
   338
by (asm_simp_tac (ack2_ss addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
lcp@16
   339
by (asm_simp_tac ack2_ss 1);
lcp@128
   340
by (etac ssubst 1);  (*get rid of the needless assumption*)
lcp@16
   341
by (eres_inst_tac [("n","a")] nat_induct 1);
lcp@29
   342
(*base case*)
lcp@29
   343
by (DO_GOAL [asm_simp_tac ack2_ss, rtac lt_trans, etac bspec,
lcp@29
   344
	     assume_tac, rtac (add_le_self RS ack_lt_mono1),
lcp@29
   345
	     REPEAT o ares_tac (ack_typechecks)] 1);
lcp@29
   346
(*ind step*)
lcp@16
   347
by (asm_simp_tac (ack2_ss addsimps [add_succ_right]) 1);
lcp@29
   348
by (rtac (succ_leI RS lt_trans1) 1);
lcp@29
   349
by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
lcp@16
   350
by (etac bspec 2);
lcp@29
   351
by (rtac (nat_le_refl RS add_le_mono) 1);
lcp@16
   352
by (tc_tac []);
lcp@29
   353
by (asm_simp_tac (ack2_ss addsimps [add_le_self2]) 1);
lcp@16
   354
(*final part of the simplification*)
lcp@29
   355
by (asm_simp_tac ack2_ss 1);
lcp@29
   356
by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
lcp@29
   357
by (etac ack_lt_mono2 5);
lcp@16
   358
by (tc_tac []);
lcp@16
   359
val PREC_case_lemma = result();
lcp@16
   360
lcp@16
   361
goal Primrec.thy
lcp@16
   362
 "!!f g. [| f: primrec;  kf: nat;				\
lcp@16
   363
\           g: primrec;  kg: nat;				\
lcp@29
   364
\           ALL l:list(nat). f`l < ack(kf, list_add(l));	\
lcp@29
   365
\           ALL l:list(nat). g`l < ack(kg, list_add(l)) 	\
lcp@16
   366
\        |] ==> EX k:nat. ALL l: list(nat). 			\
lcp@29
   367
\		    PREC(f,g)`l< ack(k, list_add(l))";
lcp@16
   368
by (rtac (ballI RS bexI) 1);
lcp@29
   369
by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
lcp@29
   370
by (REPEAT
lcp@16
   371
    (SOMEGOAL
lcp@16
   372
     (FIRST' [test_assume_tac,
lcp@29
   373
	      match_tac (ack_typechecks),
lcp@29
   374
	      rtac (ack_add_bound2 RS ballI) THEN' etac bspec])));
lcp@16
   375
val PREC_case = result();
lcp@16
   376
lcp@16
   377
goal Primrec.thy
lcp@29
   378
    "!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
lcp@16
   379
by (etac Primrec.induct 1);
lcp@16
   380
by (safe_tac ZF_cs);
lcp@16
   381
by (DEPTH_SOLVE
lcp@16
   382
    (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
lcp@16
   383
		       bexI, ballI] @ nat_typechecks) 1));
lcp@16
   384
val ack_bounds_primrec = result();
lcp@16
   385
lcp@16
   386
goal Primrec.thy
lcp@16
   387
    "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec";
lcp@16
   388
by (rtac notI 1);
lcp@16
   389
by (etac (ack_bounds_primrec RS bexE) 1);
lcp@29
   390
by (rtac lt_anti_refl 1);
lcp@16
   391
by (dres_inst_tac [("x", "[x]")] bspec 1);
lcp@16
   392
by (asm_simp_tac ack2_ss 1);
lcp@16
   393
by (asm_full_simp_tac (ack2_ss addsimps [add_0_right]) 1);
lcp@16
   394
val ack_not_primrec = result();
lcp@16
   395