# HG changeset patch
# User Andreas Lochbihler
# Date 1447231704 -3600
# Node ID 608520e0e8e28ea3d23dfa53990140b583c1eaae
# Parent  90f54d9e63f2c263b45cde938f652dc5bb2d9f3a
add various lemmas

diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/Complete_Lattices.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -1346,6 +1346,8 @@
 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
   by (fact Sup_inf_eq_bot_iff)
 
+lemma SUP_UNION: "(SUP x:(UN y:A. g y). f x) = (SUP y:A. SUP x:g y. f x :: _ :: complete_lattice)"
+by(rule order_antisym)(blast intro: SUP_least SUP_upper2)+
 
 subsection \<open>Injections and bijections\<close>
 
diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/Fun.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -663,6 +663,8 @@
 lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
   by auto
 
+lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z"
+by(simp add: fun_eq_iff split: split_if_asm)
 
 subsection \<open>@{text override_on}\<close>
 
diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/Lifting.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -570,6 +570,12 @@
 ML_file "Tools/Lifting/lifting_setup.ML"
 ML_file "Tools/Lifting/lifting_def_code_dt.ML"
 
+lemma pred_prod_beta: "pred_prod P Q xy \<longleftrightarrow> P (fst xy) \<and> Q (snd xy)"
+by(cases xy) simp
+
+lemma pred_prod_split: "P (pred_prod Q R xy) \<longleftrightarrow> (\<forall>x y. xy = (x, y) \<longrightarrow> P (Q x \<and> R y))"
+by(cases xy) simp
+
 hide_const (open) POS NEG
 
 end
diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/List.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -795,6 +795,8 @@
 lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
   by (auto intro!: inj_onI)
 
+lemma inj_on_Cons1 [simp]: "inj_on (op # x) A"
+by(simp add: inj_on_def)
 
 subsubsection \<open>@{const length}\<close>
 
@@ -2501,6 +2503,9 @@
 apply (case_tac j, auto)
 done
 
+lemma zip_replicate1: "zip (replicate n x) ys = map (Pair x) (take n ys)"
+by(induction ys arbitrary: n)(case_tac [2] n, simp_all)
+
 lemma take_zip:
   "take n (zip xs ys) = zip (take n xs) (take n ys)"
 apply (induct n arbitrary: xs ys)
@@ -2718,6 +2723,20 @@
 lemma list_all2_same: "list_all2 P xs xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x x)"
 by(auto simp add: list_all2_conv_all_nth set_conv_nth)
 
+lemma zip_assoc:
+  "zip xs (zip ys zs) = map (\<lambda>((x, y), z). (x, y, z)) (zip (zip xs ys) zs)"
+by(rule list_all2_all_nthI[where P="op =", unfolded list.rel_eq]) simp_all
+
+lemma zip_commute: "zip xs ys = map (\<lambda>(x, y). (y, x)) (zip ys xs)"
+by(rule list_all2_all_nthI[where P="op =", unfolded list.rel_eq]) simp_all
+
+lemma zip_left_commute:
+  "zip xs (zip ys zs) = map (\<lambda>(y, (x, z)). (x, y, z)) (zip ys (zip xs zs))"
+by(rule list_all2_all_nthI[where P="op =", unfolded list.rel_eq]) simp_all
+
+lemma zip_replicate2: "zip xs (replicate n y) = map (\<lambda>x. (x, y)) (take n xs)"
+by(subst zip_commute)(simp add: zip_replicate1)
+
 subsubsection \<open>@{const List.product} and @{const product_lists}\<close>
 
 lemma set_product[simp]: "set (List.product xs ys) = set xs \<times> set ys"
diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/Num.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -174,6 +174,9 @@
   using nat_of_num_pos [of n] nat_of_num_pos [of m]
   by (auto simp add: less_eq_num_def less_num_def)
 
+lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One"
+by (simp add: antisym_conv)
+
 text \<open>Rules using @{text One} and @{text inc} as constructors\<close>
 
 lemma add_One: "x + One = inc x"
@@ -646,6 +649,26 @@
   zero_less_numeral
   not_numeral_less_zero
 
