aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--spartan/data/List.thy24
1 files changed, 14 insertions, 10 deletions
diff --git a/spartan/data/List.thy b/spartan/data/List.thy
index c581019..a053a53 100644
--- a/spartan/data/List.thy
+++ b/spartan/data/List.thy
@@ -85,32 +85,26 @@ section \<open>Standard functions\<close>
Lemma (derive) head:
assumes "A: U i" "xs: List A"
shows "Maybe A"
-proof (elim xs)
+proof (cases xs)
show "none: Maybe A" by intro
show "\<And>x. x: A \<Longrightarrow> some x: Maybe A" by intro
qed
-thm head_def
- \<comment> \<open>head ?A ?xs \<equiv> ListRec ?A (Maybe ?A) none (\<lambda>x xs c. some x) ?xs\<close>
-
Lemma (derive) tail:
assumes "A: U i" "xs: List A"
shows "List A"
-proof (elim xs)
+proof (cases xs)
show "[]: List A" by intro
show "\<And>xs. xs: List A \<Longrightarrow> xs: List A" .
qed
-thm tail_def
- \<comment> \<open>tail ?A ?xs \<equiv> ListRec ?A (List ?A) [] (\<lambda>x xs c. xs) ?xs\<close>
-
Lemma (derive) map:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
shows "List B"
proof (elim xs)
show "[]: List B" by intro
- next fix x xs ys
- assume "x: A" "xs: List A" "ys: List B"
+ next fix x ys
+ assume "x: A" "ys: List B"
show "f x # ys: List B" by typechk
qed
@@ -136,11 +130,21 @@ Lemma head_type [typechk]:
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
+
Lemma map_type [typechk]:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
shows "map f xs: List B"