src/ZF/ex/Primrec.ML
author paulson
Fri Jan 29 17:08:20 1999 +0100 (1999-01-29)
changeset 6163 be8234f37e48
parent 6154 6a00a5baef2b
child 7499 23e090051cb8
permissions -rw-r--r--
expandshort
clasohm@1461
     1
(*  Title:      ZF/ex/Primrec
lcp@515
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@515
     4
    Copyright   1994  University of Cambridge
lcp@515
     5
lcp@515
     6
Primitive Recursive Functions
lcp@515
     7
lcp@515
     8
Proof adopted from
lcp@515
     9
Nora Szasz, 
lcp@515
    10
A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
lcp@515
    11
In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
lcp@515
    12
lcp@515
    13
See also E. Mendelson, Introduction to Mathematical Logic.
lcp@515
    14
(Van Nostrand, 1964), page 250, exercise 11.
lcp@515
    15
*)
lcp@515
    16
lcp@515
    17
(*** Inductive definition of the PR functions ***)
lcp@515
    18
paulson@6044
    19
(* c: prim_rec ==> c: list(nat) -> nat *)
paulson@6044
    20
val prim_rec_into_fun = prim_rec.dom_subset RS subsetD;
lcp@515
    21
paulson@6153
    22
AddTCs ([prim_rec_into_fun] @ prim_rec.intrs);
lcp@515
    23
paulson@6071
    24
Goal "i:nat ==> ACK(i): prim_rec";
paulson@6070
    25
by (induct_tac "i" 1);
paulson@2469
    26
by (ALLGOALS Asm_simp_tac);
paulson@6044
    27
qed "ACK_in_prim_rec";
lcp@515
    28
paulson@6153
    29
AddTCs [ACK_in_prim_rec, prim_rec_into_fun RS apply_type,
paulson@6153
    30
	list_add_type, nat_into_Ord, rec_type];
lcp@515
    31
paulson@5137
    32
Goal "[| i:nat;  j:nat |] ==>  ack(i,j): nat";
paulson@6071
    33
by Auto_tac;
clasohm@760
    34
qed "ack_type";
paulson@6153
    35
AddTCs [ack_type];
lcp@515
    36
lcp@515
    37
(** Ackermann's function cases **)
lcp@515
    38
lcp@515
    39
(*PROPERTY A 1*)
paulson@6071
    40
Goal "j:nat ==> ack(0,j) = succ(j)";
wenzelm@4091
    41
by (asm_simp_tac (simpset() addsimps [SC]) 1);
clasohm@782
    42
qed "ack_0";
lcp@515
    43
lcp@515
    44
(*PROPERTY A 2*)
paulson@6071
    45
Goal "ack(succ(i), 0) = ack(i,1)";
wenzelm@4091
    46
by (asm_simp_tac (simpset() addsimps [CONST,PREC_0]) 1);
clasohm@782
    47
qed "ack_succ_0";
lcp@515
    48
lcp@515
    49
(*PROPERTY A 3*)
paulson@6071
    50
Goal "[| i:nat;  j:nat |]  \
paulson@6071
    51
\     ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
wenzelm@4091
    52
by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
clasohm@782
    53
qed "ack_succ_succ";
lcp@515
    54
paulson@2469
    55
Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type, nat_into_Ord];
paulson@6071
    56
Delsimps [ACK_0, ACK_succ];
paulson@6071
    57
lcp@515
    58
lcp@515
    59
(*PROPERTY A 4*)
paulson@5137
    60
Goal "i:nat ==> ALL j:nat. j < ack(i,j)";
paulson@6070
    61
by (induct_tac "i" 1);
paulson@2469
    62
by (Asm_simp_tac 1);
lcp@515
    63
by (rtac ballI 1);
paulson@6070
    64
by (induct_tac "j" 1);
paulson@6071
    65
by (etac (succ_leI RS lt_trans1) 2);
paulson@6071
    66
by (rtac (nat_0I RS nat_0_le RS lt_trans) 1);
paulson@6071
    67
by Auto_tac;
paulson@6112
    68
qed_spec_mp "lt_ack2";
lcp@515
    69
lcp@515
    70
(*PROPERTY A 5-, the single-step lemma*)
paulson@5137
    71
Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
paulson@6070
    72
by (induct_tac "i" 1);
wenzelm@4091
    73
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack2])));
clasohm@782
    74
qed "ack_lt_ack_succ2";
lcp@515
    75
lcp@515
    76
(*PROPERTY A 5, monotonicity for < *)
paulson@5137
    77
Goal "[| j<k; i:nat; k:nat |] ==> ack(i,j) < ack(i,k)";
lcp@515
    78
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
lcp@515
    79
