summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 08 Nov 2021 11:45:15 +0100 | |

changeset 75117 | 8eb1cbe7c889 |

parent 75116 | 58ae06d382ee |

child 75118 | 30b6042d122f |

added eq_iff_swap for generating symmetric versions; applied it in List.

src/HOL/HOL.thy | file | annotate | diff | comparison | revisions | |

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/HOL.thy Sun Nov 07 23:35:11 2021 +0100 +++ b/src/HOL/HOL.thy Mon Nov 08 11:45:15 2021 +0100 @@ -1678,6 +1678,9 @@ subsection \<open>Other simple lemmas and lemma duplicates\<close> +lemma eq_iff_swap: "(x = y \<longleftrightarrow> P) \<Longrightarrow> (y = x \<longleftrightarrow> P)" +by blast + lemma all_cong1: "(\<And>x. P x = P' x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>x. P' x)" by auto

--- a/src/HOL/List.thy Sun Nov 07 23:35:11 2021 +0100 +++ b/src/HOL/List.thy Mon Nov 08 11:45:15 2021 +0100 @@ -795,8 +795,7 @@ lemma tl_Nil: "tl xs = [] \<longleftrightarrow> xs = [] \<or> (\<exists>x. xs = [x])" by (cases xs) auto -lemma Nil_tl: "[] = tl xs \<longleftrightarrow> xs = [] \<or> (\<exists>x. xs = [x])" -by (cases xs) auto +lemmas Nil_tl = tl_Nil[THEN eq_iff_swap] lemma length_induct: "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs" @@ -847,9 +846,7 @@ lemma length_Suc_conv: "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" by (induct xs) auto -lemma Suc_length_conv: - "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" -by (induct xs; simp; blast) +lemmas Suc_length_conv = length_Suc_conv[THEN eq_iff_swap] lemma Suc_le_length_iff: "(Suc n \<le> length xs) = (\<exists>x ys. xs = x # ys \<and> n \<le> length ys)" @@ -924,14 +921,12 @@ lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])" by (induct xs) auto -lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])" -by (induct xs) auto +lemmas Nil_is_append_conv [iff] = append_is_Nil_conv[THEN eq_iff_swap] lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])" by (induct xs) auto -lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])" -by (induct xs) auto +lemmas self_append_conv [iff] = append_self_conv[THEN eq_iff_swap] lemma append_eq_append_conv [simp]: "length xs = length ys \<or> length us = length vs @@ -958,8 +953,7 @@ lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])" using append_same_eq [of _ _ "[]"] by auto -lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])" -using append_same_eq [of "[]"] by auto +lemmas self_append_conv2 [iff] = append_self_conv2[THEN eq_iff_swap] lemma hd_Cons_tl: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs" by (fact list.collapse) @@ -981,9 +975,7 @@ (ys = [] \<and> x#xs = zs \<or> (\<exists>ys'. x#ys' = ys \<and> xs = ys'@zs))" by(cases ys) auto -lemma append_eq_Cons_conv: "(ys@zs = x#xs) = - (ys = [] \<and> zs = x#xs \<or> (\<exists>ys'. ys = x#ys' \<and> ys'@zs = xs))" -by(cases ys) auto +lemmas append_eq_Cons_conv = Cons_eq_append_conv[THEN eq_iff_swap] lemma longest_common_prefix: "\<exists>ps xs' ys'. xs = ps @ xs' \<and> ys = ps @ ys' @@ -1087,18 +1079,15 @@ by simp lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" -by (cases xs) auto - -lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])" -by (cases xs) auto +by (rule list.map_disc_iff) + +lemmas Nil_is_map_conv [iff] = map_is_Nil_conv[THEN eq_iff_swap] lemma map_eq_Cons_conv: "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)" by (cases xs) auto -lemma Cons_eq_map_conv: - "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)" -by (cases ys) auto +lemmas Cons_eq_map_conv = map_eq_Cons_conv[THEN eq_iff_swap] lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1] @@ -1199,14 +1188,12 @@ lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])" by (induct xs) auto -lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])" -by (induct xs) auto +lemmas Nil_is_rev_conv [iff] = rev_is_Nil_conv[THEN eq_iff_swap] lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])" by (cases xs) auto -lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])" -by (cases xs) auto +lemmas singleton_rev_conv [simp] = rev_singleton_conv[THEN eq_iff_swap] lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)" proof (induct xs arbitrary: ys) @@ -1249,9 +1236,11 @@ qed qed simp -lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])" +lemma rev_eq_Cons_iff[simp]: "(rev xs = y#ys) = (xs = rev ys @ [y])" by(rule rev_cases[of xs]) auto +lemmas Cons_eq_rev_iff[simp] = rev_eq_Cons_iff[THEN eq_iff_swap] + subsubsection \<open>\<^const>\<open>set\<close>\<close> @@ -1275,8 +1264,7 @@ lemma set_empty [iff]: "(set xs = {}) = (xs = [])" by (induct xs) auto -lemma set_empty2[iff]: "({} = set xs) = (xs = [])" -by(induct xs) auto +lemmas set_empty2[iff] = set_empty[THEN eq_iff_swap] lemma set_rev [simp]: "set (rev xs) = set xs" by (induct xs) auto @@ -1429,8 +1417,7 @@ lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])" by (induct xss) auto -lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])" - by (induct xss) auto +lemmas Nil_eq_concat_conv [simp] = concat_eq_Nil_conv[THEN eq_iff_swap] lemma set_concat [simp]: "set (concat xs) = (\<Union>x\<in>set xs. set x)" by (induct xs) auto @@ -1654,10 +1641,7 @@ (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)" by(auto dest:filter_eq_ConsD) -lemma Cons_eq_filter_iff: - "(x#xs = filter P ys) = - (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)" - by(auto dest:Cons_eq_filterD) +lemmas Cons_eq_filter_iff = filter_eq_Cons_iff[THEN eq_iff_swap] lemma inj_on_filter_key_eq: assumes "inj_on f (insert y (set xs))" @@ -2128,9 +2112,18 @@ lemma take_all_iff [simp]: "take n xs = xs \<longleftrightarrow> length xs \<le> n" by (metis length_take min.order_iff take_all) +lemmas take_all_iff2[simp] = take_all_iff[THEN eq_iff_swap] + lemma drop_all_iff [simp]: "drop n xs = [] \<longleftrightarrow> length xs \<le> n" by (metis diff_is_0_eq drop_all length_drop list.size(3)) +lemmas drop_all_iff2 [simp] = drop_all_iff[THEN eq_iff_swap] + +lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])" + by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split) + +lemmas take_eq_Nil2[simp] = take_eq_Nil[THEN eq_iff_swap] + lemma take_append [simp]: "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)" by (induct n arbitrary: xs) (auto, case_tac xs, auto) @@ -2178,12 +2171,6 @@ then show ?case by (cases xs) simp_all qed -lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])" - by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split) - -lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs \<le> n)" - by (induct xs arbitrary: n) (auto simp: drop_Cons split:nat.split) - lemma take_map: "take n (map f xs) = map f (take n xs)" proof (induct n arbitrary: xs) case 0 @@ -2308,9 +2295,7 @@ using map_append by blast qed -lemma append_eq_map_conv: - "ys @ zs = map f xs \<longleftrightarrow> (\<exists>us vs. xs = us @ vs \<and> ys = map f us \<and> zs = map f vs)" -by (metis map_eq_append_conv) +lemmas append_eq_map_conv = map_eq_append_conv[THEN eq_iff_swap] lemma take_add: "take (i+j) xs = take i xs @ take j (drop i xs)" proof (induct xs arbitrary: i) @@ -2763,10 +2748,12 @@ from this that show ?thesis by fastforce qed -lemma zip_eq_Nil_iff: +lemma zip_eq_Nil_iff[simp]: "zip xs ys = [] \<longleftrightarrow> xs = [] \<or> ys = []" by (cases xs; cases ys) simp_all +lemmas Nil_eq_zip_iff[simp] = zip_eq_Nil_iff[THEN eq_iff_swap] + lemma zip_eq_ConsE: assumes "zip xs ys = xy # xys" obtains x xs' y ys' where "xs = x # xs'" @@ -3434,8 +3421,7 @@ lemma upto_Nil[simp]: "[i..j] = [] \<longleftrightarrow> j < i" by (simp add: upto.simps) -lemma upto_Nil2[simp]: "[] = [i..j] \<longleftrightarrow> j < i" -by (simp add: upto.simps) +lemmas upto_Nil2[simp] = upto_Nil[THEN eq_iff_swap] lemma upto_rec1: "i \<le> j \<Longrightarrow> [i..j] = i#[i+1..j]" by(simp add: upto.simps) @@ -3601,8 +3587,7 @@ lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])" by (induct x, auto) -lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])" -by (induct x, auto) +lemmas remdups_eq_nil_right_iff [simp] = remdups_eq_nil_iff[THEN eq_iff_swap] lemma length_remdups_leq[iff]: "length(remdups xs) \<le> length xs" by (induct xs) auto @@ -4546,8 +4531,7 @@ lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0" by (induct n) auto -lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0" -by (induct n) auto +lemmas empty_replicate[simp] = replicate_empty[THEN eq_iff_swap] lemma replicate_eq_replicate[simp]: "(replicate m x = replicate n y) \<longleftrightarrow> (m=n \<and> (m\<noteq>0 \<longrightarrow> x=y))"