adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: connection between exs_valid and wp conjugate (#588) 

Draw connection between conjugate wp in the literature and our
exs_valid definition.

Add exs_valid_alt lemma, which is one of the main rules that is
different between wp and conjugate wp (or vs and).

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-03-08 13:02:54 +11:00 committed by GitHub
parent 1a7eb92111
commit a454a093c0
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 28 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
lib/Monads/NonDetMonad_Sat.thy
View File

@ -20,13 +20,36 @@ definition exs_valid ::
"('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b) nondet_monad \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>") where
"\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>(rv, s') \<in> fst (f s). Q rv s')"
text \<open>The above for the exception monad\<close>
definition ex_exs_validE ::
"('a \<Rightarrow> bool) \<Rightarrow> ('a, 'e + 'b) nondet_monad \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('e \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>, \<lbrace>_\<rbrace>") where
"\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<equiv> \<lbrace>P\<rbrace> f \<exists>\<lbrace>\<lambda>rv. case rv of Inl e \<Rightarrow> E e | Inr v \<Rightarrow> Q v\<rbrace>"
text \<open>
Seen as predicate transformer, @{const exs_valid} is the so-called conjugate wp in the literature,
i.e. with
@{term "wp f Q \<equiv> \<lambda>s. fst (f s) \<subseteq> {(rv,s). Q rv s}"} and
@{term "cwp f Q \<equiv> not (wp f (not Q))"}, we get
@{prop "valid P f Q = (\<forall>s. P s \<longrightarrow> wp f Q s)"} and
@{prop "exs_valid P f Q = (\<forall>s. P s \<longrightarrow> cwp f Q s)"}.
See also "Predicate Calculus and Program Semantics" by E. W. Dijkstra and C. S. Scholten.\<close>
experiment
begin
definition
"wp f Q \<equiv> \<lambda>s. fst (f s) \<subseteq> {(rv,s). Q rv s}"
definition
"cwp f Q \<equiv> not (wp f (not Q))"
lemma
"exs_valid P f Q = (\<forall>s. P s \<longrightarrow> cwp f Q s)"
unfolding exs_valid_def cwp_def wp_def by auto
end
subsection \<open>Set up for @{method wp}\<close>
@ -73,6 +96,10 @@ lemma exs_valid_select[wp]:
"\<lbrace>\<lambda>s. \<exists>r \<in> S. Q r s\<rbrace> select S \<exists>\<lbrace>Q\<rbrace>"
by (clarsimp simp: exs_valid_def select_def)
lemma exs_valid_alt[wp]:
"\<lbrakk> \<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g \<exists>\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P or P'\<rbrace> f \<sqinter> g \<exists>\<lbrace>Q\<rbrace>"
by (fastforce simp: exs_valid_def alternative_def)
lemma exs_valid_get[wp]:
"\<lbrace>\<lambda>s. Q s s\<rbrace> get \<exists>\<lbrace> Q \<rbrace>"
by (clarsimp simp: exs_valid_def get_def)