38 ack_def: |
38 ack_def: |
39 "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. |
39 "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. |
40 ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y)))) |
40 ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y)))) |
41 in ack(a,b)" |
41 in ack(a,b)" |
42 |
42 |
43 ML {* use_legacy_bindings (the_context ()) *} |
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 |
44 |
102 |
45 end |
103 end |
46 |
104 |