7 |
7 |
8 theory Nat |
8 theory Nat |
9 imports "../Wfd" |
9 imports "../Wfd" |
10 begin |
10 begin |
11 |
11 |
12 definition not :: "i=>i" |
12 definition not :: "i\<Rightarrow>i" |
13 where "not(b) == if b then false else true" |
13 where "not(b) == if b then false else true" |
14 |
14 |
15 definition add :: "[i,i]=>i" (infixr "#+" 60) |
15 definition add :: "[i,i]\<Rightarrow>i" (infixr "#+" 60) |
16 where "a #+ b == nrec(a,b,%x g. succ(g))" |
16 where "a #+ b == nrec(a, b, \<lambda>x g. succ(g))" |
17 |
17 |
18 definition mult :: "[i,i]=>i" (infixr "#*" 60) |
18 definition mult :: "[i,i]\<Rightarrow>i" (infixr "#*" 60) |
19 where "a #* b == nrec(a,zero,%x g. b #+ g)" |
19 where "a #* b == nrec(a, zero, \<lambda>x g. b #+ g)" |
20 |
20 |
21 definition sub :: "[i,i]=>i" (infixr "#-" 60) |
21 definition sub :: "[i,i]\<Rightarrow>i" (infixr "#-" 60) |
22 where |
22 where |
23 "a #- b == |
23 "a #- b == |
24 letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy))) |
24 letrec sub x y be ncase(y, x, \<lambda>yy. ncase(x, zero, \<lambda>xx. sub(xx,yy))) |
25 in sub(a,b)" |
25 in sub(a,b)" |
26 |
26 |
27 definition le :: "[i,i]=>i" (infixr "#<=" 60) |
27 definition le :: "[i,i]\<Rightarrow>i" (infixr "#<=" 60) |
28 where |
28 where |
29 "a #<= b == |
29 "a #<= b == |
30 letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy))) |
30 letrec le x y be ncase(x, true, \<lambda>xx. ncase(y, false, \<lambda>yy. le(xx,yy))) |
31 in le(a,b)" |
31 in le(a,b)" |
32 |
32 |
33 definition lt :: "[i,i]=>i" (infixr "#<" 60) |
33 definition lt :: "[i,i]\<Rightarrow>i" (infixr "#<" 60) |
34 where "a #< b == not(b #<= a)" |
34 where "a #< b == not(b #<= a)" |
35 |
35 |
36 definition div :: "[i,i]=>i" (infixr "##" 60) |
36 definition div :: "[i,i]\<Rightarrow>i" (infixr "##" 60) |
37 where |
37 where |
38 "a ## b == |
38 "a ## b == |
39 letrec div x y be if x #< y then zero else succ(div(x#-y,y)) |
39 letrec div x y be if x #< y then zero else succ(div(x#-y,y)) |
40 in div(a,b)" |
40 in div(a,b)" |
41 |
41 |
42 definition ackermann :: "[i,i]=>i" |
42 definition ackermann :: "[i,i]\<Rightarrow>i" |
43 where |
43 where |
44 "ackermann(a,b) == |
44 "ackermann(a,b) == |
45 letrec ack n m be ncase(n,succ(m),%x. |
45 letrec ack n m be ncase(n, succ(m), \<lambda>x. |
46 ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y)))) |
46 ncase(m,ack(x,succ(zero)), \<lambda>y. ack(x,ack(succ(x),y)))) |
47 in ack(a,b)" |
47 in ack(a,b)" |
48 |
48 |
49 lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ackermann_def napply_def |
49 lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ackermann_def napply_def |
50 |
50 |
51 lemma natBs [simp]: |
51 lemma natBs [simp]: |
58 "f^zero`a = a" |
58 "f^zero`a = a" |
59 "f^succ(n)`a = f(f^n`a)" |
59 "f^succ(n)`a = f(f^n`a)" |
60 by (simp_all add: nat_defs) |
60 by (simp_all add: nat_defs) |
61 |
61 |
62 |
62 |
63 lemma napply_f: "n:Nat ==> f^n`f(a) = f^succ(n)`a" |
63 lemma napply_f: "n:Nat \<Longrightarrow> f^n`f(a) = f^succ(n)`a" |
64 apply (erule Nat_ind) |
64 apply (erule Nat_ind) |
65 apply simp_all |
65 apply simp_all |
66 done |
66 done |
67 |
67 |
68 lemma addT: "[| a:Nat; b:Nat |] ==> a #+ b : Nat" |
68 lemma addT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #+ b : Nat" |
69 apply (unfold add_def) |
69 apply (unfold add_def) |
70 apply typechk |
70 apply typechk |
71 done |
71 done |
72 |
72 |
73 lemma multT: "[| a:Nat; b:Nat |] ==> a #* b : Nat" |
73 lemma multT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #* b : Nat" |
74 apply (unfold add_def mult_def) |
74 apply (unfold add_def mult_def) |
75 apply typechk |
75 apply typechk |
76 done |
76 done |
77 |
77 |
78 (* Defined to return zero if a<b *) |
78 (* Defined to return zero if a<b *) |
79 lemma subT: "[| a:Nat; b:Nat |] ==> a #- b : Nat" |
79 lemma subT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #- b : Nat" |
80 apply (unfold sub_def) |
80 apply (unfold sub_def) |
81 apply typechk |
81 apply typechk |
82 apply clean_ccs |
82 apply clean_ccs |
83 apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) |
83 apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) |
84 done |
84 done |
85 |
85 |
86 lemma leT: "[| a:Nat; b:Nat |] ==> a #<= b : Bool" |
86 lemma leT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #<= b : Bool" |
87 apply (unfold le_def) |
87 apply (unfold le_def) |
88 apply typechk |
88 apply typechk |
89 apply clean_ccs |
89 apply clean_ccs |
90 apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) |
90 apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) |
91 done |
91 done |
92 |
92 |
93 lemma ltT: "[| a:Nat; b:Nat |] ==> a #< b : Bool" |
93 lemma ltT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #< b : Bool" |
94 apply (unfold not_def lt_def) |
94 apply (unfold not_def lt_def) |
95 apply (typechk leT) |
95 apply (typechk leT) |
96 done |
96 done |
97 |
97 |
98 |
98 |
99 subsection {* Termination Conditions for Ackermann's Function *} |
99 subsection {* Termination Conditions for Ackermann's Function *} |
100 |
100 |
101 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]] |
101 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]] |
102 |
102 |
103 lemma "[| a:Nat; b:Nat |] ==> ackermann(a,b) : Nat" |
103 lemma "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> ackermann(a,b) : Nat" |
104 apply (unfold ackermann_def) |
104 apply (unfold ackermann_def) |
105 apply gen_ccs |
105 apply gen_ccs |
106 apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+ |
106 apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+ |
107 done |
107 done |
108 |
108 |