From 62c1c8f306bff84b74b3b1c935d0d6722e1251a2 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Wed, 27 May 2020 21:31:35 +0200
Subject: 1. Define Maybe in terms of other types. 2. Move More_Types to
 Spartan

---
 spartan/data/Maybe.thy | 70 ++++++++++++++++++++++++++++++--------------------
 1 file changed, 42 insertions(+), 28 deletions(-)

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

diff --git a/spartan/data/Maybe.thy b/spartan/data/Maybe.thy
index 532879a..dc3ad04 100644
--- a/spartan/data/Maybe.thy
+++ b/spartan/data/Maybe.thy
@@ -1,43 +1,57 @@
 theory Maybe
-imports Spartan
+imports More_Types
 
 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
+definition "Maybe A \<equiv> A \<or> \<top>"
+definition "none A \<equiv> inr A \<top> tt"
+definition "some A a \<equiv> inl A \<top> a"
 
+lemma
+  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"
+  unfolding Maybe_def none_def some_def by typechk+
 
-  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
+Lemma (derive) MaybeInd:
+  assumes
+    "A: U i"
+    "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
+    "c\<^sub>0: C (none A)"
+    "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
+    "m: Maybe A"
+  shows "?MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) m: C m"
+  supply assms[unfolded Maybe_def none_def some_def]
+  apply (elim m)
+  \<guillemotright> unfolding Maybe_def .
+  \<guillemotright> by (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
+  \<guillemotright> by elim (rule \<open>_: C (inr _ _ _)\<close>)
+  done
 
-  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
+Lemma Maybe_comp_none:
+  assumes
+    "A: U i"
+    "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"
+  shows "MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (none A) \<equiv> c\<^sub>0"
+  supply assms[unfolded Maybe_def some_def none_def]
+  unfolding MaybeInd_def none_def by reduce
 
-  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"
+Lemma Maybe_comp_some:
+  assumes
+    "A: U i"
+    "a: 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"
+  shows "MaybeInd A (\<lambda>m. C m) c\<^sub>0 (\<lambda>a. f a) (some A a) \<equiv> f a"
+  supply assms[unfolded Maybe_def some_def none_def]
+  unfolding MaybeInd_def some_def by (reduce add: Maybe_def)
 
 lemmas
   [intros] = MaybeF Maybe_none Maybe_some and
-  [elims "?m"] = MaybeE and
+  MaybeE [elims "?m"] = MaybeInd and
   [comps] = Maybe_comp_none Maybe_comp_some
 
 abbreviation "MaybeRec A C \<equiv> MaybeInd A (K C)"
-- 
cgit v1.2.3