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