doc-src/Intro/theorems-out.txt
 author clasohm Thu, 29 Jun 1995 12:28:27 +0200 changeset 1163 c080ff36d24e parent 105 216d6ed87399 permissions -rw-r--r--
changed 'chol' labels to 'hol'; added a few parentheses
```
> 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