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

lib: add option_Some_value_independent

This commit is contained in:
Rafal Kolanski 2019-07-30 15:39:19 +10:00
parent 4319e81887
commit 4cc9a1fb19
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/Lib.thy
View File

@ -2507,6 +2507,10 @@ lemma rsubst:
lemma ex_impE: "((\<exists>x. P x) \<longrightarrow> Q) \<Longrightarrow> P x \<Longrightarrow> Q"
by blast
lemma option_Some_value_independent:
"\<lbrakk> f x = Some v; \<And>v'. f x = Some v' \<Longrightarrow> f y = Some v' \<rbrakk> \<Longrightarrow> f y = Some v"
by blast
text \<open>Some int bitwise lemmas. Helpers for proofs about \<^file>\<open>NatBitwise.thy\<close>\<close>
lemma int_2p_eq_shiftl:
"(2::int)^x = 1 << x"