doc-src/Intro/theorems-out.txt
 author aspinall Sun Dec 31 15:34:21 2006 +0100 (2006-12-31) changeset 21973 e7c9b0d3ce82 parent 105 216d6ed87399 permissions -rw-r--r--
Quote arguments in PGIP exceptions. Tune comment.
```     1 > goal Nat.thy "(k+m)+n = k+(m+n)";
```
```     2 Level 0
```
```     3 k + m + n = k + (m + n)
```
```     4  1. k + m + n = k + (m + n)
```
```     5 val it = [] : thm list
```
```     6 > by (resolve_tac [induct] 1);
```
```     7 Level 1
```
```     8 k + m + n = k + (m + n)
```
```     9  1. k + m + n = 0
```
```    10  2. !!x. k + m + n = x ==> k + m + n = Suc(x)
```
```    11 val it = () : unit
```
```    12 > back();
```
```    13 Level 1
```
```    14 k + m + n = k + (m + n)
```
```    15  1. k + m + n = k + 0
```
```    16  2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)
```
```    17 val it = () : unit
```
```    18 > back();
```
```    19 Level 1
```
```    20 k + m + n = k + (m + n)
```
```    21  1. k + m + 0 = k + (m + 0)
```
```    22  2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x))
```
```    23 val it = () : unit
```
```    24 > back();
```
```    25 Level 1
```
```    26 k + m + n = k + (m + n)
```
```    27  1. k + m + n = k + (m + 0)
```
```    28  2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))
```
```    29 val it = () : unit
```
```    30
```
```    31 > val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]);
```
```    32 ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)
```
```    33
```
```    34 [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb
```
```    35
```
```    36 ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)
```
```    37 [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb
```
```    38 val nat_congs = [, ] : thm list
```
```    39 > val add_ss = FOL_ss  addcongs nat_congs
```
```    40 #                    addrews  [add_0, add_Suc];
```
```    41 val add_ss = ? : simpset
```
```    42 > goal Nat.thy "(k+m)+n = k+(m+n)";
```
```    43 Level 0
```
```    44 k + m + n = k + (m + n)
```
```    45  1. k + m + n = k + (m + n)
```
```    46 val it = [] : thm list
```
```    47 > by (res_inst_tac [("n","k")] induct 1);
```
```    48 Level 1
```
```    49 k + m + n = k + (m + n)
```
```    50  1. 0 + m + n = 0 + (m + n)
```
```    51  2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)
```
```    52 val it = () : unit
```
```    53 > by (SIMP_TAC add_ss 1);
```
```    54 Level 2
```
```    55 k + m + n = k + (m + n)
```
```    56  1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)
```
```    57 val it = () : unit
```
```    58 > by (ASM_SIMP_TAC add_ss 1);
```
```    59 Level 3
```
```    60 k + m + n = k + (m + n)
```
```    61 No subgoals!
```
```    62 val it = () : unit
```
```    63 > val add_assoc = result();
```
```    64 ?k + ?m + ?n = ?k + (?m + ?n)
```
```    65 val add_assoc =  : thm
```