2 files changed, 123 insertions, 7 deletions
diff --git a/spartan/data/List.thy b/spartan/data/List.thy
index a6c41c6..3399da6 100644
--- a/spartan/data/List.thy
+++ b/spartan/data/List.thy
@@ -1,5 +1,5 @@
 theory List
-imports Spartan
+imports Maybe
 
 begin
 
@@ -17,7 +17,7 @@ where
 
   List_nil: "A: U i \<Longrightarrow> nil A: List A" and
 
-  List_cons: "\<lbrakk>x: A; l: List A\<rbrakk> \<Longrightarrow> cons A x l: List A" and
+  List_cons: "\<lbrakk>x: A; xs: List A\<rbrakk> \<Longrightarrow> cons A x xs: List A" and
 
   ListE: "\<lbrakk>
     xs: List A;
@@ -46,24 +46,78 @@ lemmas
   [elims "?xs"] = ListE and
   [comps] = List_comp_nil List_comp_cons
 
-abbreviation "ListRec A C \<equiv> ListInd A (K C)"
-
-
-section \<open>Implicit notation\<close>
+abbreviation "ListRec A C \<equiv> ListInd A (\<lambda>_. C)"
 
 definition nil_i ("[]")
   where [implicit]: "[] \<equiv> nil ?"
 
 definition cons_i (infixr "#" 50)
-  where [implicit]: "x # l \<equiv> cons ? x l"
+  where [implicit]: "x # xs \<equiv> cons ? x xs"
+
+translations
+  "[]" \<leftharpoondown> "CONST List.nil A"
+  "x # xs" \<leftharpoondown> "CONST List.cons A x xs"
+
+
+section \<open>List notation\<close>
+
+syntax
+  "_list" :: \<open>args \<Rightarrow> o\<close> ("[_]")
+translations
+  "[x, xs]" \<rightleftharpoons> "x # [xs]"
+  "[x]" \<rightleftharpoons> "x # []"
 
 
 section \<open>Standard functions\<close>
 
+\<comment> \<open>
+definition "head A \<equiv> \<lambda>xs: List A.
+  ListRec A (Maybe A) (Maybe.none A) (\<lambda>x _ _. Maybe.some A x) xs"
+\<close>
+
+Lemma (derive) head:
+  assumes "A: U i" "xs: List A"
+  shows "Maybe A"
+proof (elim 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>
+
+\<comment> \<open>
 definition "tail A \<equiv> \<lambda>xs: List A. ListRec A (List A) (nil A) (\<lambda>x xs _. xs) xs"
+\<close>
+
+Lemma (derive) tail:
+  assumes "A: U i" "xs: List A"
+  shows "List A"
+proof (elim xs)
+  show "[]: List A" by intro
+  show "\<And>xs. xs: List A \<Longrightarrow> xs: List A" .
+qed
 
+thm tail_def
+
+\<comment> \<open>
 definition "map A B \<equiv> \<lambda>f: A \<rightarrow> B. \<lambda>xs: List A.
   ListRec A (List B) (nil B) (\<lambda>x _ c. cons B (f `x) c) 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"
+  show "f x # ys: List B" by typechk
+qed
+
+thm map_def
+
+definition head_i ("head")
+  where [implicit]: "head xs \<equiv> List.head ? xs"
 
 definition tail_i ("tail")
   where [implicit]: "tail xs \<equiv> List.tail ? xs"
@@ -72,9 +126,15 @@ definition map_i ("map")
   where [implicit]: "map \<equiv> List.map ? ?"
 
 translations
+  "head" \<leftharpoondown> "CONST List.head A"
   "tail" \<leftharpoondown> "CONST List.tail A"
   "map" \<leftharpoondown> "CONST List.map A B"
 
+Lemma head_type [typechk]:
+  assumes "A: U i" "xs: List A"
+  shows "head xs: Maybe A"
+  unfolding head_def by typechk
+
 Lemma tail_type [typechk]:
   assumes "A: U i" "xs: List A"
   shows "tail xs: List A"
diff --git a/spartan/data/Maybe.thy b/spartan/data/Maybe.thy
new file mode 100644
index 0000000..532879a
--- /dev/null
+++ b/spartan/data/Maybe.thy
@@ -0,0 +1,56 @@
+theory Maybe
+imports Spartan
+
+begin
+
+axiomatization
+  Maybe    :: \<open>o \<Rightarrow> o\<close> and
+  none     :: \<open>o \<Rightarrow> o\<close> and
+  some     :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> and
+  MaybeInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
+where
+  MaybeF: "A: U i \<Longrightarrow> Maybe A: U i" and
+
+  Maybe_none: "A: U i \<Longrightarrow> none A: Maybe A" and
+
+  Maybe_some: "a: A \<Longrightarrow> some A a: Maybe A" and
+
+  MaybeE: "\<lbrakk>
+    m: Maybe A;
+    c\<^sub>0: C (none A);
+    \<And>a. a: A \<Longrightarrow> f a: C (some A a);
+    \<And>m. m: Maybe A \<Longrightarrow> C m: U i
+    \<rbrakk> \<Longrightarrow> MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) m: C m" and
+
+  Maybe_comp_none: "\<lbrakk>
+    c\<^sub>0: C (none A);
+    \<And>a. a: A \<Longrightarrow> f a: C (some A a);
+    \<And>m. m: Maybe A \<Longrightarrow> C m: U i
+    \<rbrakk> \<Longrightarrow> MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (none A) \<equiv> c\<^sub>0" and
+
+  Maybe_comp_some: "\<lbrakk>
+    m: Maybe A;
+    c\<^sub>0: C (none A);
+    \<And>a. a: A \<Longrightarrow> f a: C (some A a);
+    \<And>m. m: Maybe A \<Longrightarrow> C m: U i
+    \<rbrakk> \<Longrightarrow> MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (some A a) \<equiv> f a"
+
+lemmas
+  [intros] = MaybeF Maybe_none Maybe_some and
+  [elims "?m"] = MaybeE and
+  [comps] = Maybe_comp_none Maybe_comp_some
+
+abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
+
+definition none_i ("none")
+  where [implicit]: "none \<equiv> Maybe.none ?"
+
+definition some_i ("some")
+  where [implicit]: "some a \<equiv> Maybe.some ? a"
+
+translations
+  "none" \<leftharpoondown> "CONST Maybe.none A"
+  "some a" \<leftharpoondown> "CONST Maybe.some A a"
+
+
+end