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