doc-src/Ref/simplifier-eg.txt
 changeset 104 d8205bb279a7 child 359 b5a2e9503a7a
equal inserted replaced
103:30bd42401ab2 104:d8205bb279a7
`       `
`     1 > goal Nat.thy "m+0 = m";`
`       `
`     2 Level 0`
`       `
`     3 m + 0 = m`
`       `
`     4  1. m + 0 = m`
`       `
`     5 > by (res_inst_tac [("n","m")] induct 1);`
`       `
`     6 Level 1`
`       `
`     7 m + 0 = m`
`       `
`     8  1. 0 + 0 = 0`
`       `
`     9  2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)`
`       `
`    10 > by (simp_tac add_ss 1);`
`       `
`    11 Level 2`
`       `
`    12 m + 0 = m`
`       `
`    13  1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)`
`       `
`    14 > by (asm_simp_tac add_ss 1);`
`       `
`    15 Level 3`
`       `
`    16 m + 0 = m`
`       `
`    17 No subgoals!`
`       `
`    18 `
`       `
`    19 `
`       `
`    20 > goal Nat.thy "m+Suc(n) = Suc(m+n)";`
`       `
`    21 Level 0`
`       `
`    22 m + Suc(n) = Suc(m + n)`
`       `
`    23  1. m + Suc(n) = Suc(m + n)`
`       `
`    24 val it = [] : thm list   `
`       `
`    25 > by (res_inst_tac [("n","m")] induct 1);`
`       `
`    26 Level 1`
`       `
`    27 m + Suc(n) = Suc(m + n)`
`       `
`    28  1. 0 + Suc(n) = Suc(0 + n)`
`       `
`    29  2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)`
`       `
`    30 val it = () : unit   `
`       `
`    31 > by (simp_tac add_ss 1);`
`       `
`    32 Level 2`
`       `
`    33 m + Suc(n) = Suc(m + n)`
`       `
`    34  1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)`
`       `
`    35 val it = () : unit   `
`       `
`    36 > trace_simp := true;`
`       `
`    37 val it = () : unit   `
`       `
`    38 > by (asm_simp_tac add_ss 1);`
`       `
`    39 Rewriting:`
`       `
`    40 Suc(x) + Suc(n) == Suc(x + Suc(n))`
`       `
`    41 Rewriting:`
`       `
`    42 x + Suc(n) == Suc(x + n)`
`       `
`    43 Rewriting:`
`       `
`    44 Suc(x) + n == Suc(x + n)`
`       `
`    45 Rewriting:`
`       `
`    46 Suc(Suc(x + n)) = Suc(Suc(x + n)) == True`
`       `
`    47 Level 3`
`       `
`    48 m + Suc(n) = Suc(m + n)`
`       `
`    49 No subgoals!`
`       `
`    50 val it = () : unit   `
`       `
`    51 `
`       `
`    52 `
`       `
`    53 `
`       `
`    54 > val prems = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";`
`       `
`    55 Level 0`
`       `
`    56 f(i + j) = i + f(j)`
`       `
`    57  1. f(i + j) = i + f(j)`
`       `
`    58 > prths prems;`
`       `
`    59 f(Suc(?n)) = Suc(f(?n))  [!!n. f(Suc(n)) = Suc(f(n))]`
`       `
`    60 `
`       `
`    61 > by (res_inst_tac [("n","i")] induct 1);`
`       `
`    62 Level 1`
`       `
`    63 f(i + j) = i + f(j)`
`       `
`    64  1. f(0 + j) = 0 + f(j)`
`       `
`    65  2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)`
`       `
`    66 > by (simp_tac f_ss 1);`
`       `
`    67 Level 2`
`       `
`    68 f(i + j) = i + f(j)`
`       `
`    69  1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)`
`       `
`    70 > by (asm_simp_tac (f_ss addrews prems) 1);`
`       `
`    71 Level 3`
`       `
`    72 f(i + j) = i + f(j)`
`       `
`    73 No subgoals!`