aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--hott/Identity.thy6
-rw-r--r--spartan/data/List.thy100
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