author | berghofe |
Fri, 16 Jul 1999 14:06:13 +0200 | |
changeset 7020 | 75ff179df7b7 |
parent 132 | b5704e45d2d2 |
permissions | -rw-r--r-- |
(* 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();