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

lib: Another trivial lemma for supporting CAmkES.

This commit is contained in:
Matthew Fernandez 2015-08-11 15:53:28 +10:00
parent 3f20d24822
commit 10f963db36
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
lib/LemmaBucket.thy
View File

@ -424,4 +424,7 @@ lemma none_some_map2: "the ` Set.filter (\<lambda>s. \<not> Option.is_none s) (r
lemma prop_map_of_prop:"\<lbrakk>\<forall>z \<in> set xs. P (g z); map_of (map (\<lambda>x. (f x, g x)) xs) y = Some a\<rbrakk> \<Longrightarrow> P a"
using map_of_SomeD by fastforce
lemma range_subsetI: "\<forall>y\<in>A. \<exists>x. f x = y \<Longrightarrow> A \<subseteq> range f"
by fast
end