author  wenzelm 
Mon, 02 Aug 2021 17:20:16 +0200  
changeset 74105  d3d6e01a6b00 
parent 60770  240563fbf41d 
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 

60770  6 
section \<open>Programs defined over the natural numbers\<close> 
17456  7 

8 
theory Nat 

58974  9 
imports "../Wfd" 
17456  10 
begin 
0  11 

58977  12 
definition not :: "i\<Rightarrow>i" 
42155
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 

58977  15 
definition add :: "[i,i]\<Rightarrow>i" (infixr "#+" 60) 
16 
where "a #+ b == nrec(a, b, \<lambda>x g. succ(g))" 

0  17 

58977  18 
definition mult :: "[i,i]\<Rightarrow>i" (infixr "#*" 60) 
19 
where "a #* b == nrec(a, zero, \<lambda>x g. b #+ g)" 

0  20 

58977  21 
definition sub :: "[i,i]\<Rightarrow>i" (infixr "#" 60) 
42155
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 == 
58977  24 
letrec sub x y be ncase(y, x, \<lambda>yy. ncase(x, zero, \<lambda>xx. sub(xx,yy))) 
42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

25 
in sub(a,b)" 
0  26 

58977  27 
definition le :: "[i,i]\<Rightarrow>i" (infixr "#<=" 60) 
42155
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 == 
58977  30 
letrec le x y be ncase(x, true, \<lambda>xx. ncase(y, false, \<lambda>yy. le(xx,yy))) 
42155
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 

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

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

58977  36 
definition div :: "[i,i]\<Rightarrow>i" (infixr "##" 60) 
42155
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 

58977  42 
definition ackermann :: "[i,i]\<Rightarrow>i" 
42155
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) == 
58977  45 
letrec ack n m be ncase(n, succ(m), \<lambda>x. 
46 
ncase(m,ack(x,succ(zero)), \<lambda>y. ack(x,ack(succ(x),y)))) 

42155
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 

58977  63 
lemma napply_f: "n:Nat \<Longrightarrow> f^n`f(a) = f^succ(n)`a" 
20140  64 
apply (erule Nat_ind) 
65 
apply simp_all 

66 
done 

67 

58977  68 
lemma addT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #+ b : Nat" 
20140  69 
apply (unfold add_def) 
58971  70 
apply typechk 
20140  71 
done 
72 

58977  73 
lemma multT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #* b : Nat" 
20140  74 
apply (unfold add_def mult_def) 
58971  75 
apply typechk 
20140  76 
done 
77 

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

58977  79 
lemma subT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a # b : Nat" 
20140  80 
apply (unfold sub_def) 
58971  81 
apply typechk 
82 
apply clean_ccs 

20140  83 
apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) 
84 
done 

85 

58977  86 
lemma leT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #<= b : Bool" 
20140  87 
apply (unfold le_def) 
58971  88 
apply typechk 
89 
apply clean_ccs 

20140  90 
apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) 
91 
done 

92 

58977  93 
lemma ltT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #< b : Bool" 
20140  94 
apply (unfold not_def lt_def) 
58971  95 
apply (typechk leT) 
20140  96 
done 
97 

98 

60770  99 
subsection \<open>Termination Conditions for Ackermann's Function\<close> 
20140  100 

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

102 

58977  103 
lemma "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> ackermann(a,b) : Nat" 
42155
ffe99b07c9c0
modernized specifications  some attempts to avoid wild axiomatizations;
wenzelm
parents:
35762
diff
changeset

104 
apply (unfold ackermann_def) 
58971  105 
apply gen_ccs 
20140  106 
apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+ 
107 
done 

17456  108 

0  109 
end 