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

lib: add unit_dc_is_eq

This commit is contained in:
Michael McInerney 2019-06-12 16:19:37 +10:00
parent 5fef6f3443
commit 81dab3dcec
1 changed files with 4 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Corres_UL.thy
View File

@ -285,6 +285,10 @@ lemma dc_o_simp1[simp]: "dc \<circ> f = dc"
lemma dc_o_simp2[simp]: "dc x \<circ> f = dc x"
by (simp add: dc_def o_def)
lemma unit_dc_is_eq:
"(dc::unit\<Rightarrow>_\<Rightarrow>_) = (=)"
by (fastforce simp: dc_def)
lemma corres_split_nor:
"\<lbrakk> corres_underlying sr nf nf' r R R' b d; corres_underlying sr nf nf' dc P P' a c;
\<lbrace>Q\<rbrace> a \<lbrace>\<lambda>x. R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>x. R'\<rbrace> \<rbrakk>