Theory List_Cpo
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