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 | |
parent | e6b5a8f3e1128495d9e956fa4f4fa56da02350dc (diff) |
Maybe and more List
Diffstat (limited to '')
-rw-r--r-- | spartan/data/List.thy | 74 | ||||
-rw-r--r-- | spartan/data/Maybe.thy | 56 |
2 files changed, 123 insertions, 7 deletions
diff --git a/spartan/data/List.thy b/spartan/data/List.thy index a6c41c6..3399da6 100644 --- a/spartan/data/List.thy +++ b/spartan/data/List.thy @@ -1,5 +1,5 @@ theory List -imports Spartan +imports Maybe begin @@ -17,7 +17,7 @@ where List_nil: "A: U i \<Longrightarrow> nil A: List A" and - List_cons: "\<lbrakk>x: A; l: List A\<rbrakk> \<Longrightarrow> cons A x l: List A" and + List_cons: "\<lbrakk>x: A; xs: List A\<rbrakk> \<Longrightarrow> cons A x xs: List A" and ListE: "\<lbrakk> xs: List A; @@ -46,24 +46,78 @@ lemmas [elims "?xs"] = ListE and [comps] = List_comp_nil List_comp_cons -abbreviation "ListRec A C \<equiv> ListInd A (K C)" - - -section \<open>Implicit notation\<close> +abbreviation "ListRec A C \<equiv> ListInd A (\<lambda>_. C)" definition nil_i ("[]") where [implicit]: "[] \<equiv> nil ?" definition cons_i (infixr "#" 50) - where [implicit]: "x # l \<equiv> cons ? x l" + 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 + "[x, xs]" \<rightleftharpoons> "x # [xs]" + "[x]" \<rightleftharpoons> "x # []" section \<open>Standard functions\<close> +\<comment> \<open> +definition "head A \<equiv> \<lambda>xs: List A. + ListRec A (Maybe A) (Maybe.none A) (\<lambda>x _ _. Maybe.some A x) xs" +\<close> + +Lemma (derive) head: + assumes "A: U i" "xs: List A" + shows "Maybe A" +proof (elim xs) + show "none: Maybe A" by intro + show "\<And>x. x: A \<Longrightarrow> some x: Maybe A" by intro +qed + +thm head_def \<comment> \<open>head ?A ?xs \<equiv> ListRec ?A (Maybe ?A) none (\<lambda>x xs c. some x) ?xs\<close> + +\<comment> \<open> definition "tail A \<equiv> \<lambda>xs: List A. ListRec A (List A) (nil A) (\<lambda>x xs _. xs) xs" +\<close> + +Lemma (derive) tail: + assumes "A: U i" "xs: List A" + shows "List A" +proof (elim xs) + show "[]: List A" by intro + show "\<And>xs. xs: List A \<Longrightarrow> xs: List A" . +qed +thm tail_def + +\<comment> \<open> definition "map A B \<equiv> \<lambda>f: A \<rightarrow> B. \<lambda>xs: List A. ListRec A (List B) (nil B) (\<lambda>x _ c. cons B (f `x) c) xs" +\<close> + +Lemma (derive) map: + assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A" + shows "List B" +proof (elim xs) + show "[]: List B" by intro + next fix x xs ys + assume "x: A" "xs: List A" "ys: List B" + show "f x # ys: List B" by typechk +qed + +thm map_def + +definition head_i ("head") + where [implicit]: "head xs \<equiv> List.head ? xs" definition tail_i ("tail") where [implicit]: "tail xs \<equiv> List.tail ? xs" @@ -72,9 +126,15 @@ definition map_i ("map") where [implicit]: "map \<equiv> List.map ? ?" translations + "head" \<leftharpoondown> "CONST List.head A" "tail" \<leftharpoondown> "CONST List.tail A" "map" \<leftharpoondown> "CONST List.map A B" +Lemma head_type [typechk]: + assumes "A: U i" "xs: List A" + shows "head xs: Maybe A" + unfolding head_def by typechk + Lemma tail_type [typechk]: assumes "A: U i" "xs: List A" shows "tail xs: List A" 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 |