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 (fn xs. C xs) c\<^sub>0 (fn 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 (fn xs. C xs) c\<^sub>0 (fn 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 (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) (cons A x xs) \ f x xs (ListInd A (fn xs. C xs) c\<^sub>0 (fn 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 (fn _. C)" Lemma list_cases [cases]: assumes "xs: List A" 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. xs: List A \ C xs: U i" shows "C xs" by (elim xs) (fact nil_case, rule cons_case) 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\ subsection \Head and tail\ Definition 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 Definition 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 definition head_i ("head") where [implicit]: "head xs \ List.head ? xs" definition tail_i ("tail") where [implicit]: "tail xs \ List.tail ? xs" translations "head" \ "CONST List.head A" "tail" \ "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) \ some x" unfolding head_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 by reduce subsection \Append\ Definition app: assumes "A: U i" "xs: List A" "ys: List A" shows "List A" apply (elim xs) \ by (fact \ys:_\) \ prems vars x _ rec proof - show "x # rec: List A" by typechk qed done definition app_i ("app") where [implicit]: "app xs ys \ List.app ? xs ys" translations "app" \ "CONST List.app A" subsection \Map\ Definition 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 definition map_i ("map") where [implicit]: "map \ List.map ? ?" translations "map" \ "CONST List.map A B" 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 subsection \Reverse\ Definition rev: assumes "A: U i" "xs: List A" shows "List A" apply (elim xs) \ by (rule List_nil) \ prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed done definition rev_i ("rev") where [implicit]: "rev \ List.rev ?" translations "rev" \ "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) \ nil A" unfolding rev_def by reduce end