author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 35762  af3ff2ba4c54 
child 42155  ffe99b07c9c0 
permissions  rwrr 
17456  1 
(* Title: CCL/ex/Nat.thy 
1474  2 
Author: Martin Coen, Cambridge University Computer Laboratory 
0  3 
Copyright 1993 University of Cambridge 
4 
*) 

5 

17456  6 
header {* Programs defined over the natural numbers *} 
7 

8 
theory Nat 

9 
imports Wfd 

10 
begin 

0  11 

12 
consts 

13 

17456  14 
not :: "i=>i" 
24825  15 
add :: "[i,i]=>i" (infixr "#+" 60) 
16 
mult :: "[i,i]=>i" (infixr "#*" 60) 

17 
sub :: "[i,i]=>i" (infixr "#" 60) 

18 
div :: "[i,i]=>i" (infixr "##" 60) 

19 
lt :: "[i,i]=>i" (infixr "#<" 60) 

20 
le :: "[i,i]=>i" (infixr "#<=" 60) 

17456  21 
ackermann :: "[i,i]=>i" 
0  22 

17456  23 
defs 
0  24 

17456  25 
not_def: "not(b) == if b then false else true" 
0  26 

17456  27 
add_def: "a #+ b == nrec(a,b,%x g. succ(g))" 
28 
mult_def: "a #* b == nrec(a,zero,%x g. b #+ g)" 

29 
sub_def: "a # b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy))) 

1149  30 
in sub(a,b)" 
17456  31 
le_def: "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy))) 
1149  32 
in le(a,b)" 
17456  33 
lt_def: "a #< b == not(b #<= a)" 
0  34 

17456  35 
div_def: "a ## b == letrec div x y be if x #< y then zero else succ(div(x#y,y)) 
1149  36 
in div(a,b)" 
17456  37 
ack_def: 
38 
"ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. 

3837  39 
ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y)))) 
1149  40 
in ack(a,b)" 
0  41 

20140  42 
lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ack_def napply_def 
43 

44 
lemma natBs [simp]: 

45 
"not(true) = false" 

46 
"not(false) = true" 

47 
"zero #+ n = n" 

48 
"succ(n) #+ m = succ(n #+ m)" 

49 
"zero #* n = zero" 

50 
"succ(n) #* m = m #+ (n #* m)" 

51 
"f^zero`a = a" 

52 
"f^succ(n)`a = f(f^n`a)" 

53 
by (simp_all add: nat_defs) 

54 

55 

56 
lemma napply_f: "n:Nat ==> f^n`f(a) = f^succ(n)`a" 

57 
apply (erule Nat_ind) 

58 
apply simp_all 

59 
done 

60 

61 
lemma addT: "[ a:Nat; b:Nat ] ==> a #+ b : Nat" 

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  64 
done 
65 

66 
lemma multT: "[ a:Nat; b:Nat ] ==> a #* b : Nat" 

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  69 
done 
70 

71 
(* Defined to return zero if a<b *) 

72 
lemma subT: "[ a:Nat; b:Nat ] ==> a # b : Nat" 

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  76 
apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) 
77 
done 

78 

79 
lemma leT: "[ a:Nat; b:Nat ] ==> a #<= b : Bool" 

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  83 
apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) 
84 
done 

85 

86 
lemma ltT: "[ a:Nat; b:Nat ] ==> a #< b : Bool" 

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  89 
done 
90 

91 

92 
subsection {* Termination Conditions for Ackermann's Function *} 

93 

94 
lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]] 

95 

96 
lemma "[ a:Nat; b:Nat ] ==> ackermann(a,b) : Nat" 

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  99 
apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+ 
100 
done 

17456  101 

0  102 
end 