doc-src/Intro/theorems-out.txt
author aspinall
Sun Dec 31 15:34:21 2006 +0100 (2006-12-31)
changeset 21973 e7c9b0d3ce82
parent 105 216d6ed87399
permissions -rw-r--r--
Quote arguments in PGIP exceptions. Tune comment.
     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
    30 
    31 > val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]);
    32 ?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)
    33 
    34 [| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb
    35 
    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