add lemmas
authorAndreas Lochbihler
Tue Apr 14 11:32:01 2015 +0200 (2015-04-14)
changeset 6005786fa63ce8156
parent 60046 894d6d863823
child 60058 f17bb06599f6
add lemmas
src/HOL/Complete_Partial_Order.thy
src/HOL/Lifting_Set.thy
src/HOL/Map.thy
src/HOL/Product_Type.thy
src/HOL/Relation.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Complete_Partial_Order.thy	Mon Apr 13 13:03:41 2015 +0200
     1.2 +++ b/src/HOL/Complete_Partial_Order.thy	Tue Apr 14 11:32:01 2015 +0200
     1.3 @@ -53,6 +53,9 @@
     1.4  lemma chain_empty: "chain ord {}"
     1.5  by(simp add: chain_def)
     1.6  
     1.7 +lemma chain_equality: "chain op = A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. x = y)"
     1.8 +by(auto simp add: chain_def)
     1.9 +
    1.10  subsection {* Chain-complete partial orders *}
    1.11  
    1.12  text {*
     2.1 --- a/src/HOL/Lifting_Set.thy	Mon Apr 13 13:03:41 2015 +0200
     2.2 +++ b/src/HOL/Lifting_Set.thy	Tue Apr 14 11:32:01 2015 +0200
     2.3 @@ -281,4 +281,9 @@
     2.4  lemmas setsum_parametric = setsum.F_parametric
     2.5  lemmas setprod_parametric = setprod.F_parametric
     2.6  
     2.7 +lemma rel_set_UNION:
     2.8 +  assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"
     2.9 +  shows "rel_set R (UNION A f) (UNION B g)"
    2.10 +by transfer_prover
    2.11 +
    2.12  end
     3.1 --- a/src/HOL/Map.thy	Mon Apr 13 13:03:41 2015 +0200
     3.2 +++ b/src/HOL/Map.thy	Tue Apr 14 11:32:01 2015 +0200
     3.3 @@ -641,6 +641,8 @@
     3.4    ultimately show ?case by (simp only: map_of.simps ran_map_upd) simp
     3.5  qed
     3.6  
     3.7 +lemma ran_map_option: "ran (\<lambda>x. map_option f (m x)) = f ` ran m"
     3.8 +by(auto simp add: ran_def)
     3.9  
    3.10  subsection {* @{text "map_le"} *}
    3.11  
     4.1 --- a/src/HOL/Product_Type.thy	Mon Apr 13 13:03:41 2015 +0200
     4.2 +++ b/src/HOL/Product_Type.thy	Tue Apr 14 11:32:01 2015 +0200
     4.3 @@ -1224,6 +1224,18 @@
     4.4      using * eq[symmetric] by auto
     4.5  qed simp_all
     4.6  
     4.7 +lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A"
     4.8 +by(auto simp add: inj_on_def)
     4.9 +
    4.10 +lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f"
    4.11 +using inj_on_apfst[of f UNIV] by simp
    4.12 +
    4.13 +lemma inj_on_apsnd [simp]: "inj_on (apsnd f) (UNIV \<times> A) \<longleftrightarrow> inj_on f A"
    4.14 +by(auto simp add: inj_on_def)
    4.15 +
    4.16 +lemma inj_apsnd [simp]: "inj (apsnd f) \<longleftrightarrow> inj f"
    4.17 +using inj_on_apsnd[of f UNIV] by simp
    4.18 +
    4.19  definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
    4.20    [code_abbrev]: "product A B = A \<times> B"
    4.21  
     5.1 --- a/src/HOL/Relation.thy	Mon Apr 13 13:03:41 2015 +0200
     5.2 +++ b/src/HOL/Relation.thy	Tue Apr 14 11:32:01 2015 +0200
     5.3 @@ -216,6 +216,8 @@
     5.4    "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)"
     5.5    by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
     5.6  
     5.7 +lemma reflp_equality [simp]: "reflp op ="
     5.8 +by(simp add: reflp_def)
     5.9  
    5.10  subsubsection {* Irreflexivity *}
    5.11  
    5.12 @@ -357,6 +359,8 @@
    5.13  lemma antisym_empty [simp]: "antisym {}"
    5.14    by (unfold antisym_def) blast
    5.15  
    5.16 +lemma antisymP_equality [simp]: "antisymP op ="
    5.17 +by(auto intro: antisymI)
    5.18  
    5.19  subsubsection {* Transitivity *}
    5.20  
     6.1 --- a/src/HOL/Set.thy	Mon Apr 13 13:03:41 2015 +0200
     6.2 +++ b/src/HOL/Set.thy	Tue Apr 14 11:32:01 2015 +0200
     6.3 @@ -647,7 +647,6 @@
     6.4  lemma empty_not_UNIV[simp]: "{} \<noteq> UNIV"
     6.5  by blast
     6.6  
     6.7 -
     6.8  subsubsection {* The Powerset operator -- Pow *}
     6.9  
    6.10  definition Pow :: "'a set => 'a set set" where
    6.11 @@ -846,6 +845,9 @@
    6.12    assume ?R thus ?L by (auto split: if_splits)
    6.13  qed
    6.14  
    6.15 +lemma insert_UNIV: "insert x UNIV = UNIV"
    6.16 +by auto
    6.17 +
    6.18  subsubsection {* Singletons, using insert *}
    6.19  
    6.20  lemma singletonI [intro!]: "a : {a}"
    6.21 @@ -1884,6 +1886,8 @@
    6.22  lemma bind_const: "Set.bind A (\<lambda>_. B) = (if A = {} then {} else B)"
    6.23    by (auto simp add: bind_def)
    6.24  
    6.25 +lemma bind_singleton_conv_image: "Set.bind A (\<lambda>x. {f x}) = f ` A"
    6.26 +  by(auto simp add: bind_def)
    6.27  
    6.28  subsubsection {* Operations for execution *}
    6.29