src/HOL/ex/Primrec.ML
author paulson
Wed, 15 Jul 1998 14:19:02 +0200
changeset 5148 74919e8f221c
parent 5143 b94cd208f073
child 5462 7c5b2a8adbf0
permissions -rw-r--r--
More tidying and removal of "\!\!... from Goal commands
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
Addsimps ack.rules;
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    48
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    49
(*PROPERTY A 4*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    50
Goal "j < ack(i,j)";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    51
by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    52
by (ALLGOALS Asm_simp_tac);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    53
by (ALLGOALS trans_tac);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    54
qed "less_ack2";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    55
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    56
AddIffs [less_ack2];
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    57
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    58
(*PROPERTY A 5-, the single-step lemma*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    59
Goal "ack(i,j) < ack(i, Suc(j))";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    60
by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    61
by (ALLGOALS Asm_simp_tac);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    62
qed "ack_less_ack_Suc2";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    63
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    64
AddIffs [ack_less_ack_Suc2];
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    65
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    66
(*PROPERTY A 5, monotonicity for < *)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    67
Goal "j<k --> ack(i,j) < ack(i,k)";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    68
by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    69
by (ALLGOALS Asm_simp_tac);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    70
by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    71
qed_spec_mp "ack_less_mono2";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    72
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    73
(*PROPERTY A 5', monotonicity for<=*)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5078
diff changeset
    74
Goal "j<=k ==> ack(i,j)<=ack(i,k)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    75
by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    76
by (blast_tac (claset() addIs [ack_less_mono2]) 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    77
qed "ack_le_mono2";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    78
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    79
(*PROPERTY A 6*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    80
Goal "ack(i, Suc(j)) <= ack(Suc(i), j)";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    81
by (induct_tac "j" 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    82
by (ALLGOALS Asm_simp_tac);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    83
by (blast_tac (claset() addIs [ack_le_mono2, less_ack2 RS Suc_leI, 
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    84
			      le_trans]) 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    85
qed "ack2_le_ack1";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    86
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    87
AddIffs [ack2_le_ack1];
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    88
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    89
(*PROPERTY A 7-, the single-step lemma*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    90
Goal "ack(i,j) < ack(Suc(i),j)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
    91
by (blast_tac (claset() addIs [ack_less_mono2, less_le_trans]) 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    92
qed "ack_less_ack_Suc1";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    93
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    94
AddIffs [ack_less_ack_Suc1];
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    95
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    96
(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
    97
Goal "i < ack(i,j)";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    98
by (induct_tac "i" 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
    99
by (ALLGOALS Asm_simp_tac);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   100
by (blast_tac (claset() addIs [Suc_leI, le_less_trans]) 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   101
qed "less_ack1";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   102
AddIffs [less_ack1];
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   103
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   104
(*PROPERTY A 8*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   105
Goal "ack(1,j) = Suc(Suc(j))";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   106
by (induct_tac "j" 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   107
by (ALLGOALS Asm_simp_tac);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   108
qed "ack_1";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   109
Addsimps [ack_1];
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   110
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   111
(*PROPERTY A 9*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   112
Goal "ack(Suc(1),j) = Suc(Suc(Suc(j+j)))";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   113
by (induct_tac "j" 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   114
by (ALLGOALS Asm_simp_tac);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   115
qed "ack_2";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   116
Addsimps [ack_2];
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   117
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   118
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   119
(*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   120
Goal "ack(i,k) < ack(Suc(i+i'),k)";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   121
by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   122
by (ALLGOALS Asm_full_simp_tac);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   123
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   124
by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   125
by (ALLGOALS Asm_simp_tac);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   126
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   127
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
   128
val lemma = result();
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   129
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5078
diff changeset
   130
Goal "i<j ==> ack(i,k) < ack(j,k)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents: 5069
diff changeset
   131
by (dtac less_eq_Suc_add 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   132
by (blast_tac (claset() addSIs [lemma]) 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   133
qed "ack_less_mono1";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   134
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   135
(*PROPERTY A 7', monotonicity for<=*)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5078
diff changeset
   136
Goal "i<=j ==> ack(i,k)<=ack(j,k)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   137
by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   138
by (blast_tac (claset() addIs [ack_less_mono1]) 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   139
qed "ack_le_mono1";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   140
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   141
(*PROPERTY A 10*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   142
Goal "ack(i1, ack(i2,j)) < ack(Suc(Suc(i1+i2)), j)";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   143
by (rtac (ack2_le_ack1 RSN (2,less_le_trans)) 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   144
by (Asm_simp_tac 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   145
by (rtac (le_add1 RS ack_le_mono1 RS le_less_trans) 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   146
by (rtac (ack_less_mono1 RS ack_less_mono2) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   147
by (simp_tac (simpset() addsimps [le_imp_less_Suc, le_add2]) 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   148
qed "ack_nest_bound";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   149
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   150
(*PROPERTY A 11*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   151
Goal "ack(i1,j) + ack(i2,j) < ack(Suc(Suc(Suc(Suc(i1+i2)))), j)";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   152
by (res_inst_tac [("j", "ack(Suc(1), ack(i1 + i2, j))")] less_trans 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   153
by (Asm_simp_tac 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   154
by (rtac (ack_nest_bound RS less_le_trans) 2);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   155
by (Asm_simp_tac 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   156
by (blast_tac (claset() addSIs [le_add1, le_add2]
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   157
		       addIs  [le_imp_less_Suc, ack_le_mono1, le_SucI, 
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   158
			       add_le_mono]) 1);
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... *)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5078
diff changeset
   163
Goal "i < ack(k,j) ==> i+j < ack(Suc(Suc(Suc(Suc(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);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   189
by (exhaust_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);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   204
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
   205
qed "COMP_map_lemma";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   206
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   207
Goalw [COMP_def]
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   208
 "[| ALL l. g l < ack(kg, list_add l);           \
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   209
\    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
   210
\ |] ==> EX k. ALL l. COMP g fs  l < ack(k, list_add l)";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   211
by (forward_tac [impOfSubs (Int_lower1 RS lists_mono)] 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   212
by (etac (COMP_map_lemma RS exE) 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   213
by (rtac exI 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   214
by (rtac allI 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   215
by (REPEAT (dtac spec 1));
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   216
by (etac less_trans 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   217
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
   218
qed "COMP_case";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   219
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   220
(** PREC case **)
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   221
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   222
Goalw [PREC_def]
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   223
 "[| 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
   224
\    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
   225
\ |] ==> PREC f g l + list_add l < ack(Suc(kf+kg), list_add l)";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   226
by (exhaust_tac "l" 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   227
by (ALLGOALS Asm_simp_tac);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   228
by (blast_tac (claset() addIs [less_trans]) 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   229
by (etac ssubst 1);  (*get rid of the needless assumption*)
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   230
by (induct_tac "a" 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   231
by (ALLGOALS Asm_simp_tac);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   232
(*base case*)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   233
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
   234
			      less_trans]) 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   235
(*induction step*)
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   236
by (rtac (Suc_leI RS le_less_trans) 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   237
by (rtac (le_refl RS add_le_mono RS le_less_trans) 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   238
by (etac spec 2);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   239
by (asm_simp_tac (simpset() addsimps [le_add2]) 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   240
(*final part of the simplification*)
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   241
by (Asm_simp_tac 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   242
by (rtac (le_add2 RS ack_le_mono1 RS le_less_trans) 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   243
by (etac ack_less_mono2 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   244
qed "PREC_case_lemma";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   245
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   246
Goal "[| ALL l. f l < ack(kf, list_add l);        \
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   247
\        ALL l. g l < ack(kg, list_add l)         \
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   248
\     |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3335
diff changeset
   249
by (rtac exI 1);
a8ab7c64817c Ran expandshort
paulson
parents: 3335
diff changeset
   250
by (rtac allI 1);
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   251
by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   252
by (REPEAT (blast_tac (claset() addIs [ack_add_bound2]) 1));
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   253
qed "PREC_case";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   254
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5078
diff changeset
   255
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
   256
by (etac PRIMREC.induct 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   257
by (ALLGOALS 
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3457
diff changeset
   258
    (blast_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   259
			       PREC_case])));
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   260
qed "ack_bounds_PRIMREC";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   261
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4153
diff changeset
   262
Goal "(%l. case l of [] => 0 | x#l' => ack(x,x)) ~: PRIMREC";
3335
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   263
by (rtac notI 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   264
by (etac (ack_bounds_PRIMREC RS exE) 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   265
by (rtac less_irrefl 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   266
by (dres_inst_tac [("x", "[x]")] spec 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   267
by (Asm_full_simp_tac 1);
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   268
qed "ack_not_PRIMREC";
b0139b83a5ee New example ported from ZF
paulson
parents:
diff changeset
   269