blob: 311f2d936b0209abc0b8c695210853696965f1b5 (
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 Base
begin
axiomatization
Nat :: ‹o› and
zero :: ‹o› ("0") and
suc :: ‹o ⇒ o› and
NatInd :: ‹(o ⇒ o) ⇒ o ⇒ (o ⇒ o ⇒ o) ⇒ o ⇒ o›
where
NatF: "Nat: U i" and
Nat_zero: "0: Nat" and
Nat_suc: "n: Nat ⟹ suc n: Nat" and
NatE: "⟦
n: Nat;
c⇩0: C 0;
⋀k c. ⟦k: Nat; c: C k⟧ ⟹ f k c: C (suc k);
⋀n. n: Nat ⟹ C n: U i
⟧ ⟹ NatInd (λn. C n) c⇩0 (λk c. f k c) n: C n" and
Nat_comp_zero: "⟦
c⇩0: C 0;
⋀k c. ⟦k: Nat; c: C k⟧ ⟹ f k c: C (suc k);
⋀n. n: Nat ⟹ C n: U i
⟧ ⟹ NatInd (λn. C n) c⇩0 (λk c. f k c) 0 ≡ c⇩0" and
Nat_comp_suc: "⟦
n: Nat;
c⇩0: C 0;
⋀k c. ⟦k: Nat; c: C k⟧ ⟹ f k c: C (suc k);
⋀n. n: Nat ⟹ C n: U i
⟧ ⟹
NatInd (λn. C n) c⇩0 (λk c. f k c) (suc n) ≡
f n (NatInd (λn. C n) c⇩0 (λk c. f k c) n)"
lemmas
[intros] = NatF Nat_zero Nat_suc and
[elims "?n"] = NatE and
[comps] = Nat_comp_zero Nat_comp_suc
text ‹Non-dependent recursion›
abbreviation "NatRec C ≡ NatInd (K C)"
section ‹Basic arithmetic›
definition add (infixl "+" 120) where "m + n ≡ 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 ≡ n"
unfolding add_def by reduce
lemma suc_add [comps]:
assumes "m: Nat" "n: Nat"
shows "suc m + n ≡ suc (m + n)"
unfolding add_def by reduce
Lemma (derive) add_zero:
assumes "n: Nat"
shows "n + 0 = n"
apply (elim n)
» by (reduce; intro)
» 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)
» by reduce intro
» vars _ ih by reduce (eq ih; intro)
done
Lemma (derive) suc_monotone:
assumes "m: Nat" "n: Nat"
shows "p: m = n ⟹ 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)
» by reduce intro
» 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)
» by (reduce; rule add_zero[symmetric])
» prems prms 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 ≡ NatRec Nat 0 (K $ add n) m"
end
|
