add various lemmas
authorAndreas Lochbihler
Wed Nov 11 09:48:24 2015 +0100 (2015-11-11)
changeset 61630608520e0e8e2
parent 61629 90f54d9e63f2
child 61631 4f7ef088c4ed
add various lemmas
src/HOL/Complete_Lattices.thy
src/HOL/Fun.thy
src/HOL/Lifting.thy
src/HOL/List.thy
src/HOL/Num.thy
src/HOL/Option.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Relation.thy
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Wed Nov 11 09:21:56 2015 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Wed Nov 11 09:48:24 2015 +0100
     1.3 @@ -1346,6 +1346,8 @@
     1.4  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) \<longleftrightarrow> (\<forall>B\<in>C. B \<inter> A = {})"
     1.5    by (fact Sup_inf_eq_bot_iff)
     1.6  
     1.7 +lemma SUP_UNION: "(SUP x:(UN y:A. g y). f x) = (SUP y:A. SUP x:g y. f x :: _ :: complete_lattice)"
     1.8 +by(rule order_antisym)(blast intro: SUP_least SUP_upper2)+
     1.9  
    1.10  subsection \<open>Injections and bijections\<close>
    1.11  
     2.1 --- a/src/HOL/Fun.thy	Wed Nov 11 09:21:56 2015 +0100
     2.2 +++ b/src/HOL/Fun.thy	Wed Nov 11 09:48:24 2015 +0100
     2.3 @@ -663,6 +663,8 @@
     2.4  lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
     2.5    by auto
     2.6  
     2.7 +lemma fun_upd_eqD: "f(x := y) = g(x := z) \<Longrightarrow> y = z"
     2.8 +by(simp add: fun_eq_iff split: split_if_asm)
     2.9  
    2.10  subsection \<open>@{text override_on}\<close>
    2.11  
     3.1 --- a/src/HOL/Lifting.thy	Wed Nov 11 09:21:56 2015 +0100
     3.2 +++ b/src/HOL/Lifting.thy	Wed Nov 11 09:48:24 2015 +0100
     3.3 @@ -570,6 +570,12 @@
     3.4  ML_file "Tools/Lifting/lifting_setup.ML"
     3.5  ML_file "Tools/Lifting/lifting_def_code_dt.ML"
     3.6  
     3.7 +lemma pred_prod_beta: "pred_prod P Q xy \<longleftrightarrow> P (fst xy) \<and> Q (snd xy)"
     3.8 +by(cases xy) simp
     3.9 +
    3.10 +lemma pred_prod_split: "P (pred_prod Q R xy) \<longleftrightarrow> (\<forall>x y. xy = (x, y) \<longrightarrow> P (Q x \<and> R y))"
    3.11 +by(cases xy) simp
    3.12 +
    3.13  hide_const (open) POS NEG
    3.14  
    3.15  end
     4.1 --- a/src/HOL/List.thy	Wed Nov 11 09:21:56 2015 +0100
     4.2 +++ b/src/HOL/List.thy	Wed Nov 11 09:48:24 2015 +0100
     4.3 @@ -795,6 +795,8 @@
     4.4  lemma inj_split_Cons: "inj_on (\<lambda>(xs, n). n#xs) X"
     4.5    by (auto intro!: inj_onI)
     4.6  
     4.7 +lemma inj_on_Cons1 [simp]: "inj_on (op # x) A"
     4.8 +by(simp add: inj_on_def)
     4.9  
    4.10  subsubsection \<open>@{const length}\<close>
    4.11  
    4.12 @@ -2501,6 +2503,9 @@
    4.13  apply (case_tac j, auto)
    4.14  done
    4.15  
    4.16 +lemma zip_replicate1: "zip (replicate n x) ys = map (Pair x) (take n ys)"
    4.17 +by(induction ys arbitrary: n)(case_tac [2] n, simp_all)
    4.18 +
    4.19  lemma take_zip:
    4.20    "take n (zip xs ys) = zip (take n xs) (take n ys)"
    4.21  apply (induct n arbitrary: xs ys)
    4.22 @@ -2718,6 +2723,20 @@
    4.23  lemma list_all2_same: "list_all2 P xs xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x x)"
    4.24  by(auto simp add: list_all2_conv_all_nth set_conv_nth)
    4.25  
    4.26 +lemma zip_assoc:
    4.27 +  "zip xs (zip ys zs) = map (\<lambda>((x, y), z). (x, y, z)) (zip (zip xs ys) zs)"
    4.28 +by(rule list_all2_all_nthI[where P="op =", unfolded list.rel_eq]) simp_all
    4.29 +
    4.30 +lemma zip_commute: "zip xs ys = map (\<lambda>(x, y). (y, x)) (zip ys xs)"
    4.31 +by(rule list_all2_all_nthI[where P="op =", unfolded list.rel_eq]) simp_all
    4.32 +
    4.33 +lemma zip_left_commute:
    4.34 +  "zip xs (zip ys zs) = map (\<lambda>(y, (x, z)). (x, y, z)) (zip ys (zip xs zs))"
    4.35 +by(rule list_all2_all_nthI[where P="op =", unfolded list.rel_eq]) simp_all
    4.36 +
    4.37 +lemma zip_replicate2: "zip xs (replicate n y) = map (\<lambda>x. (x, y)) (take n xs)"
    4.38 +by(subst zip_commute)(simp add: zip_replicate1)
    4.39 +
    4.40  subsubsection \<open>@{const List.product} and @{const product_lists}\<close>
    4.41  
    4.42  lemma set_product[simp]: "set (List.product xs ys) = set xs \<times> set ys"
     5.1 --- a/src/HOL/Num.thy	Wed Nov 11 09:21:56 2015 +0100
     5.2 +++ b/src/HOL/Num.thy	Wed Nov 11 09:48:24 2015 +0100
     5.3 @@ -174,6 +174,9 @@
     5.4    using nat_of_num_pos [of n] nat_of_num_pos [of m]
     5.5    by (auto simp add: less_eq_num_def less_num_def)
     5.6  
     5.7 +lemma le_num_One_iff: "x \<le> num.One \<longleftrightarrow> x = num.One"
     5.8 +by (simp add: antisym_conv)
     5.9 +
    5.10  text \<open>Rules using @{text One} and @{text inc} as constructors\<close>
    5.11  
    5.12  lemma add_One: "x + One = inc x"
    5.13 @@ -646,6 +649,26 @@
    5.14    zero_less_numeral
    5.15    not_numeral_less_zero
    5.16  
    5.17 +lemma min_0_1 [simp]:
    5.18 +  fixes min' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "min' \<equiv> min" shows
    5.19 +  "min' 0 1 = 0"
    5.20 +  "min' 1 0 = 0"
    5.21 +  "min' 0 (numeral x) = 0"
    5.22 +  "min' (numeral x) 0 = 0"
    5.23 +  "min' 1 (numeral x) = 1"
    5.24 +  "min' (numeral x) 1 = 1"
    5.25 +by(simp_all add: min'_def min_def le_num_One_iff)
    5.26 +
    5.27 +lemma max_0_1 [simp]: 
    5.28 +  fixes max' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" defines "max' \<equiv> max" shows
    5.29 +  "max' 0 1 = 1"
    5.30 +  "max' 1 0 = 1"
    5.31 +  "max' 0 (numeral x) = numeral x"
    5.32 +  "max' (numeral x) 0 = numeral x"
    5.33 +  "max' 1 (numeral x) = numeral x"
    5.34 +  "max' (numeral x) 1 = numeral x"
    5.35 +by(simp_all add: max'_def max_def le_num_One_iff)
    5.36 +
    5.37  end
    5.38  
    5.39  subsubsection \<open>
     6.1 --- a/src/HOL/Option.thy	Wed Nov 11 09:21:56 2015 +0100
     6.2 +++ b/src/HOL/Option.thy	Wed Nov 11 09:48:24 2015 +0100
     6.3 @@ -65,6 +65,12 @@
     6.4  lemma rel_option_None2 [simp]: "rel_option P x None \<longleftrightarrow> x = None"
     6.5    by (cases x) simp_all
     6.6  
     6.7 +lemma option_rel_Some1: "rel_option A (Some x) y \<longleftrightarrow> (\<exists>y'. y = Some y' \<and> A x y')" (* Option *)
     6.8 +by(cases y) simp_all
     6.9 +
    6.10 +lemma option_rel_Some2: "rel_option A x (Some y) \<longleftrightarrow> (\<exists>x'. x = Some x' \<and> A x' y)" (* Option *)
    6.11 +by(cases x) simp_all
    6.12 +
    6.13  lemma rel_option_inf: "inf (rel_option A) (rel_option B) = rel_option (inf A B)"
    6.14    (is "?lhs = ?rhs")
    6.15  proof (rule antisym)
    6.16 @@ -96,6 +102,9 @@
    6.17  lemma map_option_is_None [iff]: "(map_option f opt = None) = (opt = None)"
    6.18    by (simp add: map_option_case split add: option.split)
    6.19  
    6.20 +lemma None_eq_map_option_iff [iff]: "None = map_option f x \<longleftrightarrow> x = None"
    6.21 +by(cases x) simp_all
    6.22 +
    6.23  lemma map_option_eq_Some [iff]: "(map_option f xo = Some y) = (\<exists>z. xo = Some z \<and> f z = y)"
    6.24    by (simp add: map_option_case split add: option.split)
    6.25  
    6.26 @@ -106,19 +115,27 @@
    6.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"
    6.28    by (cases x) auto
    6.29  
    6.30 +lemma map_option_idI: "(\<And>y. y \<in> set_option x \<Longrightarrow> f y = y) \<Longrightarrow> map_option f x = x"
    6.31 +by(cases x)(simp_all)
    6.32 +
    6.33  functor map_option: map_option
    6.34    by (simp_all add: option.map_comp fun_eq_iff option.map_id)
    6.35  
    6.36  lemma case_map_option [simp]: "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
    6.37    by (cases x) simp_all
    6.38  
    6.39 +lemma None_notin_image_Some [simp]: "None \<notin> Some ` A"
    6.40 +by auto
    6.41 +
    6.42 +lemma notin_range_Some: "x \<notin> range Some \<longleftrightarrow> x = None"
    6.43 +by(cases x) auto
    6.44 +
    6.45  lemma rel_option_iff:
    6.46    "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
    6.47      | (Some x, Some y) \<Rightarrow> R x y
    6.48      | _ \<Rightarrow> False)"
    6.49    by (auto split: prod.split option.split)
    6.50  
    6.51 -
    6.52  context
    6.53  begin
    6.54  
    6.55 @@ -183,6 +200,9 @@
    6.56  lemma bind_eq_Some_conv: "bind f g = Some x \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
    6.57    by (cases f) simp_all
    6.58  
    6.59 +lemma bind_eq_None_conv: "Option.bind a f = None \<longleftrightarrow> a = None \<or> f (the a) = None"
    6.60 +by(cases a) simp_all
    6.61 +
    6.62  lemma map_option_bind: "map_option f (bind x g) = bind x (map_option f \<circ> g)"
    6.63    by (cases x) simp_all
    6.64  
    6.65 @@ -197,6 +217,15 @@
    6.66  lemma bind_option_cong_code: "x = y \<Longrightarrow> bind x f = bind y f"
    6.67    by simp
    6.68  
    6.69 +lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)"
    6.70 +by(cases x) simp_all
    6.71 +
    6.72 +lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)"
    6.73 +by(cases x) auto
    6.74 +
    6.75 +lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)"
    6.76 +by(cases x) simp_all
    6.77 +
    6.78  end
    6.79  
    6.80  setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm bind_option_cong_code})\<close>
     7.1 --- a/src/HOL/Orderings.thy	Wed Nov 11 09:21:56 2015 +0100
     7.2 +++ b/src/HOL/Orderings.thy	Wed Nov 11 09:48:24 2015 +0100
     7.3 @@ -256,7 +256,6 @@
     7.4  unfolding Least_def by (rule theI2)
     7.5    (blast intro: assms antisym)+
     7.6  
     7.7 -
     7.8  text \<open>Dual order\<close>
     7.9  
    7.10  lemma dual_order:
    7.11 @@ -1171,6 +1170,10 @@
    7.12  lemma max_absorb1: "(y::'a::order) \<le> x \<Longrightarrow> max x y = x"
    7.13    by (simp add: max_def)
    7.14  
    7.15 +lemma max_min_same [simp]:
    7.16 +  fixes x y :: "'a :: linorder"
    7.17 +  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"
    7.18 +by(auto simp add: max_def min_def)
    7.19  
    7.20  subsection \<open>(Unique) top and bottom elements\<close>
    7.21  
     8.1 --- a/src/HOL/Product_Type.thy	Wed Nov 11 09:21:56 2015 +0100
     8.2 +++ b/src/HOL/Product_Type.thy	Wed Nov 11 09:48:24 2015 +0100
     8.3 @@ -1144,6 +1144,9 @@
     8.4    "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)"
     8.5    by blast
     8.6  
     8.7 +lemma Pair_vimage_Sigma: "Pair x -` Sigma A f = (if x \<in> A then f x else {})"
     8.8 +  by auto
     8.9 +
    8.10  text \<open>
    8.11    Non-dependent versions are needed to avoid the need for higher-order
    8.12    matching, especially when the rules are re-oriented.
     9.1 --- a/src/HOL/Relation.thy	Wed Nov 11 09:21:56 2015 +0100
     9.2 +++ b/src/HOL/Relation.thy	Wed Nov 11 09:48:24 2015 +0100
     9.3 @@ -219,6 +219,9 @@
     9.4  lemma reflp_equality [simp]: "reflp op ="
     9.5  by(simp add: reflp_def)
     9.6  
     9.7 +lemma reflp_mono: "\<lbrakk> reflp R; \<And>x y. R x y \<longrightarrow> Q x y \<rbrakk> \<Longrightarrow> reflp Q"
     9.8 +by(auto intro: reflpI dest: reflpD)
     9.9 +
    9.10  subsubsection \<open>Irreflexivity\<close>
    9.11  
    9.12  definition irrefl :: "'a rel \<Rightarrow> bool"
    9.13 @@ -676,6 +679,8 @@
    9.14  lemma eq_OO: "op= OO R = R"
    9.15  by blast
    9.16  
    9.17 +lemma OO_eq: "R OO op = = R"
    9.18 +by blast
    9.19  
    9.20  subsubsection \<open>Converse\<close>
    9.21  
    10.1 --- a/src/HOL/Transfer.thy	Wed Nov 11 09:21:56 2015 +0100
    10.2 +++ b/src/HOL/Transfer.thy	Wed Nov 11 09:48:24 2015 +0100
    10.3 @@ -620,6 +620,10 @@
    10.4    shows "((A ===> B ===> op =) ===> op =) right_unique right_unique"
    10.5  unfolding right_unique_def[abs_def] by transfer_prover
    10.6  
    10.7 +lemma map_fun_parametric [transfer_rule]:
    10.8 +  "((A ===> B) ===> (C ===> D) ===> (B ===> C) ===> A ===> D) map_fun map_fun"
    10.9 +unfolding map_fun_def[abs_def] by transfer_prover
   10.10 +
   10.11  end
   10.12  
   10.13  end