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