+lemma min_0_1 [simp]:
+  fixes min' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "min' \<equiv> min" shows
+  "min' 0 1 = 0"
+  "min' 1 0 = 0"
+  "min' 0 (numeral x) = 0"
+  "min' (numeral x) 0 = 0"
+  "min' 1 (numeral x) = 1"
+  "min' (numeral x) 1 = 1"
+by(simp_all add: min'_def min_def le_num_One_iff)
+
+lemma max_0_1 [simp]: 
+  fixes max' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "max' \<equiv> max" shows
+  "max' 0 1 = 1"
+  "max' 1 0 = 1"
+  "max' 0 (numeral x) = numeral x"
+  "max' (numeral x) 0 = numeral x"
+  "max' 1 (numeral x) = numeral x"
+  "max' (numeral x) 1 = numeral x"
+by(simp_all add: max'_def max_def le_num_One_iff)
+
 end
 
 subsubsection \<open>
diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/Option.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -65,6 +65,12 @@
 lemma rel_option_None2 [simp]: "rel_option P x None \<longleftrightarrow> x = None"
   by (cases x) simp_all
 
+lemma option_rel_Some1: "rel_option A (Some x) y \<longleftrightarrow> (\<exists>y'. y = Some y' \<and> A x y')" (* Option *)
+by(cases y) simp_all
+
+lemma option_rel_Some2: "rel_option A x (Some y) \<longleftrightarrow> (\<exists>x'. x = Some x' \<and> A x' y)" (* Option *)
+by(cases x) simp_all
+
 lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)"
   (is "?lhs = ?rhs")
 proof (rule antisym)
@@ -96,6 +102,9 @@
 lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
   by (simp add: map_option_case split add: option.split)
 
+lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None"
+by(cases x) simp_all
+
 lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
   by (simp add: map_option_case split add: option.split)
 
@@ -106,19 +115,27 @@
 lemma map_option_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map_option f x = map_option g y"
   by (cases x) auto
 
+lemma map_option_idI: "(\<And>y. y \<in> set_option x \<Longrightarrow> f y = y) \<Longrightarrow> map_option f x = x"
+by(cases x)(simp_all)
+
 functor map_option: map_option
   by (simp_all add: option.map_comp fun_eq_iff option.map_id)
 
 lemma case_map_option [simp]: "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
   by (cases x) simp_all
 
+lemma None_notin_image_Some [simp]: "None \<notin> Some ` A"
+by auto
+
+lemma notin_range_Some: "x \<notin> range Some \<longleftrightarrow> x = None"
+by(cases x) auto
+
 lemma rel_option_iff:
   "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
     | (Some x, Some y) \<Rightarrow> R x y
     | _ \<Rightarrow> False)"
   by (auto split: prod.split option.split)
 
-
 context
 begin
 
@@ -183,6 +200,9 @@
 lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
   by (cases f) simp_all
 
+lemma bind_eq_None_conv: "Option.bind a f = None \<longleftrightarrow> a = None \<or> f (the a) = None"
+by(cases a) simp_all
+
 lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)"
   by (cases x) simp_all
 
@@ -197,6 +217,15 @@
 lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f"
   by simp
 
+lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)"
+by(cases x) simp_all
+
+lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)"
+by(cases x) auto
+
+lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)"
+by(cases x) simp_all
+
 end
 
 setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/Orderings.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -256,7 +256,6 @@
 unfolding Least_def by (rule theI2)
   (blast intro: assms antisym)+
 
-
 text \<open>Dual order\<close>
 
 lemma dual_order:
@@ -1171,6 +1170,10 @@
 lemma max_absorb1: "(y::'a::order) \<le> x \<Longrightarrow> max x y = x"
   by (simp add: max_def)
 
+lemma max_min_same [simp]:
+  fixes x y :: "'a :: linorder"
+  shows "max x (min x y) = x" "max (min x y) x = x" "max (min x y) y = y" "max y (min x y) = y"
+by(auto simp add: max_def min_def)
 
 subsection \<open>(Unique) top and bottom elements\<close>
 
diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/Product_Type.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -1144,6 +1144,9 @@
   "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)"
   by blast
 
+lemma Pair_vimage_Sigma: "Pair x -` Sigma A f = (if x \<in> A then f x else {})"
+  by auto
+
 text \<open>
   Non-dependent versions are needed to avoid the need for higher-order
   matching, especially when the rules are re-oriented.
diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/Relation.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -219,6 +219,9 @@
 lemma reflp_equality [simp]: "reflp op ="
 by(simp add: reflp_def)
 
+lemma reflp_mono: "\<lbrakk> reflp R; \<And>x y. R x y \<longrightarrow> Q x y \<rbrakk> \<Longrightarrow> reflp Q"
+by(auto intro: reflpI dest: reflpD)
+
 subsubsection \<open>Irreflexivity\<close>
 
 definition irrefl :: "'a rel \<Rightarrow> bool"
@@ -676,6 +679,8 @@
 lemma eq_OO: "op= OO R = R"
 by blast
 
+lemma OO_eq: "R OO op = = R"
+by blast
 
 subsubsection \<open>Converse\<close>
 
diff -r 90f54d9e63f2 -r 608520e0e8e2 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Wed Nov 11 09:21:56 2015 +0100
+++ b/src/HOL/Transfer.thy	Wed Nov 11 09:48:24 2015 +0100
@@ -620,6 +620,10 @@
   shows "((A ===> B ===> op =) ===> op =) right_unique right_unique"
 unfolding right_unique_def[abs_def] by transfer_prover
 
+lemma map_fun_parametric [transfer_rule]:
+  "((A ===> B) ===> (C ===> D) ===> (B ===> C) ===> A ===> D) map_fun map_fun"
+unfolding map_fun_def[abs_def] by transfer_prover
+
 end
 
 end