Theory List_Cpo

(*  Title:      HOL/HOLCF/Library/List_Cpo.thy
    Author:     Brian Huffman
*)

section ‹Lists as a complete partial order›

theory List_Cpo
imports HOLCF
begin

subsection ‹Lists are a partial order›

instantiation list :: (po) po
begin

definition
  "xs ⊑ ys ⟷ list_all2 (⊑) xs ys"

instance proof
  fix xs :: "'a list"
  from below_refl show "xs ⊑ xs"
    unfolding below_list_def
    by (rule list_all2_refl)
next
  fix xs ys zs :: "'a list"
  assume "xs ⊑ ys" and "ys ⊑ zs"
  with below_trans show "xs ⊑ zs"
    unfolding below_list_def
    by (rule list_all2_trans)
next
  fix xs ys zs :: "'a list"
  assume "xs ⊑ ys" and "ys ⊑ xs"
  with below_antisym show "xs = ys"
    unfolding below_list_def
    by (rule list_all2_antisym)
qed

end

lemma below_list_simps [simp]:
  "[] ⊑ []"
  "x # xs ⊑ y # ys ⟷ x ⊑ y ∧ xs ⊑ ys"
  "¬ [] ⊑ y # ys"
  "¬ x # xs ⊑ []"
by (simp_all add: below_list_def)

lemma Nil_below_iff [simp]: "[] ⊑ xs ⟷ xs = []"
by (cases xs, simp_all)

lemma below_Nil_iff [simp]: "xs ⊑ [] ⟷ xs = []"
by (cases xs, simp_all)

lemma list_below_induct [consumes 1, case_names Nil Cons]:
  assumes "xs ⊑ ys"
  assumes 1: "P [] []"
  assumes 2: "⋀x y xs ys. ⟦x ⊑ y; xs ⊑ ys; P xs ys⟧ ⟹ P (x # xs) (y # ys)"
  shows "P xs ys"
using ‹xs ⊑ ys›
proof (induct xs arbitrary: ys)
  case Nil thus ?case by (simp add: 1)
next
  case (Cons x xs) thus ?case by (cases ys, simp_all add: 2)
qed

lemma list_below_cases:
  assumes "xs ⊑ ys"
  obtains "xs = []" and "ys = []" |
    x y xs' ys' where "xs = x # xs'" and "ys = y # ys'"
using assms by (cases xs, simp, cases ys, auto)

text "Thanks to Joachim Breitner"

lemma list_Cons_below:
  assumes "a # as ⊑ xs"
  obtains b and bs where "a ⊑ b" and "as ⊑ bs" and "xs = b # bs"
  using assms by (cases xs, auto)

lemma list_below_Cons:
  assumes "xs ⊑ b # bs"
  obtains a and as where "a ⊑ b" and "as ⊑ bs" and "xs = a # as"
  using assms by (cases xs, auto)

lemma hd_mono: "xs ⊑ ys ⟹ hd xs ⊑ hd ys"
by (cases xs, simp, cases ys, simp, simp)

lemma tl_mono: "xs ⊑ ys ⟹ tl xs ⊑ tl ys"
by (cases xs, simp, cases ys, simp, simp)

lemma ch2ch_hd [simp]: "chain (λi. S i) ⟹ chain (λi. hd (S i))"
by (rule chainI, rule hd_mono, erule chainE)

lemma ch2ch_tl [simp]: "chain (λi. S i) ⟹ chain (λi. tl (S i))"
by (rule chainI, rule tl_mono, erule chainE)

lemma below_same_length: "xs ⊑ ys ⟹ length xs = length ys"
unfolding below_list_def by (rule list_all2_lengthD)

lemma list_chain_induct [consumes 1, case_names Nil Cons]:
  assumes "chain S"
  assumes 1: "P (λi. [])"
  assumes 2: "⋀A B. chain A ⟹ chain B ⟹ P B ⟹ P (λi. A i # B i)"
  shows "P S"
using ‹chain S›
proof (induct "S 0" arbitrary: S)
  case Nil
  have "∀i. S 0 ⊑ S i" by (simp add: chain_mono [OF ‹chain S›])
  with Nil have "∀i. S i = []" by simp
  thus ?case by (simp add: 1)
