changeset 74966 | 8a378e99d9a8 |
parent 74802 | b61bd2c12de3 |
child 75233 | 99b83e701c8e |
--- 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>