src/HOL/ex/Primrec.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 5069 3ea049f7979d
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/ex/Primrec
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  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 
    18 (** Useful special cases of evaluation ***)
    19 
    20 goalw thy [SC_def] "SC (x#l) = Suc x";
    21 by (Asm_simp_tac 1);
    22 qed "SC";
    23 
    24 goalw thy [CONST_def] "CONST k l = k";
    25 by (Asm_simp_tac 1);
    26 qed "CONST";
    27 
    28 goalw thy [PROJ_def] "PROJ(0) (x#l) = x";
    29 by (Asm_simp_tac 1);
    30 qed "PROJ_0";
    31 
    32 goalw thy [COMP_def] "COMP g [f] l = g [f l]";
    33 by (Asm_simp_tac 1);
    34 qed "COMP_1";
    35 
    36 goalw thy [PREC_def] "PREC f g (0#l) = f l";
    37 by (Asm_simp_tac 1);
    38 qed "PREC_0";
    39 
    40 goalw thy [PREC_def] "PREC f g (Suc x # l) = g (PREC f g (x#l) # x # l)";
    41 by (Asm_simp_tac 1);
    42 qed "PREC_Suc";
    43 
    44 Addsimps [SC, CONST, PROJ_0, COMP_1, PREC_0, PREC_Suc];
    45 
    46 
    47 Addsimps ack.rules;
    48 
    49 (*PROPERTY A 4*)
    50 goal thy "j < ack(i,j)";
    51 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
    52 by (ALLGOALS Asm_simp_tac);
    53 by (ALLGOALS trans_tac);
    54 qed "less_ack2";
    55 
    56 AddIffs [less_ack2];
    57 
    58 (*PROPERTY A 5-, the single-step lemma*)
    59 goal thy "ack(i,j) < ack(i, Suc(j))";
    60 by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
    61 by (ALLGOALS Asm_simp_tac);
    62 qed "ack_less_ack_Suc2";
    63 
    64 AddIffs [ack_less_ack_Suc2];
    65 
    66 (*PROPERTY A 5, monotonicity for < *)
    67 goal thy "j<k --> ack(i,j) < ack(i,k)";
    68 by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
    69 by (ALLGOALS Asm_simp_tac);
    70 by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1);
    71 qed_spec_mp "ack_less_mono2";
    72 
    73 (*PROPERTY A 5', monotonicity for<=*)
    74 goal thy "!!i j k. j<=k ==> ack(i,j)<=ack(i,k)";
    75 by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
    76 by (blast_tac (claset() addIs [ack_less_mono2]) 1);
    77 qed "ack_le_mono2";
    78 
    79 (*PROPERTY A 6*)
    80 goal thy "ack(i, Suc(j)) <= ack(Suc(i), j)";
    81 by (induct_tac "j" 1);
    82 by (ALLGOALS Asm_simp_tac);
    83 by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI, 
    84 			      le_trans]) 1);
    85 qed "ack2_le_ack1";
    86 
    87 AddIffs [ack2_le_ack1];
    88 
    89 (*PROPERTY A 7-, the single-step lemma*)
    90 goal thy "ack(i,j) < ack(Suc(i),j)";
    91 by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1);
    92 qed "ack_less_ack_Suc1";
    93 
    94 AddIffs [ack_less_ack_Suc1];
    95 
    96 (*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
    97 goal thy "i < ack(i,j)";
    98 by (induct_tac "i" 1);
    99 by (ALLGOALS Asm_simp_tac);
   100 by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1);
   101 qed "less_ack1";
   102 AddIffs [less_ack1];
   103 
   104 (*PROPERTY A 8*)
   105 goal thy "ack(1,j) = Suc(Suc(j))";
   106 by (induct_tac "j" 1);
   107 by (ALLGOALS Asm_simp_tac);
   108 qed "ack_1";
   109 Addsimps [ack_1];
   110 
   111 (*PROPERTY A 9*)
   112 goal thy "ack(Suc(1),j) = Suc(Suc(Suc(j+j)))";
   113 by (induct_tac "j" 1);
   114 by (ALLGOALS Asm_simp_tac);
   115 qed "ack_2";
   116 Addsimps [ack_2];
   117 
   118 
   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)";
   121 by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
   122 by (ALLGOALS Asm_full_simp_tac);
   123 by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2);
   124 by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1);
   125 by (ALLGOALS Asm_simp_tac);
   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);
   128 val lemma = result();
   129 
   130 goal thy "!!i j k. i<j ==> ack(i,k) < ack(j,k)";
   131 by (etac less_natE 1);
   132 by (blast_tac (claset() addSIs [lemma]) 1);
   133 qed "ack_less_mono1";
   134 
   135 (*PROPERTY A 7', monotonicity for<=*)
   136 goal thy "!!i j k. i<=j ==> ack(i,k)<=ack(j,k)";
   137 by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
   138 by (blast_tac (claset() addIs [ack_less_mono1]) 1);
   139 qed "ack_le_mono1";
   140 
   141 (*PROPERTY A 10*)
   142 goal thy "ack(i1, ack(i2,j)) < ack(Suc(Suc(i1+i2)), j)";
   143 by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1);
   144 by (Asm_simp_tac 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);
   147 by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1);
   148 qed "ack_nest_bound";
   149 
   150 (*PROPERTY A 11*)
   151 goal thy "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);
   153 by (Asm_simp_tac 1);
   154 by (rtac (ack_nest_bound RS less_le_trans) 2);
   155 by (Asm_simp_tac 2);
   156 by (blast_tac (claset() addSIs [le_add1, le_add2]
   157 		       addIs  [le_imp_less_Suc, ack_le_mono1, le_SucI, 
   158 			       add_le_mono]) 1);
   159 qed "ack_add_bound";
   160 
   161 (*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
   162   used k+4.  Quantified version must be nested EX k'. ALL i,j... *)
   163 goal thy "!!i j k. i < ack(k,j) ==> i+j < ack(Suc(Suc(Suc(Suc(k)))), j)";
   164 by (res_inst_tac [("j", "ack(k,j) + ack(0,j)")] less_trans 1);
   165 by (rtac (ack_add_bound RS less_le_trans) 2);
   166 by (Asm_simp_tac 2);
   167 by (REPEAT (ares_tac ([add_less_mono, less_ack2]) 1));
   168 qed "ack_add_bound2";
   169 
   170 
   171 (*** Inductive definition of the PR functions ***)
   172 
   173 (*** MAIN RESULT ***)
   174 
   175 goalw thy [SC_def] "SC l < ack(1, list_add l)";
   176 by (induct_tac "l" 1);
   177 by (ALLGOALS (simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc])));
   178 qed "SC_case";
   179 
   180 goal thy "CONST k l < ack(k, list_add l)";
   181 by (Simp_tac 1);
   182 qed "CONST_case";
   183 
   184 goalw thy [PROJ_def] "ALL i. PROJ i l < ack(0, list_add l)";
   185 by (Simp_tac 1);
   186 by (induct_tac "l" 1);
   187 by (ALLGOALS Asm_simp_tac);
   188 by (rtac allI 1);
   189 by (exhaust_tac "i" 1);
   190 by (asm_simp_tac (simpset() addsimps [le_add1, le_imp_less_Suc]) 1);
   191 by (Asm_simp_tac 1);
   192 by (blast_tac (claset() addIs [less_le_trans] 
   193                        addSIs [le_add2]) 1);
   194 qed_spec_mp "PROJ_case";
   195 
   196 (** COMP case **)
   197 
   198 goal thy
   199  "!!fs. fs : lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
   200 \      ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)";
   201 by (etac lists.induct 1);
   202 by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1);
   203 by Safe_tac;
   204 by (Asm_simp_tac 1);
   205 by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1);
   206 qed "COMP_map_lemma";
   207 
   208 goalw thy [COMP_def]
   209  "!!g. [| ALL l. g l < ack(kg, list_add l);           \
   210 \         fs: lists(PRIMREC Int {f. EX kf. ALL l. f l < ack(kf, list_add l)}) \
   211 \      |] ==> EX k. ALL l. COMP g fs  l < ack(k, list_add l)";
   212 by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1);
   213 by (etac (COMP_map_lemma RS exE) 1);
   214 by (rtac exI 1);
   215 by (rtac allI 1);
   216 by (REPEAT (dtac spec 1));
   217 by (etac less_trans 1);
   218 by (blast_tac (claset() addIs [ack_less_mono2, ack_nest_bound, less_trans]) 1);
   219 qed "COMP_case";
   220 
   221 (** PREC case **)
   222 
   223 goalw thy [PREC_def]
   224  "!!f g. [| ALL l. f l + list_add l < ack(kf, list_add l); \
   225 \           ALL l. g l + list_add l < ack(kg, list_add l)  \
   226 \        |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
   227 by (exhaust_tac "l" 1);
   228 by (ALLGOALS Asm_simp_tac);
   229 by (blast_tac (claset() addIs [less_trans]) 1);
   230 by (etac ssubst 1);  (*get rid of the needless assumption*)
   231 by (induct_tac "a" 1);
   232 by (ALLGOALS Asm_simp_tac);
   233 (*base case*)
   234 by (blast_tac (claset() addIs [le_add1 RS le_imp_less_Suc RS ack_less_mono1, 
   235 			      less_trans]) 1);
   236 (*induction step*)
   237 by (rtac (Suc_leI RS le_less_trans) 1);
   238 by (rtac (le_refl RS add_le_mono RS le_less_trans) 1);
   239 by (etac spec 2);
   240 by (asm_simp_tac (simpset() addsimps [le_add2]) 1);
   241 (*final part of the simplification*)
   242 by (Asm_simp_tac 1);
   243 by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1);
   244 by (etac ack_less_mono2 1);
   245 qed "PREC_case_lemma";
   246 
   247 goal thy
   248  "!!f g. [| ALL l. f l < ack(kf, 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)";
   251 by (rtac exI 1);
   252 by (rtac allI 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));
   255 qed "PREC_case";
   256 
   257 goal thy "!!f. f:PRIMREC ==> EX k. ALL l. f l < ack(k, list_add l)";
   258 by (etac PRIMREC.induct 1);
   259 by (ALLGOALS 
   260     (blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
   261 			       PREC_case])));
   262 qed "ack_bounds_PRIMREC";
   263 
   264 goal thy "(%l. case l of [] => 0 | x#l' => ack(x,x)) ~: PRIMREC";
   265 by (rtac notI 1);
   266 by (etac (ack_bounds_PRIMREC RS exE) 1);
   267 by (rtac less_irrefl 1);
   268 by (dres_inst_tac [("x", "[x]")] spec 1);
   269 by (Asm_full_simp_tac 1);
   270 qed "ack_not_PRIMREC";
   271