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

lib: adjust some congruence rules for strengthen. 

Adjusting the strengthen congruence rules for conjunction
and disjunction makes other conjuncts available as assumptions
in strengthening a conjunction. This may be useful occasionally.
This commit is contained in:
Thomas Sewell 2018-07-16 15:38:05 +10:00
parent 8392624f6c
commit bfce624b2b
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Monad_WP/Strengthen.thy
View File

@ -418,12 +418,12 @@ lemma strengthen_imp_ord[simp]:
by (auto simp add: st_def)
lemma strengthen_imp_conj [strg]:
"\<lbrakk> B \<Longrightarrow> st F (op \<longrightarrow>) A A'; st F (op \<longrightarrow>) B B' \<rbrakk>
"\<lbrakk> A' \<Longrightarrow> st F (op \<longrightarrow>) B B'; B \<Longrightarrow> st F (op \<longrightarrow>) A A' \<rbrakk>
\<Longrightarrow> st F (op \<longrightarrow>) (A \<and> B) (A' \<and> B')"
by (cases F, auto)
lemma strengthen_imp_disj [strg]:
"\<lbrakk> \<not> B \<Longrightarrow> st F (op \<longrightarrow>) A A'; st F (op \<longrightarrow>) B B' \<rbrakk>
"\<lbrakk> \<not> A' \<Longrightarrow> st F (op \<longrightarrow>) B B'; \<not> B \<Longrightarrow> st F (op \<longrightarrow>) A A' \<rbrakk>
\<Longrightarrow> st F (op \<longrightarrow>) (A \<or> B) (A' \<or> B')"
by (cases F, auto)