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