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
  [intro, intros] = 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 [typechk]:
  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 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 [comp]:
  assumes "A: U i" "x: A" "xs: List A"
  shows "tail (x # xs) \<equiv> xs"
  unfolding tail_def by reduce

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
    assume "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 [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


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 [typechk]:
  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 reduce


end