1477

1 
(* Title: FOLP/ex/nat.thy

0

2 
ID: $Id$

1477

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1992 University of Cambridge


5 
*)


6 

17480

7 
header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}


8 


9 
theory Nat


10 
imports FOLP


11 
begin


12 


13 
typedecl nat

25991

14 
arities nat :: "term"


15 


16 
consts


17 
0 :: nat ("0")


18 
Suc :: "nat => nat"


19 
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"


20 
add :: "[nat, nat] => nat" (infixl "+" 60)

0

21 


22 
(*Proof terms*)

25991

23 
nrec :: "[nat, p, [nat, p] => p] => p"


24 
ninj :: "p => p"


25 
nneq :: "p => p"


26 
rec0 :: "p"


27 
recSuc :: "p"

17480

28 


29 
axioms


30 
induct: "[ b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))


31 
] ==> nrec(n,b,c):P(n)"

0

32 

17480

33 
Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"


34 
Suc_neq_0: "p:Suc(m)=0 ==> nneq(p) : R"


35 
rec_0: "rec0 : rec(0,a,f) = a"


36 
rec_Suc: "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"

25991

37 


38 
defs

17480

39 
add_def: "m+n == rec(m, n, %x y. Suc(y))"

0

40 

25991

41 
axioms

17480

42 
nrecB0: "b: A ==> nrec(0,b,c) = b : A"


43 
nrecBSuc: "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"


44 

25991

45 


46 
subsection {* Proofs about the natural numbers *}


47 


48 
lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"


49 
apply (rule_tac n = k in induct)


50 
apply (rule notI)


51 
apply (erule Suc_neq_0)


52 
apply (rule notI)


53 
apply (erule notE)


54 
apply (erule Suc_inject)


55 
done


56 


57 
lemma "?p : (k+m)+n = k+(m+n)"


58 
apply (rule induct)


59 
back


60 
back


61 
back


62 
back


63 
back


64 
back


65 
oops


66 


67 
lemma add_0 [simp]: "?p : 0+n = n"


68 
apply (unfold add_def)


69 
apply (rule rec_0)


70 
done


71 


72 
lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"


73 
apply (unfold add_def)


74 
apply (rule rec_Suc)


75 
done


76 


77 


78 
lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"


79 
apply (erule subst)


80 
apply (rule refl)


81 
done


82 


83 
lemma Plus_cong: "[ p : a = x; q: b = y ] ==> ?p : a + b = x + y"


84 
apply (erule subst, erule subst, rule refl)


85 
done


86 


87 
lemmas nat_congs = Suc_cong Plus_cong


88 


89 
ML {*


90 
val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]


91 
*}


92 


93 
lemma add_assoc: "?p : (k+m)+n = k+(m+n)"


94 
apply (rule_tac n = k in induct)


95 
apply (tactic {* SIMP_TAC add_ss 1 *})


96 
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})


97 
done


98 


99 
lemma add_0_right: "?p : m+0 = m"


100 
apply (rule_tac n = m in induct)


101 
apply (tactic {* SIMP_TAC add_ss 1 *})


102 
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})


103 
done


104 


105 
lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"


106 
apply (rule_tac n = m in induct)


107 
apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})


108 
done


109 


110 
(*mk_typed_congs appears not to work with FOLP's version of subst*)

17480

111 

0

112 
end
