Theory List_Cpo

theory List_Cpo
imports HOLCF
```(*  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 (op ⊑) 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 ⊑ []"

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]
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" thus "∃x. range S <<| x"
proof (induct rule: list_chain_induct)
case Nil thus ?case by (auto intro: is_lub_const)
next
case (Cons A B) thus ?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: 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])
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 (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
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 ‹