| author | Walther Neuper <neuper@ist.tugraz.at> |
| Thu, 12 Aug 2010 15:03:34 +0200 | |
| branch | isac-from-Isabelle2009-2 |
| changeset 37913 | 20e3616b2d9c |
| parent 105 | 216d6ed87399 |
| permissions | -rw-r--r-- |
| lcp@105 | 1 |
> goal Nat.thy "(k+m)+n = k+(m+n)"; |
| lcp@105 | 2 |
Level 0 |
| lcp@105 | 3 |
k + m + n = k + (m + n) |
| lcp@105 | 4 |
1. k + m + n = k + (m + n) |
| lcp@105 | 5 |
val it = [] : thm list |
| lcp@105 | 6 |
> by (resolve_tac [induct] 1); |
| lcp@105 | 7 |
Level 1 |
| lcp@105 | 8 |
k + m + n = k + (m + n) |
| lcp@105 | 9 |
1. k + m + n = 0 |
| lcp@105 | 10 |
2. !!x. k + m + n = x ==> k + m + n = Suc(x) |
| lcp@105 | 11 |
val it = () : unit |
| lcp@105 | 12 |
> back(); |
| lcp@105 | 13 |
Level 1 |
| lcp@105 | 14 |
k + m + n = k + (m + n) |
| lcp@105 | 15 |
1. k + m + n = k + 0 |
| lcp@105 | 16 |
2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x) |
| lcp@105 | 17 |
val it = () : unit |
| lcp@105 | 18 |
> back(); |
| lcp@105 | 19 |
Level 1 |
| lcp@105 | 20 |
k + m + n = k + (m + n) |
| lcp@105 | 21 |
1. k + m + 0 = k + (m + 0) |
| lcp@105 | 22 |
2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x)) |
| lcp@105 | 23 |
val it = () : unit |
| lcp@105 | 24 |
> back(); |
| lcp@105 | 25 |
Level 1 |
| lcp@105 | 26 |
k + m + n = k + (m + n) |
| lcp@105 | 27 |
1. k + m + n = k + (m + 0) |
| lcp@105 | 28 |
2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x)) |
| lcp@105 | 29 |
val it = () : unit |
| lcp@105 | 30 |
|
| lcp@105 | 31 |
> val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]); |
| lcp@105 | 32 |
?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya) |
| lcp@105 | 33 |
|
| lcp@105 | 34 |
[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb |
| lcp@105 | 35 |
|
| lcp@105 | 36 |
?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya) |
| lcp@105 | 37 |
[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb |
| lcp@105 | 38 |
val nat_congs = [, ] : thm list |
| lcp@105 | 39 |
> val add_ss = FOL_ss addcongs nat_congs |
| lcp@105 | 40 |
# addrews [add_0, add_Suc]; |
| lcp@105 | 41 |
val add_ss = ? : simpset |
| lcp@105 | 42 |
> goal Nat.thy "(k+m)+n = k+(m+n)"; |
| lcp@105 | 43 |
Level 0 |
| lcp@105 | 44 |
k + m + n = k + (m + n) |
| lcp@105 | 45 |
1. k + m + n = k + (m + n) |
| lcp@105 | 46 |
val it = [] : thm list |
| lcp@105 | 47 |
> by (res_inst_tac [("n","k")] induct 1);
|
| lcp@105 | 48 |
Level 1 |
| lcp@105 | 49 |
k + m + n = k + (m + n) |
| lcp@105 | 50 |
1. 0 + m + n = 0 + (m + n) |
| lcp@105 | 51 |
2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n) |
| lcp@105 | 52 |
val it = () : unit |
| lcp@105 | 53 |
> by (SIMP_TAC add_ss 1); |
| lcp@105 | 54 |
Level 2 |
| lcp@105 | 55 |
k + m + n = k + (m + n) |
| lcp@105 | 56 |
1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n) |
| lcp@105 | 57 |
val it = () : unit |
| lcp@105 | 58 |
> by (ASM_SIMP_TAC add_ss 1); |
| lcp@105 | 59 |
Level 3 |
| lcp@105 | 60 |
k + m + n = k + (m + n) |
| lcp@105 | 61 |
No subgoals! |
| lcp@105 | 62 |
val it = () : unit |
| lcp@105 | 63 |
> val add_assoc = result(); |
| lcp@105 | 64 |
?k + ?m + ?n = ?k + (?m + ?n) |
| lcp@105 | 65 |
val add_assoc = : thm |