src/FOL/ex/Nat2.ML
author wenzelm
Sun, 26 Nov 2006 23:43:53 +0100
changeset 21539 c5cf9243ad62
parent 17245 1c519a3cca59
permissions -rw-r--r--
converted legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1459
d12da312eff4 expanded tabs
clasohm
parents: 755
diff changeset
     1
(*  Title:      FOL/ex/nat2.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 755
diff changeset
     3
    Author:     Tobias Nipkow
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 5050
diff changeset
     7
Addsimps [pred_0, pred_succ, plus_0, plus_succ,
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 5050
diff changeset
     8
          nat_distinct1, nat_distinct2, succ_inject,
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 5050
diff changeset
     9
          leq_0, leq_succ_succ, leq_succ_0,
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 5050
diff changeset
    10
          lt_0_succ, lt_succ_succ, lt_0];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 5050
diff changeset
    13
val prems = goal (the_context ())
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
    "[| P(0);  !!x. P(succ(x)) |] ==> All(P)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
by (rtac nat_ind 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
725
d9c629fbacc6 replaced 'val ... = result();' by 'qed "...";'
clasohm
parents: 0
diff changeset
    17
qed "nat_exh";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    19
Goal "~ n=succ(n)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    20
by (IND_TAC nat_ind Simp_tac "n" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    23
Goal "~ succ(n)=n";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    24
by (IND_TAC nat_ind Simp_tac "n" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    27
Goal "~ succ(succ(n))=n";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    28
by (IND_TAC nat_ind Simp_tac "n" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    31
Goal "~ n=succ(succ(n))";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    32
by (IND_TAC nat_ind Simp_tac "n" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    35
Goal "m+0 = m";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    36
by (IND_TAC nat_ind Simp_tac "m" 1);
725
d9c629fbacc6 replaced 'val ... = result();' by 'qed "...";'
clasohm
parents: 0
diff changeset
    37
qed "plus_0_right";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    39
Goal "m+succ(n) = succ(m+n)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    40
by (IND_TAC nat_ind Simp_tac "m" 1);
725
d9c629fbacc6 replaced 'val ... = result();' by 'qed "...";'
clasohm
parents: 0
diff changeset
    41
qed "plus_succ_right";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    43
Addsimps [plus_0_right, plus_succ_right];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    44
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    45
Goal "~n=0 --> m+pred(n) = pred(m+n)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    46
by (IND_TAC nat_ind Simp_tac "n" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    49
Goal "~n=0 --> succ(pred(n))=n";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    50
by (IND_TAC nat_ind Simp_tac "n" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    53
Goal "m+n=0 <-> m=0 & n=0";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    54
by (IND_TAC nat_ind Simp_tac "m" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    57
Goal "m <= n --> m <= succ(n)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    58
by (IND_TAC nat_ind Simp_tac "m" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
by (rtac (impI RS allI) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    60
by (ALL_IND_TAC nat_ind Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    61
by (Fast_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    62
bind_thm("le_imp_le_succ", result() RS mp);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    64
Goal "n<succ(n)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    65
by (IND_TAC nat_ind Simp_tac "n" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    68
Goal "~ n<n";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    69
by (IND_TAC nat_ind Simp_tac "n" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    72
Goal "m < n --> m < succ(n)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    73
by (IND_TAC nat_ind Simp_tac "m" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
by (rtac (impI RS allI) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    75
by (ALL_IND_TAC nat_ind Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    76
by (Fast_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    79
Goal "m <= n --> m <= n+k";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2469
diff changeset
    80
by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_imp_le_succ]))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
     "k" 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
    82
qed "le_plus";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    84
Goal "succ(m) <= n --> m <= n";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
by (res_inst_tac [("x","n")]spec 1);
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2469
diff changeset
    86
by (ALL_IND_TAC nat_exh (simp_tac (simpset() addsimps [le_imp_le_succ])) 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
    87
qed "succ_le";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    89
Goal "~m<n <-> n<=m";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    90
by (IND_TAC nat_ind Simp_tac "n" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
by (rtac (impI RS allI) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
    92
by (ALL_IND_TAC nat_ind Asm_simp_tac 1);
725
d9c629fbacc6 replaced 'val ... = result();' by 'qed "...";'
clasohm
parents: 0
diff changeset
    93
qed "not_less";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    95
Goal "n<=m --> ~m<n";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2469
diff changeset
    96
by (simp_tac (simpset() addsimps [not_less]) 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
    97
qed "le_imp_not_less";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
    99
Goal "m<n --> ~n<=m";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   100
by (cut_facts_tac [not_less] 1 THEN Fast_tac 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   101
qed "not_le";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
   103
Goal "m+k<=n --> m<=n";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
by (IND_TAC nat_ind (K all_tac) "k" 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   105
by (Simp_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
by (rtac (impI RS allI) 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   107
by (Simp_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
by (REPEAT (resolve_tac [allI,impI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
by (cut_facts_tac [succ_le] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   110
by (Fast_tac 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   111
qed "plus_le";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
17245
1c519a3cca59 converted to Isar theory format;
wenzelm
parents: 5050
diff changeset
   113
val prems = goal (the_context ()) "[| ~m=0;  m <= n |] ==> ~n=0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
by (REPEAT (etac rev_mp 1));
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   116
by (IND_TAC nat_exh Simp_tac "m" 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   117
by (ALL_IND_TAC nat_exh Simp_tac 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   118
qed "not0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
   120
Goal "a<=a' & b<=b' --> a+b<=a'+b'";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 2469
diff changeset
   121
by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_plus])) "b" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
by (resolve_tac [impI RS allI] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
by (resolve_tac [allI RS allI] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   124
by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   125
qed "plus_le_plus";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
   127
Goal "i<=j --> j<=k --> i<=k";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
by (IND_TAC nat_ind (K all_tac) "i" 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   129
by (Simp_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
by (resolve_tac [impI RS allI] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   131
by (ALL_IND_TAC nat_exh Simp_tac 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4091
diff changeset
   132
by (rtac impI 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   133
by (ALL_IND_TAC nat_exh Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   134
by (Fast_tac 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   135
qed "le_trans";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
   137
Goal "i < j --> j <=k --> i < k";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
by (IND_TAC nat_ind (K all_tac) "j" 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   139
by (Simp_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
by (resolve_tac [impI RS allI] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   141
by (ALL_IND_TAC nat_exh Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   142
by (ALL_IND_TAC nat_exh Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   143
by (ALL_IND_TAC nat_exh Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   144
by (Fast_tac 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   145
qed "less_le_trans";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
   147
Goal "succ(i) <= j <-> i < j";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   148
by (IND_TAC nat_ind Simp_tac "j" 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
by (resolve_tac [impI RS allI] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   150
by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   151
qed "succ_le2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
5050
e925308df78b isatool fixgoal;
wenzelm
parents: 4423
diff changeset
   153
Goal "i<succ(j) <-> i=j | i<j";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   154
by (IND_TAC nat_ind Simp_tac "j" 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   155
by (ALL_IND_TAC nat_exh Simp_tac 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
by (resolve_tac [impI RS allI] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   157
by (ALL_IND_TAC nat_exh Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1959
diff changeset
   158
by (Asm_simp_tac 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   159
qed "less_succ";