doc-src/Intro/theorems-out.txt
author kleing
Mon, 29 Dec 2003 06:49:26 +0100
changeset 14333 14f29eb097a3
parent 105 216d6ed87399
permissions -rw-r--r--
\<^bsub> .. \<^esub>
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     1
> goal Nat.thy "(k+m)+n = k+(m+n)";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     2
Level 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     3
k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     4
 1. k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     5
val it = [] : thm list
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     6
> by (resolve_tac [induct] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     7
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     8
k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     9
 1. k + m + n = 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    10
 2. !!x. k + m + n = x ==> k + m + n = Suc(x)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    11
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    12
> back();
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    13
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    14
k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    15
 1. k + m + n = k + 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    16
 2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    17
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    18
> back();
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    19
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    20
k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    21
 1. k + m + 0 = k + (m + 0)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    22
 2. !!x. k + m + x = k + (m + x) ==> k + m + Suc(x) = k + (m + Suc(x))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    23
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    24
> back();
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    25
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    26
k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    27
 1. k + m + n = k + (m + 0)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    28
 2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    29
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    30
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    31
> val nat_congs = prths (mk_congs Nat.thy ["Suc", "op +"]);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    32
?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    33
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    34
[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    35
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    36
?Xa = ?Ya ==> Suc(?Xa) = Suc(?Ya)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    37
[| ?Xa = ?Ya; ?Xb = ?Yb |] ==> ?Xa + ?Xb = ?Ya + ?Yb
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    38
val nat_congs = [, ] : thm list
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    39
> val add_ss = FOL_ss  addcongs nat_congs
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    40
#                    addrews  [add_0, add_Suc];
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    41
val add_ss = ? : simpset
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    42
> goal Nat.thy "(k+m)+n = k+(m+n)";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    43
Level 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    44
k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    45
 1. k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    46
val it = [] : thm list
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    47
> by (res_inst_tac [("n","k")] induct 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    48
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    49
k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    50
 1. 0 + m + n = 0 + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    51
 2. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    52
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    53
> by (SIMP_TAC add_ss 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    54
Level 2
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    55
k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    56
 1. !!x. x + m + n = x + (m + n) ==> Suc(x) + m + n = Suc(x) + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    57
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    58
> by (ASM_SIMP_TAC add_ss 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    59
Level 3
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    60
k + m + n = k + (m + n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    61
No subgoals!
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    62
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    63
> val add_assoc = result();
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    64
?k + ?m + ?n = ?k + (?m + ?n)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    65
val add_assoc =  : thm