src/CCL/ex/Nat.thy
author wenzelm
Sat Jun 14 23:52:51 2008 +0200 (2008-06-14)
changeset 27221 31328dc30196
parent 24825 c4f13ab78f9d
child 35762 af3ff2ba4c54
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
wenzelm@17456
     1
(*  Title:      CCL/ex/Nat.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1474
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
*)
clasohm@0
     6
wenzelm@17456
     7
header {* Programs defined over the natural numbers *}
wenzelm@17456
     8
wenzelm@17456
     9
theory Nat
wenzelm@17456
    10
imports Wfd
wenzelm@17456
    11
begin
clasohm@0
    12
clasohm@0
    13
consts
clasohm@0
    14
wenzelm@17456
    15
  not   :: "i=>i"
wenzelm@24825
    16
  add   :: "[i,i]=>i"            (infixr "#+" 60)
wenzelm@24825
    17
  mult  :: "[i,i]=>i"            (infixr "#*" 60)
wenzelm@24825
    18
  sub   :: "[i,i]=>i"            (infixr "#-" 60)
wenzelm@24825
    19
  div   :: "[i,i]=>i"            (infixr "##" 60)
wenzelm@24825
    20
  lt    :: "[i,i]=>i"            (infixr "#<" 60)
wenzelm@24825
    21
  le    :: "[i,i]=>i"            (infixr "#<=" 60)
wenzelm@17456
    22
  ackermann :: "[i,i]=>i"
clasohm@0
    23
wenzelm@17456
    24
defs
clasohm@0
    25
wenzelm@17456
    26
  not_def:     "not(b) == if b then false else true"
clasohm@0
    27
wenzelm@17456
    28
  add_def:     "a #+ b == nrec(a,b,%x g. succ(g))"
wenzelm@17456
    29
  mult_def:    "a #* b == nrec(a,zero,%x g. b #+ g)"
wenzelm@17456
    30
  sub_def:     "a #- b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy)))
clasohm@1149
    31
                        in sub(a,b)"
wenzelm@17456
    32
  le_def:     "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy)))
clasohm@1149
    33
                        in le(a,b)"
wenzelm@17456
    34
  lt_def:     "a #< b == not(b #<= a)"
clasohm@0
    35
wenzelm@17456
    36
  div_def:    "a ## b == letrec div x y be if x #< y then zero else succ(div(x#-y,y))
clasohm@1149
    37
                       in div(a,b)"
wenzelm@17456
    38
  ack_def:
wenzelm@17456
    39
  "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x.
wenzelm@3837
    40
                          ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
clasohm@1149
    41
                    in ack(a,b)"
clasohm@0
    42
wenzelm@20140
    43
lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ack_def napply_def
wenzelm@20140
    44
wenzelm@20140
    45
lemma natBs [simp]:
wenzelm@20140
    46
  "not(true) = false"
wenzelm@20140
    47
  "not(false) = true"
wenzelm@20140
    48
  "zero #+ n = n"
wenzelm@20140
    49
  "succ(n) #+ m = succ(n #+ m)"
wenzelm@20140
    50
  "zero #* n = zero"
wenzelm@20140
    51
  "succ(n) #* m = m #+ (n #* m)"
wenzelm@20140
    52
  "f^zero`a = a"
wenzelm@20140
    53
  "f^succ(n)`a = f(f^n`a)"
wenzelm@20140
    54
  by (simp_all add: nat_defs)
wenzelm@20140
    55
wenzelm@20140
    56
wenzelm@20140
    57
lemma napply_f: "n:Nat ==> f^n`f(a) = f^succ(n)`a"
wenzelm@20140
    58
  apply (erule Nat_ind)
wenzelm@20140
    59
   apply simp_all
wenzelm@20140
    60
  done
wenzelm@20140
    61
wenzelm@20140
    62
lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
wenzelm@20140
    63
  apply (unfold add_def)
wenzelm@27221
    64
  apply (tactic {* typechk_tac @{context} [] 1 *})
wenzelm@20140
    65
  done
wenzelm@20140
    66
wenzelm@20140
    67
lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
wenzelm@20140
    68
  apply (unfold add_def mult_def)
wenzelm@27221
    69
  apply (tactic {* typechk_tac @{context} [] 1 *})
wenzelm@20140
    70
  done
wenzelm@20140
    71
wenzelm@20140
    72
(* Defined to return zero if a<b *)
wenzelm@20140
    73
lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
wenzelm@20140
    74
  apply (unfold sub_def)
wenzelm@27221
    75
  apply (tactic {* typechk_tac @{context} [] 1 *})
wenzelm@27221
    76
  apply (tactic {* clean_ccs_tac @{context} *})
wenzelm@20140
    77
  apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
wenzelm@20140
    78
  done
wenzelm@20140
    79
wenzelm@20140
    80
lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
wenzelm@20140
    81
  apply (unfold le_def)
wenzelm@27221
    82
  apply (tactic {* typechk_tac @{context} [] 1 *})
wenzelm@27221
    83
  apply (tactic {* clean_ccs_tac @{context} *})
wenzelm@20140
    84
  apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
wenzelm@20140
    85
  done
wenzelm@20140
    86
wenzelm@20140
    87
lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
wenzelm@20140
    88
  apply (unfold not_def lt_def)
wenzelm@27221
    89
  apply (tactic {* typechk_tac @{context} @{thms leT} 1 *})
wenzelm@20140
    90
  done
wenzelm@20140
    91
wenzelm@20140
    92
wenzelm@20140
    93
subsection {* Termination Conditions for Ackermann's Function *}
wenzelm@20140
    94
wenzelm@20140
    95
lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
wenzelm@20140
    96
wenzelm@20140
    97
lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
wenzelm@20140
    98
  apply (unfold ack_def)
wenzelm@27221
    99
  apply (tactic {* gen_ccs_tac @{context} [] 1 *})
wenzelm@20140
   100
  apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
wenzelm@20140
   101
  done
wenzelm@17456
   102
clasohm@0
   103
end