doc-src/Intro/theorems-out.txt
 author wenzelm Mon Oct 01 21:19:50 2007 +0200 (2007-10-01) changeset 24803 38577b4b1fde parent 105 216d6ed87399 permissions -rw-r--r--
Norbert Schirmer: record improvements;
 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 ```