src/CCL/ex/nat.ML
author wenzelm
Mon, 09 Nov 1998 15:32:43 +0100
changeset 5824 91113aa09371
parent 8 c3d2c6dcf3f0
permissions -rw-r--r--
Proof methods.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	CCL/ex/nat
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Martin Coen, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For nat.thy.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open Nat;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val nat_defs = [not_def,add_def,mult_def,sub_def,le_def,lt_def,ack_def,napply_def];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    13
val natBs = map (fn s=>prove_goalw Nat.thy nat_defs s (fn _ => [simp_tac term_ss 1]))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
     ["not(true) = false",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
      "not(false) = true",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
      "zero #+ n = n",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
      "succ(n) #+ m = succ(n #+ m)",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
      "zero #* n = zero",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
      "succ(n) #* m = m #+ (n #* m)",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
      "f^zero`a = a",
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
      "f^succ(n)`a = f(f^n`a)"];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    23
val nat_ss = term_ss addsimps natBs;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
(*** Lemma for napply ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
br (prem RS Nat_ind) 1;
8
c3d2c6dcf3f0 Installation of new simplfier. Previously appeared to set up the old
lcp
parents: 0
diff changeset
    29
by (ALLGOALS (asm_simp_tac nat_ss));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
val napply_f = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
(****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val prems = goalw Nat.thy [add_def] "[| a:Nat;  b:Nat |] ==> a #+ b : Nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
by (typechk_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
val addT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val prems = goalw Nat.thy [mult_def] "[| a:Nat;  b:Nat |] ==> a #* b : Nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
by (typechk_tac (addT::prems) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
val multT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
(* Defined to return zero if a<b *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val prems = goalw Nat.thy [sub_def] "[| a:Nat;  b:Nat |] ==> a #- b : Nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
by (typechk_tac (prems) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
by clean_ccs_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val subT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
val prems = goalw Nat.thy [le_def] "[| a:Nat;  b:Nat |] ==> a #<= b : Bool";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
by (typechk_tac (prems) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
by clean_ccs_tac;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
be (NatPRI RS wfstI RS (NatPR_wf RS wmap_wf RS wfI)) 1;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
val leT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
val prems = goalw Nat.thy [not_def,lt_def] "[| a:Nat;  b:Nat |] ==> a #< b : Bool";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
by (typechk_tac (prems@[leT]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val ltT = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
(* Correctness conditions for subtractive division **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
val prems = goalw Nat.thy [div_def] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
    "[| a:Nat;  b:{x:Nat.~x=zero} |] ==> a ## b : {x:Nat. DIV(a,b,x)}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
by (gen_ccs_tac (prems@[ltT,subT]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
(* Termination Conditions for Ackermann's Function *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val prems = goalw Nat.thy [ack_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
    "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
by (gen_ccs_tac prems 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val relI = NatPR_wf RS (NatPR_wf RS lex_wf RS wfI);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
by (REPEAT (eresolve_tac [NatPRI RS (lexI1 RS relI),NatPRI RS (lexI2 RS relI)] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
result();