--- 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>
--- 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>
--- 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
--- 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"
--- 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>
--- 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>
--- 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>
--- 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.
--- 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>
--- 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