1(* Title: CCL/ex/Nat.thy 2 Author: Martin Coen, Cambridge University Computer Laboratory 3 Copyright 1993 University of Cambridge 4*) 5 6section \<open>Programs defined over the natural numbers\<close> 7 8theory Nat 9imports "../Wfd" 10begin 11 12definition not :: "i\<Rightarrow>i" 13 where "not(b) == if b then false else true" 14 15definition add :: "[i,i]\<Rightarrow>i" (infixr "#+" 60) 16 where "a #+ b == nrec(a, b, \<lambda>x g. succ(g))" 17 18definition mult :: "[i,i]\<Rightarrow>i" (infixr "#*" 60) 19 where "a #* b == nrec(a, zero, \<lambda>x g. b #+ g)" 20 21definition sub :: "[i,i]\<Rightarrow>i" (infixr "#-" 60) 22 where 23 "a #- b == 24 letrec sub x y be ncase(y, x, \<lambda>yy. ncase(x, zero, \<lambda>xx. sub(xx,yy))) 25 in sub(a,b)" 26 27definition le :: "[i,i]\<Rightarrow>i" (infixr "#<=" 60) 28 where 29 "a #<= b == 30 letrec le x y be ncase(x, true, \<lambda>xx. ncase(y, false, \<lambda>yy. le(xx,yy))) 31 in le(a,b)" 32 33definition lt :: "[i,i]\<Rightarrow>i" (infixr "#<" 60) 34 where "a #< b == not(b #<= a)" 35 36definition div :: "[i,i]\<Rightarrow>i" (infixr "##" 60) 37 where 38 "a ## b == 39 letrec div x y be if x #< y then zero else succ(div(x#-y,y)) 40 in div(a,b)" 41 42definition ackermann :: "[i,i]\<Rightarrow>i" 43 where 44 "ackermann(a,b) == 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)))) 47 in ack(a,b)" 48 49lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ackermann_def napply_def 50 51lemma 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 63lemma napply_f: "n:Nat \<Longrightarrow> f^n`f(a) = f^succ(n)`a" 64 apply (erule Nat_ind) 65 apply simp_all 66 done 67 68lemma addT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #+ b : Nat" 69 apply (unfold add_def) 70 apply typechk 71 done 72 73lemma multT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #* b : Nat" 74 apply (unfold add_def mult_def) 75 apply typechk 76 done 77 78(* Defined to return zero if a<b *) 79lemma subT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #- b : Nat" 80 apply (unfold sub_def) 81 apply typechk 82 apply clean_ccs 83 apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) 84 done 85 86lemma leT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #<= b : Bool" 87 apply (unfold le_def) 88 apply typechk 89 apply clean_ccs 90 apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]]) 91 done 92 93lemma ltT: "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> a #< b : Bool" 94 apply (unfold not_def lt_def) 95 apply (typechk leT) 96 done 97 98 99subsection \<open>Termination Conditions for Ackermann's Function\<close> 100 101lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]] 102 103lemma "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> ackermann(a,b) : Nat" 104 apply (unfold ackermann_def) 105 apply gen_ccs 106 apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+ 107 done 108 109end 110