From 417af1adf5453720c55e27de212b830569311f0e Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 28 May 2020 16:00:42 +0200
Subject: bit more material

---
 spartan/data/List.thy | 24 ++++++++++++++----------
 1 file changed, 14 insertions(+), 10 deletions(-)

(limited to 'spartan/data/List.thy')

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"
-- 
cgit v1.2.3