doc-src/Intro/theorems-out.txt
 author wenzelm Thu, 17 Jul 1997 15:03:38 +0200 changeset 3524 c02cb15830de parent 105 216d6ed87399 permissions -rw-r--r--
fixed EqI meta rule;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 105 216d6ed87399 Initial revision lcp parents: diff changeset ` 1` ```> goal Nat.thy "(k+m)+n = k+(m+n)"; ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 2` ```Level 0 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 3` ```k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 4` ``` 1. k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 5` ```val it = [] : thm list ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 6` ```> by (resolve_tac [induct] 1); ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 7` ```Level 1 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 8` ```k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 9` ``` 1. k + m + n = 0 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 10` ``` 2. !!x. k + m + n = x ==> k + m + n = Suc(x) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 11` ```val it = () : unit ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 12` ```> back(); ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 13` ```Level 1 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 14` ```k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 15` ``` 1. k + m + n = k + 0 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 16` ``` 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 17` ```val it = () : unit ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 18` ```> back(); ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 19` ```Level 1 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 20` ```k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 21` ``` 1. k + m + 0 = k + (m + 0) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 22` ``` 2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x)) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 23` ```val it = () : unit ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 24` ```> back(); ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 25` ```Level 1 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 26` ```k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 27` ``` 1. k + m + n = k + (m + 0) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 28` ``` 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x)) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 29` ```val it = () : unit ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 30` 216d6ed87399 Initial revision lcp parents: diff changeset ` 31` ```> val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]); ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 32` ```?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 33` 216d6ed87399 Initial revision lcp parents: diff changeset ` 34` ```[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 35` 216d6ed87399 Initial revision lcp parents: diff changeset ` 36` ```?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 37` ```[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 38` ```val nat_congs = [, ] : thm list ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 39` ```> val add_ss = FOL_ss addcongs nat_congs ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 40` ```# addrews [add_0, add_Suc]; ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 41` ```val add_ss = ? : simpset ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 42` ```> goal Nat.thy "(k+m)+n = k+(m+n)"; ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 43` ```Level 0 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 44` ```k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 45` ``` 1. k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 46` ```val it = [] : thm list ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 47` ```> by (res_inst_tac [("n","k")] induct 1); ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 48` ```Level 1 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 49` ```k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 50` ``` 1. 0 + m + n = 0 + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 51` ``` 2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 52` ```val it = () : unit ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 53` ```> by (SIMP_TAC add_ss 1); ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 54` ```Level 2 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 55` ```k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 56` ``` 1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 57` ```val it = () : unit ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 58` ```> by (ASM_SIMP_TAC add_ss 1); ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 59` ```Level 3 ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 60` ```k + m + n = k + (m + n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 61` ```No subgoals! ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 62` ```val it = () : unit ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 63` ```> val add_assoc = result(); ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 64` ```?k + ?m + ?n = ?k + (?m + ?n) ``` 216d6ed87399 Initial revision lcp parents: diff changeset ` 65` ```val add_assoc = : thm ```