1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(*  WP-specific Eisbach methods *)
8
9theory Eisbach_WP
10imports
11  Eisbach_Methods
12  NonDetMonadVCG
13  Conjuncts
14  Rule_By_Method
15  WPI
16begin
17
18
19text \<open>
20  Methods for manipulating the post conditions of hoare triples as if they
21  were proper subgoals.
22
23  post_asm can be used with the @ attribute to modify existing proofs. Useful
24  for proving large postconditions in one proof and then subsequently decomposing it.
25
26\<close>
27context begin
28
29definition "packed_valid P f si r s \<equiv> P si \<and> (r, s) \<in> fst (f si)"
30
31lemma packed_validE:"(\<And>si r s. packed_valid P f si r s \<Longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
32  by (clarsimp simp: valid_def packed_valid_def)
33
34lemma packed_validI: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>si r s. packed_valid P f si r s \<longrightarrow> Q r s"
35  apply (clarsimp simp: valid_def packed_valid_def)
36  by auto
37
38definition "packed_validR P f si r s \<equiv> P si \<and> (Inr r, s) \<in> fst (f si)"
39
40
41lemma packed_validRE:"(\<And>si r s. packed_validR P f si r s \<Longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
42  apply (clarsimp simp: validE_R_def validE_def valid_def packed_validR_def)
43  by (metis sum.case sumE)
44
45lemma packed_validRI: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<forall>si r s. packed_validR P f si r s \<longrightarrow> Q r s"
46  apply (clarsimp simp: valid_def validE_R_def validE_def packed_validR_def)
47  by fastforce
48
49lemma trivial_imp: "\<forall>r s. Q r s \<longrightarrow> Q r s" by simp
50
51lemma uncurry2: "\<forall>r s. Q r s \<and> Q' r s \<longrightarrow> Q'' r s \<Longrightarrow> \<forall>r s. Q r s \<longrightarrow> Q' r s \<longrightarrow> Q'' r s"
52  by simp
53
54named_theorems hoare_post_imps
55
56lemmas [hoare_post_imps] = hoare_post_imp_R hoare_post_imp[rotated]
57
58method post_asm_raw methods m =
59  (drule hoare_post_imps,
60   atomize (full),
61   focus_concl
62     \<open>intro impI allI,
63      m,
64      atomize (full),
65      ((rule uncurry2)+)?\<close>,
66   rule trivial_imp)
67
68method post_asm methods m =
69  (post_asm_raw \<open>(simp only: bipred_conj_def pred_conj_def)?,(elim conjE)?,m\<close>)
70
71
72named_theorems packed_validEs
73
74lemmas [packed_validEs] = packed_validE packed_validRE
75
76named_theorems packed_validIs
77
78lemmas [packed_validIs] = packed_validI packed_validRI
79
80method post_raw methods m =
81  (focus_concl
82    \<open>rule packed_validEs,
83     focus_concl \<open>m,fold_subgoals\<close>,
84     atomize (full),
85     rule packed_validI\<close>)
86
87method post_strong methods m_distinct m_all =
88  (post_raw
89     \<open>(simp only: pred_conj_def bipred_conj_def)?,
90      (intro impI conjI allI)?,
91      distinct_subgoals_strong \<open>m_distinct\<close>,
92      all \<open>m_all\<close>,
93      fold_subgoals\<close>)
94
95method post methods m = post_strong \<open>(assumption | erule mp)+\<close> \<open>m\<close>
96
97end
98
99
100text \<open>
101  Method (meant to be used with @ as an attribute) used for producing multiple facts out of
102  a single hoare triple with a conjunction in its post condition.
103\<close>
104
105context begin
106
107private lemma hoare_decompose:
108  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<and> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>"
109  by (fastforce simp add: valid_def pred_conj_def)
110
111private lemma hoare_decomposeE_R:
112  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<and> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-"
113  by (fastforce simp add: validE_R_def validE_def valid_def pred_conj_def split: prod.splits sum.splits)
114
115private lemma hoare_decomposeE_E:
116  "\<lbrace>P\<rbrace> f -,\<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<and> \<lbrace>P\<rbrace> f -,\<lbrace>Q'\<rbrace>"
117  by (fastforce simp add: validE_E_def validE_def valid_def pred_conj_def split: prod.splits sum.splits)
118
119private lemma hoare_decomposeE:
120  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. E r s \<and> E' r s\<rbrace>,\<lbrace>\<lambda>r s. R r s \<and> R' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>E\<rbrace>,- \<and> \<lbrace>P\<rbrace> f \<lbrace>E'\<rbrace>,- \<and> \<lbrace>P\<rbrace> f -,\<lbrace>R\<rbrace> \<and> \<lbrace>P\<rbrace> f -,\<lbrace>R'\<rbrace>"
121  by (fastforce simp add: validE_R_def validE_E_def validE_def valid_def pred_conj_def split: prod.splits sum.splits)
122
123private lemmas hoare_decomposes' = hoare_decompose hoare_decomposeE_R hoare_decomposeE_E hoare_decomposeE
124
125private method add_pred_conj = (subst pred_conj_def[symmetric])
126private method add_bipred_conj = (subst bipred_conj_def[symmetric])
127
128private lemmas hoare_decomposes[THEN conjE] =
129  hoare_decomposes'
130  hoare_decomposes'[# \<open>add_pred_conj\<close>]
131  hoare_decomposes'[# \<open>add_bipred_conj\<close>]
132  hoare_decomposeE[# \<open>add_pred_conj, add_pred_conj\<close>]
133  hoare_decomposeE[# \<open>add_bipred_conj, add_pred_conj\<close>]
134  hoare_decomposeE[# \<open>add_pred_conj, add_bipred_conj\<close>]
135  hoare_decomposeE[# \<open>add_bipred_conj, add_bipred_conj\<close>]
136
137method hoare_decompose = (elim hoare_decomposes)
138
139end
140
141
142notepad begin
143  fix A :: "'a \<Rightarrow> bool" and B C D f
144  assume A: "\<And>s. A s = True" and
145         B: "\<And>s :: 'a. B s = True" and
146         C: "\<And>s :: 'a. C s = True" and
147         D: "\<And>s :: 'a. D s = True" and
148         f: "f = (return () :: ('a,unit) nondet_monad)"
149
150  have f_valid[@ \<open>hoare_decompose\<close>,conjuncts]: "\<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B and C and D\<rbrace>"
151  apply (simp add: f)
152  apply wp
153  by (simp add: B C D)
154
155  note f_valid' = conjuncts
156
157  have f_d: "\<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. D\<rbrace>" by (rule f_valid')
158
159  have f_valid_interm: "\<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B and C and (\<lambda>s. D s \<longrightarrow> B s)\<rbrace>"
160  apply (post_strong \<open>simp\<close> \<open>-\<close>)
161  apply (wp f_valid')
162  by simp
163
164  (* All rotations are attempted when strengthening *)
165
166  have f_valid_interm: "\<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. (\<lambda>s. D s \<longrightarrow> B s) and B and C \<rbrace>"
167  apply (post_strong \<open>simp\<close> \<open>-\<close>, wp f_valid')
168  by simp
169
170end
171
172
173
174
175end
176