From 29112d66eb3ecf4139db1da16878d8a817640696 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 1 Jun 2020 17:19:27 +0200
Subject: reorganize and add some material

---
 spartan/data/List.thy | 100 +++++++++++++++++++++++++++++---------------------
 1 file changed, 59 insertions(+), 41 deletions(-)

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

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