(* 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 ys zs ::
"'a list"
show "xs \ xs"
using below_refl
unfolding below_list_def
by (rule list_all2_refl)
show "xs \ ys \ ys \ zs \ xs \ zs"
using below_trans
unfolding below_list_def
by (rule list_all2_trans)
show "xs \ ys \ ys \ xs \ xs = ys"
using below_antisym
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
[ (
🍋‹Nil
›,
🍋‹match_Nil
›),
(
🍋‹Cons
›,
🍋‹match_Cons
›) ]
›
end