by (etac succ_lt_induct 1);
lcp@515
    80
by (assume_tac 1);
lcp@515
    81
by (rtac lt_trans 2);
paulson@6153
    82
by (auto_tac (claset() addIs [ack_lt_ack_succ2], simpset()));
clasohm@760
    83
qed "ack_lt_mono2";
lcp@515
    84
lcp@515
    85
(*PROPERTY A 5', monotonicity for le *)
paulson@5147
    86
Goal "[| j le k;  i: nat;  k:nat |] ==> ack(i,j) le ack(i,k)";
wenzelm@3840
    87
by (res_inst_tac [("f", "%j. ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
lcp@515
    88
by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
clasohm@782
    89
qed "ack_le_mono2";
lcp@515
    90
lcp@515
    91
(*PROPERTY A 6*)
paulson@5147
    92
Goal "[| i:nat;  j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
paulson@6070
    93
by (induct_tac "j" 1);
paulson@2469
    94
by (ALLGOALS Asm_simp_tac);
lcp@515
    95
by (rtac ack_le_mono2 1);
lcp@515
    96
by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
paulson@6153
    97
by Auto_tac;
clasohm@760
    98
qed "ack2_le_ack1";
lcp@515
    99
lcp@515
   100
(*PROPERTY A 7-, the single-step lemma*)
paulson@5137
   101
Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(succ(i),j)";
lcp@515
   102
by (rtac (ack_lt_mono2 RS lt_trans2) 1);
lcp@515
   103
by (rtac ack2_le_ack1 4);
paulson@6153
   104
by Auto_tac;
clasohm@760
   105
qed "ack_lt_ack_succ1";
lcp@515
   106
lcp@515
   107
(*PROPERTY A 7, monotonicity for < *)
paulson@5137
   108
Goal "[| i<j; j:nat; k:nat |] ==> ack(i,k) < ack(j,k)";
lcp@515
   109
by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
lcp@515
   110
by (etac succ_lt_induct 1);
lcp@515
   111
by (assume_tac 1);
lcp@515
   112
by (rtac lt_trans 2);
paulson@6153
   113
by (auto_tac (claset() addIs [ack_lt_ack_succ1], simpset()));
clasohm@760
   114
qed "ack_lt_mono1";
lcp@515
   115
lcp@515
   116
(*PROPERTY A 7', monotonicity for le *)
paulson@5147
   117
Goal "[| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)";
wenzelm@3840
   118
by (res_inst_tac [("f", "%j. ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
lcp@515
   119
by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
clasohm@760
   120
qed "ack_le_mono1";
lcp@515
   121
lcp@515
   122
(*PROPERTY A 8*)
paulson@5137
   123
Goal "j:nat ==> ack(1,j) = succ(succ(j))";
paulson@6070
   124
by (induct_tac "j" 1);
paulson@2469
   125
by (ALLGOALS Asm_simp_tac);
clasohm@760
   126
qed "ack_1";
lcp@515
   127
lcp@515
   128
(*PROPERTY A 9*)
paulson@5137
   129
Goal "j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
paulson@6070
   130
by (induct_tac "j" 1);
wenzelm@4091
   131
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ack_1, add_succ_right])));
clasohm@782
   132
qed "ack_2";
lcp@515
   133
lcp@515
   134
(*PROPERTY A 10*)
paulson@5147
   135
Goal "[| i1:nat; i2:nat; j:nat |] ==> \
lcp@515
   136
\               ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)";
lcp@515
   137
by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1);
paulson@2469
   138
by (Asm_simp_tac 1);
lcp@515
   139
by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
lcp@515
   140
by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 5);
paulson@6071
   141
by Auto_tac;
clasohm@760
   142
qed "ack_nest_bound";
lcp@515
   143
lcp@515
   144
(*PROPERTY A 11*)
paulson@5147
   145
Goal "[| i1:nat; i2:nat; j:nat |] ==> \
lcp@515
   146
\          ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)";
lcp@515
   147
by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1);
wenzelm@4091
   148
by (asm_simp_tac (simpset() addsimps [ack_2]) 1);
lcp@515
   149
by (rtac (ack_nest_bound RS lt_trans2) 2);
paulson@2469
   150
by (Asm_simp_tac 5);
lcp@515
   151
by (rtac (add_le_mono RS leI RS leI) 1);
paulson@6153
   152
by (auto_tac (claset() addIs [add_le_self, add_le_self2, ack_le_mono1], 
paulson@6153
   153
	      simpset()));
clasohm@760
   154
qed "ack_add_bound";
lcp@515
   155
