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