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