src/FOLP/ex/Nat.ML
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 17480 fd19f77dcf60
child 24584 01e83ffa6c54
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
     1
(*  Title:      FOLP/ex/nat.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1459
diff changeset
     7
Goal "?p : ~ (Suc(k) = k)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
by (res_inst_tac [("n","k")] induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
by (rtac notI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
by (etac Suc_neq_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
by (rtac notI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
by (etac notE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
by (etac Suc_inject 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
val Suc_n_not_n = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1459
diff changeset
    17
Goal "?p : (k+m)+n = k+(m+n)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
by (rtac induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
back();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1459
diff changeset
    27
Goalw [add_def] "?p : 0+n = n";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
by (rtac rec_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
val add_0 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1459
diff changeset
    31
Goalw [add_def] "?p : Suc(m)+n = Suc(m+n)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
by (rtac rec_Suc 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val add_Suc = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
(*
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 5061
diff changeset
    36
val nat_congs = mk_congs (the_context ()) ["Suc", "op +"];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
prths nat_congs;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
*)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 5061
diff changeset
    39
val prems = goal (the_context ()) "p: x=y ==> ?p : Suc(x) = Suc(y)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
by (resolve_tac (prems RL [subst]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
by (rtac refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
val Suc_cong = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 5061
diff changeset
    44
val prems = goal (the_context ()) "[| p : a=x;  q: b=y |] ==> ?p : a+b=x+y";
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 5061
diff changeset
    45
by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
    rtac refl 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val Plus_cong = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
val nat_congs = [Suc_cong,Plus_cong];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 5061
diff changeset
    52
val add_ss = FOLP_ss  addcongs nat_congs
1459
d12da312eff4 expanded tabs
clasohm
parents: 0
diff changeset
    53
                     addrews  [add_0, add_Suc];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1459
diff changeset
    55
Goal "?p : (k+m)+n = k+(m+n)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
by (res_inst_tac [("n","k")] induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
by (SIMP_TAC add_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
by (ASM_SIMP_TAC add_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
val add_assoc = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1459
diff changeset
    61
Goal "?p : m+0 = m";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
by (res_inst_tac [("n","m")] induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (SIMP_TAC add_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
by (ASM_SIMP_TAC add_ss 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val add_0_right = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
5061
f947332d5465 isatool fixgoal;
wenzelm
parents: 1459
diff changeset
    67
Goal "?p : m+Suc(n) = Suc(m+n)";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
by (res_inst_tac [("n","m")] induct 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
by (ALLGOALS (ASM_SIMP_TAC add_ss));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val add_Suc_right = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
(*mk_typed_congs appears not to work with FOLP's version of subst*)