doc-src/Ref/simplifier-eg.txt
author haftmann
Thu, 12 Nov 2009 15:49:01 +0100
changeset 33633 9f7280e0c231
parent 4396 d103e5e164f8
permissions -rw-r--r--
explicit code lemmas produce nices code
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4396
wenzelm
parents: 359
diff changeset
     1
359
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
     2
Pretty.setmargin 70;
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
     3
4396
wenzelm
parents: 359
diff changeset
     4
wenzelm
parents: 359
diff changeset
     5
context Arith.thy;
wenzelm
parents: 359
diff changeset
     6
goal Arith.thy "0 + (x + 0) = x + 0 + 0";
wenzelm
parents: 359
diff changeset
     7
by (Simp_tac 1);
wenzelm
parents: 359
diff changeset
     8
wenzelm
parents: 359
diff changeset
     9
wenzelm
parents: 359
diff changeset
    10
wenzelm
parents: 359
diff changeset
    11
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
> goal Nat.thy "m+0 = m";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
m + 0 = m
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
 1. m + 0 = m
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
> by (res_inst_tac [("n","m")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
m + 0 = m
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
 1. 0 + 0 = 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
> by (simp_tac add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
m + 0 = m
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
> by (asm_simp_tac add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
m + 0 = m
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
> goal Nat.thy "m+Suc(n) = Suc(m+n)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
m + Suc(n) = Suc(m + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
 1. m + Suc(n) = Suc(m + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
val it = [] : thm list   
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
> by (res_inst_tac [("n","m")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
m + Suc(n) = Suc(m + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
 1. 0 + Suc(n) = Suc(0 + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
 2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
val it = () : unit   
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
> by (simp_tac add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
m + Suc(n) = Suc(m + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
 1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
val it = () : unit   
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
> trace_simp := true;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
val it = () : unit   
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
> by (asm_simp_tac add_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
Rewriting:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
Suc(x) + Suc(n) == Suc(x + Suc(n))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
Rewriting:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
x + Suc(n) == Suc(x + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
Rewriting:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
Suc(x) + n == Suc(x + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
Rewriting:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
Suc(Suc(x + n)) = Suc(Suc(x + n)) == True
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
m + Suc(n) = Suc(m + n)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
No subgoals!
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
val it = () : unit   
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
> val prems = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
Level 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
f(i + j) = i + f(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
 1. f(i + j) = i + f(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
> prths prems;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
f(Suc(?n)) = Suc(f(?n))  [!!n. f(Suc(n)) = Suc(f(n))]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
> by (res_inst_tac [("n","i")] induct 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
Level 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
f(i + j) = i + f(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
 1. f(0 + j) = 0 + f(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
> by (simp_tac f_ss 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
Level 2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
f(i + j) = i + f(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
> by (asm_simp_tac (f_ss addrews prems) 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
Level 3
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
f(i + j) = i + f(j)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
No subgoals!
359
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    85
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    86
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    87
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    88
> goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    89
Level 0
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    90
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    91
 1. Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    92
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    93
> by (simp_tac natsum_ss 1);
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    94
Level 1
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    95
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    96
 1. n + (n + (sum(%i. i, n) + sum(%i. i, n))) = n + n * n
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    97
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    98
> by (nat_ind_tac "n" 1);
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
    99
Level 2
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   100
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   101
 1. 0 + (0 + (sum(%i. i, 0) + sum(%i. i, 0))) = 0 + 0 * 0
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   102
 2. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   103
          n1 + n1 * n1 ==>
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   104
          Suc(n1) +
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   105
          (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   106
          Suc(n1) + Suc(n1) * Suc(n1)
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   107
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   108
> by (simp_tac natsum_ss 1);
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   109
Level 3
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   110
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   111
 1. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   112
          n1 + n1 * n1 ==>
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   113
          Suc(n1) +
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   114
          (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   115
          Suc(n1) + Suc(n1) * Suc(n1)
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   116
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   117
> by (asm_simp_tac natsum_ss 1);
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   118
Level 4
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   119
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
b5a2e9503a7a final Springer version
lcp
parents: 104
diff changeset
   120
No subgoals!