19087
|
1 |
(*
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Abstract Natural Numbers with polymorphic recursion *}
|
|
7 |
|
|
8 |
theory Abstract_NAT
|
|
9 |
imports Main
|
|
10 |
begin
|
|
11 |
|
|
12 |
text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *}
|
|
13 |
|
|
14 |
locale NAT =
|
|
15 |
fixes zero :: 'n
|
|
16 |
and succ :: "'n \<Rightarrow> 'n"
|
|
17 |
assumes succ_inject [simp]: "(succ m = succ n) = (m = n)"
|
|
18 |
and succ_neq_zero [simp]: "succ m \<noteq> zero"
|
|
19 |
and induct [case_names zero succ, induct type: 'n]:
|
|
20 |
"P zero \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (succ n)) \<Longrightarrow> P n"
|
|
21 |
|
|
22 |
lemma (in NAT) zero_neq_succ [simp]: "zero \<noteq> succ m"
|
|
23 |
by (rule succ_neq_zero [symmetric])
|
|
24 |
|
|
25 |
|
|
26 |
text {*
|
|
27 |
Primitive recursion as a (functional) relation -- polymorphic!
|
|
28 |
|
|
29 |
(We simulate a localized version of the inductive packages using
|
|
30 |
explicit premises + parameters, and an abbreviation.) *}
|
|
31 |
|
|
32 |
consts
|
|
33 |
REC :: "'n \<Rightarrow> ('n \<Rightarrow> 'n) \<Rightarrow> 'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('n * 'a) set"
|
|
34 |
inductive "REC zero succ e r"
|
|
35 |
intros
|
|
36 |
Rec_zero: "NAT zero succ \<Longrightarrow> (zero, e) \<in> REC zero succ e r"
|
|
37 |
Rec_succ: "NAT zero succ \<Longrightarrow> (m, n) \<in> REC zero succ e r \<Longrightarrow>
|
|
38 |
(succ m, r m n) \<in> REC zero succ e r"
|
|
39 |
|
19363
|
40 |
abbreviation (in NAT)
|
|
41 |
"Rec == REC zero succ"
|
19087
|
42 |
|
|
43 |
lemma (in NAT) Rec_functional:
|
|
44 |
fixes x :: 'n
|
|
45 |
shows "\<exists>!y::'a. (x, y) \<in> Rec e r" (is "\<exists>!y::'a. _ \<in> ?Rec")
|
|
46 |
proof (induct x)
|
|
47 |
case zero
|
|
48 |
show "\<exists>!y. (zero, y) \<in> ?Rec"
|
|
49 |
proof
|
|
50 |
show "(zero, e) \<in> ?Rec" by (rule Rec_zero)
|
|
51 |
fix y assume "(zero, y) \<in> ?Rec"
|
|
52 |
then show "y = e" by cases simp_all
|
|
53 |
qed
|
|
54 |
next
|
|
55 |
case (succ m)
|
|
56 |
from `\<exists>!y. (m, y) \<in> ?Rec`
|
|
57 |
obtain y where y: "(m, y) \<in> ?Rec"
|
|
58 |
and yy': "\<And>y'. (m, y') \<in> ?Rec \<Longrightarrow> y = y'" by blast
|
|
59 |
show "\<exists>!z. (succ m, z) \<in> ?Rec"
|
|
60 |
proof
|
|
61 |
from _ y show "(succ m, r m y) \<in> ?Rec" by (rule Rec_succ)
|
|
62 |
fix z assume "(succ m, z) \<in> ?Rec"
|
|
63 |
then obtain u where "z = r m u" and "(m, u) \<in> ?Rec" by cases simp_all
|
|
64 |
with yy' show "z = r m y" by (simp only:)
|
|
65 |
qed
|
|
66 |
qed
|
|
67 |
|
|
68 |
|
|
69 |
text {* The recursion operator -- polymorphic! *}
|
|
70 |
|
|
71 |
definition (in NAT)
|
|
72 |
"rec e r x = (THE y. (x, y) \<in> Rec e r)"
|
|
73 |
|
|
74 |
lemma (in NAT) rec_eval:
|
|
75 |
assumes Rec: "(x, y) \<in> Rec e r"
|
|
76 |
shows "rec e r x = y"
|
|
77 |
unfolding rec_def
|
|
78 |
using Rec_functional and Rec by (rule the1_equality)
|
|
79 |
|
|
80 |
lemma (in NAT) rec_zero: "rec e r zero = e"
|
|
81 |
proof (rule rec_eval)
|
|
82 |
show "(zero, e) \<in> Rec e r" by (rule Rec_zero)
|
|
83 |
qed
|
|
84 |
|
|
85 |
lemma (in NAT) rec_succ: "rec e r (succ m) = r m (rec e r m)"
|
|
86 |
proof (rule rec_eval)
|
|
87 |
let ?Rec = "Rec e r"
|
|
88 |
have "(m, rec e r m) \<in> ?Rec"
|
|
89 |
unfolding rec_def
|
|
90 |
using Rec_functional by (rule theI')
|
|
91 |
with _ show "(succ m, r m (rec e r m)) \<in> ?Rec" by (rule Rec_succ)
|
|
92 |
qed
|
|
93 |
|
|
94 |
|
|
95 |
text {* Just see that our abstract specification makes sense \dots *}
|
|
96 |
|
|
97 |
interpretation NAT [0 Suc]
|
|
98 |
proof (rule NAT.intro)
|
|
99 |
fix m n
|
|
100 |
show "(Suc m = Suc n) = (m = n)" by simp
|
|
101 |
show "Suc m \<noteq> 0" by simp
|
|
102 |
fix P
|
|
103 |
assume zero: "P 0"
|
|
104 |
and succ: "\<And>n. P n \<Longrightarrow> P (Suc n)"
|
|
105 |
show "P n"
|
|
106 |
proof (induct n)
|
|
107 |
case 0 show ?case by (rule zero)
|
|
108 |
next
|
|
109 |
case Suc then show ?case by (rule succ)
|
|
110 |
qed
|
|
111 |
qed
|
|
112 |
|
|
113 |
end
|