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

lib: three lemmas moved from refine theories

This commit is contained in:
MiladKetabi 2019-10-03 15:03:25 +10:00
parent de9c069473
commit 1a49aacc31
2 changed files with 24 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Monad_WP/NonDetMonadVCG.thy
View File

@ -216,6 +216,10 @@ lemma pred_and_false[simp]: "(P and \<bottom>) = \<bottom>"
lemma pred_and_false_var[simp]: "(\<bottom> and P) = \<bottom>"
by(simp add:pred_conj_def)
lemma pred_conj_assoc:
"(P and Q and R) = (P and (Q and R))"
unfolding pred_conj_def by simp
subsection "Hoare Logic Rules"
lemma validE_def2:

20
lib/NonDetMonadLemmaBucket.thy
View File

@ -1146,6 +1146,22 @@ lemma case_options_weak_wp:
apply simp+
done
lemma case_option_wp_None_return:
assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace> f x \<lbrace>\<lambda>_. Q\<rbrace>"
shows "\<lbrakk>\<And>x s. (Q and P x) s \<Longrightarrow> P' x s \<rbrakk>
\<Longrightarrow> \<lbrace>Q and (\<lambda>s. opt \<noteq> None \<longrightarrow> P (the opt) s)\<rbrace>
(case opt of None \<Rightarrow> return () | Some x \<Rightarrow> f x)
\<lbrace>\<lambda>_. Q\<rbrace>"
by (cases opt; wpsimp)
lemma case_option_wp_None_returnOk:
assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace> f x \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>"
shows "\<lbrakk>\<And>x s. (Q and P x) s \<Longrightarrow> P' x s \<rbrakk>
\<Longrightarrow> \<lbrace>Q and (\<lambda>s. opt \<noteq> None \<longrightarrow> P (the opt) s)\<rbrace>
(case opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> f x)
\<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>"
by (cases opt; wpsimp)
lemma list_cases_weak_wp:
assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
assumes "\<And>x xs. \<lbrace>P_B\<rbrace> b x xs \<lbrace>Q\<rbrace>"
@ -1453,6 +1469,10 @@ lemma static_imp_wp:
"\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>"
by (cases P, simp_all add: valid_def)
lemma static_imp_wpE :
"\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
by (cases P, simp_all)
lemma static_imp_conj_wp:
"\<lbrakk> \<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>; \<lbrace>R\<rbrace> m \<lbrace>R'\<rbrace> \<rbrakk>
\<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. (P \<longrightarrow> Q' rv s) \<and> R' rv s\<rbrace>"