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 \<open>Equality on Nat\<close>
text \<open>Via the encode-decode method.\<close>
context begin
Lemma (derive) eq: shows "Nat \<rightarrow> Nat \<rightarrow> U O"
apply intro focus vars m apply elim
\<comment> \<open>m \<equiv> 0\<close>
apply intro focus vars n apply elim
\<guillemotright> by (rule TopF) \<comment> \<open>n \<equiv> 0\<close>
\<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> suc _\<close>
\<guillemotright> by (rule U_in_U)
done
\<comment> \<open>m \<equiv> suc k\<close>
apply intro focus vars k k_eq n apply (elim n)
\<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> 0\<close>
\<guillemotright> prems vars l proof - show "k_eq l: U O" by typechk qed
\<guillemotright> by (rule U_in_U)
done
by (rule U_in_U)
done
text \<open>
\<^term>\<open>eq\<close> is defined by
eq 0 0 \<equiv> \<top>
eq 0 (suc k) \<equiv> \<bottom>
eq (suc k) 0 \<equiv> \<bottom>
eq (suc k) (suc l) \<equiv> eq k l
\<close>
end
end
|
