src/FOL/ex/nat.ML

fixed subgoal_tac; fails on non-existent subgoal;

(*  Title: 	FOL/ex/nat.ML
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

Examples for the manual "Introduction to Isabelle"

Proofs about the natural numbers

INCOMPATIBLE with nat2.ML, Nipkow's examples

To generate similar output to manual, execute these commands:
    Pretty.setmargin 72; print_depth 0;
*)

open Nat;

goal Nat.thy "Suc(k) ~= k";
by (res_inst_tac [("n","k")] induct 1);
by (resolve_tac [notI] 1);
by (eresolve_tac [Suc_neq_0] 1);
by (resolve_tac [notI] 1);
by (eresolve_tac [notE] 1);
by (eresolve_tac [Suc_inject] 1);
val Suc_n_not_n = result();


goal Nat.thy "(k+m)+n = k+(m+n)";
prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
by (resolve_tac [induct] 1);
back();
back();
back();
back();
back();
back();

goalw Nat.thy [add_def] "0+n = n";
by (resolve_tac [rec_0] 1);
val add_0 = result();

goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
by (resolve_tac [rec_Suc] 1);
val add_Suc = result();

val add_ss = FOL_ss addsimps [add_0, add_Suc];

goal Nat.thy "(k+m)+n = k+(m+n)";
by (res_inst_tac [("n","k")] induct 1);
by (simp_tac add_ss 1);
by (asm_simp_tac add_ss 1);
val add_assoc = result();

goal Nat.thy "m+0 = m";
by (res_inst_tac [("n","m")] induct 1);
by (simp_tac add_ss 1);
by (asm_simp_tac add_ss 1);
val add_0_right = result();

goal Nat.thy "m+Suc(n) = Suc(m+n)";
by (res_inst_tac [("n","m")] induct 1);
by (ALLGOALS (asm_simp_tac add_ss));
val add_Suc_right = result();

val [prem] = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
by (res_inst_tac [("n","i")] induct 1);
by (simp_tac add_ss 1);
by (asm_simp_tac (add_ss addsimps [prem]) 1);
result();