Email Gateway (Oct 13 2022 at 20:30): Email Gateway (Oct 13 2022 at 20:30):From: Jeremy Sylvestre <jsylvest@ualberta.ca>
A few more --- wondering if any of the below is of interest for
src/HOL/List.thy.
Cheers,
Jeremy S
lemma inj_rotate1: "inj rotate1"
proof
fix xs ys :: "'a list" show "rotate1 xs = rotate1 ys ⟹ xs = ys"
by (cases xs, cases ys, simp_all, cases ys, simp_all)
qed
lemma surj_rotate1: "surj rotate1"
proof (safe, simp_all)
fix xs :: "'a list" show "xs ∈ range rotate1"
proof (cases xs rule: rev_exhaust)
case Nil
hence "xs = rotate1 []" by auto
thus ?thesis by fast
next
case (snoc as a)
hence "xs = rotate1 (a#as)" by force
thus ?thesis by fast
qed
qed
lemma bij_rotate1: "bij (rotate1 :: 'a list ⇒ 'a list)"
using bijI inj_rotate1 surj_rotate1 by blast
lemma the_inv_rotate1_simps:
"the_inv rotate1 [] = []"
"the_inv rotate1 (xs@[x]) = x#xs"
using inj_rotate1 the_inv_f_f[of rotate1 "[]"] the_inv_f_f[of rotate1
"x#xs"] by auto
lemma rotate1_replicate: "rotate1 (replicate n a) = replicate n a"
by (cases n, simp_all add: replicate_append_same)
lemma rotate1_fixed_pt:
assumes "rotate1 xs = xs"
obtains x where "xs = replicate (length xs) x"
proof (cases xs, simp)
case (Cons a as)
have nth_as: "\<forall>i<length as. as!i = a"
proof clarify
fix i from assms Cons show "i < length as \<Longrightarrow> as!i = a"
using nth_append[of as "[a]" 0] nth_append[of as "[a]" "Suc _"] by
(induct i) auto
qed
have "xs = replicate (length xs) a"
proof (intro nth_equalityI, simp)
fix i from Cons show "i < length xs ⟹ xs!i = replicate (length xs) a !
i"
using nth_as by (cases i) auto
qed
with that show thesis by force
qed
Email Gateway (Oct 13 2022 at 20:36):From: Jeremy Sylvestre <jsylvest@ualberta.ca>
Hit send too soon, here's a shorter proof for that last one
lemma rotate1_fixed_pts:
assumes "rotate1 xs = xs"
obtains x where "xs = replicate (length xs) x"
proof (cases xs, simp)
case (Cons a as)
moreover have "as = replicate (length as) a"
proof (intro nth_equalityI, simp_all)
fix i from assms Cons show "i < length as \<Longrightarrow> as!i = a"
using nth_append[of as "[a]" 0] nth_append[of as "[a]" "Suc _"] by
(induct i) auto
qed
ultimately show thesis using that by simp
qed
Email Gateway (Oct 14 2022 at 16:09):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks Jeremy, I have added all except for the the_inv ones (for no strong
reason) and rotate1_fixed_pt. The latter follows from what I feel is a (new)
more basic lemma
lemma rotate1_fixpoint_card: "rotate1 xs = xs ⟹ xs = [] ∨ card(set xs) = 1"
together with the new
lemma card_set_1_iff_replicate:
"card(set xs) = Suc 0 ⟷ xs ≠ [] ∧ (∃x. xs = replicate (length xs) x)"
like this:
lemma rotate1_fixpoint_replicate:
assumes "rotate1 xs = xs"
obtains x where "xs = replicate (length xs) x"
using rotate1_fixpoint_card[OF assms]
by (auto simp add: card_set_1_iff_replicate)
which I have not included - it is always difficult to draw the line ...
https://isabelle.in.tum.de/repos/isabelle/rev/642f1a36e1d6
Thanks again
Tobias
smime.p7s
Last updated: Apr 16 2024 at 04:18 UTC