author | haftmann |
Sat, 15 Sep 2007 19:27:35 +0200 | |
changeset 24584 | 01e83ffa6c54 |
parent 10140 | ba9297b71897 |
child 25985 | 8d69087f6a4b |
permissions | -rw-r--r-- |
haftmann@24584 | 1 |
(* Title: Doc/AxClass/Nat/NatClass.ML |
wenzelm@8890 | 2 |
ID: $Id$ |
wenzelm@8890 | 3 |
Author: Markus Wenzel, TU Muenchen |
wenzelm@8890 | 4 |
|
wenzelm@8890 | 5 |
This is Nat.ML with some trivial modifications in order to make it |
wenzelm@8890 | 6 |
work with NatClass.thy. |
wenzelm@8890 | 7 |
*) |
wenzelm@8890 | 8 |
|
wenzelm@8890 | 9 |
val induct = thm "induct"; |
wenzelm@8890 | 10 |
val Suc_inject = thm "Suc_inject"; |
wenzelm@8890 | 11 |
val Suc_neq_0 = thm "Suc_neq_0"; |
wenzelm@8890 | 12 |
val rec_0 = thm "rec_0"; |
wenzelm@8890 | 13 |
val rec_Suc = thm "rec_Suc"; |
wenzelm@8890 | 14 |
val add_def = thm "add_def"; |
wenzelm@8890 | 15 |
|
wenzelm@8890 | 16 |
|
wenzelm@8890 | 17 |
Goal "Suc(k) ~= (k::'a::nat)"; |
wenzelm@8890 | 18 |
by (res_inst_tac [("n","k")] induct 1); |
wenzelm@8890 | 19 |
by (rtac notI 1); |
wenzelm@8890 | 20 |
by (etac Suc_neq_0 1); |
wenzelm@8890 | 21 |
by (rtac notI 1); |
wenzelm@8890 | 22 |
by (etac notE 1); |
wenzelm@8890 | 23 |
by (etac Suc_inject 1); |
wenzelm@8890 | 24 |
qed "Suc_n_not_n"; |
wenzelm@8890 | 25 |
|
wenzelm@8890 | 26 |
|
wenzelm@8890 | 27 |
Goal "(k+m)+n = k+(m+n)"; |
wenzelm@8890 | 28 |
prths ([induct] RL [topthm()]); (*prints all 14 next states!*) |
wenzelm@8890 | 29 |
by (rtac induct 1); |
wenzelm@8890 | 30 |
back(); |
wenzelm@8890 | 31 |
back(); |
wenzelm@8890 | 32 |
back(); |
wenzelm@8890 | 33 |
back(); |
wenzelm@8890 | 34 |
back(); |
wenzelm@8890 | 35 |
back(); |
wenzelm@8890 | 36 |
|
wenzelm@10140 | 37 |
Goalw [add_def] "\\<zero>+n = n"; |
wenzelm@8890 | 38 |
by (rtac rec_0 1); |
wenzelm@8890 | 39 |
qed "add_0"; |
wenzelm@8890 | 40 |
|
wenzelm@8890 | 41 |
Goalw [add_def] "Suc(m)+n = Suc(m+n)"; |
wenzelm@8890 | 42 |
by (rtac rec_Suc 1); |
wenzelm@8890 | 43 |
qed "add_Suc"; |
wenzelm@8890 | 44 |
|
wenzelm@8890 | 45 |
Addsimps [add_0, add_Suc]; |
wenzelm@8890 | 46 |
|
wenzelm@8890 | 47 |
Goal "(k+m)+n = k+(m+n)"; |
wenzelm@8890 | 48 |
by (res_inst_tac [("n","k")] induct 1); |
wenzelm@8890 | 49 |
by (Simp_tac 1); |
wenzelm@8890 | 50 |
by (Asm_simp_tac 1); |
wenzelm@8890 | 51 |
qed "add_assoc"; |
wenzelm@8890 | 52 |
|
wenzelm@10140 | 53 |
Goal "m+\\<zero> = m"; |
wenzelm@8890 | 54 |
by (res_inst_tac [("n","m")] induct 1); |
wenzelm@8890 | 55 |
by (Simp_tac 1); |
wenzelm@8890 | 56 |
by (Asm_simp_tac 1); |
wenzelm@8890 | 57 |
qed "add_0_right"; |
wenzelm@8890 | 58 |
|
wenzelm@8890 | 59 |
Goal "m+Suc(n) = Suc(m+n)"; |
wenzelm@8890 | 60 |
by (res_inst_tac [("n","m")] induct 1); |
wenzelm@8890 | 61 |
by (ALLGOALS (Asm_simp_tac)); |
wenzelm@8890 | 62 |
qed "add_Suc_right"; |
wenzelm@8890 | 63 |
|
wenzelm@8890 | 64 |
val [prem] = Goal "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; |
wenzelm@8890 | 65 |
by (res_inst_tac [("n","i")] induct 1); |
wenzelm@8890 | 66 |
by (Simp_tac 1); |
wenzelm@8890 | 67 |
by (asm_simp_tac (simpset() addsimps [prem]) 1); |
wenzelm@8890 | 68 |
qed ""; |
wenzelm@8890 | 69 |