1(* Title: HOL/HOLCF/Library/List_Cpo.thy 2 Author: Brian Huffman 3*) 4 5section \<open>Lists as a complete partial order\<close> 6 7theory List_Cpo 8imports HOLCF 9begin 10 11subsection \<open>Lists are a partial order\<close> 12 13instantiation list :: (po) po 14begin 15 16definition 17 "xs \<sqsubseteq> ys \<longleftrightarrow> list_all2 (\<sqsubseteq>) xs ys" 18 19instance proof 20 fix xs :: "'a list" 21 from below_refl show "xs \<sqsubseteq> xs" 22 unfolding below_list_def 23 by (rule list_all2_refl) 24next 25 fix xs ys zs :: "'a list" 26 assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> zs" 27 with below_trans show "xs \<sqsubseteq> zs" 28 unfolding below_list_def 29 by (rule list_all2_trans) 30next 31 fix xs ys zs :: "'a list" 32 assume "xs \<sqsubseteq> ys" and "ys \<sqsubseteq> xs" 33 with below_antisym show "xs = ys" 34 unfolding below_list_def 35 by (rule list_all2_antisym) 36qed 37 38end 39 40lemma below_list_simps [simp]: 41 "[] \<sqsubseteq> []" 42 "x # xs \<sqsubseteq> y # ys \<longleftrightarrow> x \<sqsubseteq> y \<and> xs \<sqsubseteq> ys" 43 "\<not> [] \<sqsubseteq> y # ys" 44 "\<not> x # xs \<sqsubseteq> []" 45by (simp_all add: below_list_def) 46 47lemma Nil_below_iff [simp]: "[] \<sqsubseteq> xs \<longleftrightarrow> xs = []" 48by (cases xs, simp_all) 49 50lemma below_Nil_iff [simp]: "xs \<sqsubseteq> [] \<longleftrightarrow> xs = []" 51by (cases xs, simp_all) 52 53lemma list_below_induct [consumes 1, case_names Nil Cons]: 54 assumes "xs \<sqsubseteq> ys" 55 assumes 1: "P [] []" 56 assumes 2: "\<And>x y xs ys. \<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys; P xs ys\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)" 57 shows "P xs ys" 58using \<open>xs \<sqsubseteq> ys\<close> 59proof (induct xs arbitrary: ys) 60 case Nil thus ?case by (simp add: 1) 61next 62 case (Cons x xs) thus ?case by (cases ys, simp_all add: 2) 63qed 64 65lemma list_below_cases: 66 assumes "xs \<sqsubseteq> ys" 67 obtains "xs = []" and "ys = []" | 68 x y xs' ys' where "xs = x # xs'" and "ys = y # ys'" 69using assms by (cases xs, simp, cases ys, auto) 70 71text "Thanks to Joachim Breitner" 72 73lemma list_Cons_below: 74 assumes "a # as \<sqsubseteq> xs" 75 obtains b and bs where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = b # bs" 76 using assms by (cases xs, auto) 77 78lemma list_below_Cons: 79 assumes "xs \<sqsubseteq> b # bs" 80 obtains a and as where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = a # as" 81 using assms by (cases xs, auto) 82 83lemma hd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> hd xs \<sqsubseteq> hd ys" 84by (cases xs, simp, cases ys, simp, simp) 85 86lemma tl_mono: "xs \<sqsubseteq> ys \<Longrightarrow> tl xs \<sqsubseteq> tl ys" 87by (cases xs, simp, cases ys, simp, simp) 88 89lemma ch2ch_hd [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. hd (S i))" 90by (rule chainI, rule hd_mono, erule chainE) 91 92lemma ch2ch_tl [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. tl (S i))" 93by (rule chainI, rule tl_mono, erule chainE) 94 95lemma below_same_length: "xs \<sqsubseteq> ys \<Longrightarrow> length xs = length ys" 96unfolding below_list_def by (rule list_all2_lengthD) 97 98lemma list_chain_induct [consumes 1, case_names Nil Cons]: 99 assumes "chain S" 100 assumes 1: "P (\<lambda>i. [])" 101 assumes 2: "\<And>A B. chain A \<Longrightarrow> chain B \<Longrightarrow> P B \<Longrightarrow> P (\<lambda>i. A i # B i)" 102 shows "P S" 103using \<open>chain S\<close> 104proof (induct "S 0" arbitrary: S) 105 case Nil 106 have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF \<open>chain S\<close>]) 107 with Nil have "\<forall>i. S i = []" by simp 108 thus ?case by (simp add: 1) 109next 110 case (Cons x xs) 111 have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF \<open>chain S\<close>]) 112 hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward, insert Cons) auto 113 have "chain (\<lambda>i. hd (S i))" and "chain (\<lambda>i. tl (S i))" 114 using \<open>chain S\<close> by simp_all 115 moreover have "P (\<lambda>i. tl (S i))" 116 using \<open>chain S\<close> and \<open>x # xs = S 0\<close> [symmetric] 117 by (simp add: Cons(1)) 118 ultimately have "P (\<lambda>i. hd (S i) # tl (S i))" 119 by (rule 2) 120 thus "P S" by (simp add: *) 121qed 122 123lemma list_chain_cases: 124 assumes S: "chain S" 125 obtains "S = (\<lambda>i. [])" | 126 A B where "chain A" and "chain B" and "S = (\<lambda>i. A i # B i)" 127using S by (induct rule: list_chain_induct) simp_all 128 129subsection \<open>Lists are a complete partial order\<close> 130 131lemma is_lub_Cons: 132 assumes A: "range A <<| x" 133 assumes B: "range B <<| xs" 134 shows "range (\<lambda>i. A i # B i) <<| x # xs" 135using assms 136unfolding is_lub_def is_ub_def 137by (clarsimp, case_tac u, simp_all) 138 139instance list :: (cpo) cpo 140proof 141 fix S :: "nat \<Rightarrow> 'a list" 142 assume "chain S" thus "\<exists>x. range S <<| x" 143 proof (induct rule: list_chain_induct) 144 case Nil thus ?case by (auto intro: is_lub_const) 145 next 146 case (Cons A B) thus ?case by (auto intro: is_lub_Cons cpo_lubI) 147 qed 148qed 149 150subsection \<open>Continuity of list operations\<close> 151 152lemma cont2cont_Cons [simp, cont2cont]: 153 assumes f: "cont (\<lambda>x. f x)" 154 assumes g: "cont (\<lambda>x. g x)" 155 shows "cont (\<lambda>x. f x # g x)" 156apply (rule contI) 157apply (rule is_lub_Cons) 158apply (erule contE [OF f]) 159apply (erule contE [OF g]) 160done 161 162lemma lub_Cons: 163 fixes A :: "nat \<Rightarrow> 'a::cpo" 164 assumes A: "chain A" and B: "chain B" 165 shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)" 166by (intro lub_eqI is_lub_Cons cpo_lubI A B) 167 168lemma cont2cont_case_list: 169 assumes f: "cont (\<lambda>x. f x)" 170 assumes g: "cont (\<lambda>x. g x)" 171 assumes h1: "\<And>y ys. cont (\<lambda>x. h x y ys)" 172 assumes h2: "\<And>x ys. cont (\<lambda>y. h x y ys)" 173 assumes h3: "\<And>x y. cont (\<lambda>ys. h x y ys)" 174 shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)" 175apply (rule cont_apply [OF f]) 176apply (rule contI) 177apply (erule list_chain_cases) 178apply (simp add: is_lub_const) 179apply (simp add: lub_Cons) 180apply (simp add: cont2contlubE [OF h2]) 181apply (simp add: cont2contlubE [OF h3]) 182apply (simp add: diag_lub ch2ch_cont [OF h2] ch2ch_cont [OF h3]) 183apply (rule cpo_lubI, rule chainI, rule below_trans) 184apply (erule cont2monofunE [OF h2 chainE]) 185apply (erule cont2monofunE [OF h3 chainE]) 186apply (case_tac y, simp_all add: g h1) 187done 188 189lemma cont2cont_case_list' [simp, cont2cont]: 190 assumes f: "cont (\<lambda>x. f x)" 191 assumes g: "cont (\<lambda>x. g x)" 192 assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))" 193 shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)" 194using assms by (simp add: cont2cont_case_list prod_cont_iff) 195 196text \<open>The simple version (due to Joachim Breitner) is needed if the 197 element type of the list is not a cpo.\<close> 198 199lemma cont2cont_case_list_simple [simp, cont2cont]: 200 assumes "cont (\<lambda>x. f1 x)" 201 assumes "\<And>y ys. cont (\<lambda>x. f2 x y ys)" 202 shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)" 203using assms by (cases l) auto 204 205text \<open>Lemma for proving continuity of recursive list functions:\<close> 206 207lemma list_contI: 208 fixes f :: "'a::cpo list \<Rightarrow> 'b::cpo" 209 assumes f: "\<And>x xs. f (x # xs) = g x xs (f xs)" 210 assumes g1: "\<And>xs y. cont (\<lambda>x. g x xs y)" 211 assumes g2: "\<And>x y. cont (\<lambda>xs. g x xs y)" 212 assumes g3: "\<And>x xs. cont (\<lambda>y. g x xs y)" 213 shows "cont f" 214proof (rule contI2) 215 obtain h where h: "\<And>x xs y. g x xs y = h\<cdot>x\<cdot>xs\<cdot>y" 216 proof 217 fix x xs y show "g x xs y = (\<Lambda> x xs y. g x xs y)\<cdot>x\<cdot>xs\<cdot>y" 218 by (simp add: cont2cont_LAM g1 g2 g3) 219 qed 220 show mono: "monofun f" 221 apply (rule monofunI) 222 apply (erule list_below_induct) 223 apply simp 224 apply (simp add: f h monofun_cfun) 225 done 226 fix Y :: "nat \<Rightarrow> 'a list" 227 assume "chain Y" thus "f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))" 228 apply (induct rule: list_chain_induct) 229 apply simp 230 apply (simp add: lub_Cons f h) 231 apply (simp add: lub_APP ch2ch_monofun [OF mono]) 232 apply (simp add: monofun_cfun) 233 done 234qed 235 236text \<open>Continuity rule for map\<close> 237 238lemma cont2cont_map [simp, cont2cont]: 239 assumes f: "cont (\<lambda>(x, y). f x y)" 240 assumes g: "cont (\<lambda>x. g x)" 241 shows "cont (\<lambda>x. map (\<lambda>y. f x y) (g x))" 242using f 243apply (simp add: prod_cont_iff) 244apply (rule cont_apply [OF g]) 245apply (rule list_contI, rule list.map, simp, simp, simp) 246apply (induct_tac y, simp, simp) 247done 248 249text \<open>There are probably lots of other list operations that also 250deserve to have continuity lemmas. I'll add more as they are 251needed.\<close> 252 253subsection \<open>Lists are a discrete cpo\<close> 254 255instance list :: (discrete_cpo) discrete_cpo 256proof 257 fix xs ys :: "'a list" 258 show "xs \<sqsubseteq> ys \<longleftrightarrow> xs = ys" 259 by (induct xs arbitrary: ys, case_tac [!] ys, simp_all) 260qed 261 262subsection \<open>Compactness and chain-finiteness\<close> 263 264lemma compact_Nil [simp]: "compact []" 265apply (rule compactI2) 266apply (erule list_chain_cases) 267apply simp 268apply (simp add: lub_Cons) 269done 270 271lemma compact_Cons: "\<lbrakk>compact x; compact xs\<rbrakk> \<Longrightarrow> compact (x # xs)" 272apply (rule compactI2) 273apply (erule list_chain_cases) 274apply (auto simp add: lub_Cons dest!: compactD2) 275apply (rename_tac i j, rule_tac x="max i j" in exI) 276apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded1]]) 277apply (drule (1) below_trans [OF _ chain_mono [OF _ max.cobounded2]]) 278apply (erule (1) conjI) 279done 280 281lemma compact_Cons_iff [simp]: 282 "compact (x # xs) \<longleftrightarrow> compact x \<and> compact xs" 283apply (safe intro!: compact_Cons) 284apply (simp only: compact_def) 285apply (subgoal_tac "cont (\<lambda>x. x # xs)") 286apply (drule (1) adm_subst, simp, simp) 287apply (simp only: compact_def) 288apply (subgoal_tac "cont (\<lambda>xs. x # xs)") 289apply (drule (1) adm_subst, simp, simp) 290done 291 292instance list :: (chfin) chfin 293proof 294 fix Y :: "nat \<Rightarrow> 'a list" assume "chain Y" 295 moreover have "\<And>(xs::'a list). compact xs" 296 by (induct_tac xs, simp_all) 297 ultimately show "\<exists>i. max_in_chain i Y" 298 by (rule compact_imp_max_in_chain) 299qed 300 301subsection \<open>Using lists with fixrec\<close> 302 303definition 304 match_Nil :: "'a::cpo list \<rightarrow> 'b match \<rightarrow> 'b match" 305where 306 "match_Nil = (\<Lambda> xs k. case xs of [] \<Rightarrow> k | y # ys \<Rightarrow> Fixrec.fail)" 307 308definition 309 match_Cons :: "'a::cpo list \<rightarrow> ('a \<rightarrow> 'a list \<rightarrow> 'b match) \<rightarrow> 'b match" 310where 311 "match_Cons = (\<Lambda> xs k. case xs of [] \<Rightarrow> Fixrec.fail | y # ys \<Rightarrow> k\<cdot>y\<cdot>ys)" 312 313lemma match_Nil_simps [simp]: 314 "match_Nil\<cdot>[]\<cdot>k = k" 315 "match_Nil\<cdot>(x # xs)\<cdot>k = Fixrec.fail" 316unfolding match_Nil_def by simp_all 317 318lemma match_Cons_simps [simp]: 319 "match_Cons\<cdot>[]\<cdot>k = Fixrec.fail" 320 "match_Cons\<cdot>(x # xs)\<cdot>k = k\<cdot>x\<cdot>xs" 321unfolding match_Cons_def by simp_all 322 323setup \<open> 324 Fixrec.add_matchers 325 [ (@{const_name Nil}, @{const_name match_Nil}), 326 (@{const_name Cons}, @{const_name match_Cons}) ] 327\<close> 328 329end 330