src/FOL/ex/Nat.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 36 70c6014c9b6f
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	FOL/ex/nat.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Examples for the manual "Introduction to Isabelle"
     7 
     8 Proofs about the natural numbers
     9 
    10 INCOMPATIBLE with nat2.ML, Nipkow's examples
    11 
    12 To generate similar output to manual, execute these commands:
    13     Pretty.setmargin 72; print_depth 0;
    14 *)
    15 
    16 open Nat;
    17 
    18 goal Nat.thy "~ (Suc(k) = k)";
    19 by (res_inst_tac [("n","k")] induct 1);
    20 by (resolve_tac [notI] 1);
    21 by (eresolve_tac [Suc_neq_0] 1);
    22 by (resolve_tac [notI] 1);
    23 by (eresolve_tac [notE] 1);
    24 by (eresolve_tac [Suc_inject] 1);
    25 val Suc_n_not_n = result();
    26 
    27 
    28 goal Nat.thy "(k+m)+n = k+(m+n)";
    29 prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
    30 by (resolve_tac [induct] 1);
    31 back();
    32 back();
    33 back();
    34 back();
    35 back();
    36 back();
    37 
    38 goalw Nat.thy [add_def] "0+n = n";
    39 by (resolve_tac [rec_0] 1);
    40 val add_0 = result();
    41 
    42 goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
    43 by (resolve_tac [rec_Suc] 1);
    44 val add_Suc = result();
    45 
    46 val add_ss = FOL_ss  addsimps  [add_0, add_Suc];
    47 
    48 goal Nat.thy "(k+m)+n = k+(m+n)";
    49 by (res_inst_tac [("n","k")] induct 1);
    50 by (simp_tac add_ss 1);
    51 by (asm_simp_tac add_ss 1);
    52 val add_assoc = result();
    53 
    54 goal Nat.thy "m+0 = m";
    55 by (res_inst_tac [("n","m")] induct 1);
    56 by (simp_tac add_ss 1);
    57 by (asm_simp_tac add_ss 1);
    58 val add_0_right = result();
    59 
    60 goal Nat.thy "m+Suc(n) = Suc(m+n)";
    61 by (res_inst_tac [("n","m")] induct 1);
    62 by (ALLGOALS (asm_simp_tac add_ss));
    63 val add_Suc_right = result();
    64 
    65 val [prem] = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
    66 by (res_inst_tac [("n","i")] induct 1);
    67 by (simp_tac add_ss 1);
    68 by (asm_simp_tac (add_ss addsimps [prem]) 1);
    69 result();