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