# HG changeset patch
# User nipkow
# Date 1614336418 -3600
# Node ID c8e317a4c905df9530af6b7f429ef1e7fc35bade
# Parent  95937cfe2628ac445701d25098ac11b24e8b7644
improved list_neq simproc

diff -r 95937cfe2628 -r c8e317a4c905 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Feb 25 13:35:54 2021 +0100
+++ b/src/HOL/List.thy	Fri Feb 26 11:46:58 2021 +0100
@@ -827,6 +827,7 @@
 lemma inj_on_Cons1 [simp]: "inj_on ((#) x) A"
 by(simp add: inj_on_def)
 
+
 subsubsection \<open>\<^const>\<open>length\<close>\<close>
 
 text \<open>
@@ -854,13 +855,12 @@
 lemma length_pos_if_in_set: "x \<in> set xs \<Longrightarrow> length xs > 0"
 by auto
 
-lemma length_Suc_conv:
-"(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
+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)
+by (induct xs; simp; blast)
 
 lemma Suc_le_length_iff:
   "(Suc n \<le> length xs) = (\<exists>x ys. xs = x # ys \<and> n \<le> length ys)"
@@ -914,45 +914,6 @@
 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
 by (rule Eq_FalseI) auto
 
-simproc_setup list_neq ("(xs::'a list) = ys") = \<open>
-(*
-Reduces xs=ys to False if xs and ys cannot be of the same length.
-This is the case if the atomic sublists of one are a submultiset
-of those of the other list and there are fewer Cons's in one than the other.
-*)
-
-let
-
-fun len (Const(\<^const_name>\<open>Nil\<close>,_)) acc = acc
-  | len (Const(\<^const_name>\<open>Cons\<close>,_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
-  | len (Const(\<^const_name>\<open>append\<close>,_) $ xs $ ys) acc = len xs (len ys acc)
-  | len (Const(\<^const_name>\<open>rev\<close>,_) $ xs) acc = len xs acc
-  | len (Const(\<^const_name>\<open>map\<close>,_) $ _ $ xs) acc = len xs acc
-  | len t (ts,n) = (t::ts,n);
-
-val ss = simpset_of \<^context>;
-
-fun list_neq ctxt ct =
-  let
-    val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
-    val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
-    fun prove_neq() =
-      let
-        val Type(_,listT::_) = eqT;
-        val size = HOLogic.size_const listT;
-        val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
-        val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
-        val thm = Goal.prove ctxt [] [] neq_len
-          (K (simp_tac (put_simpset ss ctxt) 1));
-      in SOME (thm RS @{thm neq_if_length_neq}) end
-  in
-    if m < n andalso submultiset (op aconv) (ls,rs) orelse
-       n < m andalso submultiset (op aconv) (rs,ls)
-    then prove_neq() else NONE
-  end;
-in K list_neq end
-\<close>
-
 
 subsubsection \<open>\<open>@\<close> -- append\<close>
 
@@ -1471,6 +1432,110 @@
 by(auto simp: append_eq_Cons_conv Cons_eq_append_conv append_eq_append_conv2)
 
 
+subsubsection \<open>\<^const>\<open>concat\<close>\<close>
+
+lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
+  by (induct xs) auto
+
+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
+
+lemma set_concat [simp]: "set (concat xs) = (\<Union>x\<in>set xs. set x)"
+  by (induct xs) auto
+
+lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
+  by (induct xs) auto
+
+lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
+  by (induct xs) auto
+
+lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
+  by (induct xs) auto
+
+lemma length_concat_rev[simp]: "length (concat (rev xs)) = length (concat xs)"
+by (induction xs) auto
+
+lemma concat_eq_concat_iff: "\<forall>(x, y) \<in> set (zip xs ys). length x = length y \<Longrightarrow> length xs = length ys \<Longrightarrow> (concat xs = concat ys) = (xs = ys)"
+proof (induct xs arbitrary: ys)
+  case (Cons x xs ys)
+  thus ?case by (cases ys) auto
+qed (auto)
+
+lemma concat_injective: "concat xs = concat ys \<Longrightarrow> length xs = length ys \<Longrightarrow> \<forall>(x, y) \<in> set (zip xs ys). length x = length y \<Longrightarrow> xs = ys"
+  by (simp add: concat_eq_concat_iff)
+
+lemma concat_eq_appendD:
+  assumes "concat xss = ys @ zs" "xss \<noteq> []"
+  shows "\<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2"
+  using assms
+proof(induction xss arbitrary: ys)
+  case (Cons xs xss)
+  from Cons.prems consider
+    us where "xs @ us = ys" "concat xss = us @ zs" |
+    us where "xs = ys @ us" "us @ concat xss = zs"
+    by(auto simp add: append_eq_append_conv2)
+  then show ?case
+  proof cases
+    case 1
+    then show ?thesis using Cons.IH[OF 1(2)]
+      by(cases xss)(auto intro: exI[where x="[]"], metis append.assoc append_Cons concat.simps(2))
+  qed(auto intro: exI[where x="[]"])
+qed simp
+
+lemma concat_eq_append_conv:
+  "concat xss = ys @ zs \<longleftrightarrow>
+  (if xss = [] then ys = [] \<and> zs = []
+   else \<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2)"
+  by(auto dest: concat_eq_appendD)
+
+lemma hd_concat: "\<lbrakk>xs \<noteq> []; hd xs \<noteq> []\<rbrakk> \<Longrightarrow> hd (concat xs) = hd (hd xs)"
+  by (metis concat.simps(2) hd_Cons_tl hd_append2)
+
+
+simproc_setup list_neq ("(xs::'a list) = ys") = \<open>
+(*
+Reduces xs=ys to False if xs and ys cannot be of the same length.
+This is the case if the atomic sublists of one are a submultiset
+of those of the other list and there are fewer Cons's in one than the other.
+*)
+
+let
+
+fun len (Const(\<^const_name>\<open>Nil\<close>,_)) acc = acc
+  | len (Const(\<^const_name>\<open>Cons\<close>,_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
+  | len (Const(\<^const_name>\<open>append\<close>,_) $ xs $ ys) acc = len xs (len ys acc)
+  | len (Const(\<^const_name>\<open>rev\<close>,_) $ xs) acc = len xs acc
+  | len (Const(\<^const_name>\<open>map\<close>,_) $ _ $ xs) acc = len xs acc
+  | len (Const(\<^const_name>\<open>concat\<close>,T) $ (Const(\<^const_name>\<open>rev\<close>,_) $ xss)) acc
+    = len (Const(\<^const_name>\<open>concat\<close>,T) $ xss) acc 
+  | len t (ts,n) = (t::ts,n);
+
+val ss = simpset_of \<^context>;
+
+fun list_neq ctxt ct =
+  let
+    val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
+    val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
+    fun prove_neq() =
+      let
+        val Type(_,listT::_) = eqT;
+        val size = HOLogic.size_const listT;
+        val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
+        val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
+        val thm = Goal.prove ctxt [] [] neq_len
+          (K (simp_tac (put_simpset ss ctxt) 1));
+      in SOME (thm RS @{thm neq_if_length_neq}) end
+  in
+    if m < n andalso submultiset (op aconv) (ls,rs) orelse
+       n < m andalso submultiset (op aconv) (rs,ls)
+    then prove_neq() else NONE
+  end;
+in K list_neq end
+\<close>
+
 subsubsection \<open>\<^const>\<open>filter\<close>\<close>
 
 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
@@ -1482,6 +1547,9 @@
 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
 by (induct xs) auto
 
+lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
+by (induct xs) auto
+
 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
 by (induct xs) (auto simp add: le_SucI)
 
@@ -1652,69 +1720,6 @@
 declare partition.simps[simp del]
 
 
-subsubsection \<open>\<^const>\<open>concat\<close>\<close>
-
-lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
-  by (induct xs) auto
-
-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
-
-lemma set_concat [simp]: "set (concat xs) = (\<Union>x\<in>set xs. set x)"
-  by (induct xs) auto
-
-lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
-  by (induct xs) auto
-
-lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
-  by (induct xs) auto
-
-lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
-  by (induct xs) auto
-
-lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
-  by (induct xs) auto
-
-lemma concat_eq_concat_iff: "\<forall>(x, y) \<in> set (zip xs ys). length x = length y \<Longrightarrow> length xs = length ys \<Longrightarrow> (concat xs = concat ys) = (xs = ys)"
-proof (induct xs arbitrary: ys)
-  case (Cons x xs ys)
-  thus ?case by (cases ys) auto
-qed (auto)
-
-lemma concat_injective: "concat xs = concat ys \<Longrightarrow> length xs = length ys \<Longrightarrow> \<forall>(x, y) \<in> set (zip xs ys). length x = length y \<Longrightarrow> xs = ys"
-  by (simp add: concat_eq_concat_iff)
-
-lemma concat_eq_appendD:
-  assumes "concat xss = ys @ zs" "xss \<noteq> []"
-  shows "\<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2"
-  using assms
-proof(induction xss arbitrary: ys)
-  case (Cons xs xss)
-  from Cons.prems consider
-    us where "xs @ us = ys" "concat xss = us @ zs" |
-    us where "xs = ys @ us" "us @ concat xss = zs"
-    by(auto simp add: append_eq_append_conv2)
-  then show ?case
-  proof cases
-    case 1
-    then show ?thesis using Cons.IH[OF 1(2)]
-      by(cases xss)(auto intro: exI[where x="[]"], metis append.assoc append_Cons concat.simps(2))
-  qed(auto intro: exI[where x="[]"])
-qed simp
-
-lemma concat_eq_append_conv:
-  "concat xss = ys @ zs \<longleftrightarrow>
-  (if xss = [] then ys = [] \<and> zs = []
-   else \<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2)"
-  by(auto dest: concat_eq_appendD)
-
-lemma hd_concat: "\<lbrakk>xs \<noteq> []; hd xs \<noteq> []\<rbrakk> \<Longrightarrow> hd (concat xs) = hd (hd xs)"
-  by (metis concat.simps(2) hd_Cons_tl hd_append2)
-
-
 subsubsection \<open>\<^const>\<open>nth\<close>\<close>
 
 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"