wneuper/isa: doc-src/Ref/simplifier-eg.txt@20e3616b2d9c

     2 Pretty.setmargin 70;

     5 context Arith.thy;

     6 goal Arith.thy "0 + (x + 0) = x + 0 + 0";

     7 by (Simp_tac 1);

    12 > goal Nat.thy "m+0 = m";

    13 Level 0

    14 m + 0 = m

    15  1. m + 0 = m

    16 > by (res_inst_tac [("n","m")] induct 1);

    17 Level 1

    18 m + 0 = m

    19  1. 0 + 0 = 0

    20  2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)

    21 > by (simp_tac add_ss 1);

    22 Level 2

    23 m + 0 = m

    24  1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)

    25 > by (asm_simp_tac add_ss 1);

    26 Level 3

    27 m + 0 = m

    28 No subgoals!

    31 > goal Nat.thy "m+Suc(n) = Suc(m+n)";

    32 Level 0

    33 m + Suc(n) = Suc(m + n)

    34  1. m + Suc(n) = Suc(m + n)

    35 val it = [] : thm list

    36 > by (res_inst_tac [("n","m")] induct 1);

    37 Level 1

    38 m + Suc(n) = Suc(m + n)

    39  1. 0 + Suc(n) = Suc(0 + n)

    40  2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)

    41 val it = () : unit

    42 > by (simp_tac add_ss 1);

    43 Level 2

    44 m + Suc(n) = Suc(m + n)

    45  1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)

    46 val it = () : unit

    47 > trace_simp := true;

    48 val it = () : unit

    49 > by (asm_simp_tac add_ss 1);

    50 Rewriting:

    51 Suc(x) + Suc(n) == Suc(x + Suc(n))

    52 Rewriting:

    53 x + Suc(n) == Suc(x + n)

    54 Rewriting:

    55 Suc(x) + n == Suc(x + n)

    56 Rewriting:

    57 Suc(Suc(x + n)) = Suc(Suc(x + n)) == True

    58 Level 3

    59 m + Suc(n) = Suc(m + n)

    60 No subgoals!

    61 val it = () : unit

    65 > val prems = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";

    66 Level 0

    67 f(i + j) = i + f(j)

    68  1. f(i + j) = i + f(j)

    69 > prths prems;

    70 f(Suc(?n)) = Suc(f(?n))  [!!n. f(Suc(n)) = Suc(f(n))]

    72 > by (res_inst_tac [("n","i")] induct 1);

    73 Level 1

    74 f(i + j) = i + f(j)

    75  1. f(0 + j) = 0 + f(j)

    76  2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)

    77 > by (simp_tac f_ss 1);

    78 Level 2

    79 f(i + j) = i + f(j)

    80  1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)

    81 > by (asm_simp_tac (f_ss addrews prems) 1);

    82 Level 3

    83 f(i + j) = i + f(j)

    84 No subgoals!

    88 > goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";

    89 Level 0

    90 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)

    91  1. Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)

    93 > by (simp_tac natsum_ss 1);

    94 Level 1

    95 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)

    96  1. n + (n + (sum(%i. i, n) + sum(%i. i, n))) = n + n * n

    98 > by (nat_ind_tac "n" 1);

    99 Level 2

   100 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)

   101  1. 0 + (0 + (sum(%i. i, 0) + sum(%i. i, 0))) = 0 + 0 * 0

   102  2. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =

   103           n1 + n1 * n1 ==>

   104           Suc(n1) +

   105           (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =

   106           Suc(n1) + Suc(n1) * Suc(n1)

   108 > by (simp_tac natsum_ss 1);

   109 Level 3

   110 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)

   111  1. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =

   112           n1 + n1 * n1 ==>

   113           Suc(n1) +

   114           (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =

   115           Suc(n1) + Suc(n1) * Suc(n1)

   117 > by (asm_simp_tac natsum_ss 1);

   118 Level 4

   119 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)

   120 No subgoals!

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 4396	d103e5e164f8
permissions	-rw-r--r--