author Andreas Lochbihler Wed Nov 11 09:48:24 2015 +0100 (2015-11-11) changeset 61630 608520e0e8e2 parent 61629 90f54d9e63f2 child 61631 4f7ef088c4ed
 src/HOL/Complete_Lattices.thy file | annotate | diff | revisions src/HOL/Fun.thy file | annotate | diff | revisions src/HOL/Lifting.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions src/HOL/Num.thy file | annotate | diff | revisions src/HOL/Option.thy file | annotate | diff | revisions src/HOL/Orderings.thy file | annotate | diff | revisions src/HOL/Product_Type.thy file | annotate | diff | revisions src/HOL/Relation.thy file | annotate | diff | revisions src/HOL/Transfer.thy file | annotate | diff | revisions
```     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.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.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.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.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.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.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.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
```