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