src/Sequents/LK/Nat.ML
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 7095 cfc11af6174a
permissions -rw-r--r--
converted to Isar theory format;
wenzelm@17481
     1
(*  Title:      Sequents/LK/Nat.ML
paulson@7091
     2
    ID:         $Id$
paulson@7091
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@7095
     4
    Copyright   1999  University of Cambridge
paulson@7091
     5
*)
paulson@7091
     6
paulson@7091
     7
Addsimps [Suc_neq_0];
paulson@7091
     8
paulson@7091
     9
Add_safes [Suc_inject RS L_of_imp];
paulson@7091
    10
paulson@7091
    11
Goal "|- Suc(k) ~= k";
paulson@7091
    12
by (res_inst_tac [("n","k")] induct 1);
paulson@7091
    13
by (Simp_tac 1);
paulson@7091
    14
by (Fast_tac 1);
paulson@7091
    15
qed "Suc_n_not_n";
paulson@7091
    16
paulson@7091
    17
Goalw [add_def] "|- 0+n = n";
paulson@7091
    18
by (rtac rec_0 1);
paulson@7091
    19
qed "add_0";
paulson@7091
    20
paulson@7091
    21
Goalw [add_def] "|- Suc(m)+n = Suc(m+n)";
paulson@7091
    22
by (rtac rec_Suc 1);
paulson@7091
    23
qed "add_Suc";
paulson@7091
    24
paulson@7091
    25
Addsimps [add_0, add_Suc];
paulson@7091
    26
paulson@7091
    27
Goal "|- (k+m)+n = k+(m+n)";
paulson@7091
    28
by (res_inst_tac [("n","k")] induct 1);
paulson@7091
    29
by (Simp_tac 1);
paulson@7091
    30
by (Asm_simp_tac 1);
paulson@7091
    31
qed "add_assoc";
paulson@7091
    32
paulson@7091
    33
Goal "|- m+0 = m";
paulson@7091
    34
by (res_inst_tac [("n","m")] induct 1);
paulson@7091
    35
by (Simp_tac 1);
paulson@7091
    36
by (Asm_simp_tac 1);
paulson@7091
    37
qed "add_0_right";
paulson@7091
    38
paulson@7091
    39
Goal "|- m+Suc(n) = Suc(m+n)";
paulson@7091
    40
by (res_inst_tac [("n","m")] induct 1);
paulson@7091
    41
by (ALLGOALS (Asm_simp_tac));
paulson@7091
    42
qed "add_Suc_right";
paulson@7091
    43
paulson@7091
    44
(*Example used in Reference Manual, Doc/Ref/simplifier.tex*)
paulson@7091
    45
val [prem] = Goal "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)";
paulson@7091
    46
by (res_inst_tac [("n","i")] induct 1);
paulson@7091
    47
by (Simp_tac 1);
paulson@7091
    48
by (simp_tac (simpset() addsimps [prem]) 1);
paulson@7091
    49
result();