# HG changeset patch
# User Andreas Lochbihler
# Date 1429003921 -7200
# Node ID 86fa63ce8156240ae6971ffaa3a0100ea5d975ec
# Parent  894d6d863823c0fbf187f0f62cee3879cb43de54
add lemmas

diff -r 894d6d863823 -r 86fa63ce8156 src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -53,6 +53,9 @@
 lemma chain_empty: "chain ord {}"
 by(simp add: chain_def)
 
+lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
+by(auto simp add: chain_def)
+
 subsection {* Chain-complete partial orders *}
 
 text {*
diff -r 894d6d863823 -r 86fa63ce8156 src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Lifting_Set.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -281,4 +281,9 @@
 lemmas setsum_parametric = setsum.F_parametric
 lemmas setprod_parametric = setprod.F_parametric
 
+lemma rel_set_UNION:
+  assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
+  shows "rel_set R (UNION A f) (UNION B g)"
+by transfer_prover
+
 end
diff -r 894d6d863823 -r 86fa63ce8156 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Map.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -641,6 +641,8 @@
   ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
 qed
 
+lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
+by(auto simp add: ran_def)
 
 subsection {* @{text "map_le"} *}
 
diff -r 894d6d863823 -r 86fa63ce8156 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Product_Type.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -1224,6 +1224,18 @@
     using * eq[symmetric] by auto
 qed simp_all
 
+lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A"
+by(auto simp add: inj_on_def)
+
+lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f"
+using inj_on_apfst[of f UNIV] by simp
+
+lemma inj_on_apsnd [simp]: "inj_on (apsnd f) (UNIV \<times> A) \<longleftrightarrow> inj_on f A"
+by(auto simp add: inj_on_def)
+
+lemma inj_apsnd [simp]: "inj (apsnd f) \<longleftrightarrow> inj f"
+using inj_on_apsnd[of f UNIV] by simp
+
 definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
   [code_abbrev]: "product A B = A \<times> B"
 
diff -r 894d6d863823 -r 86fa63ce8156 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Relation.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -216,6 +216,8 @@
   "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
   by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
 
+lemma reflp_equality [simp]: "reflp op ="
+by(simp add: reflp_def)
 
 subsubsection {* Irreflexivity *}
 
@@ -357,6 +359,8 @@
 lemma antisym_empty [simp]: "antisym {}"
   by (unfold antisym_def) blast
 
+lemma antisymP_equality [simp]: "antisymP op ="
+by(auto intro: antisymI)
 
 subsubsection {* Transitivity *}
 
diff -r 894d6d863823 -r 86fa63ce8156 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Apr 13 13:03:41 2015 +0200
+++ b/src/HOL/Set.thy	Tue Apr 14 11:32:01 2015 +0200
@@ -647,7 +647,6 @@
 lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
 by blast
 
-
 subsubsection {* The Powerset operator -- Pow *}
 
 definition Pow :: "'a set => 'a set set" where
@@ -846,6 +845,9 @@
   assume ?R thus ?L by (auto split: if_splits)
 qed
 
+lemma insert_UNIV: "insert x UNIV = UNIV"
+by auto
+
 subsubsection {* Singletons, using insert *}
 
 lemma singletonI [intro!]: "a : {a}"
@@ -1884,6 +1886,8 @@
 lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
   by (auto simp add: bind_def)
 
+lemma bind_singleton_conv_image: "Set.bind A (\<lambda>x. {f x}) = f ` A"
+  by(auto simp add: bind_def)
 
 subsubsection {* Operations for execution *}