src/FOL/ex/Nat2.ML
author paulson
Fri, 06 Sep 1996 10:45:48 +0200
changeset 1959 58f8379eca73
parent 1662 a6b55b9d2f22
child 2469 b50b8c0eec01
permissions -rw-r--r--
Modified proof to work with miniscoping
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
For ex/nat.thy.  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
Examples of simplification and induction on the natural numbers
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
open Nat2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
val nat_rews = [pred_0, pred_succ, plus_0, plus_succ, 
1459
d12da312eff4 expanded tabs
clasohm
parents: 755
diff changeset
    13
                    nat_distinct1, nat_distinct2, succ_inject,
d12da312eff4 expanded tabs
clasohm
parents: 755
diff changeset
    14
                    leq_0,leq_succ_succ,leq_succ_0, 
d12da312eff4 expanded tabs
clasohm
parents: 755
diff changeset
    15
                    lt_0_succ,lt_succ_succ,lt_0];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
val nat_ss = FOL_ss addsimps nat_rews;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
val prems = goal Nat2.thy 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
    "[| P(0);  !!x. P(succ(x)) |] ==> All(P)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
by (rtac nat_ind 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
725
d9c629fbacc6 replaced 'val ... = result();' by 'qed "...";'
clasohm
parents: 0
diff changeset
    23
qed "nat_exh";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
goal Nat2.thy "~ n=succ(n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
goal Nat2.thy "~ succ(n)=n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
goal Nat2.thy "~ succ(succ(n))=n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
goal Nat2.thy "~ n=succ(succ(n))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
goal Nat2.thy "m+0 = m";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
725
d9c629fbacc6 replaced 'val ... = result();' by 'qed "...";'
clasohm
parents: 0
diff changeset
    43
qed "plus_0_right";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
goal Nat2.thy "m+succ(n) = succ(m+n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
725
d9c629fbacc6 replaced 'val ... = result();' by 'qed "...";'
clasohm
parents: 0
diff changeset
    47
qed "plus_succ_right";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
goal Nat2.thy "~n=0 --> m+pred(n) = pred(m+n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
by (IND_TAC nat_ind (simp_tac (nat_ss addsimps [plus_succ_right])) "n" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
goal Nat2.thy "~n=0 --> succ(pred(n))=n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
goal Nat2.thy "m+n=0 <-> m=0 & n=0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
goal Nat2.thy "m <= n --> m <= succ(n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (rtac (impI RS allI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (ALL_IND_TAC nat_ind (simp_tac nat_ss) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
by (fast_tac FOL_cs 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
    66
val le_imp_le_succ = store_thm("le_imp_le_succ", result() RS mp);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
goal Nat2.thy "n<succ(n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
goal Nat2.thy "~ n<n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
goal Nat2.thy "m < n --> m < succ(n)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (rtac (impI RS allI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
by (ALL_IND_TAC nat_ind (simp_tac nat_ss) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
by (fast_tac FOL_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
goal Nat2.thy "m <= n --> m <= n+k";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
by (IND_TAC nat_ind 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
    (simp_tac (nat_ss addsimps [plus_0_right, plus_succ_right, le_imp_le_succ]))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
     "k" 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
    87
qed "le_plus";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
goal Nat2.thy "succ(m) <= n --> m <= n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
by (res_inst_tac [("x","n")]spec 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
by (ALL_IND_TAC nat_exh (simp_tac (nat_ss addsimps [le_imp_le_succ])) 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
    92
qed "succ_le";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
goal Nat2.thy "~m<n <-> n<=m";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
by (rtac (impI RS allI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
by (ALL_IND_TAC nat_ind (asm_simp_tac nat_ss) 1);
725
d9c629fbacc6 replaced 'val ... = result();' by 'qed "...";'
clasohm
parents: 0
diff changeset
    98
qed "not_less";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
goal Nat2.thy "n<=m --> ~m<n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
by (simp_tac (nat_ss addsimps [not_less]) 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   102
qed "le_imp_not_less";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
goal Nat2.thy "m<n --> ~n<=m";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
by (cut_facts_tac [not_less] 1 THEN fast_tac FOL_cs 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   106
qed "not_le";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
goal Nat2.thy "m+k<=n --> m<=n";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
by (IND_TAC nat_ind (K all_tac) "k" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
by (simp_tac (nat_ss addsimps [plus_0_right]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
by (rtac (impI RS allI) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
by (simp_tac (nat_ss addsimps [plus_succ_right]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
by (REPEAT (resolve_tac [allI,impI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
by (cut_facts_tac [succ_le] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
by (fast_tac FOL_cs 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   116
qed "plus_le";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
val prems = goal Nat2.thy "[| ~m=0;  m <= n |] ==> ~n=0";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
by (cut_facts_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
by (REPEAT (etac rev_mp 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
by (IND_TAC nat_exh (simp_tac nat_ss) "m" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   123
qed "not0";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
goal Nat2.thy "a<=a' & b<=b' --> a+b<=a'+b'";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
by (IND_TAC nat_ind (simp_tac (nat_ss addsimps [plus_0_right,le_plus])) "b" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
by (resolve_tac [impI RS allI] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
by (resolve_tac [allI RS allI] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
by (ALL_IND_TAC nat_exh (asm_simp_tac (nat_ss addsimps [plus_succ_right])) 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   130
qed "plus_le_plus";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
goal Nat2.thy "i<=j --> j<=k --> i<=k";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
by (IND_TAC nat_ind (K all_tac) "i" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
by (simp_tac nat_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
by (resolve_tac [impI RS allI] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
1959
58f8379eca73 Modified proof to work with miniscoping
paulson
parents: 1662
diff changeset
   137
by (resolve_tac [impI] 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
by (fast_tac FOL_cs 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   140
qed "le_trans";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
goal Nat2.thy "i < j --> j <=k --> i < k";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
by (IND_TAC nat_ind (K all_tac) "j" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
by (simp_tac nat_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
by (resolve_tac [impI RS allI] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
by (fast_tac FOL_cs 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   150
qed "less_le_trans";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
goal Nat2.thy "succ(i) <= j <-> i < j";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
by (resolve_tac [impI RS allI] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
by (ALL_IND_TAC nat_exh (asm_simp_tac nat_ss) 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   156
qed "succ_le2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
goal Nat2.thy "i<succ(j) <-> i=j | i<j";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
by (resolve_tac [impI RS allI] 1);
1662
a6b55b9d2f22 adapted proof of less_succ: problem because of non-confluent SimpSet removed
oheimb
parents: 1661
diff changeset
   162
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
1661
1e2462c3fece *** empty log message ***
oheimb
parents: 1459
diff changeset
   163
by (asm_simp_tac nat_ss 1);
755
dfb3894d78e4 replaced "val ... = result()" by "qed ..."
clasohm
parents: 725
diff changeset
   164
qed "less_succ";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165