911 "list_all2 P xs ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)" |
911 "list_all2 P xs ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)" |
912 by (induct xs ys rule: list_induct2') auto |
912 by (induct xs ys rule: list_induct2') auto |
913 |
913 |
914 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" |
914 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False" |
915 by (rule Eq_FalseI) auto |
915 by (rule Eq_FalseI) auto |
916 |
|
917 simproc_setup list_neq ("(xs::'a list) = ys") = \<open> |
|
918 (* |
|
919 Reduces xs=ys to False if xs and ys cannot be of the same length. |
|
920 This is the case if the atomic sublists of one are a submultiset |
|
921 of those of the other list and there are fewer Cons's in one than the other. |
|
922 *) |
|
923 |
|
924 let |
|
925 |
|
926 fun len (Const(\<^const_name>\<open>Nil\<close>,_)) acc = acc |
|
927 | len (Const(\<^const_name>\<open>Cons\<close>,_) $ _ $ xs) (ts,n) = len xs (ts,n+1) |
|
928 | len (Const(\<^const_name>\<open>append\<close>,_) $ xs $ ys) acc = len xs (len ys acc) |
|
929 | len (Const(\<^const_name>\<open>rev\<close>,_) $ xs) acc = len xs acc |
|
930 | len (Const(\<^const_name>\<open>map\<close>,_) $ _ $ xs) acc = len xs acc |
|
931 | len t (ts,n) = (t::ts,n); |
|
932 |
|
933 val ss = simpset_of \<^context>; |
|
934 |
|
935 fun list_neq ctxt ct = |
|
936 let |
|
937 val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct; |
|
938 val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0); |
|
939 fun prove_neq() = |
|
940 let |
|
941 val Type(_,listT::_) = eqT; |
|
942 val size = HOLogic.size_const listT; |
|
943 val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs); |
|
944 val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len); |
|
945 val thm = Goal.prove ctxt [] [] neq_len |
|
946 (K (simp_tac (put_simpset ss ctxt) 1)); |
|
947 in SOME (thm RS @{thm neq_if_length_neq}) end |
|
948 in |
|
949 if m < n andalso submultiset (op aconv) (ls,rs) orelse |
|
950 n < m andalso submultiset (op aconv) (rs,ls) |
|
951 then prove_neq() else NONE |
|
952 end; |
|
953 in K list_neq end |
|
954 \<close> |
|
955 |
916 |
956 |
917 |
957 subsubsection \<open>\<open>@\<close> -- append\<close> |
918 subsubsection \<open>\<open>@\<close> -- append\<close> |
958 |
919 |
959 global_interpretation append: monoid append Nil |
920 global_interpretation append: monoid append Nil |
1469 "\<lbrakk> x \<notin> set xs; x \<notin> set ys \<rbrakk> \<Longrightarrow> |
1430 "\<lbrakk> x \<notin> set xs; x \<notin> set ys \<rbrakk> \<Longrightarrow> |
1470 xs @ x # ys = xs' @ x # ys' \<longleftrightarrow> (xs = xs' \<and> ys = ys')" |
1431 xs @ x # ys = xs' @ x # ys' \<longleftrightarrow> (xs = xs' \<and> ys = ys')" |
1471 by(auto simp: append_eq_Cons_conv Cons_eq_append_conv append_eq_append_conv2) |
1432 by(auto simp: append_eq_Cons_conv Cons_eq_append_conv append_eq_append_conv2) |
1472 |
1433 |
1473 |
1434 |
|
1435 subsubsection \<open>\<^const>\<open>concat\<close>\<close> |
|
1436 |
|
1437 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" |
|
1438 by (induct xs) auto |
|
1439 |
|
1440 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])" |
|
1441 by (induct xss) auto |
|
1442 |
|
1443 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])" |
|
1444 by (induct xss) auto |
|
1445 |
|
1446 lemma set_concat [simp]: "set (concat xs) = (\<Union>x\<in>set xs. set x)" |
|
1447 by (induct xs) auto |
|
1448 |
|
1449 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" |
|
1450 by (induct xs) auto |
|
1451 |
|
1452 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" |
|
1453 by (induct xs) auto |
|
1454 |
|
1455 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" |
|
1456 by (induct xs) auto |
|
1457 |
|
1458 lemma length_concat_rev[simp]: "length (concat (rev xs)) = length (concat xs)" |
|
1459 by (induction xs) auto |
|
1460 |
|
1461 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)" |
|
1462 proof (induct xs arbitrary: ys) |
|
1463 case (Cons x xs ys) |
|
1464 thus ?case by (cases ys) auto |
|
1465 qed (auto) |
|
1466 |
|
1467 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" |
|
1468 by (simp add: concat_eq_concat_iff) |
|
1469 |
|
1470 lemma concat_eq_appendD: |
|
1471 assumes "concat xss = ys @ zs" "xss \<noteq> []" |
|
1472 shows "\<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2" |
|
1473 using assms |
|
1474 proof(induction xss arbitrary: ys) |
|
1475 case (Cons xs xss) |
|
1476 from Cons.prems consider |
|
1477 us where "xs @ us = ys" "concat xss = us @ zs" | |
|
1478 us where "xs = ys @ us" "us @ concat xss = zs" |
|
1479 by(auto simp add: append_eq_append_conv2) |
|
1480 then show ?case |
|
1481 proof cases |
|
1482 case 1 |
|
1483 then show ?thesis using Cons.IH[OF 1(2)] |
|
1484 by(cases xss)(auto intro: exI[where x="[]"], metis append.assoc append_Cons concat.simps(2)) |
|
1485 qed(auto intro: exI[where x="[]"]) |
|
1486 qed simp |
|
1487 |
|
1488 lemma concat_eq_append_conv: |
|
1489 "concat xss = ys @ zs \<longleftrightarrow> |
|
1490 (if xss = [] then ys = [] \<and> zs = [] |
|
1491 else \<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2)" |
|
1492 by(auto dest: concat_eq_appendD) |
|
1493 |
|
1494 lemma hd_concat: "\<lbrakk>xs \<noteq> []; hd xs \<noteq> []\<rbrakk> \<Longrightarrow> hd (concat xs) = hd (hd xs)" |
|
1495 by (metis concat.simps(2) hd_Cons_tl hd_append2) |
|
1496 |
|
1497 |
|
1498 simproc_setup list_neq ("(xs::'a list) = ys") = \<open> |
|
1499 (* |
|
1500 Reduces xs=ys to False if xs and ys cannot be of the same length. |
|
1501 This is the case if the atomic sublists of one are a submultiset |
|
1502 of those of the other list and there are fewer Cons's in one than the other. |
|
1503 *) |
|
1504 |
|
1505 let |
|
1506 |
|
1507 fun len (Const(\<^const_name>\<open>Nil\<close>,_)) acc = acc |
|
1508 | len (Const(\<^const_name>\<open>Cons\<close>,_) $ _ $ xs) (ts,n) = len xs (ts,n+1) |
|
1509 | len (Const(\<^const_name>\<open>append\<close>,_) $ xs $ ys) acc = len xs (len ys acc) |
|
1510 | len (Const(\<^const_name>\<open>rev\<close>,_) $ xs) acc = len xs acc |
|
1511 | len (Const(\<^const_name>\<open>map\<close>,_) $ _ $ xs) acc = len xs acc |
|
1512 | len (Const(\<^const_name>\<open>concat\<close>,T) $ (Const(\<^const_name>\<open>rev\<close>,_) $ xss)) acc |
|
1513 = len (Const(\<^const_name>\<open>concat\<close>,T) $ xss) acc |
|
1514 | len t (ts,n) = (t::ts,n); |
|
1515 |
|
1516 val ss = simpset_of \<^context>; |
|
1517 |
|
1518 fun list_neq ctxt ct = |
|
1519 let |
|
1520 val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct; |
|
1521 val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0); |
|
1522 fun prove_neq() = |
|
1523 let |
|
1524 val Type(_,listT::_) = eqT; |
|
1525 val size = HOLogic.size_const listT; |
|
1526 val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs); |
|
1527 val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len); |
|
1528 val thm = Goal.prove ctxt [] [] neq_len |
|
1529 (K (simp_tac (put_simpset ss ctxt) 1)); |
|
1530 in SOME (thm RS @{thm neq_if_length_neq}) end |
|
1531 in |
|
1532 if m < n andalso submultiset (op aconv) (ls,rs) orelse |
|
1533 n < m andalso submultiset (op aconv) (rs,ls) |
|
1534 then prove_neq() else NONE |
|
1535 end; |
|
1536 in K list_neq end |
|
1537 \<close> |
|
1538 |
1474 subsubsection \<open>\<^const>\<open>filter\<close>\<close> |
1539 subsubsection \<open>\<^const>\<open>filter\<close>\<close> |
1475 |
1540 |
1476 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" |
1541 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys" |
1477 by (induct xs) auto |
1542 by (induct xs) auto |
1478 |
1543 |
1479 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" |
1544 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)" |
1480 by (induct xs) simp_all |
1545 by (induct xs) simp_all |
1481 |
1546 |
1482 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs" |
1547 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs" |
|
1548 by (induct xs) auto |
|
1549 |
|
1550 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" |
1483 by (induct xs) auto |
1551 by (induct xs) auto |
1484 |
1552 |
1485 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs" |
1553 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs" |
1486 by (induct xs) (auto simp add: le_SucI) |
1554 by (induct xs) (auto simp add: le_SucI) |
1487 |
1555 |
1648 "partition f xs = (filter f xs,filter (Not \<circ> f) xs)" |
1716 "partition f xs = (filter f xs,filter (Not \<circ> f) xs)" |
1649 unfolding partition_filter2[symmetric] |
1717 unfolding partition_filter2[symmetric] |
1650 unfolding partition_filter1[symmetric] by simp |
1718 unfolding partition_filter1[symmetric] by simp |
1651 |
1719 |
1652 declare partition.simps[simp del] |
1720 declare partition.simps[simp del] |
1653 |
|
1654 |
|
1655 subsubsection \<open>\<^const>\<open>concat\<close>\<close> |
|
1656 |
|
1657 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys" |
|
1658 by (induct xs) auto |
|
1659 |
|
1660 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])" |
|
1661 by (induct xss) auto |
|
1662 |
|
1663 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])" |
|
1664 by (induct xss) auto |
|
1665 |
|
1666 lemma set_concat [simp]: "set (concat xs) = (\<Union>x\<in>set xs. set x)" |
|
1667 by (induct xs) auto |
|
1668 |
|
1669 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs" |
|
1670 by (induct xs) auto |
|
1671 |
|
1672 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" |
|
1673 by (induct xs) auto |
|
1674 |
|
1675 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" |
|
1676 by (induct xs) auto |
|
1677 |
|
1678 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))" |
|
1679 by (induct xs) auto |
|
1680 |
|
1681 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)" |
|
1682 proof (induct xs arbitrary: ys) |
|
1683 case (Cons x xs ys) |
|
1684 thus ?case by (cases ys) auto |
|
1685 qed (auto) |
|
1686 |
|
1687 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" |
|
1688 by (simp add: concat_eq_concat_iff) |
|
1689 |
|
1690 lemma concat_eq_appendD: |
|
1691 assumes "concat xss = ys @ zs" "xss \<noteq> []" |
|
1692 shows "\<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2" |
|
1693 using assms |
|
1694 proof(induction xss arbitrary: ys) |
|
1695 case (Cons xs xss) |
|
1696 from Cons.prems consider |
|
1697 us where "xs @ us = ys" "concat xss = us @ zs" | |
|
1698 us where "xs = ys @ us" "us @ concat xss = zs" |
|
1699 by(auto simp add: append_eq_append_conv2) |
|
1700 then show ?case |
|
1701 proof cases |
|
1702 case 1 |
|
1703 then show ?thesis using Cons.IH[OF 1(2)] |
|
1704 by(cases xss)(auto intro: exI[where x="[]"], metis append.assoc append_Cons concat.simps(2)) |
|
1705 qed(auto intro: exI[where x="[]"]) |
|
1706 qed simp |
|
1707 |
|
1708 lemma concat_eq_append_conv: |
|
1709 "concat xss = ys @ zs \<longleftrightarrow> |
|
1710 (if xss = [] then ys = [] \<and> zs = [] |
|
1711 else \<exists>xss1 xs xs' xss2. xss = xss1 @ (xs @ xs') # xss2 \<and> ys = concat xss1 @ xs \<and> zs = xs' @ concat xss2)" |
|
1712 by(auto dest: concat_eq_appendD) |
|
1713 |
|
1714 lemma hd_concat: "\<lbrakk>xs \<noteq> []; hd xs \<noteq> []\<rbrakk> \<Longrightarrow> hd (concat xs) = hd (hd xs)" |
|
1715 by (metis concat.simps(2) hd_Cons_tl hd_append2) |
|
1716 |
1721 |
1717 |
1722 |
1718 subsubsection \<open>\<^const>\<open>nth\<close>\<close> |
1723 subsubsection \<open>\<^const>\<open>nth\<close>\<close> |
1719 |
1724 |
1720 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x" |
1725 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x" |