author | wenzelm |
Sun, 21 May 2017 23:10:39 +0200 | |
changeset 65894 | 54f621d5fa00 |
parent 61337 | 4645502c3c64 |
child 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
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 |