aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--ROOT5
-rw-r--r--hott/HoTT.thy10
-rw-r--r--hott/Identity.thy4
-rw-r--r--hott/More_Types.thy (renamed from hott/Base.thy)10
-rw-r--r--hott/Nat.thy2
-rw-r--r--spartan/core/Spartan.thy9
-rw-r--r--spartan/data/List.thy79
7 files changed, 103 insertions, 16 deletions
diff --git a/ROOT b/ROOT
index 1e8017c..b716396 100644
--- a/ROOT
+++ b/ROOT
@@ -17,7 +17,7 @@ session Spartan in spartan = Spartan_Core +
directories
data
theories
- "data/List"
+ List
session HoTT in hott = Spartan +
description "
@@ -28,8 +28,9 @@ session HoTT in hott = Spartan +
Available online at https://homotopytypetheory.org/book.
"
theories
- Base
+ HoTT (global)
Identity
Equivalence
+ More_Types
Nat
diff --git a/hott/HoTT.thy b/hott/HoTT.thy
new file mode 100644
index 0000000..0b3040c
--- /dev/null
+++ b/hott/HoTT.thy
@@ -0,0 +1,10 @@
+theory HoTT
+imports
+ Identity
+ Equivalence
+ More_Types
+ Nat
+
+begin
+
+end
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 3a982f6..3fef536 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -30,13 +30,13 @@ axiomatization where
b: A;
\<And>x y p. \<lbrakk>p: x =\<^bsub>A\<^esub> y; x: A; y: A\<rbrakk> \<Longrightarrow> C x y p: U i;
\<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
- \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a b p: C a b p" and
+ \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a b p: C a b p" and
Id_comp: "\<lbrakk>
a: A;
\<And>x y p. \<lbrakk>x: A; y: A; p: x =\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow> C x y p: U i;
\<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
- \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a a (refl a) \<equiv> f a"
+ \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a a (refl a) \<equiv> f a"
lemmas
[intros] = IdF IdI and
diff --git a/hott/Base.thy b/hott/More_Types.thy
index 610a373..17789f8 100644
--- a/hott/Base.thy
+++ b/hott/More_Types.thy
@@ -1,17 +1,9 @@
-theory Base
+theory More_Types
imports Equivalence
begin
-section \<open>Notation\<close>
-
-syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
-translations "a $ b" \<rightharpoonup> "a (b)"
-
-abbreviation (input) K where "K x \<equiv> \<lambda>_. x"
-
-
section \<open>Sum type\<close>
axiomatization
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 311f2d9..e129be0 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -1,5 +1,5 @@
theory Nat
-imports Base
+imports Equivalence
begin
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index b4f7772..50002a6 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -18,6 +18,11 @@ section \<open>Preamble\<close>
declare [[eta_contract=false]]
+syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
+translations "a $ b" \<rightharpoonup> "a (b)"
+
+abbreviation (input) K where "K x \<equiv> \<lambda>_. x"
+
section \<open>Metatype setup\<close>
@@ -118,8 +123,8 @@ axiomatization where
p: \<Sum>x: A. B x;
A: U i;
\<And>x. x : A \<Longrightarrow> B x: U i;
- \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i;
- \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>
+ \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>;
+ \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i
\<rbrakk> \<Longrightarrow> SigInd A (\<lambda>x. B x) (\<lambda>p. C p) f p: C p" and
Sig_comp: "\<lbrakk>
diff --git a/spartan/data/List.thy b/spartan/data/List.thy
index 71a879b..323ef7e 100644
--- a/spartan/data/List.thy
+++ b/spartan/data/List.thy
@@ -3,4 +3,83 @@ imports Spartan
begin
+(*TODO: Inductive type and recursive function definitions. The ad-hoc
+ axiomatization below should be subsumed once general inductive types are
+ properly implemented.*)
+
+axiomatization
+ List :: \<open>o \<Rightarrow> o\<close> and
+ nil :: \<open>o \<Rightarrow> o\<close> and
+ cons :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> and
+ ListInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
+where
+ ListF: "A: U i \<Longrightarrow> List A: U i" and
+
+ List_nil: "A: U i \<Longrightarrow> nil A: List A" and
+
+ List_cons: "\<lbrakk>x: A; l: List A\<rbrakk> \<Longrightarrow> cons A x l: List A" and
+
+ ListE: "\<lbrakk>
+ xs: List A;
+ c\<^sub>0: C (nil A);
+ \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs);
+ \<And>xs. xs: List A \<Longrightarrow> C xs: U i
+ \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) xs: C xs" and
+
+ List_comp_nil: "\<lbrakk>
+ c\<^sub>0: C (nil A);
+ \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs);
+ \<And>xs. xs: List A \<Longrightarrow> C xs: U i
+ \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) (nil A) \<equiv> c\<^sub>0" and
+
+ List_comp_cons: "\<lbrakk>
+ xs: List A;
+ c\<^sub>0: C (nil A);
+ \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs);
+ \<And>xs. xs: List A \<Longrightarrow> C xs: U i
+ \<rbrakk> \<Longrightarrow>
+ ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) (cons A x xs) \<equiv>
+ f x xs (ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) xs)"
+
+lemmas
+ [intros] = ListF List_nil List_cons and
+ [elims "?xs"] = ListE and
+ [comps] = List_comp_nil List_comp_cons
+
+abbreviation "ListRec A C \<equiv> ListInd A (K C)"
+
+
+section \<open>Implicit notation\<close>
+
+definition nil_i ("[]")
+ where [implicit]: "[] \<equiv> nil ?"
+
+definition cons_i (infixr "#" 50)
+ where [implicit]: "x # l \<equiv> cons ? x l"
+
+
+section \<open>Standard functions\<close>
+
+definition "tail A \<equiv> \<lambda>xs: List A. ListRec A (List A) (nil A) (\<lambda>x xs _. xs) xs"
+
+definition "map A B \<equiv> \<lambda>f: A \<rightarrow> B. \<lambda>xs: List A.
+ ListRec A (List B) (nil B) (\<lambda>x _ c. cons B (f `x) c) xs"
+
+definition tail_i ("tail")
+ where [implicit]: "tail xs \<equiv> List.tail ? xs"
+
+definition map_i ("map")
+ where [implicit]: "map \<equiv> List.map ? ?"
+
+Lemma tail_type [typechk]:
+ assumes "A: U i" "xs: List A"
+ shows "tail xs: List A"
+ unfolding tail_def by typechk
+
+Lemma map_type [typechk]:
+ assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
+ shows "map f xs: List B"
+ unfolding map_def by typechk
+
+
end