blob: 59ec517ad5d5bd2e80a27cfab00dafa9bbde1a85 (
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
|
theory Nat
imports Base
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>n. n: Nat \<Longrightarrow> C n: U i;
\<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k)
\<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) n: C n" and
Nat_comp_zero: "\<lbrakk>
c\<^sub>0: C 0;
\<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k);
\<And>n. n: Nat \<Longrightarrow> C n: U i
\<rbrakk> \<Longrightarrow> NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) 0 \<equiv> c\<^sub>0" and
Nat_comp_suc: "\<lbrakk>
n: Nat;
c\<^sub>0: C 0;
\<And>k c. \<lbrakk>k: Nat; c: C k\<rbrakk> \<Longrightarrow> f k c: C (suc k);
\<And>n. n: Nat \<Longrightarrow> C n: U i
\<rbrakk> \<Longrightarrow>
NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) (suc n) \<equiv>
f n (NatInd (\<lambda>n. C n) c\<^sub>0 (\<lambda>k c. f k c) n)"
lemmas
[intros] = NatF Nat_zero Nat_suc and
[elims] = NatE and
[comps] = Nat_comp_zero Nat_comp_suc
text \<open>Non-dependent recursion\<close>
abbreviation "NatRec C \<equiv> NatInd (K C)"
section \<open>Basic arithmetic\<close>
definition add (infixl "+" 50) where
[comps]: "m + n \<equiv> NatRec Nat n (K suc) m"
definition mul (infixl "*" 55) where
[comps]: "m * n \<equiv> NatRec Nat 0 (K $ add n) m"
end
|
