author | nipkow |
Wed, 29 Dec 2021 08:07:51 +0100 | |
changeset 74966 | 8a378e99d9a8 |
parent 74965 | 9469d9223689 |
child 74968 | 507203e30db4 |
src/HOL/List.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/List.thy Sun Dec 26 11:01:27 2021 +0000 +++ b/src/HOL/List.thy Wed Dec 29 08:07:51 2021 +0100 @@ -1244,6 +1244,9 @@ lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])" by(rule rev_cases[of xs]) auto +lemma length_Suc_conv_rev: "(length xs = Suc n) = (\<exists>y ys. xs = ys @ [y] \<and> length ys = n)" +by (induct xs rule: rev_induct) auto + subsubsection \<open>\<^const>\<open>set\<close>\<close>