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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
theory HoTT
imports Pure
begin
section \<open>Setup\<close>
text "For ML files, routines and setup."
section \<open>Basic definitions\<close>
text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
We do not implement universes, but simply follow the informal notation in the HoTT book."
typedecl Term
subsection \<open>Judgments\<close>
consts
is_a_type :: "Term \<Rightarrow> prop" ("(_ : U)" [0] 1000)
is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(3_ :/ _)" [0, 0] 1000)
subsection \<open>Type families\<close>
text "Type families are implemented as meta-level lambda terms of type \<open>Term \<Rightarrow> Term\<close> that further satisfy the following property."
abbreviation is_type_family :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> prop" ("(3_:/ _ \<rightarrow> U)")
where "P: A \<rightarrow> U \<equiv> (\<And>x::Term. x : A \<Longrightarrow> P(x) : U)"
subsection \<open>Definitional equality\<close>
text "We take the meta-equality \<open>\<equiv>\<close>, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory.
Note that the Pure framework already provides axioms and results for various properties of \<open>\<equiv>\<close>, which we make use of and extend where necessary."
theorem equal_types:
assumes "A \<equiv> B" and "A : U"
shows "B : U" using assms by simp
theorem equal_type_element:
assumes "A \<equiv> B" and "x : A"
shows "x : B" using assms by simp
lemmas type_equality [intro] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated]
subsection \<open>Basic types\<close>
subsubsection \<open>Dependent function/product\<close>
consts
Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
syntax
"_Prod" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 10)
"__lambda" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<^bold>\<lambda>_:_./ _)" 10)
translations
"\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
"\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
(* The above syntax translations bind the x in the expressions B, b. *)
abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 30)
where "A\<rightarrow>B \<equiv> \<Prod>_:A. B"
axiomatization
appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60)
where
Prod_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U" and
Prod_intro [intro]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (b::Term \<Rightarrow> Term).
(\<And>x::Term. x : A \<Longrightarrow> b(x) : B(x)) \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : \<Prod>x:A. B(x)" and
Prod_elim [elim]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (f::Term) (a::Term).
\<lbrakk>f : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> f`a : B(a)" and
Prod_comp [simp]: "\<And>(A::Term) (b::Term \<Rightarrow> Term) (a::Term). (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" and
Prod_uniq [simp]: "\<And>(A::Term) (f::Term). \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
lemmas Prod_formation = Prod_form Prod_form[rotated]
text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)."
subsubsection \<open>Dependent pair/sum\<close>
consts
Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
syntax
"_Sum" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 10)
translations
"\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50)
where "A\<times>B \<equiv> \<Sum>_:A. B"
axiomatization
pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and
indSum :: "[Term \<Rightarrow> Term, [Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term"
where
Sum_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) : U" and
Sum_intro [intro]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (a::Term) (b::Term).
\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> (a, b) : \<Sum>x:A. B(x)" and
Sum_elim [elim]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (C::Term \<Rightarrow> Term) (f::[Term, Term] \<Rightarrow> Term) (p::Term).
\<lbrakk>C: \<Sum>x:A. B(x) \<rightarrow> U; \<And>x y::Term. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C((x,y)); p : \<Sum>x:A. B(x)\<rbrakk> \<Longrightarrow> (indSum C f p) : C(p)" and
Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::[Term, Term] \<Rightarrow> Term) (a::Term) (b::Term). (indSum C f (a,b)) \<equiv> f a b"
lemmas Sum_formation = Sum_form Sum_form[rotated]
definition fst :: "[Term, [Term, Term] \<Rightarrow> Term] \<Rightarrow> (Term \<Rightarrow> Term)" ("(1fst[/_,/ _])")
where "fst[A, B] \<equiv> indSum (\<lambda>_. A) (\<lambda>a. \<lambda>b. a)"
lemma "fst[A, B](a,b) \<equiv> a" unfolding fst_def by simp
text "A choice had to be made for the elimination rule: we formalize the function \<open>f\<close> taking \<open>a : A\<close> and \<open>b : B(x)\<close> and returning \<open>C((a,b))\<close> as a meta level \<open>f::Term \<Rightarrow> Term\<close> instead of an object logic dependent function \<open>f : \<Prod>x:A. B(x)\<close>.
However we should be able to later show the equivalence of the formalizations."
\<comment> \<open>Projection onto first component\<close>
(*
definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1\<langle>_,_\<rangle>)") where
"\<And>A B x y. proj1\<langle>A,B\<rangle> \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. (\<lambda>x. x))"
*)
subsubsection \<open>Empty type\<close>
axiomatization
Null :: Term and
ind_Null :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(ind'_Null'(_,/ _'))")
where
Null_form: "Null : U" and
Null_elim: "\<And>C x a. \<lbrakk>x : Null \<Longrightarrow> C(x) : U; a : Null\<rbrakk> \<Longrightarrow> ind_Null(C(x), a) : C(a)"
subsubsection \<open>Natural numbers\<close>
axiomatization
Nat :: Term and
zero :: Term ("0") and
succ :: "Term \<Rightarrow> Term" and (* how to enforce \<open>succ : Nat\<rightarrow>Nat\<close>? *)
ind_Nat :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term"
where
Nat_form: "Nat : U" and
Nat_intro1: "0 : Nat" and
Nat_intro2: "\<And>n. n : Nat \<Longrightarrow> succ n : Nat"
(* computation rules *)
subsubsection \<open>Equality type\<close>
axiomatization
Equal :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term" ("(_ =_ _)") and
refl :: "Term \<Rightarrow> Term" ("(refl'(_'))")
where
Equal_form: "\<And>A a b. \<lbrakk>a : A; b : A\<rbrakk> \<Longrightarrow> a =A b : U" and
Equal_intro: "\<And>A x. x : A \<Longrightarrow> refl x : x =A x"
end
|
