diff options
Diffstat (limited to 'spartan/lib/List.thy')
-rw-r--r-- | spartan/lib/List.thy | 191 |
1 files changed, 0 insertions, 191 deletions
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy deleted file mode 100644 index 4beb9b6..0000000 --- a/spartan/lib/List.thy +++ /dev/null @@ -1,191 +0,0 @@ -chapter \<open>Lists\<close> - -theory List -imports Maybe - -begin - -(*TODO: Inductive type and recursive function definitions. The ad-hoc - axiomatization below should be subsumed once general inductive types are - properly implemented.*) - -axiomatization - List :: \<open>o \<Rightarrow> o\<close> and - nil :: \<open>o \<Rightarrow> o\<close> and - cons :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> and - ListInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close> -where - ListF: "A: U i \<Longrightarrow> List A: U i" and - - List_nil: "A: U i \<Longrightarrow> nil A: 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; - c\<^sub>0: C (nil A); - \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs); - \<And>xs. xs: List A \<Longrightarrow> C xs: U i - \<rbrakk> \<Longrightarrow> ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs: C xs" and - - List_comp_nil: "\<lbrakk> - c\<^sub>0: C (nil A); - \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs); - \<And>xs. xs: List A \<Longrightarrow> C xs: U i - \<rbrakk> \<Longrightarrow> ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (nil A) \<equiv> c\<^sub>0" and - - List_comp_cons: "\<lbrakk> - xs: List A; - c\<^sub>0: C (nil A); - \<And>x xs rec. \<lbrakk>x: A; xs: List A; rec: C xs\<rbrakk> \<Longrightarrow> f x xs rec: C (cons A x xs); - \<And>xs. xs: List A \<Longrightarrow> C xs: U i - \<rbrakk> \<Longrightarrow> - ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (cons A x xs) \<equiv> - f x xs (ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs)" - -lemmas - [form] = ListF and - [intr, intro] = List_nil List_cons and - [elim "?xs"] = ListE and - [comp] = List_comp_nil List_comp_cons - -abbreviation "ListRec A C \<equiv> ListInd A (fn _. C)" - -Lemma list_cases [cases]: - assumes - "xs: List A" and - nil_case: "c\<^sub>0: C (nil A)" and - cons_case: "\<And>x xs. \<lbrakk>x: A; xs: List A\<rbrakk> \<Longrightarrow> f x xs: C (cons A x xs)" and - "\<And>xs. xs: List A \<Longrightarrow> C xs: U i" - shows "C xs" - by (elim xs) (fact nil_case, rule cons_case) - - -section \<open>Notation\<close> - -definition nil_i ("[]") - where [implicit]: "[] \<equiv> nil {}" - -definition cons_i (infixr "#" 120) - where [implicit]: "x # xs \<equiv> cons {} x xs" - -translations - "[]" \<leftharpoondown> "CONST List.nil A" - "x # xs" \<leftharpoondown> "CONST List.cons A x xs" -syntax - "_list" :: \<open>args \<Rightarrow> o\<close> ("[_]") -translations - "[x, xs]" \<rightleftharpoons> "x # [xs]" - "[x]" \<rightleftharpoons> "x # []" - - -section \<open>Standard functions\<close> - -subsection \<open>Head and tail\<close> - -Definition head: - assumes "A: U i" "xs: List A" - shows "Maybe A" -proof (cases xs) - show "none: Maybe A" by intro - show "\<And>x. x: A \<Longrightarrow> some x: Maybe A" by intro -qed - -Definition tail: - assumes "A: U i" "xs: List A" - shows "List A" -proof (cases xs) - show "[]: List A" by intro - 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 [type]: - assumes "A: U i" "xs: List A" - shows "head xs: Maybe A" - unfolding head_def by typechk - -Lemma head_of_cons [comp]: - assumes "A: U i" "x: A" "xs: List A" - shows "head (x # xs) \<equiv> some x" - unfolding head_def by compute - -Lemma tail_type [type]: - assumes "A: U i" "xs: List A" - shows "tail xs: List A" - unfolding tail_def by typechk - -Lemma tail_of_cons [comp]: - assumes "A: U i" "x: A" "xs: List A" - shows "tail (x # xs) \<equiv> xs" - unfolding tail_def by compute - -subsection \<open>Append\<close> - -Definition app: - assumes "A: U i" "xs: List A" "ys: List A" - shows "List A" - apply (elim xs) - \<^item> by (fact \<open>ys:_\<close>) - \<^item> vars x _ rec - proof - show "x # rec: List A" by typechk qed - done - -definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app {} xs ys" - -translations "app" \<leftharpoondown> "CONST List.app A" - -subsection \<open>Map\<close> - -Definition 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 ys - assuming "x: A" "ys: List B" - show "f x # ys: List B" by typechk -qed - -definition map_i ("map") where [implicit]: "map \<equiv> List.map {} {}" - -translations "map" \<leftharpoondown> "CONST List.map A B" - -Lemma map_type [type]: - 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 - - -subsection \<open>Reverse\<close> - -Definition rev: - assumes "A: U i" "xs: List A" - shows "List A" - apply (elim xs) - \<^item> by (rule List_nil) - \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed - done - -definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev {}" - -translations "rev" \<leftharpoondown> "CONST List.rev A" - -Lemma rev_type [type]: - assumes "A: U i" "xs: List A" - shows "rev xs: List A" - unfolding rev_def by typechk - -Lemma rev_nil [comp]: - assumes "A: U i" - shows "rev (nil A) \<equiv> nil A" - unfolding rev_def by compute - - -end |