author  paulson 
Thu, 14 Jun 2018 14:23:48 +0100  
changeset 68446  92ddca1edc43 
parent 61337  4645502c3c64 
child 69593  3dda49e08b9d 
permissions  rwrr 
41777  1 
(* Title: FOLP/ex/Nat.thy 
1477  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1992 University of Cambridge 
4 
*) 

5 

60770  6 
section \<open>Theory of the natural numbers: Peano's axioms, primitive recursion\<close> 
17480  7 

8 
theory Nat 

9 
imports FOLP 

10 
begin 

11 

12 
typedecl nat 

55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
51306
diff
changeset

13 
instance nat :: "term" .. 
25991  14 

51306  15 
axiomatization 
16 
Zero :: nat ("0") and 

17 
Suc :: "nat => nat" and 

18 
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" and 

0  19 

20 
(*Proof terms*) 

51306  21 
nrec :: "[nat, p, [nat, p] => p] => p" and 
22 
ninj :: "p => p" and 

23 
nneq :: "p => p" and 

24 
rec0 :: "p" and 

25991  25 
recSuc :: "p" 
51306  26 
where 
17480  27 
induct: "[ b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x)) 
51306  28 
] ==> nrec(n,b,c):P(n)" and 
0  29 

51306  30 
Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n" and 
31 
Suc_neq_0: "p:Suc(m)=0 ==> nneq(p) : R" and 

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

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

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

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

25991  36 

51306  37 
definition add :: "[nat, nat] => nat" (infixl "+" 60) 
38 
where "m + n == rec(m, n, %x y. Suc(y))" 

17480  39 

25991  40 

60770  41 
subsection \<open>Proofs about the natural numbers\<close> 
25991  42 

61337  43 
schematic_goal Suc_n_not_n: "?p : ~ (Suc(k) = k)" 
25991  44 
apply (rule_tac n = k in induct) 
45 
apply (rule notI) 

46 
apply (erule Suc_neq_0) 

47 
apply (rule notI) 

48 
apply (erule notE) 

49 
apply (erule Suc_inject) 

50 
done 

51 

61337  52 
schematic_goal "?p : (k+m)+n = k+(m+n)" 
25991  53 
apply (rule induct) 
54 
back 

55 
back 

56 
back 

57 
back 

58 
back 

59 
back 

60 
oops 

61 

61337  62 
schematic_goal add_0 [simp]: "?p : 0+n = n" 
25991  63 
apply (unfold add_def) 
64 
apply (rule rec_0) 

65 
done 

66 

61337  67 
schematic_goal add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)" 
25991  68 
apply (unfold add_def) 
69 
apply (rule rec_Suc) 

70 
done 

71 

72 

61337  73 
schematic_goal Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)" 
25991  74 
apply (erule subst) 
75 
apply (rule refl) 

76 
done 

77 

61337  78 
schematic_goal Plus_cong: "[ p : a = x; q: b = y ] ==> ?p : a + b = x + y" 
25991  79 
apply (erule subst, erule subst, rule refl) 
80 
done 

81 

82 
lemmas nat_congs = Suc_cong Plus_cong 

83 

60770  84 
ML \<open> 
60644  85 
val add_ss = 
86 
FOLP_ss addcongs @{thms nat_congs} 

87 
> fold (addrew @{context}) @{thms add_0 add_Suc} 

60770  88 
\<close> 
25991  89 

61337  90 
schematic_goal add_assoc: "?p : (k+m)+n = k+(m+n)" 
25991  91 
apply (rule_tac n = k in induct) 
60770  92 
apply (tactic \<open>SIMP_TAC @{context} add_ss 1\<close>) 
93 
apply (tactic \<open>ASM_SIMP_TAC @{context} add_ss 1\<close>) 

25991  94 
done 
95 

61337  96 
schematic_goal add_0_right: "?p : m+0 = m" 
25991  97 
apply (rule_tac n = m in induct) 
60770  98 
apply (tactic \<open>SIMP_TAC @{context} add_ss 1\<close>) 
99 
apply (tactic \<open>ASM_SIMP_TAC @{context} add_ss 1\<close>) 

25991  100 
done 
101 

61337  102 
schematic_goal add_Suc_right: "?p : m+Suc(n) = Suc(m+n)" 
25991  103 
apply (rule_tac n = m in induct) 
60770  104 
apply (tactic \<open>ALLGOALS (ASM_SIMP_TAC @{context} add_ss)\<close>) 
25991  105 
done 
106 

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

17480  108 

0  109 
end 