From dc3800fa4e98e8feeae86f95bf4aafb80f01880c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 31 May 2020 13:14:35 +0200
Subject: more list

---
 spartan/data/List.thy | 36 ++++++++++++++++++++++++++++--------
 1 file changed, 28 insertions(+), 8 deletions(-)

diff --git a/spartan/data/List.thy b/spartan/data/List.thy
index a053a53..5d6cb15 100644
--- a/spartan/data/List.thy
+++ b/spartan/data/List.thy
@@ -98,6 +98,32 @@ proof (cases xs)
   show "\<And>xs. xs: List A \<Longrightarrow> xs: List A" .
 qed
 
+Lemma (derive) app:
+  assumes "A: U i" "xs: List A" "ys: List A"
+  shows "List A"
+  apply (elim xs)
+  \<guillemotright> by (fact \<open>ys:_\<close>)
+  \<guillemotright> prems vars x _ rec
+    proof - show "x # rec: List A" by typechk qed
+  done
+
+definition head_i ("head")
+  where [implicit]: "head xs \<equiv> List.head ? xs"
+
+definition tail_i ("tail")
+  where [implicit]: "tail xs \<equiv> List.tail ? xs"
+
+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
+
 Lemma (derive) map:
   assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
   shows "List B"
@@ -108,14 +134,8 @@ proof (elim xs)
   show "f x # ys: List B" by typechk
 qed
 
-thm map_def
-  \<comment> \<open>map ?A ?B ?f ?xs \<equiv> ListRec ?A (List ?B) [] (\<lambda>x xs. cons ?B (?f x)) ?xs\<close>
-
-definition head_i ("head")
-  where [implicit]: "head xs \<equiv> List.head ? xs"
-
-definition tail_i ("tail")
-  where [implicit]: "tail xs \<equiv> List.tail ? xs"
+definition rev_i ("rev")
+  where [implicit]: "rev \<equiv> List.rev ?"
 
 definition map_i ("map")
   where [implicit]: "map \<equiv> List.map ? ?"
-- 
cgit v1.2.3