doc-src/Intro/theorems-out.txt
 author wenzelm Fri, 16 Jul 1999 22:24:42 +0200 changeset 7024 44bd3c094fd6 parent 105 216d6ed87399 permissions -rw-r--r--
tuned;
```
> 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 = ? : 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