diff options
author | Josh Chen | 2020-05-26 16:39:35 +0200 |
---|---|---|
committer | Josh Chen | 2020-05-26 16:39:35 +0200 |
commit | 8ba8357a0b4640a3be817fd0645d026b568bc552 (patch) | |
tree | 2deb740dfc97187f5124025b610dc7ef0906a988 /spartan/data/Maybe.thy | |
parent | e6b5a8f3e1128495d9e956fa4f4fa56da02350dc (diff) |
Maybe and more List
Diffstat (limited to '')
-rw-r--r-- | spartan/data/Maybe.thy | 56 |
1 files changed, 56 insertions, 0 deletions
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 |