blob: e8657a4a451be9030d9532d19fed8140035f2983 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
theory Nat
imports Identity
begin
axiomatization
Nat :: \<open>o\<close> and
zero :: \<open>o\<close> ("0") and
suc :: \<open>o \<Rightarrow> o\<close> and
NatInd :: \<open>(o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
where
NatF: "Nat: U i" and
Nat_zero: "0: Nat" and
Nat_suc: "n: Nat \<Longrightarrow> suc n: Nat" and
NatE: "\<lbrakk>
n: Nat;
c\<^sub>0: C 0;
\<And>k rec. \<lbrakk>k: Nat; rec: C k\<rbrakk> \<Longrightarrow> f k rec: C (suc k);
\<And>n. n: Nat \<Longrightarrow> C n: U i
\<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) n: C n" and
Nat_comp_zero: "\<lbrakk>
c\<^sub>0: C 0;
\<And>k rec. \<lbrakk>k: Nat; rec: C k\<rbrakk> \<Longrightarrow> f k rec: C (suc k);
\<And>n. n: Nat \<Longrightarrow> C n: U i
\<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) 0 \<equiv> c\<^sub>0" and
Nat_comp_suc: "\<lbrakk>
n: Nat;
c\<^sub>0: C 0;
\<And>k rec. \<lbrakk>k: Nat; rec: C k\<rbrakk> \<Longrightarrow> f k rec: C (suc k);
\<And>n. n: Nat \<Longrightarrow> C n: U i
\<rbrakk> \<Longrightarrow>
NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) (suc n) \<equiv>
f n (NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k rec. f k rec) n)"
lemmas
[intros] = NatF Nat_zero Nat_suc and
[elims "?n"] = NatE and
[comps] = Nat_comp_zero Nat_comp_suc
text \<open>Non-dependent recursion\<close>
abbreviation "NatRec C \<equiv> NatInd (\<lambda>_. C)"
section \<open>Basic arithmetic\<close>
definition add (infixl "+" 120) where "m + n \<equiv> NatRec Nat n (K suc) m"
lemma add_type [typechk]:
assumes "m: Nat" "n: Nat"
shows "m + n: Nat"
unfolding add_def by typechk
lemma zero_add [comps]:
assumes "n: Nat"
shows "0 + n \<equiv> n"
unfolding add_def by reduce
lemma suc_add [comps]:
assumes "m: Nat" "n: Nat"
shows "suc m + n \<equiv> suc (m + n)"
unfolding add_def by reduce
Lemma (derive) add_zero:
assumes "n: Nat"
shows "n + 0 = n"
apply (elim n)
\<guillemotright> by (reduce; intro)
\<guillemotright> vars _ ih by reduce (eq ih; intro)
done
Lemma (derive) add_suc:
assumes "m: Nat" "n: Nat"
shows "m + suc n = suc (m + n)"
apply (elim m)
\<guillemotright> by reduce intro
\<guillemotright> vars _ ih by reduce (eq ih; intro)
done
Lemma (derive) suc_monotone:
assumes "m: Nat" "n: Nat"
shows "p: m = n \<Longrightarrow> suc m = suc n"
by (eq p) intro
Lemma (derive) add_assoc:
assumes "l: Nat" "m: Nat" "n: Nat"
shows "l + (m + n) = (l + m) + n"
apply (elim l)
\<guillemotright> by reduce intro
\<guillemotright> vars _ ih by reduce (eq ih; intro)
done
Lemma (derive) add_comm:
assumes "m: Nat" "n: Nat"
shows "m + n = n + m"
apply (elim m)
\<guillemotright> by (reduce; rule add_zero[symmetric])
\<guillemotright> prems vars m ih
proof reduce
have "suc (m + n) = suc (n + m)" by (eq ih) intro
also have ".. = n + suc m" by (rule add_suc[symmetric])
finally show "suc (m + n) = n + suc m" by this
qed
done
definition mul (infixl "*" 120) where
[comps]: "m * n \<equiv> NatRec Nat 0 (K $ add n) m"
end
|
