1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory HaskellLemmaBucket
8imports
9  HaskellLib_H
10  NonDetMonadLemmaBucket
11begin
12
13lemma map_bits_to_bl:
14  "map ((!!) x) [0..<size x] = reverse (to_bl x)"
15  by (simp add: map_bits_rev_to_bl)
16
17lemma not_orList_is_replicate:
18  "\<not> orList ls \<Longrightarrow> ls = replicate (length ls) False"
19proof (induct ls rule: rev_induct)
20  case Nil thus ?case unfolding orList_def by simp
21next
22  case (snoc l ls)
23
24  from snoc.prems have ol: "\<not> orList ls" and nl: "\<not> l" unfolding orList_def by auto
25  have "ls = replicate (length ls) False" by (rule snoc.hyps [OF ol])
26  thus ?case
27    by (rule ssubst) (simp add: nl replicate_app_Cons_same [where xs = "[]", simplified])
28qed
29
30lemma andList_Cons:
31  assumes al: "andList $ map P (y # ys)"
32  shows   "P y"
33  using al unfolding andList_def
34  by simp (induct rule: rev_induct, simp+)
35
36lemma andList_mapE:
37  assumes al: "andList $ map P xs"
38  and     xv: "x \<in> set xs"
39  shows   "P x"
40  using al xv
41proof (induct xs arbitrary: x rule: rev_induct)
42  case Nil thus ?case by simp
43next
44  case (snoc y ys)
45
46  show ?case
47  proof (cases "x = y")
48    case True
49    with snoc.prems show ?thesis by (simp add: andList_def)
50  next
51    case False
52    with snoc.prems show ?thesis
53      by (auto simp: andList_def intro!: snoc.hyps)
54  qed
55qed
56
57lemma andList_to_aligned:
58  assumes al: "andList $ map (\<lambda>x. x && mask pageBits = 0) xs"
59  and     xv: "x \<in> set xs"
60  shows   "is_aligned x pageBits"
61proof (subst is_aligned_mask)
62  from al show "x && mask pageBits = 0" by (rule andList_mapE) fact
63qed
64
65(* minimum/maximum *)
66
67lemma maximum_ge: "x \<in> set b \<Longrightarrow> x \<le> maximum b"
68  unfolding maximum_def by (auto intro: Max_ge)
69
70lemma less_minimum_not_in:
71  "\<lbrakk> ls \<noteq> []; x < minimum ls \<rbrakk> \<Longrightarrow> x \<notin> set ls"
72  unfolding minimum_def by auto
73
74lemma minimum_le_member:
75  "\<lbrakk> x \<in> set ls; ls \<noteq> []\<rbrakk> \<Longrightarrow> minimum ls \<le> x"
76  unfolding minimum_def
77  apply (rule Min_le)
78    apply simp
79   apply simp
80  done
81
82lemma minimum_map_distrib:
83  fixes f :: "('a :: linorder) \<Rightarrow> 'a" and ls :: "'a list"
84  assumes minf: "\<And>x y. \<lbrakk>x \<in> set ls; y \<in> set ls\<rbrakk> \<Longrightarrow> min (f x) (f y) = f (min x y)"
85  and      lsn: "ls \<noteq> []"
86  shows "minimum (map f ls) = f (minimum ls)"
87  unfolding minimum_def
88  apply simp
89  apply (rule Min_image_distrib)
90    apply (erule (1) minf)
91   apply simp
92  apply (simp add: lsn)
93  done
94
95lemma minimum_enum_upto:
96  fixes x :: "'a::len word"
97  assumes le: "x \<le> y"
98  shows   "minimum [x .e. y] = x"
99  unfolding minimum_def using le by (auto intro!: MinI)
100
101lemma break_subsetsD:
102  "break f xs = (ys, zs) \<Longrightarrow> set ys \<subseteq> set xs \<and> set zs \<subseteq> set xs"
103  apply (induct xs arbitrary: ys zs)
104   apply simp
105  apply (case_tac "break f xs")
106  apply (elim meta_allE, drule(1) meta_mp)
107  apply (fastforce simp: split_def split: if_split_asm)
108  done
109
110lemma distinct_prop_breakD:
111  "\<lbrakk> distinct_prop P xs; break f xs = (ys, zs) \<rbrakk>
112    \<Longrightarrow> \<forall>y \<in> set ys. \<forall>z \<in> set zs. P y z"
113  apply (induct xs arbitrary: ys zs)
114   apply simp
115  apply (simp add: split_def split: if_split_asm)
116  apply (case_tac "break f xs")
117  apply (elim meta_allE, drule(1) meta_mp)
118  apply (frule break_subsetsD)
119  apply fastforce
120  done
121
122lemma stateAssert_wp:
123  "\<lbrace>\<lambda>s. P s \<longrightarrow> Q () s\<rbrace> stateAssert P e \<lbrace>Q\<rbrace>"
124  by (clarsimp simp: stateAssert_def) wp
125
126lemma haskell_assert_wp:
127  "\<lbrace>\<lambda>s. Q \<longrightarrow> P s\<rbrace> haskell_assert Q xs \<lbrace>\<lambda>_. P\<rbrace>"
128  by simp wp
129
130lemma init_append_last:
131  "xs \<noteq> [] \<Longrightarrow> init xs @ [last xs] = xs"
132  apply (induct xs rule: rev_induct)
133   apply simp
134  apply (simp add: init_def)
135  done
136
137lemma init_Snoc[simp]:
138  "init (xs @ [x]) = xs"
139  by (induct xs) (auto simp: init_def)
140
141lemma init_upto_enum_upt[simp]:
142  "init [0.e.n] = [0..<n]"
143  by (induct n) (auto simp: init_def)
144
145lemma no_fail_stateAssert:
146  "no_fail P (stateAssert P xs)"
147  apply (simp add: stateAssert_def)
148  apply (rule no_fail_pre, wp no_fail_bind)
149  apply simp
150  done
151
152lemma empty_fail_stateAssert:
153  "empty_fail (stateAssert P s)"
154  by (simp add: stateAssert_def assert_def empty_fail_get)
155
156lemma haskell_fail_wp:
157  "\<lbrace>\<top>\<rbrace> haskell_fail x \<lbrace>P\<rbrace>"
158  by simp
159
160lemma no_fail_haskell_fail [simp, wp]:
161  "no_fail \<bottom> (haskell_fail xs)"
162  by simp
163
164lemma in_assocs_is_fun:
165  "(x \<in> set (assocs f)) = (f (fst x) = snd x)"
166  by (cases x) (auto simp add: assocs_def)
167
168lemma fun_is_in_assocs:
169  "(f x = y) = ((x,y) \<in> set (assocs f))"
170  by (simp add: in_assocs_is_fun)
171
172lemma empty_set_is_null:
173  "(set xs = {}) = null xs"
174  by (clarsimp simp: null_def)
175
176lemma assert_into_when:
177  "(assert P) = (when (\<not> P) (haskell_fail []))"
178  by (simp add: assert_def when_def)
179
180lemma const_apply:
181  "const x y = x"
182  by (simp add: const_def)
183
184lemma const_None_empty:
185  "const None = Map.empty"
186  by (rule ext, simp add: const_apply)
187
188lemma headM_tailM_Cons:
189  "headM (x # xs) = return x"
190  "tailM (x # xs) = return xs"
191  by (simp add: headM_def tailM_def)+
192
193lemma replicateM_mapM:
194  "replicateM n f = mapM (\<lambda>x. f) (replicate n ())"
195  by (simp add: replicateM_def mapM_def)
196
197lemma orList_False:
198  "(\<not> orList bs) = (set bs \<subseteq> {False})"
199  apply (induct bs)
200  apply (simp_all add: orList_def foldl_True)
201  apply (case_tac a)
202  apply (simp_all add: orList_def foldl_True)
203  done
204
205lemma Cons_eq_tails:
206  "((xs # xxs) = tails ys) = (ys = xs \<and> xxs = tl (tails ys))"
207  by (case_tac ys, auto)
208
209lemma findM_on_outcome':
210  assumes x: "\<And>x xs. \<lbrace>\<lambda>s. Q None s \<and> x \<in> fn s \<and> set xs \<subseteq> fn s\<rbrace> f x
211                     \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xs \<subseteq> fn s)\<rbrace>"
212  shows      "\<lbrace>\<lambda>s. Q None s \<and> set xs \<subseteq> fn s\<rbrace> findM f xs \<lbrace>Q\<rbrace>"
213  apply (induct xs)
214   apply (simp, wp)
215  apply (simp, wp)
216   apply (rule x)
217  apply simp
218  done
219
220
221lemma findM_on_outcome:
222  assumes x: "\<And>x ys. x \<in> set xs \<Longrightarrow> \<lbrace>Q None and I\<rbrace> f x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> I s)\<rbrace>"
223  shows      "\<lbrace>Q None and I\<rbrace> findM f xs \<lbrace>Q\<rbrace>"
224  apply (rule hoare_vcg_precond_imp)
225   apply (rule findM_on_outcome' [where fn="\<lambda>s. if I s then set xs else {}"])
226   apply (case_tac "x \<notin> set xs")
227    apply simp
228   apply (simp cong: rev_conj_cong)
229   apply (case_tac "\<not> set xsa \<subseteq> set xs")
230    apply simp
231   apply simp
232   apply (rule hoare_vcg_precond_imp)
233    apply (rule hoare_post_imp [OF _ x])
234     apply clarsimp
235    apply assumption
236   apply simp
237  apply simp
238  done
239
240lemma in_set_tailsD: "xs \<in> set (tails ys) \<Longrightarrow> set xs \<subseteq> set ys"
241  apply (induct ys)
242   apply simp
243  apply simp
244  apply (erule disjE)
245   apply simp
246  apply simp
247  apply blast
248  done
249
250lemma notin_set_tails_set:
251  "x \<notin> set xs \<Longrightarrow> \<forall>xs' \<in> set (tails xs). \<forall>x' \<in> set xs'. x \<noteq> x'"
252  by (fastforce dest!: in_set_tailsD)
253
254lemma set_tails_set: "(set (tails v) \<subseteq> {x. set x \<subseteq> S}) = (set v \<subseteq> S)"
255  apply (induct v, simp_all)
256  done
257
258lemma filter_assocs_Cons:
259  fixes v :: "('a :: len) word" shows
260  "\<lbrakk> f (v, g v); \<forall>x < v. \<not> f (x, g x) \<rbrakk> \<Longrightarrow>
261     filter f (assocs g) = (v, g v) # tl (filter f (assocs g))"
262  apply (simp add: assocs_def)
263  apply (cut_tac v=v in enum_word_div)
264  apply clarsimp
265  apply (subst map_cong [OF _ refl], assumption)+
266  apply (simp(no_asm))
267  apply simp
268  done
269
270lemma snd_stateAssert_after:
271  "\<not> snd ((do _ \<leftarrow> f; stateAssert R vs od) s) \<Longrightarrow>
272  \<not>snd (f s) \<and> (\<forall>(rv, s') \<in> fst (f s). R s')"
273  apply (clarsimp simp: bind_def stateAssert_def get_def assert_def
274      return_def fail_def split_def split: if_split_asm)
275  done
276
277lemma oblivious_stateAssert [simp]:
278  "oblivious f (stateAssert g xs) = (\<forall>s. g (f s) = g s)"
279  apply (simp add: oblivious_def stateAssert_def exec_get
280                   assert_def return_def fail_def split: if_split)
281  apply auto
282  done
283
284lemma stateAssert_def2:
285  "stateAssert f xs = do v \<leftarrow> gets f; if v then return () else fail od"
286  by (simp add: stateAssert_def gets_def assert_def)
287
288lemma findM_is_mapME:
289  "(findM f xs >>= g)
290   = liftM (\<lambda>_. ())
291      (doE ys \<leftarrow> mapME_x (\<lambda>x. do v \<leftarrow> f x;
292                             if v then do g (Some x); throwError () od
293                             else returnOk () od) xs;
294              liftE (g None) odE)"
295  apply (induct xs)
296   apply (simp add: mapME_x_def sequenceE_x_def liftM_def returnOk_bind)
297   apply (simp add: liftE_def)
298  apply (simp add: mapME_x_Cons bindE_assoc liftE_bindE[symmetric]
299                   liftM_def cong: if_cong)
300  apply (simp add: liftE_bindE bind_assoc)
301  apply (rule bind_cong[OF refl])
302  apply (simp add: bindE_assoc split: if_split)
303  apply (simp add: liftE_bindE bind_assoc throwError_bind)
304  done
305
306
307(* FIXME word_eqI: move up *)
308add_try_method word_eqI_solve
309
310end
311