blob: 8177170bb538f091c45d1c74a4c5a67025bbb54b (
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
|
theory More_Nat
imports Nat Spartan.More_Types
begin
section ‹Equality on Nat›
text ‹Via the encode-decode method.›
context begin
Lemma (derive) eq: shows "Nat → Nat → U O"
apply intro focus vars m apply elim
― ‹m ≡ 0›
apply intro focus vars n apply elim
» by (rule TopF) ― ‹n ≡ 0›
» by (rule BotF) ― ‹n ≡ suc _›
» by (rule U_in_U)
done
― ‹m ≡ suc k›
apply intro focus vars k k_eq n apply (elim n)
» by (rule BotF) ― ‹n ≡ 0›
» prems vars l proof - show "k_eq l: U O" by typechk qed
» by (rule U_in_U)
done
by (rule U_in_U)
done
text ‹
�‹eq› is defined by
eq 0 0 ≡ ⊤
eq 0 (suc k) ≡ ⊥
eq (suc k) 0 ≡ ⊥
eq (suc k) (suc l) ≡ eq k l
›
end
end
|
