doc-src/Intro/theorems-out.txt

modernized/simplified Sign.set_defsort;

> 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