diff options
author | Josh Chen | 2020-07-08 15:55:48 +0200 |
---|---|---|
committer | Josh Chen | 2020-07-08 15:55:48 +0200 |
commit | 07c51b1801bd701bef61cedd571a944d9bd37e8b (patch) | |
tree | 16b9581f9f52af4058594cd503aa2eec1d2cb801 /spartan/lib/List.thy | |
parent | f0fab6e197510ce0e6d23a669f69de966701d495 (diff) |
1. Initial `Definition` keyword. 2. ifelse.
Diffstat (limited to '')
-rw-r--r-- | spartan/lib/List.thy | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy index 1798a23..11b8406 100644 --- a/spartan/lib/List.thy +++ b/spartan/lib/List.thy @@ -50,7 +50,7 @@ lemmas abbreviation "ListRec A C \<equiv> ListInd A (\<lambda>_. C)" -Lemma (derive) ListCase: +Lemma list_cases [cases]: assumes "xs: List A" and nil_case: "c\<^sub>0: C (nil A)" and @@ -59,8 +59,6 @@ Lemma (derive) ListCase: shows "?List_cases A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs. f x xs) xs: C xs" by (elim xs) (fact nil_case, rule cons_case) -lemmas List_cases [cases] = ListCase[unfolded ListCase_def] - section \<open>Notation\<close> @@ -84,7 +82,7 @@ section \<open>Standard functions\<close> subsection \<open>Head and tail\<close> -Lemma (derive) head: +Definition head: assumes "A: U i" "xs: List A" shows "Maybe A" proof (cases xs) @@ -92,7 +90,7 @@ proof (cases xs) show "\<And>x. x: A \<Longrightarrow> some x: Maybe A" by intro qed -Lemma (derive) tail: +Definition tail: assumes "A: U i" "xs: List A" shows "List A" proof (cases xs) @@ -115,7 +113,7 @@ Lemma head_type [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 + unfolding head_def by reduce Lemma tail_type [typechk]: assumes "A: U i" "xs: List A" @@ -125,11 +123,11 @@ Lemma tail_type [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 + unfolding tail_def by reduce subsection \<open>Append\<close> -Lemma (derive) app: +Definition app: assumes "A: U i" "xs: List A" "ys: List A" shows "List A" apply (elim xs) @@ -144,7 +142,7 @@ translations "app" \<leftharpoondown> "CONST List.app A" subsection \<open>Map\<close> -Lemma (derive) map: +Definition map: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A" shows "List B" proof (elim xs) @@ -166,7 +164,7 @@ Lemma map_type [typechk]: subsection \<open>Reverse\<close> -Lemma (derive) rev: +Definition rev: assumes "A: U i" "xs: List A" shows "List A" apply (elim xs) |