From 29112d66eb3ecf4139db1da16878d8a817640696 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 1 Jun 2020 17:19:27 +0200
Subject: reorganize and add some material

---
 hott/Identity.thy     |   6 +--
 spartan/data/List.thy | 100 +++++++++++++++++++++++++++++---------------------
 2 files changed, 62 insertions(+), 44 deletions(-)

diff --git a/hott/Identity.thy b/hott/Identity.thy
index b82c9c2..8675134 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -313,7 +313,7 @@ Lemma (derive) transport_left_inv:
     "x: A" "y: A"
     "p: x =\<^bsub>A\<^esub> y"
   shows "(trans P p\<inverse>) \<circ> (trans P p) = id (P x)"
-  by (eq p) (reduce; intro)
+  by (eq p) (reduce; refl)
 
 Lemma (derive) transport_right_inv:
   assumes
@@ -632,8 +632,8 @@ Lemma (derive) eckmann_hilton:
   proof -
     have "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>"
       by (rule pathcomp_eq_horiz_pathcomp)
-    also have ".. = \<alpha> \<star>' \<beta>"
-      by (rule \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp'[simplified comps])
+    also have [simplified comps]: ".. = \<alpha> \<star>' \<beta>"
+      by (transport eq: \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp') refl
     also have ".. = \<beta> \<bullet> \<alpha>"
       by (rule pathcomp_eq_horiz_pathcomp')
     finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>"
diff --git a/spartan/data/List.thy b/spartan/data/List.thy
index 5d6cb15..8fdaa1d 100644
--- a/spartan/data/List.thy
+++ b/spartan/data/List.thy
@@ -82,6 +82,8 @@ translations
 
 section \<open>Standard functions\<close>
 
+subsection \<open>Head and tail\<close>
+
 Lemma (derive) head:
   assumes "A: U i" "xs: List A"
   shows "Maybe A"
@@ -98,6 +100,35 @@ proof (cases xs)
   show "\<And>xs. xs: List A \<Longrightarrow> xs: List A" .
 qed
 
+definition head_i ("head") where [implicit]: "head xs \<equiv> List.head ? xs"
+definition tail_i ("tail") where [implicit]: "tail xs \<equiv> List.tail ? xs"
+
+translations
+  "head" \<leftharpoondown> "CONST List.head A"
+  "tail" \<leftharpoondown> "CONST List.tail A"
+
+Lemma head_type [typechk]:
+  assumes "A: U i" "xs: List A"
+  shows "head xs: Maybe A"
+  unfolding head_def by typechk
+
+Lemma head_of_cons [comps]:
+  assumes "A: U i" "x: A" "xs: List A"
+  shows "head (x # xs) \<equiv> some x"
+  unfolding head_def ListCase_def by reduce
+
+Lemma tail_type [typechk]:
+  assumes "A: U i" "xs: List A"
+  shows "tail xs: List A"
+  unfolding tail_def by typechk
+
+Lemma tail_of_cons [comps]:
+  assumes "A: U i" "x: A" "xs: List A"
+  shows "tail (x # xs) \<equiv> xs"
+  unfolding tail_def ListCase_def by reduce
+
+subsection \<open>Append\<close>
+
 Lemma (derive) app:
   assumes "A: U i" "xs: List A" "ys: List A"
   shows "List A"
@@ -107,22 +138,11 @@ Lemma (derive) app:
     proof - show "x # rec: List A" by typechk qed
   done
 
-definition head_i ("head")
-  where [implicit]: "head xs \<equiv> List.head ? xs"
+definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app ? xs ys"
 
-definition tail_i ("tail")
-  where [implicit]: "tail xs \<equiv> List.tail ? xs"
+translations "app" \<leftharpoondown> "CONST List.app A"
 
-definition app_i ("app")
-  where [implicit]: "app xs ys \<equiv> List.app ? xs ys"
-
-Lemma (derive) rev:
-  assumes "A: U i" "xs: List A"
-  shows "List A"
-  apply (elim xs)
-  \<guillemotright> by (rule List_nil)
-  \<guillemotright> prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed
-  done
+subsection \<open>Map\<close>
 
 Lemma (derive) map:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
@@ -134,41 +154,39 @@ proof (elim xs)
   show "f x # ys: List B" by typechk
 qed
 
-definition rev_i ("rev")
-  where [implicit]: "rev \<equiv> List.rev ?"
+definition map_i ("map") where [implicit]: "map \<equiv> List.map ? ?"
 
-definition map_i ("map")
-  where [implicit]: "map \<equiv> List.map ? ?"
+translations "map" \<leftharpoondown> "CONST List.map A B"
 
-translations
-  "head" \<leftharpoondown> "CONST List.head A"
-  "tail" \<leftharpoondown> "CONST List.tail A"
-  "map" \<leftharpoondown> "CONST List.map A B"
+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
 
-Lemma head_type [typechk]:
-  assumes "A: U i" "xs: List A"
-  shows "head xs: Maybe A"
-  unfolding head_def by typechk
 
-Lemma head_of_cons [comps]:
-  assumes "A: U i" "x: A" "xs: List A"
-  shows "head (x # xs) \<equiv> some x"
-  unfolding head_def ListCase_def by reduce
+subsection \<open>Reverse\<close>
 
-Lemma tail_type [typechk]:
+Lemma (derive) rev:
   assumes "A: U i" "xs: List A"
-  shows "tail xs: List A"
-  unfolding tail_def by typechk
+  shows "List A"
+  apply (elim xs)
+  \<guillemotright> by (rule List_nil)
+  \<guillemotright> prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed
+  done
 
-Lemma tail_of_cons [comps]:
-  assumes "A: U i" "x: A" "xs: List A"
-  shows "tail (x # xs) \<equiv> xs"
-  unfolding tail_def ListCase_def by reduce
+definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
 
-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
+translations "rev" \<leftharpoondown> "CONST List.rev A"
+
+Lemma rev_type [typechk]:
+  assumes "A: U i" "xs: List A"
+  shows "rev xs: List A"
+  unfolding rev_def by typechk
+
+Lemma rev_nil [comps]:
+  assumes "A: U i"
+  shows "rev (nil A) \<equiv> nil A"
+  unfolding rev_def by reduce
 
 
 end
-- 
cgit v1.2.3