diff options
| -rw-r--r-- | hott/Identity.thy | 6 | ||||
| -rw-r--r-- | 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 |