|
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 |
|
40 abbreviation (in NAT) (output) |
|
41 "Rec = REC zero succ" |
|
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 |