(* 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 ⊑ []" 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" 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: 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