author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 42155  ffe99b07c9c0 
child 58889  5b7a9633cfa8 
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 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

12 
definition not :: "i=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

13 
where "not(b) == if b then false else true" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

14 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

15 
definition add :: "[i,i]=>i" (infixr "#+" 60) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

16 
where "a #+ b == nrec(a,b,%x g. succ(g))" 
0  17 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

18 
definition mult :: "[i,i]=>i" (infixr "#*" 60) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

19 
where "a #* b == nrec(a,zero,%x g. b #+ g)" 
0  20 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

21 
definition sub :: "[i,i]=>i" (infixr "#" 60) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

22 
where 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

23 
"a # b == 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

24 
letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy))) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

25 
in sub(a,b)" 
0  26 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

27 
definition le :: "[i,i]=>i" (infixr "#<=" 60) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

28 
where 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

29 
"a #<= b == 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

30 
letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy))) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

31 
in le(a,b)" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

32 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

33 
definition lt :: "[i,i]=>i" (infixr "#<" 60) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

34 
where "a #< b == not(b #<= a)" 
0  35 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

36 
definition div :: "[i,i]=>i" (infixr "##" 60) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

37 
where 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

38 
"a ## b == 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

39 
letrec div x y be if x #< y then zero else succ(div(x#y,y)) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

40 
in div(a,b)" 
0  41 

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

42 
definition ackermann :: "[i,i]=>i" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

43 
where 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

44 
"ackermann(a,b) == 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

45 
letrec ack n m be ncase(n,succ(m),%x. 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

46 
ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y)))) 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

47 
in ack(a,b)" 
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

48 

ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

49 
lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ackermann_def napply_def 
20140  50 

51 
lemma natBs [simp]: 

52 
"not(true) = false" 

53 
"not(false) = true" 

54 
"zero #+ n = n" 

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

56 
"zero #* n = zero" 

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

58 
"f^zero`a = a" 

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

60 
by (simp_all add: nat_defs) 

61 

62 

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

64 
apply (erule Nat_ind) 

65 
apply simp_all 

66 
done 

67 

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

69 
apply (unfold add_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

70 
apply (tactic {* typechk_tac @{context} [] 1 *}) 
20140  71 
done 
72 

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

74 
apply (unfold add_def mult_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

75 
apply (tactic {* typechk_tac @{context} [] 1 *}) 
20140  76 
done 
77 

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

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

80 
apply (unfold sub_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 leT: "[ a:Nat; b:Nat ] ==> a #<= b : Bool" 

87 
apply (unfold le_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

88 
apply (tactic {* typechk_tac @{context} [] 1 *}) 
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

89 
apply (tactic {* clean_ccs_tac @{context} *}) 
20140  90 
apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) 
91 
done 

92 

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

94 
apply (unfold not_def lt_def) 

27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

95 
apply (tactic {* typechk_tac @{context} @{thms leT} 1 *}) 
20140  96 
done 
97 

98 

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

100 

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

102 

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

42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

104 
apply (unfold ackermann_def) 
27221
31328dc30196
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
24825
diff
changeset

105 
apply (tactic {* gen_ccs_tac @{context} [] 1 *}) 
20140  106 
apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+ 
107 
done 

17456  108 

0  109 
end 