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