1(*
2 *
3 * Copyright 2017, Data61, CSIRO
4 *
5 * This software may be distributed and modified according to the terms of
6 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
7 * See "LICENSE_BSD2.txt" for details.
8 *
9 * @TAG(DATA61_BSD)
10 *)
11
12
13theory CorresK_Lemmas
14imports
15  "Lib.Corres_Method"
16  "ExecSpec.Syscall_H"
17  "ASpec.Syscall_A"
18begin
19
20lemma corres_throwError_str [corres_concrete_rER]:
21  "corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throw b)"
22  "corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throwError b)"
23 by (simp add: corres_underlyingK_def)+
24
25lemma corresK_use_guard:
26  "(F \<Longrightarrow> corres_underlyingK sr nf nf' F r Q Q' f g) \<Longrightarrow> corres_underlyingK sr nf nf' F r Q Q' f g"
27  by (simp add: corres_underlyingK_def)
28
29lemma mapME_x_corresK_inv:
30  assumes x: "\<And>x. corres_underlyingK sr nf nf' (F x) (f \<oplus> dc) (P x) (P' x) (m x) (m' x)"
31  assumes y: "\<And>x P. \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>x. P\<rbrace>,-" "\<And>x P'. \<lbrace>P'\<rbrace> m' x \<lbrace>\<lambda>x. P'\<rbrace>,-"
32  shows      "corres_underlyingK sr nf nf' (xs = ys \<and> (\<forall>x \<in> set xs. F x)) (f \<oplus> dc) (\<lambda>s. \<forall>x \<in> set xs. P x s) (\<lambda>s. \<forall>y \<in> set ys. P' y s)
33                              (mapME_x m xs) (mapME_x m' ys)"
34  apply (rule corresK_use_guard, elim conjE)
35  subgoal premises prems
36  unfolding \<open>xs = ys\<close>
37  proof (induct ys)
38    case Nil
39    show ?case
40      by (simp add: mapME_x_def sequenceE_x_def returnOk_def corres_underlyingK_def)
41  next
42    case (Cons z zs)
43    from Cons have IH:
44      "corres_underlyingK sr nf nf' (\<forall>x\<in>set zs. F x) (f \<oplus> dc) (\<lambda>s. \<forall>x\<in>set zs. P x s) (\<lambda>s. \<forall>y\<in>set zs. P' y s)
45                       (mapME_x m zs) (mapME_x m' zs)" by (auto simp add:  dc_def)
46    show ?case
47      apply (simp add: mapME_x_def sequenceE_x_def)
48      apply (fold mapME_x_def sequenceE_x_def dc_def)
49      apply (corressimp corresK: x IH wp: y)
50      done
51  qed
52  done
53
54lemma corresK_mapM:
55  assumes S: "set (zip xs ys) \<subseteq> S"
56  assumes z: "\<And>x y. corres_protect ((x, y) \<in> S) \<Longrightarrow> corres_underlyingK R nf nf' (F x y) r' P P' (f x) (f' y)"
57  assumes w: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
58             "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>"
59  shows      "corres_underlyingK R nf nf'
60                  ((length xs = length ys) \<and>
61                   (r [] []) \<and> (\<forall>x xs y ys. r xs ys \<longrightarrow> r' x y \<longrightarrow> r (x # xs) (y # ys)) \<and>
62                  (\<forall>(x,y)\<in>S. F x y)) r P P' (mapM f xs) (mapM f' ys)"
63  unfolding corres_underlyingK_def
64  apply (rule impI, rule corres_mapM[of r r' S])
65  using assms unfolding corres_underlyingK_def by (auto simp: corres_protect_def)
66
67definition
68  "F_all2 F xs ys =
69    (\<exists>F'.
70      (\<forall>x y xs ys.
71        (F' x y \<longrightarrow> list_all2 F' xs ys \<longrightarrow> F x y xs ys)) \<and> list_all2 F' xs ys)"
72
73
74lemma F_all2_pointwise[simp]:
75  "F_all2 (\<lambda>x y _ _. F x y) xs ys = list_all2 F xs ys"
76  apply (rule iffI)
77  apply (clarsimp simp: F_all2_def)
78  subgoal for F'
79  apply (rule list_all2_induct_suffixeq[where Q=F']; simp)
80  apply (drule_tac x=x in spec)
81  apply (drule_tac x=y in spec)
82  apply fastforce
83  done
84  apply (clarsimp simp:F_all2_def)
85  apply (rule_tac x=F in exI)
86  apply clarsimp
87  done
88
89lemma F_all2_list:
90   "F xs ys \<Longrightarrow> \<exists>F'. (\<forall>xs ys. (F xs ys = list_all2 F' xs ys)) \<Longrightarrow> F_all2 (\<lambda>_ _ xs ys. F xs ys) xs ys"
91  apply (clarsimp simp: F_all2_def)
92  apply (rule_tac x=F' in exI)
93  by auto
94
95lemma list_all2_conjD:
96  "list_all2 (\<lambda>x y. Q x y \<and> P x y) xs ys \<Longrightarrow> list_all2 Q xs ys \<and> list_all2 P xs ys"
97  by (induct rule: list_all2_induct; simp)
98
99
100lemma
101  list_all2_to_list_all:
102  "list_all2 P xs xs = list_all (\<lambda>x. P x x) xs"
103  by (induct xs;simp)
104
105lemma list_all_mem_subset:
106  "list_all (\<lambda>y. y \<in> set xs) ys = (set ys \<subseteq> set xs)"
107  by (induct ys; simp)
108
109lemma F_all2_eq:
110  "(\<And>x xs'. x \<in> set xs \<Longrightarrow> set xs' \<subseteq> set xs \<Longrightarrow> F x x xs' xs') \<Longrightarrow> F_all2 F xs xs"
111 apply (simp add: F_all2_def)
112 apply (rule_tac x="\<lambda>x y. x \<in> set xs \<and> x = y" in exI)
113 apply (intro conjI impI allI)
114 apply (drule list_all2_conjD)
115 apply (simp add: list.rel_eq)
116 apply clarsimp
117 apply (simp add: list_all2_to_list_all list_all_mem_subset)
118 apply (rule list.rel_refl_strong;simp)
119 done
120
121lemma F_all2_conjI:
122  "F_all2 F xs ys \<Longrightarrow> F_all2 F' xs ys \<Longrightarrow>
123    F_all2 (\<lambda>x y xs ys. F x y xs ys \<and> F' x y xs ys) xs ys"
124  apply (clarsimp simp: F_all2_def)
125  apply (rule_tac x="\<lambda>x y. F'a x y \<and> F'aa x y" in exI)
126  by (auto dest: list_all2_conjD intro: list_all2_conj)
127
128lemma corresK_mapM_list_all2:
129  assumes x: "\<And>x y xs ys. corres_underlyingK sr nf nf' (F x y xs ys) r' (I (x#xs)) (I' (y#ys)) (f x) (f' y)"
130  assumes "\<And>x y xs. \<lbrakk> S x y; suffix (x#xs) as \<rbrakk> \<Longrightarrow> \<lbrace> I  (x#xs) \<rbrace> f  x \<lbrace> \<lambda>rv. I  xs \<rbrace>"
131  assumes "\<And>x y ys. \<lbrakk> S x y; suffix (y#ys) cs \<rbrakk> \<Longrightarrow> \<lbrace> I' (y#ys) \<rbrace> f' y \<lbrace> \<lambda>rv. I' ys \<rbrace>"
132  shows "corres_underlyingK sr nf nf'
133          (r [] [] \<and> (\<forall> x y xs ys. r' x y \<longrightarrow> r xs ys \<longrightarrow> r (x # xs) (y # ys)) \<and>
134            list_all2 S as cs \<and> F_all2 F as cs)
135                            r (I as) (I' cs) (mapM f as) (mapM f' cs)"
136  unfolding corres_underlyingK_def
137  apply (clarsimp simp: F_all2_def)
138  subgoal for F'
139  apply (rule corres_mapM_list_all2[of r r' "\<lambda>x y. S x y \<and> F' x y"]; (rule assms | assumption | clarsimp)?)
140  apply (rule x[THEN corresK_unlift])
141  apply (drule list_all2_conjD)
142  apply (clarsimp simp: assms | assumption)+
143  apply (rule list_all2_conj; simp)
144  done
145  done
146
147lemma corresK_discard_rv:
148  assumes A[corresK]: "corres_underlyingK sr nf nf' F r' P P' a c"
149  shows "corres_underlyingK sr nf nf' F dc P P' (do x \<leftarrow> a; return () od) (do x \<leftarrow> c; return () od)"
150  by corressimp
151
152lemma corresK_mapM_mapM_x:
153  assumes "corres_underlyingK sr nf nf' F r' P P' (mapM f as) (mapM f' cs)"
154  shows "corres_underlyingK sr nf nf' F dc P P' (mapM_x f as) (mapM_x f' cs)"
155  unfolding mapM_x_mapM by (rule corresK_discard_rv, rule assms)
156
157lemmas corresK_mapM_x_list_all2
158  = corresK_mapM_list_all2[where r'=dc,
159                           THEN corresK_mapM_mapM_x[where r'=dc],
160                           simplified]
161lemmas corresK_mapM_x
162  = corresK_mapM[where r'=dc,
163                 THEN corresK_mapM_mapM_x[where r'=dc],
164                 simplified]
165
166lemma corresK_subst_both: "g' = f' \<Longrightarrow> g = f \<Longrightarrow>
167  corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
168  corres_underlyingK sr nf nf' F r P P' g g'" by simp
169
170lemma if_fun_true: "(if A then B else (\<lambda>_. True)) = (\<lambda>s. (A  \<longrightarrow> B s))" by simp
171
172lemmas corresK_whenE [corres_splits] =
173  corresK_if[THEN
174    corresK_subst_both[OF whenE_def[THEN meta_eq_to_obj_eq] whenE_def[THEN meta_eq_to_obj_eq]],
175    OF _ corresK_returnOk[where r="f \<oplus> dc" for f], simplified, simplified if_fun_true]
176
177lemmas corresK_head_splits[corres_splits] =
178  corresK_split[where d="return", simplified]
179  corresK_splitE[where d="returnOk", simplified]
180  corresK_split[where b="return", simplified]
181  corresK_splitE[where b="returnOk", simplified]
182
183lemmas corresK_modify =
184  corres_modify[atomized, @corresK_convert]
185
186lemmas corresK_modifyT = corresK_modify[where P=\<top> and P'=\<top>, simplified]
187
188lemma corresK_Id:
189  "(nf' \<Longrightarrow> no_fail P' g) \<Longrightarrow>
190    corres_underlyingK Id nf nf' (f = g \<and> (\<forall>rv. r rv rv)) r (\<lambda>_. True) P' f g"
191  apply (rule corresK_assume_guard)
192  apply (rule corres_Id;simp)
193  done
194
195lemmas [corresK] =
196  corresK_Id[where nf'=False and r="(=)",simplified]
197  corresK_Id[where nf'=False,simplified]
198  corresK_Id[where nf'=True and r="(=)", simplified]
199  corresK_Id[where nf'=True, simplified]
200
201lemma corresK_unit_rv_eq_any[corres_concrete_r]:
202  "corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
203    corres_underlyingK sr nf nf' F
204      (\<lambda>(x :: unit) (y :: unit). x = y) P P' f f'"
205  apply (clarsimp simp add: corres_underlyingK_def)
206  apply (erule corres_rel_imp)
207  apply simp
208  done
209
210lemma corresK_unit_rv_dc_any[corres_concrete_r]:
211  "corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
212    corres_underlyingK sr nf nf' F
213      (\<lambda>(x :: unit) (y :: unit). dc x y) P P' f f'"
214  apply (clarsimp simp add: corres_underlyingK_def)
215  apply (erule corres_rel_imp)
216  apply simp
217  done
218
219end
220