chapter \Lists\ 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 :: \o \ o\ and nil :: \o \ o\ and cons :: \o \ o \ o \ o\ and ListInd :: \o \ (o \ o) \ o \ (o \ o \ o \ o) \ o \ o\ where ListF: "A: U i \ List A: U i" and List_nil: "A: U i \ nil A: List A" and List_cons: "\x: A; xs: List A\ \ cons A x xs: List A" and ListE: "\ xs: List A; c\<^sub>0: C (nil A); \x xs rec. \x: A; xs: List A; rec: C xs\ \ f x xs rec: C (cons A x xs); \xs. xs: List A \ C xs: U i \ \ ListInd A (\xs. C xs) c\<^sub>0 (\x xs rec. f x xs rec) xs: C xs" and List_comp_nil: "\ c\<^sub>0: C (nil A); \x xs rec. \x: A; xs: List A; rec: C xs\ \ f x xs rec: C (cons A x xs); \xs. xs: List A \ C xs: U i \ \ ListInd A (\xs. C xs) c\<^sub>0 (\x xs rec. f x xs rec) (nil A) \ c\<^sub>0" and List_comp_cons: "\ xs: List A; c\<^sub>0: C (nil A); \x xs rec. \x: A; xs: List A; rec: C xs\ \ f x xs rec: C (cons A x xs); \xs. xs: List A \ C xs: U i \ \ ListInd A (\xs. C xs) c\<^sub>0 (\x xs rec. f x xs rec) (cons A x xs) \ f x xs (ListInd A (\xs. C xs) c\<^sub>0 (\x xs rec. f x xs rec) xs)" lemmas [intros] = ListF List_nil List_cons and [elims "?xs"] = ListE and [comps] = List_comp_nil List_comp_cons abbreviation "ListRec A C \ ListInd A (\_. C)" Lemma (derive) ListCase: assumes "A: U i" "\xs. xs: List A \ C xs: U i" and nil_case: "c\<^sub>0: C (nil A)" and cons_case: "\x xs. \x: A; xs: List A\ \ f x xs: C (cons A x xs)" and "xs: List A" shows "?List_cases A (\xs. C xs) c\<^sub>0 (\x xs. f x xs) xs: C xs" by (elim xs) (fact nil_case, rule cons_case) lemmas List_cases [cases] = ListCase[rotated 4] section \Notation\ definition nil_i ("[]") where [implicit]: "[] \ nil ?" definition cons_i (infixr "#" 120) where [implicit]: "x # xs \ cons ? x xs" translations "[]" \ "CONST List.nil A" "x # xs" \ "CONST List.cons A x xs" syntax "_list" :: \args \ o\ ("[_]") translations "[x, xs]" \ "x # [xs]" "[x]" \ "x # []" section \Standard functions\ Lemma (derive) head: assumes "A: U i" "xs: List A" shows "Maybe A" proof (cases xs) show "none: Maybe A" by intro show "\x. x: A \ some x: Maybe A" by intro qed Lemma (derive) tail: assumes "A: U i" "xs: List A" shows "List A" proof (cases xs) show "[]: List A" by intro show "\xs. xs: List A \ xs: List A" . qed Lemma (derive) map: assumes "A: U i" "B: U i" "f: A \ B" "xs: List A" shows "List B" proof (elim xs) show "[]: List B" by intro next fix x ys assume "x: A" "ys: List B" show "f x # ys: List B" by typechk qed thm map_def \ \map ?A ?B ?f ?xs \ ListRec ?A (List ?B) [] (\x xs. cons ?B (?f x)) ?xs\ definition head_i ("head") where [implicit]: "head xs \ List.head ? xs" definition tail_i ("tail") where [implicit]: "tail xs \ List.tail ? xs" definition map_i ("map") where [implicit]: "map \ List.map ? ?" translations "head" \ "CONST List.head A" "tail" \ "CONST List.tail A" "map" \ "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 head_of_cons [comps]: assumes "A: U i" "x: A" "xs: List A" shows "head (x # xs) \ 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) \ xs" unfolding tail_def ListCase_def by reduce Lemma map_type [typechk]: assumes "A: U i" "B: U i" "f: A \ B" "xs: List A" shows "map f xs: List B" unfolding map_def by typechk end