--- a/doc-src/AxClass/IsaMakefile Sat Jan 26 23:15:33 2008 +0100
+++ b/doc-src/AxClass/IsaMakefile Sun Jan 27 18:32:32 2008 +0100
@@ -36,7 +36,7 @@
FOL:
@cd $(SRC)/FOL; $(ISATOOL) make FOL
-$(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/NatClass.ML Nat/NatClass.thy
+$(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/NatClass.thy
@$(USEDIR) $(OUT)/FOL Nat
@rm -f Nat/document/*.sty Nat/document/session.tex
--- a/doc-src/AxClass/Nat/NatClass.ML Sat Jan 26 23:15:33 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(* Title: Doc/AxClass/Nat/NatClass.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-This is Nat.ML with some trivial modifications in order to make it
-work with NatClass.thy.
-*)
-
-val induct = thm "induct";
-val Suc_inject = thm "Suc_inject";
-val Suc_neq_0 = thm "Suc_neq_0";
-val rec_0 = thm "rec_0";
-val rec_Suc = thm "rec_Suc";
-val add_def = thm "add_def";
-
-
-Goal "Suc(k) ~= (k::'a::nat)";
-by (res_inst_tac [("n","k")] induct 1);
-by (rtac notI 1);
-by (etac Suc_neq_0 1);
-by (rtac notI 1);
-by (etac notE 1);
-by (etac Suc_inject 1);
-qed "Suc_n_not_n";
-
-
-Goal "(k+m)+n = k+(m+n)";
-prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
-by (rtac induct 1);
-back();
-back();
-back();
-back();
-back();
-back();
-
-Goalw [add_def] "\<zero>+n = n";
-by (rtac rec_0 1);
-qed "add_0";
-
-Goalw [add_def] "Suc(m)+n = Suc(m+n)";
-by (rtac rec_Suc 1);
-qed "add_Suc";
-
-Addsimps [add_0, add_Suc];
-
-Goal "(k+m)+n = k+(m+n)";
-by (res_inst_tac [("n","k")] induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_assoc";
-
-Goal "m+\<zero> = m";
-by (res_inst_tac [("n","m")] induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_0_right";
-
-Goal "m+Suc(n) = Suc(m+n)";
-by (res_inst_tac [("n","m")] induct 1);
-by (ALLGOALS (Asm_simp_tac));
-qed "add_Suc_right";
-
-val [prem] = Goal "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
-by (res_inst_tac [("n","i")] induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [prem]) 1);
-qed "";
-
--- a/doc-src/AxClass/Nat/NatClass.thy Sat Jan 26 23:15:33 2008 +0100
+++ b/doc-src/AxClass/Nat/NatClass.thy Sun Jan 27 18:32:32 2008 +0100
@@ -58,4 +58,60 @@
constraints).
*}
+(*<*)
+lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)"
+apply (rule_tac n = k in induct)
+apply (rule notI)
+apply (erule Suc_neq_0)
+apply (rule notI)
+apply (erule notE)
+apply (erule Suc_inject)
+done
+
+lemma "(k+m)+n = k+(m+n)"
+apply (rule induct)
+back
+back
+back
+back
+back
+back
+oops
+
+lemma add_0 [simp]: "\<zero>+n = n"
+apply (unfold add_def)
+apply (rule rec_0)
+done
+
+lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
+apply (unfold add_def)
+apply (rule rec_Suc)
+done
+
+lemma add_assoc: "(k+m)+n = k+(m+n)"
+apply (rule_tac n = k in induct)
+apply simp
+apply simp
+done
+
+lemma add_0_right: "m+\<zero> = m"
+apply (rule_tac n = m in induct)
+apply simp
+apply simp
+done
+
+lemma add_Suc_right: "m+Suc(n) = Suc(m+n)"
+apply (rule_tac n = m in induct)
+apply simp_all
+done
+
+lemma
+ assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
+ shows "f(i+j) = i+f(j)"
+apply (rule_tac n = i in induct)
+apply simp
+apply (simp add: prem)
+done
+(*>*)
+
end
\ No newline at end of file
--- a/doc-src/AxClass/Nat/document/NatClass.tex Sat Jan 26 23:15:33 2008 +0100
+++ b/doc-src/AxClass/Nat/document/NatClass.tex Sun Jan 27 18:32:32 2008 +0100
@@ -76,6 +76,111 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+%
\isadelimtheory
%
\endisadelimtheory