17481

1 
(* Title: Sequents/LK/Nat.thy

7091

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

7095

3 
Copyright 1999 University of Cambridge

7091

4 
*)


5 

17481

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


7 


8 
theory Nat


9 
imports LK


10 
begin


11 


12 
typedecl nat


13 
arities nat :: "term"

7091

14 
consts "0" :: nat ("0")

17481

15 
Suc :: "nat=>nat"


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

22896

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

7091

18 

17481

19 
axioms


20 
induct: "[ $H  $E, P(0), $F;

7123

21 
!!x. $H, P(x)  $E, P(Suc(x)), $F ] ==> $H  $E, P(n), $F"

7095

22 

17481

23 
Suc_inject: " Suc(m)=Suc(n) > m=n"


24 
Suc_neq_0: " Suc(m) ~= 0"


25 
rec_0: " rec(0,a,f) = a"


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


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


28 

21426

29 


30 
declare Suc_neq_0 [simp]


31 


32 
lemma Suc_inject_rule: "$H, $G, m = n  $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G  $E"


33 
by (rule L_of_imp [OF Suc_inject])


34 


35 
lemma Suc_n_not_n: " Suc(k) ~= k"


36 
apply (rule_tac n = k in induct)

22896

37 
apply (tactic {* simp_tac (LK_ss addsimps @{thms Suc_neq_0}) 1 *})


38 
apply (tactic {* fast_tac (LK_pack add_safes @{thms Suc_inject_rule}) 1 *})

21426

39 
done


40 


41 
lemma add_0: " 0+n = n"


42 
apply (unfold add_def)


43 
apply (rule rec_0)


44 
done


45 


46 
lemma add_Suc: " Suc(m)+n = Suc(m+n)"


47 
apply (unfold add_def)


48 
apply (rule rec_Suc)


49 
done


50 


51 
declare add_0 [simp] add_Suc [simp]


52 


53 
lemma add_assoc: " (k+m)+n = k+(m+n)"


54 
apply (rule_tac n = "k" in induct)

22896

55 
apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})


56 
apply (tactic {* simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})

21426

57 
done


58 


59 
lemma add_0_right: " m+0 = m"


60 
apply (rule_tac n = "m" in induct)

22896

61 
apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})


62 
apply (tactic {* simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})

21426

63 
done


64 


65 
lemma add_Suc_right: " m+Suc(n) = Suc(m+n)"


66 
apply (rule_tac n = "m" in induct)

22896

67 
apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})


68 
apply (tactic {* simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})

21426

69 
done


70 


71 
lemma "(!!n.  f(Suc(n)) = Suc(f(n))) ==>  f(i+j) = i+f(j)"


72 
apply (rule_tac n = "i" in induct)

22896

73 
apply (tactic {* simp_tac (LK_ss addsimps @{thms add_0}) 1 *})


74 
apply (tactic {* asm_simp_tac (LK_ss addsimps @{thms add_Suc}) 1 *})

21426

75 
done

17481

76 

7091

77 
end
