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