1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory ExtraCorres
8imports Corres_UL
9begin
10
11lemma corres_mapM:
12  assumes x: "r [] []"
13  assumes y: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)"
14  assumes z: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying R nf nf' r' P P' (f x) (f' y)"
15  assumes w: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
16             "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>"
17  shows      "\<lbrakk> length xs = length ys; set (zip xs ys) \<subseteq> S \<rbrakk> \<Longrightarrow>
18                   corres_underlying R nf nf' r P P' (mapM f xs) (mapM f' ys)"
19proof (induct xs ys rule: list_induct2)
20  case Nil
21  show ?case
22    by (simp add: mapM_def sequence_def x)
23next
24  case (Cons a as b bs)
25  from Cons have P: "(a, b) \<in> S"
26    by simp
27  from Cons have Q: "corres_underlying R nf nf' r P P' (mapM f as) (mapM f' bs)"
28    by simp
29  show ?case
30    apply (simp add: mapM_Cons)
31    apply (rule corres_guard_imp)
32      apply (rule corres_split[OF _ z [OF P] w [OF P]])
33      apply (rule corres_split' [OF Q])
34        apply (rule corres_trivial, simp add: y)
35       apply (wp | simp)+
36    done
37qed
38
39(* list_all2 has _much_ nicer simps than set (zip _ _).
40    See KernelInit_R: corres_init_objs for an example *)
41lemma corres_mapM_list_all2:
42  assumes rn: "r [] []"
43  and     rc: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)"
44  and   corr: "\<And>x xs y ys. \<lbrakk> S x y; list_all2 S xs ys \<rbrakk>
45               \<Longrightarrow> corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y)"
46  and     ha: "\<And>x xs y. \<lbrakk> S x y; suffix (x#xs) as \<rbrakk> \<Longrightarrow> \<lbrace>Q  (x # xs)\<rbrace> f x \<lbrace>\<lambda>r. Q xs\<rbrace>"
47  and     hc: "\<And>x y ys. \<lbrakk> S x y; suffix (y#ys) cs \<rbrakk> \<Longrightarrow> \<lbrace>Q' (y # ys) \<rbrace> f' y \<lbrace>\<lambda>r. Q' ys\<rbrace>"
48  and   lall: "list_all2 S as cs"
49  shows       "corres_underlying sr nf nf' r (Q as) (Q' cs) (mapM f as) (mapM f' cs)"
50  using lall
51proof (induct rule: list_all2_induct_suffixeq)
52  case Nil
53  thus ?case
54    unfolding mapM_def sequence_def by (auto intro: rn)
55next
56  case  (Cons x xs y ys)
57
58  have corr': "corres_underlying sr nf nf' r' (Q (x # xs)) (Q' (y # ys)) (f x) (f' y)"
59  proof (rule corr)
60    show "list_all2 S xs ys" by (simp add: Cons)
61  qed fact+
62
63  show ?case
64    apply (simp add: mapM_Cons)
65    apply (rule corres_split' [OF corr' _ ha [OF Cons(2)] hc [OF Cons(2)]])
66    apply (rule corres_split' [OF Cons(3) _ hoare_post_taut hoare_post_taut])
67    apply (simp add: rc)
68    apply (rule Cons.hyps)+
69    done
70qed
71
72lemma corres_mapM_x:
73  assumes x: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying sr nf nf' dc P P' (f x) (f' y)"
74  assumes y: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
75             "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>"
76  assumes z: "length xs = length ys"
77  assumes w: "set (zip xs ys) \<subseteq> S"
78  shows      "corres_underlying sr nf nf' dc P P' (mapM_x f xs) (mapM_x f' ys)"
79  apply (simp add: mapM_x_mapM)
80  apply (rule corres_guard_imp)
81    apply (rule corres_split_nor)
82       apply (rule corres_trivial, simp)
83      apply (rule corres_mapM [OF _ _ x y z w])
84          apply (simp | wp)+
85  done
86
87lemma corres_mapME:
88  assumes x: "r [] []"
89  assumes y: "\<And>x xs y ys. \<lbrakk> r xs ys; r' x y \<rbrakk> \<Longrightarrow> r (x # xs) (y # ys)"
90  assumes z: "\<And>x y. (x, y) \<in> S \<Longrightarrow> corres_underlying R nf nf' (F \<oplus> r') P P' (f x) (f' y)"
91  assumes w: "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>"
92             "\<And>x y. (x, y) \<in> S \<Longrightarrow> \<lbrace>P'\<rbrace> f' y \<lbrace>\<lambda>rv. P'\<rbrace>"
93  shows      "\<lbrakk> length xs = length ys; set (zip xs ys) \<subseteq> S \<rbrakk> \<Longrightarrow>
94                   corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f xs) (mapME f' ys)"
95proof (induct xs ys rule: list_induct2)
96  case Nil
97  show ?case
98    by (simp add: mapME_def sequenceE_def x returnOk_def)
99next
100  case (Cons a as b bs)
101  from Cons have P: "(a, b) \<in> S"
102    by simp
103  from Cons have Q: "corres_underlying R nf nf' (F \<oplus> r) P P' (mapME f as) (mapME f' bs)"
104    by simp
105  show ?case
106    apply (simp add: mapME_Cons)
107    apply (rule corres_guard_imp)
108    apply (unfold bindE_def validE_def)
109      apply (rule corres_underlying_split [OF z [OF P]])
110        prefer 3
111        apply clarify
112       apply (simp add: lift_def)
113      apply (case_tac rv)
114       apply (clarsimp simp: throwError_def)
115       apply clarsimp
116        apply (rule corres_split[OF _ Q])
117          apply (rule corres_trivial)
118          apply (case_tac rv)
119           apply (clarsimp simp add: lift_def throwError_def)
120          apply (clarsimp simp add: y lift_def returnOk_def throwError_def)
121         apply (wpsimp wp: w P)+
122  done
123qed
124
125lemma corres_Id:
126  "\<lbrakk> f = g; \<And>rv. r rv rv; nf' \<Longrightarrow> no_fail P' g \<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' r \<top> P' f g"
127  apply (clarsimp simp: corres_underlying_def Ball_def no_fail_def)
128  apply (rule rev_bexI, assumption)
129  apply simp
130  done
131
132lemma select_pick_corres_underlying:
133  "corres_underlying sr nf nf' r P Q (f x) g
134     \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g"
135  by (fastforce simp: corres_underlying_def select_def bind_def)
136
137lemma select_pick_corres:
138  "corres_underlying sr nf nf' r P Q (f x) g
139     \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g"
140  by (fastforce simp: intro: select_pick_corres_underlying)
141
142lemma select_pick_corresE:
143  "corres_underlying sr nf nf' r P Q (f x) g
144     \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (liftE (select S) >>=E f) g"
145  by (fastforce simp: liftE_bindE intro: select_pick_corres)
146
147lemma corres_modify:
148  assumes rl:
149  "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> (f s, g s') \<in> sr"
150  shows "corres_underlying sr nf nf' dc P P' (modify f) (modify g)"
151  by (simp add: simpler_modify_def corres_singleton rl)
152
153lemma corres_gets_the:
154  assumes x: "corres_underlying sr nf nf' (r \<circ> the) P P' (gets f) y"
155  shows      "corres_underlying sr nf nf' r (P and (\<lambda>s. f s \<noteq> None)) P' (gets_the f) y"
156proof -
157  have z: "corres_underlying sr nf nf' (\<lambda>x y. \<exists>x'. x = Some x' \<and> r x' y)
158                 (P and (\<lambda>s. f s \<noteq> None)) P' (gets f) y"
159    apply (subst corres_cong [OF refl refl refl refl])
160     defer
161     apply (rule corres_guard_imp[OF x], simp+)
162    apply (clarsimp simp: simpler_gets_def)
163    done
164  show ?thesis
165    apply (rule corres_guard_imp)
166      apply (unfold gets_the_def)
167      apply (subst bind_return[symmetric], rule corres_split [OF _ z])
168        apply (rule corres_trivial, clarsimp simp: assert_opt_def)
169       apply (wp | simp)+
170  done
171qed
172
173
174lemma corres_u_nofail:
175  "corres_underlying S nf True r P P' f g \<Longrightarrow> (nf \<Longrightarrow> no_fail P f) \<Longrightarrow>
176  no_fail (\<lambda>s'. \<exists>s. (s,s') \<in> S \<and> P s \<and> P' s') g"
177  apply (clarsimp simp add: corres_underlying_def no_fail_def)
178  apply fastforce
179  done
180
181lemma wp_from_corres_u:
182  "\<lbrakk> corres_underlying R nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow>
183  \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> R \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace> f' \<lbrace>\<lambda>rv' s'. \<exists>rv s. (s,s') \<in> R \<and> r rv rv' \<and> Q rv s \<and> Q' rv' s'\<rbrace>"
184  apply (fastforce simp: corres_underlying_def valid_def no_fail_def)
185  done
186
187lemma wp_from_corres_u_unit:
188  "\<lbrakk> corres_underlying R nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>_. Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow>
189  \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> R \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace>
190  f' \<lbrace>\<lambda>_ s'. \<exists>s. (s,s') \<in> R \<and> Q s \<and> Q' s'\<rbrace>"
191  apply (fastforce dest: wp_from_corres_u elim: hoare_strengthen_post)
192  done
193
194lemma corres_nofail:
195  "corres_underlying state_relation nf True r P P' f g \<Longrightarrow> (nf \<Longrightarrow> no_fail P f) \<Longrightarrow>
196  no_fail (\<lambda>s'. \<exists>s. (s,s') \<in> state_relation \<and> P s \<and> P' s') g"
197  by (rule corres_u_nofail)
198
199lemma wp_from_corres_unit:
200  "\<lbrakk> corres_underlying state_relation nf nf' r G G' f f';
201     \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>_. Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow>
202  \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> state_relation \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace>
203  f' \<lbrace>\<lambda>_ s'. \<exists>s. (s,s') \<in> state_relation \<and> Q s \<and> Q' s'\<rbrace>"
204  by (auto intro!: wp_from_corres_u_unit)
205
206end
207