lcp@515
   156
(*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
lcp@515
   157
  used k#+4.  Quantified version must be nested EX k'. ALL i,j... *)
paulson@5147
   158
Goal "[| i < ack(k,j);  j:nat;  k:nat |] ==> \
lcp@515
   159
\             i#+j < ack(succ(succ(succ(succ(k)))), j)";
lcp@515
   160
by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
lcp@515
   161
by (rtac (ack_add_bound RS lt_trans2) 2);
paulson@6163
   162
by (rtac add_lt_mono 1);
paulson@6153
   163
by Auto_tac;
clasohm@782
   164
qed "ack_add_bound2";
lcp@515
   165
lcp@515
   166
(*** MAIN RESULT ***)
lcp@515
   167
paulson@2469
   168
Addsimps [list_add_type, nat_into_Ord];
lcp@515
   169
paulson@6065
   170
Goalw [SC_def] "l: list(nat) ==> SC ` l < ack(1, list_add(l))";
paulson@6065
   171
by (exhaust_tac "l" 1);
wenzelm@4091
   172
by (asm_simp_tac (simpset() addsimps [succ_iff]) 1);
wenzelm@4091
   173
by (asm_simp_tac (simpset() addsimps [ack_1, add_le_self]) 1);
clasohm@782
   174
qed "SC_case";
lcp@515
   175
lcp@515
   176
(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
paulson@5137
   177
Goal "[| i:nat; j:nat |] ==> i < ack(i,j)";
paulson@6070
   178
by (induct_tac "i" 1);
wenzelm@4091
   179
by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
lcp@515
   180
by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
paulson@6071
   181
by Auto_tac;
clasohm@760
   182
qed "lt_ack1";
lcp@515
   183
wenzelm@5068
   184
Goalw [CONST_def]
paulson@5147
   185
    "[| l: list(nat);  k: nat |] ==> CONST(k) ` l < ack(k, list_add(l))";
wenzelm@4091
   186
by (asm_simp_tac (simpset() addsimps [lt_ack1]) 1);
clasohm@782
   187
qed "CONST_case";
lcp@515
   188
wenzelm@5068
   189
Goalw [PROJ_def]
paulson@5147
   190
    "l: list(nat) ==> ALL i:nat. PROJ(i) ` l < ack(0, list_add(l))";
paulson@2469
   191
by (Asm_simp_tac 1);
lcp@515
   192
by (etac list.induct 1);
wenzelm@4091
   193
by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
paulson@2469
   194
by (Asm_simp_tac 1);
lcp@515
   195
by (rtac ballI 1);
lcp@515
   196
by (eres_inst_tac [("n","x")] natE 1);
wenzelm@4091
   197
by (asm_simp_tac (simpset() addsimps [add_le_self]) 1);
paulson@2469
   198
by (Asm_simp_tac 1);
lcp@515
   199
by (etac (bspec RS lt_trans2) 1);
lcp@515
   200
by (rtac (add_le_self2 RS succ_leI) 2);
paulson@6071
   201
by Auto_tac;
paulson@6154
   202
qed_spec_mp "PROJ_case";
lcp@515
   203
lcp@515
   204
(** COMP case **)
lcp@515
   205
paulson@6044
   206
Goal "fs : list({f: prim_rec .                                 \
clasohm@1461
   207
\                  EX kf:nat. ALL l:list(nat).                  \
clasohm@1461
   208
\                             f`l < ack(kf, list_add(l))})      \
clasohm@1461
   209
\      ==> EX k:nat. ALL l: list(nat).                          \
lcp@515
   210
\                list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
lcp@515
   211
by (etac list.induct 1);
paulson@6071
   212
by (res_inst_tac [("x","0")] bexI 1);
paulson@6154
   213
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le])));
paulson@6154
   214
by (Clarify_tac 1);
lcp@515
   215
by (rtac (ballI RS bexI) 1);
lcp@515
   216
by (rtac (add_lt_mono RS lt_trans) 1);
lcp@515
   217
by (REPEAT (FIRSTGOAL (etac bspec)));
lcp@515
   218
by (rtac ack_add_bound 5);
paulson@6071
   219
by Auto_tac;
clasohm@782
   220
qed "COMP_map_lemma";
lcp@515
   221
wenzelm@5068
   222
Goalw [COMP_def]
paulson@5147
   223
 "[| kg: nat;                                 \
clasohm@1461
   224
\         ALL l:list(nat). g`l < ack(kg, list_add(l));          \
paulson@6044
   225
\         fs : list({f: prim_rec .                               \
clasohm@1461
   226
\                    EX kf:nat. ALL l:list(nat).                \
clasohm@1461
   227
\                       f`l < ack(kf, list_add(l))})            \
lcp@515
   228
\      |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l < ack(k, list_add(l))";
paulson@2469
   229
by (Asm_simp_tac 1);
lcp@515
   230
by (forward_tac [list_CollectD] 1);
lcp@515
   231
by (etac (COMP_map_lemma RS bexE) 1);
lcp@515
   232
by (rtac (ballI RS bexI) 1);
lcp@515
   233
by (etac (bspec RS lt_trans) 1);
lcp@515
   234
by (rtac lt_trans 2);
lcp@515
   235
by (rtac ack_nest_bound 3);
lcp@515
   236
by (etac (bspec RS ack_lt_mono2) 2);
paulson@6071
   237
by Auto_tac;
clasohm@782
   238
qed "COMP_case";
lcp@515
   239
lcp@515
   240
(** PREC case **)
lcp@515
   241
wenzelm@5068
   242
Goalw [PREC_def]
paulson@5147
   243
 "[| ALL l:list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \
clasohm@1461
   244
\           ALL l:list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \
paulson@6044
   245
\           f: prim_rec;  kf: nat;                                       \
paulson@6044
   246
\           g: prim_rec;  kg: nat;                                       \
clasohm@1461
   247
\           l: list(nat)                                                \
lcp@515
   248
\        |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))";
paulson@6065
   249
by (exhaust_tac "l" 1);
wenzelm@4091
   250
by (asm_simp_tac (simpset() addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
paulson@2469
   251
by (Asm_simp_tac 1);
lcp@515
   252
by (etac ssubst 1);  (*get rid of the needless assumption*)
paulson@6070
   253
by (induct_tac "a" 1);
lcp@515
   254
(*base case*)
paulson@6071
   255
by (EVERY1 [Asm_simp_tac, rtac lt_trans, etac bspec,
paulson@6153
   256
	    assume_tac, rtac (add_le_self RS ack_lt_mono1)]);
paulson@6154
   257
by (ALLGOALS Asm_simp_tac);
lcp@515
   258
(*ind step*)
lcp@515
   259
by (rtac (succ_leI RS lt_trans1) 1);
lcp@515
   260
by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
lcp@515
   261
by (etac bspec 2);
lcp@515
   262
by (rtac (nat_le_refl RS add_le_mono) 1);
paulson@6153
   263
by Typecheck_tac;
wenzelm@4091
   264
by (asm_simp_tac (simpset() addsimps [add_le_self2]) 1);
lcp@515
   265
(*final part of the simplification*)
paulson@2469
   266
by (Asm_simp_tac 1);
lcp@515
   267
by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
lcp@515
   268
by (etac ack_lt_mono2 5);
paulson@6071
   269
by Auto_tac;
clasohm@782
   270
qed "PREC_case_lemma";
lcp@515
   271
paulson@6044
   272
Goal "[| f: prim_rec;  kf: nat;                               \
paulson@6044
   273
\        g: prim_rec;  kg: nat;                               \
paulson@5147
   274
\        ALL l:list(nat). f`l < ack(kf, list_add(l));        \
paulson@5147
   275
\        ALL l:list(nat). g`l < ack(kg, list_add(l))         \
paulson@5147
   276
\     |] ==> EX k:nat. ALL l: list(nat). PREC(f,g)`l< ack(k, list_add(l))";
lcp@515
   277
by (rtac (ballI RS bexI) 1);
lcp@515
   278
by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
paulson@6153
   279
by (REPEAT_FIRST (rtac (ack_add_bound2 RS ballI) THEN' etac bspec));
paulson@6153
   280
by Typecheck_tac;
clasohm@782
   281
qed "PREC_case";
lcp@515
   282
paulson@6044
   283
Goal "f:prim_rec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
paulson@6044
   284
by (etac prim_rec.induct 1);
paulson@6153
   285
by (auto_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
paulson@6153
   286
			      PREC_case], 
paulson@6153
   287
	      simpset()));
paulson@6044
   288
qed "ack_bounds_prim_rec";
lcp@515
   289
paulson@6044
   290
Goal "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : prim_rec";
lcp@515
   291
by (rtac notI 1);
paulson@6044
   292
by (etac (ack_bounds_prim_rec RS bexE) 1);
lcp@515
   293
by (rtac lt_irrefl 1);
lcp@515
   294
by (dres_inst_tac [("x", "[x]")] bspec 1);
paulson@6153
   295
by Auto_tac;
paulson@6044
   296
qed "ack_not_prim_rec";
lcp@515
   297