diff options
Diffstat (limited to 'spartan/data')
-rw-r--r-- | spartan/data/List.thy | 100 |
1 files changed, 59 insertions, 41 deletions
diff --git a/spartan/data/List.thy b/spartan/data/List.thy index 5d6cb15..8fdaa1d 100644 --- a/spartan/data/List.thy +++ b/spartan/data/List.thy @@ -82,6 +82,8 @@ translations section \<open>Standard functions\<close> +subsection \<open>Head and tail\<close> + Lemma (derive) head: assumes "A: U i" "xs: List A" shows "Maybe A" @@ -98,6 +100,35 @@ proof (cases xs) show "\<And>xs. xs: List A \<Longrightarrow> xs: List A" . qed +definition head_i ("head") where [implicit]: "head xs \<equiv> List.head ? xs" +definition tail_i ("tail") where [implicit]: "tail xs \<equiv> List.tail ? xs" + +translations + "head" \<leftharpoondown> "CONST List.head A" + "tail" \<leftharpoondown> "CONST List.tail A" + +Lemma head_type [typechk]: + assumes "A: U i" "xs: List A" + shows "head xs: Maybe A" + unfolding head_def by typechk + +Lemma head_of_cons [comps]: + assumes "A: U i" "x: A" "xs: List A" + shows "head (x # xs) \<equiv> some x" + unfolding head_def ListCase_def by reduce + +Lemma tail_type [typechk]: + assumes "A: U i" "xs: List A" + shows "tail xs: List A" + unfolding tail_def by typechk + +Lemma tail_of_cons [comps]: + assumes "A: U i" "x: A" "xs: List A" + shows "tail (x # xs) \<equiv> xs" + unfolding tail_def ListCase_def by reduce + +subsection \<open>Append\<close> + Lemma (derive) app: assumes "A: U i" "xs: List A" "ys: List A" shows "List A" @@ -107,22 +138,11 @@ Lemma (derive) app: proof - show "x # rec: List A" by typechk qed done -definition head_i ("head") - where [implicit]: "head xs \<equiv> List.head ? xs" +definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app ? xs ys" -definition tail_i ("tail") - where [implicit]: "tail xs \<equiv> List.tail ? xs" +translations "app" \<leftharpoondown> "CONST List.app A" -definition app_i ("app") - where [implicit]: "app xs ys \<equiv> List.app ? xs ys" - -Lemma (derive) rev: - assumes "A: U i" "xs: List A" - shows "List A" - apply (elim xs) - \<guillemotright> by (rule List_nil) - \<guillemotright> prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed - done +subsection \<open>Map\<close> Lemma (derive) map: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A" @@ -134,41 +154,39 @@ proof (elim xs) show "f x # ys: List B" by typechk qed -definition rev_i ("rev") - where [implicit]: "rev \<equiv> List.rev ?" +definition map_i ("map") where [implicit]: "map \<equiv> List.map ? ?" -definition map_i ("map") - where [implicit]: "map \<equiv> List.map ? ?" +translations "map" \<leftharpoondown> "CONST List.map A B" -translations - "head" \<leftharpoondown> "CONST List.head A" - "tail" \<leftharpoondown> "CONST List.tail A" - "map" \<leftharpoondown> "CONST List.map A B" +Lemma map_type [typechk]: + assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A" + shows "map f xs: List B" + unfolding map_def by typechk -Lemma head_type [typechk]: - assumes "A: U i" "xs: List A" - shows "head xs: Maybe A" - unfolding head_def by typechk -Lemma head_of_cons [comps]: - assumes "A: U i" "x: A" "xs: List A" - shows "head (x # xs) \<equiv> some x" - unfolding head_def ListCase_def by reduce +subsection \<open>Reverse\<close> -Lemma tail_type [typechk]: +Lemma (derive) rev: assumes "A: U i" "xs: List A" - shows "tail xs: List A" - unfolding tail_def by typechk + shows "List A" + apply (elim xs) + \<guillemotright> by (rule List_nil) + \<guillemotright> prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed + done -Lemma tail_of_cons [comps]: - assumes "A: U i" "x: A" "xs: List A" - shows "tail (x # xs) \<equiv> xs" - unfolding tail_def ListCase_def by reduce +definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?" -Lemma map_type [typechk]: - assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A" - shows "map f xs: List B" - unfolding map_def by typechk +translations "rev" \<leftharpoondown> "CONST List.rev A" + +Lemma rev_type [typechk]: + assumes "A: U i" "xs: List A" + shows "rev xs: List A" + unfolding rev_def by typechk + +Lemma rev_nil [comps]: + assumes "A: U i" + shows "rev (nil A) \<equiv> nil A" + unfolding rev_def by reduce end |