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.
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