src/FOLP/ex/nat.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title: 	FOLP/ex/nat.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Examples for the manual "Introduction to Isabelle"
clasohm@0
     7
clasohm@0
     8
Proofs about the natural numbers
clasohm@0
     9
clasohm@0
    10
To generate similar output to manual, execute these commands:
clasohm@0
    11
    Pretty.setmargin 72; print_depth 0;
clasohm@0
    12
*)
clasohm@0
    13
clasohm@0
    14
open Nat;
clasohm@0
    15
clasohm@0
    16
goal Nat.thy "?p : ~ (Suc(k) = k)";
clasohm@0
    17
by (res_inst_tac [("n","k")] induct 1);
clasohm@0
    18
by (rtac notI 1);
clasohm@0
    19
by (etac Suc_neq_0 1);
clasohm@0
    20
by (rtac notI 1);
clasohm@0
    21
by (etac notE 1);
clasohm@0
    22
by (etac Suc_inject 1);
clasohm@0
    23
val Suc_n_not_n = result();
clasohm@0
    24
clasohm@0
    25
clasohm@0
    26
goal Nat.thy "?p : (k+m)+n = k+(m+n)";
clasohm@0
    27
prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
clasohm@0
    28
by (rtac induct 1);
clasohm@0
    29
back();
clasohm@0
    30
back();
clasohm@0
    31
back();
clasohm@0
    32
back();
clasohm@0
    33
back();
clasohm@0
    34
back();
clasohm@0
    35
clasohm@0
    36
goalw Nat.thy [add_def] "?p : 0+n = n";
clasohm@0
    37
by (rtac rec_0 1);
clasohm@0
    38
val add_0 = result();
clasohm@0
    39
clasohm@0
    40
goalw Nat.thy [add_def] "?p : Suc(m)+n = Suc(m+n)";
clasohm@0
    41
by (rtac rec_Suc 1);
clasohm@0
    42
val add_Suc = result();
clasohm@0
    43
clasohm@0
    44
(*
clasohm@0
    45
val nat_congs = mk_congs Nat.thy ["Suc", "op +"];
clasohm@0
    46
prths nat_congs;
clasohm@0
    47
*)
clasohm@0
    48
val prems = goal Nat.thy "p: x=y ==> ?p : Suc(x) = Suc(y)";
clasohm@0
    49
by (resolve_tac (prems RL [subst]) 1);
clasohm@0
    50
by (rtac refl 1);
clasohm@0
    51
val Suc_cong = result();
clasohm@0
    52
clasohm@0
    53
val prems = goal Nat.thy "[| p : a=x;  q: b=y |] ==> ?p : a+b=x+y";
clasohm@0
    54
by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN 
clasohm@0
    55
    rtac refl 1);
clasohm@0
    56
val Plus_cong = result();
clasohm@0
    57
clasohm@0
    58
val nat_congs = [Suc_cong,Plus_cong];
clasohm@0
    59
clasohm@0
    60
clasohm@0
    61
val add_ss = FOLP_ss  addcongs nat_congs  
clasohm@0
    62
	             addrews  [add_0, add_Suc];
clasohm@0
    63
clasohm@0
    64
goal Nat.thy "?p : (k+m)+n = k+(m+n)";
clasohm@0
    65
by (res_inst_tac [("n","k")] induct 1);
clasohm@0
    66
by (SIMP_TAC add_ss 1);
clasohm@0
    67
by (ASM_SIMP_TAC add_ss 1);
clasohm@0
    68
val add_assoc = result();
clasohm@0
    69
clasohm@0
    70
goal Nat.thy "?p : m+0 = m";
clasohm@0
    71
by (res_inst_tac [("n","m")] induct 1);
clasohm@0
    72
by (SIMP_TAC add_ss 1);
clasohm@0
    73
by (ASM_SIMP_TAC add_ss 1);
clasohm@0
    74
val add_0_right = result();
clasohm@0
    75
clasohm@0
    76
goal Nat.thy "?p : m+Suc(n) = Suc(m+n)";
clasohm@0
    77
by (res_inst_tac [("n","m")] induct 1);
clasohm@0
    78
by (ALLGOALS (ASM_SIMP_TAC add_ss));
clasohm@0
    79
val add_Suc_right = result();
clasohm@0
    80
clasohm@0
    81
(*mk_typed_congs appears not to work with FOLP's version of subst*)
clasohm@0
    82