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 +++++++++++++++-----
 spartan/data/Maybe.thy      |  6 ++++--
 spartan/data/More_Types.thy |  3 +++
 3 files changed, 22 insertions(+), 7 deletions(-)

(limited to 'spartan')

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
diff --git a/spartan/data/Maybe.thy b/spartan/data/Maybe.thy
index 98f5283..1efbb95 100644
--- a/spartan/data/Maybe.thy
+++ b/spartan/data/Maybe.thy
@@ -55,8 +55,10 @@ Lemma Maybe_comp_some:
 
 lemmas
   [intros] = MaybeF Maybe_none Maybe_some and
-  MaybeE [elims "?m"] = MaybeInd and
-  [comps] = Maybe_comp_none Maybe_comp_some
+  [comps] = Maybe_comp_none Maybe_comp_some and
+  MaybeE [elims "?m"] = MaybeInd[rotated 4]
+lemmas
+  Maybe_cases [cases] = MaybeE
 
 abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
 
diff --git a/spartan/data/More_Types.thy b/spartan/data/More_Types.thy
index fecf378..625f639 100644
--- a/spartan/data/More_Types.thy
+++ b/spartan/data/More_Types.thy
@@ -48,6 +48,9 @@ lemmas
   [elims ?s] = SumE and
   [comps] = Sum_comp_inl Sum_comp_inr
 
+method left = rule Sum_inl
+method right = rule Sum_inr
+
 
 section \<open>Empty and unit types\<close>
 
-- 
cgit v1.2.3