|
1 (* Title: HOLCF/Library/List_Cpo.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Lists as a complete partial order *} |
|
6 |
|
7 theory List_Cpo |
|
8 imports HOLCF |
|
9 begin |
|
10 |
|
11 subsection {* Lists are a partial order *} |
|
12 |
|
13 instantiation list :: (po) po |
|
14 begin |
|
15 |
|
16 definition |
|
17 "xs \<sqsubseteq> ys \<longleftrightarrow> list_all2 (op \<sqsubseteq>) xs ys" |
|
18 |
|
19 instance 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) |
|
24 next |
|
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) |
|
30 next |
|
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) |
|
36 qed |
|
37 |
|
38 end |
|
39 |
|
40 lemma 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> []" |
|
45 by (simp_all add: below_list_def) |
|
46 |
|
47 lemma Nil_below_iff [simp]: "[] \<sqsubseteq> xs \<longleftrightarrow> xs = []" |
|
48 by (cases xs, simp_all) |
|
49 |
|
50 lemma below_Nil_iff [simp]: "xs \<sqsubseteq> [] \<longleftrightarrow> xs = []" |
|
51 by (cases xs, simp_all) |
|
52 |
|
53 text "Thanks to Joachim Breitner" |
|
54 |
|
55 lemma list_Cons_below: |
|
56 assumes "a # as \<sqsubseteq> xs" |
|
57 obtains b and bs where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = b # bs" |
|
58 using assms by (cases xs, auto) |
|
59 |
|
60 lemma list_below_Cons: |
|
61 assumes "xs \<sqsubseteq> b # bs" |
|
62 obtains a and as where "a \<sqsubseteq> b" and "as \<sqsubseteq> bs" and "xs = a # as" |
|
63 using assms by (cases xs, auto) |
|
64 |
|
65 lemma hd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> hd xs \<sqsubseteq> hd ys" |
|
66 by (cases xs, simp, cases ys, simp, simp) |
|
67 |
|
68 lemma tl_mono: "xs \<sqsubseteq> ys \<Longrightarrow> tl xs \<sqsubseteq> tl ys" |
|
69 by (cases xs, simp, cases ys, simp, simp) |
|
70 |
|
71 lemma ch2ch_hd [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. hd (S i))" |
|
72 by (rule chainI, rule hd_mono, erule chainE) |
|
73 |
|
74 lemma ch2ch_tl [simp]: "chain (\<lambda>i. S i) \<Longrightarrow> chain (\<lambda>i. tl (S i))" |
|
75 by (rule chainI, rule tl_mono, erule chainE) |
|
76 |
|
77 lemma below_same_length: "xs \<sqsubseteq> ys \<Longrightarrow> length xs = length ys" |
|
78 unfolding below_list_def by (rule list_all2_lengthD) |
|
79 |
|
80 lemma list_chain_cases: |
|
81 assumes S: "chain S" |
|
82 obtains "\<forall>i. S i = []" | |
|
83 A B where "chain A" and "chain B" and "\<forall>i. S i = A i # B i" |
|
84 proof (cases "S 0") |
|
85 case Nil |
|
86 have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF S]) |
|
87 with Nil have "\<forall>i. S i = []" by simp |
|
88 thus ?thesis .. |
|
89 next |
|
90 case (Cons x xs) |
|
91 have "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono [OF S]) |
|
92 hence *: "\<forall>i. S i \<noteq> []" by (rule all_forward) (auto simp add: Cons) |
|
93 let ?A = "\<lambda>i. hd (S i)" |
|
94 let ?B = "\<lambda>i. tl (S i)" |
|
95 from S have "chain ?A" and "chain ?B" by simp_all |
|
96 moreover have "\<forall>i. S i = ?A i # ?B i" by (simp add: *) |
|
97 ultimately show ?thesis .. |
|
98 qed |
|
99 |
|
100 subsection {* Lists are a complete partial order *} |
|
101 |
|
102 lemma is_lub_Cons: |
|
103 assumes A: "range A <<| x" |
|
104 assumes B: "range B <<| xs" |
|
105 shows "range (\<lambda>i. A i # B i) <<| x # xs" |
|
106 using assms |
|
107 unfolding is_lub_def is_ub_def Ball_def [symmetric] |
|
108 by (clarsimp, case_tac u, simp_all) |
|
109 |
|
110 lemma list_cpo_lemma: |
|
111 fixes S :: "nat \<Rightarrow> 'a::cpo list" |
|
112 assumes "chain S" and "\<forall>i. length (S i) = n" |
|
113 shows "\<exists>x. range S <<| x" |
|
114 using assms |
|
115 apply (induct n arbitrary: S) |
|
116 apply (subgoal_tac "S = (\<lambda>i. [])") |
|
117 apply (fast intro: lub_const) |
|
118 apply (simp add: expand_fun_eq) |
|
119 apply (drule_tac x="\<lambda>i. tl (S i)" in meta_spec, clarsimp) |
|
120 apply (rule_tac x="(\<Squnion>i. hd (S i)) # x" in exI) |
|
121 apply (subgoal_tac "range (\<lambda>i. hd (S i) # tl (S i)) = range S") |
|
122 apply (erule subst) |
|
123 apply (rule is_lub_Cons) |
|
124 apply (rule thelubE [OF _ refl]) |
|
125 apply (erule ch2ch_hd) |
|
126 apply assumption |
|
127 apply (rule_tac f="\<lambda>S. range S" in arg_cong) |
|
128 apply (rule ext) |
|
129 apply (rule hd_Cons_tl) |
|
130 apply (drule_tac x=i in spec, auto) |
|
131 done |
|
132 |
|
133 instance list :: (cpo) cpo |
|
134 proof |
|
135 fix S :: "nat \<Rightarrow> 'a list" |
|
136 assume "chain S" |
|
137 hence "\<forall>i. S 0 \<sqsubseteq> S i" by (simp add: chain_mono) |
|
138 hence "\<forall>i. length (S i) = length (S 0)" |
|
139 by (fast intro: below_same_length [symmetric]) |
|
140 with `chain S` show "\<exists>x. range S <<| x" |
|
141 by (rule list_cpo_lemma) |
|
142 qed |
|
143 |
|
144 subsection {* Continuity of list operations *} |
|
145 |
|
146 lemma cont2cont_Cons [simp, cont2cont]: |
|
147 assumes f: "cont (\<lambda>x. f x)" |
|
148 assumes g: "cont (\<lambda>x. g x)" |
|
149 shows "cont (\<lambda>x. f x # g x)" |
|
150 apply (rule contI) |
|
151 apply (rule is_lub_Cons) |
|
152 apply (erule contE [OF f]) |
|
153 apply (erule contE [OF g]) |
|
154 done |
|
155 |
|
156 lemma lub_Cons: |
|
157 fixes A :: "nat \<Rightarrow> 'a::cpo" |
|
158 assumes A: "chain A" and B: "chain B" |
|
159 shows "(\<Squnion>i. A i # B i) = (\<Squnion>i. A i) # (\<Squnion>i. B i)" |
|
160 by (intro thelubI is_lub_Cons cpo_lubI A B) |
|
161 |
|
162 lemma cont2cont_list_case: |
|
163 assumes f: "cont (\<lambda>x. f x)" |
|
164 assumes g: "cont (\<lambda>x. g x)" |
|
165 assumes h1: "\<And>y ys. cont (\<lambda>x. h x y ys)" |
|
166 assumes h2: "\<And>x ys. cont (\<lambda>y. h x y ys)" |
|
167 assumes h3: "\<And>x y. cont (\<lambda>ys. h x y ys)" |
|
168 shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)" |
|
169 apply (rule cont_apply [OF f]) |
|
170 apply (rule contI) |
|
171 apply (erule list_chain_cases) |
|
172 apply (simp add: lub_const) |
|
173 apply (simp add: lub_Cons) |
|
174 apply (simp add: cont2contlubE [OF h2]) |
|
175 apply (simp add: cont2contlubE [OF h3]) |
|
176 apply (simp add: diag_lub ch2ch_cont [OF h2] ch2ch_cont [OF h3]) |
|
177 apply (rule cpo_lubI, rule chainI, rule below_trans) |
|
178 apply (erule cont2monofunE [OF h2 chainE]) |
|
179 apply (erule cont2monofunE [OF h3 chainE]) |
|
180 apply (case_tac y, simp_all add: g h1) |
|
181 done |
|
182 |
|
183 lemma cont2cont_list_case' [simp, cont2cont]: |
|
184 assumes f: "cont (\<lambda>x. f x)" |
|
185 assumes g: "cont (\<lambda>x. g x)" |
|
186 assumes h: "cont (\<lambda>p. h (fst p) (fst (snd p)) (snd (snd p)))" |
|
187 shows "cont (\<lambda>x. case f x of [] \<Rightarrow> g x | y # ys \<Rightarrow> h x y ys)" |
|
188 proof - |
|
189 have "\<And>y ys. cont (\<lambda>x. h x (fst (y, ys)) (snd (y, ys)))" |
|
190 by (rule h [THEN cont_fst_snd_D1]) |
|
191 hence h1: "\<And>y ys. cont (\<lambda>x. h x y ys)" by simp |
|
192 note h2 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D1] |
|
193 note h3 = h [THEN cont_fst_snd_D2, THEN cont_fst_snd_D2] |
|
194 from f g h1 h2 h3 show ?thesis by (rule cont2cont_list_case) |
|
195 qed |
|
196 |
|
197 text {* The simple version (due to Joachim Breitner) is needed if the |
|
198 element type of the list is not a cpo. *} |
|
199 |
|
200 lemma cont2cont_list_case_simple [simp, cont2cont]: |
|
201 assumes "cont (\<lambda>x. f1 x)" |
|
202 assumes "\<And>y ys. cont (\<lambda>x. f2 x y ys)" |
|
203 shows "cont (\<lambda>x. case l of [] \<Rightarrow> f1 x | y # ys \<Rightarrow> f2 x y ys)" |
|
204 using assms by (cases l) auto |
|
205 |
|
206 text {* There are probably lots of other list operations that also |
|
207 deserve to have continuity lemmas. I'll add more as they are |
|
208 needed. *} |
|
209 |
|
210 end |