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 
