doc-src/Intro/theorems-out.txt

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Intro/theorems-out.txt	Wed Nov 10 05:06:55 1993 +0100
@@ -0,0 +1,65 @@
+> goal Nat.thy "(k+m)+n = k+(m+n)";
+Level 0
+k + m + n = k + (m + n)
+ 1. k + m + n = k + (m + n)
+val it = [] : thm list
+> by (resolve_tac [induct] 1);
+Level 1
+k + m + n = k + (m + n)
+ 1. k + m + n = 0
+ 2. !!x. k + m + n = x ==> k + m + n = Suc(x)
+val it = () : unit
+> back();
+Level 1
+k + m + n = k + (m + n)
+ 1. k + m + n = k + 0
+ 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)
+val it = () : unit
+> back();
+Level 1
+k + m + n = k + (m + n)
+ 1. k + m + 0 = k + (m + 0)
+ 2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x))
+val it = () : unit
+> back();
+Level 1
+k + m + n = k + (m + n)
+ 1. k + m + n = k + (m + 0)
+ 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))
+val it = () : unit
+
+> val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]);
+?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)
+
+[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb
+
+?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)
+[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb
+val nat_congs = [, ] : thm list
+> val add_ss = FOL_ss  addcongs nat_congs
+#                    addrews  [add_0, add_Suc];
+val add_ss = ? : simpset
+> goal Nat.thy "(k+m)+n = k+(m+n)";
+Level 0
+k + m + n = k + (m + n)
+ 1. k + m + n = k + (m + n)
+val it = [] : thm list
+> by (res_inst_tac [("n","k")] induct 1);
+Level 1
+k + m + n = k + (m + n)
+ 1. 0 + m + n = 0 + (m + n)
+ 2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)
+val it = () : unit
+> by (SIMP_TAC add_ss 1);
+Level 2
+k + m + n = k + (m + n)
+ 1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)
+val it = () : unit
+> by (ASM_SIMP_TAC add_ss 1);
+Level 3
+k + m + n = k + (m + n)
+No subgoals!
+val it = () : unit
+> val add_assoc = result();
+?k + ?m + ?n = ?k + (?m + ?n)
+val add_assoc =  : thm