From 1ccd93665a01acdc25b37409e94b71615ced5393 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 28 May 2020 14:08:26 +0200
Subject: more List and Maybe

---
 spartan/data/List.thy | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

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

diff --git a/spartan/data/List.thy b/spartan/data/List.thy
index 52f042b..c581019 100644
--- a/spartan/data/List.thy
+++ b/spartan/data/List.thy
@@ -50,19 +50,29 @@ lemmas
 
 abbreviation "ListRec A C \<equiv> ListInd A (\<lambda>_. C)"
 
+Lemma (derive) ListCase:
+  assumes
+    "A: U i" "\<And>xs. xs: List A \<Longrightarrow> C xs: U i" and
+    nil_case: "c\<^sub>0: C (nil A)" and
+    cons_case: "\<And>x xs. \<lbrakk>x: A; xs: List A\<rbrakk> \<Longrightarrow> f x xs: C (cons A x xs)" and
+    "xs: List A"
+  shows "?List_cases A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs. f x xs) xs: C xs"
+  by (elim xs) (fact nil_case, rule cons_case)
+
+lemmas List_cases [cases] = ListCase[rotated 4]
+
+
+section \<open>Notation\<close>
+
 definition nil_i ("[]")
   where [implicit]: "[] \<equiv> nil ?"
 
-definition cons_i (infixr "#" 50)
+definition cons_i (infixr "#" 120)
   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
-- 
cgit v1.2.3