1 files changed, 0 insertions, 76 deletions
diff --git a/spartan/data/Maybe.thy b/spartan/data/Maybe.thy
deleted file mode 100644
index 1efbb95..0000000
--- a/spartan/data/Maybe.thy
+++ /dev/null
@@ -1,76 +0,0 @@
-chapter \<open>Maybe type\<close>
-
-theory Maybe
-imports More_Types
-
-begin
-
-text \<open>Defined as a sum.\<close>
-
-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+
-
-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
-
-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
-
-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
-  [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)"
-
-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