diff options
| -rw-r--r-- | spartan/data/Maybe.thy | 70 | ||||
| -rw-r--r-- | spartan/data/More_Types.thy (renamed from hott/More_Types.thy) | 5 |
2 files changed, 45 insertions, 30 deletions
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)" diff --git a/hott/More_Types.thy b/spartan/data/More_Types.thy index d29d794..f0cee6d 100644 --- a/hott/More_Types.thy +++ b/spartan/data/More_Types.thy @@ -44,7 +44,7 @@ axiomatization where lemmas [intros] = SumF Sum_inl Sum_inr and - [elims] = SumE and + [elims ?s] = SumE and [comps] = Sum_comp_inl Sum_comp_inr @@ -75,7 +75,8 @@ and lemmas [intros] = TopF TopI BotF and - [elims] = TopE BotE and + [elims ?a] = TopE and + [elims ?x] = BotE and [comps] = Top_comp |