wneuper/isa: doc-src/Intro/theorems-out.txt@20e3616b2d9c

     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

    31 > val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]);

    32 ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)

    34 [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb

    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

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