next
  case (Cons x xs)
  have "∀i. S 0 ⊑ S i" by (simp add: chain_mono [OF ‹chain S›])
  hence *: "∀i. S i ≠ []" by (rule all_forward, insert Cons) auto
  have "chain (λi. hd (S i))" and "chain (λi. tl (S i))"
    using ‹chain S› by simp_all
  moreover have "P (λi. tl (S i))"
    using ‹chain S› and ‹x # xs = S 0› [symmetric]
    by (simp add: Cons(1))
  ultimately have "P (λi. hd (S i) # tl (S i))"
    by (rule 2)
  thus "P S" by (simp add: *)
qed

lemma list_chain_cases:
  assumes S: "chain S"
  obtains "S = (λi. [])" |
    A B where "chain A" and "chain B" and "S = (λi. A i # B i)"
using S by (induct rule: list_chain_induct) simp_all

subsection ‹Lists are a complete partial order›

lemma is_lub_Cons:
  assumes A: "range A <<| x"
  assumes B: "range B <<| xs"
  shows "range (λi. A i # B i) <<| x # xs"
using assms
unfolding is_lub_def is_ub_def
by (clarsimp, case_tac u, simp_all)

instance list :: (cpo) cpo
proof
  fix S :: "nat ⇒ 'a list"
  assume "chain S"
  then show "∃x. range S <<| x"
  proof (induct rule: list_chain_induct)
    case Nil
    have "{[]} <<| []"
      by simp
    then obtain x :: "'a list" where "{[]} <<| x" ..
    then show ?case
      by auto
  next
    case (Cons A B) then show ?case
      by (auto intro: is_lub_Cons cpo_lubI)
  qed
qed

subsection ‹Continuity of list operations›

lemma cont2cont_Cons [simp, cont2cont]:
  assumes f: "cont (λx. f x)"
  assumes g: "cont (λx. g x)"
  shows "cont (λx. f x # g x)"
apply (rule contI)
apply (rule is_lub_Cons)
apply (erule contE [OF f])
apply (erule contE [OF g])
done

lemma lub_Cons:
  fixes A :: "nat ⇒ 'a::cpo"
  assumes A: "chain A" and B: "chain B"
  shows "(⨆i. A i # B i) = (⨆i. A i) # (⨆i. B i)"
by (intro lub_eqI is_lub_Cons cpo_lubI A B)

lemma cont2cont_case_list:
  assumes f: "cont (λx. f x)"
  assumes g: "cont (λx. g x)"
  assumes h1: "⋀y ys. cont (λx. h x y ys)"
  assumes h2: "⋀x ys. cont (λy. h x y ys)"
  assumes h3: "⋀x y. cont (λys. h x y ys)"
  shows "cont (λx. case f x of [] ⇒ g x | y # ys ⇒ h x y ys)"
apply (rule cont_apply [OF f])
apply (rule contI)
apply (erule list_chain_cases)
apply (simp add: is_lub_const)
apply (simp add: lub_Cons)
apply (simp add: cont2contlubE [OF h2])
apply (simp add: cont2contlubE [OF h3])
apply (simp add: diag_lub ch2ch_cont [OF h2] ch2ch_cont [OF h3])
apply (rule cpo_lubI, rule chainI, rule below_trans)
apply (erule cont2monofunE [OF h2 chainE])
apply (erule cont2monofunE [OF h3 chainE])
apply (case_tac y, simp_all add: g h1)
done

lemma cont2cont_case_list' [simp, cont2cont]:
  assumes f: "cont (λx. f x)"
  assumes g: "cont (λx. g x)"
  assumes h: "cont (λp. h (fst p) (fst (snd p)) (snd (snd p)))"
  shows "cont (λx. case f x of [] ⇒ g x | y # ys ⇒ h x y ys)"
using assms by (simp add: cont2cont_case_list prod_cont_iff)

text ‹The simple version (due to Joachim Breitner) is needed if the
  element type of the list is not a cpo.›

lemma cont2cont_case_list_simple [simp, cont2cont]:
  assumes "cont (λx. f1 x)"
  assumes "⋀y ys. cont (λx. f2 x y ys)"
  shows "cont (λx. case l of [] ⇒ f1 x | y # ys ⇒ f2 x y ys)"
using assms by (cases l) auto

text ‹Lemma for proving continuity of recursive list functions:›

lemma list_contI:
  fixes f :: "'a::cpo list ⇒ 'b::cpo"
  assumes f: "⋀x xs. f (x # xs) = g x xs (f xs)"
  assumes g1: "⋀xs y. cont (λx. g x xs y)"
  assumes g2: "⋀x y. cont (λxs. g x xs y)"
  assumes g3: "⋀x xs. cont (λy. g x xs y)"
  shows "cont f"
