aboutsummaryrefslogtreecommitdiff
path: root/spartan/data/List.thy
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--spartan/data/List.thy100
1 files changed, 59 insertions, 41 deletions
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