proof (rule contI2)
  obtain h where h: "⋀x xs y. g x xs y = h⋅x⋅xs⋅y"
  proof
    fix x xs y show "g x xs y = (Λ x xs y. g x xs y)⋅x⋅xs⋅y"
    by (simp add: cont2cont_LAM g1 g2 g3)
  qed
  show mono: "monofun f"
    apply (rule monofunI)
    apply (erule list_below_induct)
    apply simp
    apply (simp add: f h monofun_cfun)
    done
  fix Y :: "nat ⇒ 'a list"
  assume "chain Y" thus "f (⨆i. Y i) ⊑ (⨆i. f (Y i))"
    apply (induct rule: list_chain_induct)
    apply simp
    apply (simp add: lub_Cons f h)
    apply (simp add: lub_APP ch2ch_monofun [OF mono])
    apply (simp add: monofun_cfun)
    done
qed

text ‹Continuity rule for map›

lemma cont2cont_map [simp, cont2cont]:
  assumes f: "cont (λ(x, y). f x y)"
  assumes g: "cont (λx. g x)"
  shows "cont (λx. map (λy. f x y) (g x))"
using f
apply (simp add: prod_cont_iff)
apply (rule cont_apply [OF g])
apply (rule list_contI, rule list.map, simp, simp, simp)
apply (induct_tac y, simp, simp)
done

text ‹There are probably lots of other list operations that also
deserve to have continuity lemmas.  I'll add more as they are
needed.›

subsection ‹Lists are a discrete cpo›

instance list :: (discrete_cpo) discrete_cpo
proof
  fix xs ys :: "'a list"
  show "xs ⊑ ys ⟷ xs = ys"
    by (induct xs arbitrary: ys, case_tac [!] ys, simp_all)
qed

subsection ‹Compactness and chain-finiteness›

lemma compact_Nil [simp]: "compact []"
apply (rule compactI2)
apply (erule list_chain_cases)
apply simp
apply (simp add: lub_Cons)
done

lemma compact_Cons: "⟦compact x; compact xs⟧ ⟹ compact (x # xs)"
apply (rule compactI2)
apply (erule list_chain_cases)
apply (auto simp add: lub_Cons dest!: compactD2)
apply (rename_tac i j, rule_tac x="max i j" in exI)
apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded1]])
apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded2]])
apply (erule (1) conjI)
done

lemma compact_Cons_iff [simp]:
  "compact (x # xs) ⟷ compact x ∧ compact xs"
apply (safe intro!: compact_Cons)
apply (simp only: compact_def)
apply (subgoal_tac "cont (λx. x # xs)")
apply (drule (1) adm_subst, simp, simp)
apply (simp only: compact_def)
apply (subgoal_tac "cont (λxs. x # xs)")
apply (drule (1) adm_subst, simp, simp)
done

instance list :: (chfin) chfin
proof
  fix Y :: "nat ⇒ 'a list" assume "chain Y"
  moreover have "⋀(xs::'a list). compact xs"
    by (induct_tac xs, simp_all)
  ultimately show "∃i. max_in_chain i Y"
    by (rule compact_imp_max_in_chain)
qed

subsection ‹Using lists with fixrec›

definition
  match_Nil :: "'a::cpo list → 'b match → 'b match"
where
  "match_Nil = (Λ xs k. case xs of [] ⇒ k | y # ys ⇒ Fixrec.fail)"

definition
  match_Cons :: "'a::cpo list → ('a → 'a list → 'b match) → 'b match"
where
  "match_Cons = (Λ xs k. case xs of [] ⇒ Fixrec.fail | y # ys ⇒ k⋅y⋅ys)"

lemma match_Nil_simps [simp]:
  "match_Nil⋅[]⋅k = k"
  "match_Nil⋅(x # xs)⋅k = Fixrec.fail"
unfolding match_Nil_def by simp_all

lemma match_Cons_simps [simp]:
  "match_Cons⋅[]⋅k = Fixrec.fail"
  "match_Cons⋅(x # xs)⋅k = k⋅x⋅xs"
unfolding match_Cons_def by simp_all

setup ‹
  Fixrec.add_matchers
    [ (\<^const_name>‹Nil›, \<^const_name>‹match_Nil›),
      (\<^const_name>‹Cons›, \<^const_name>‹match_Cons›) ]
›

end