# [isabelle-dev] extra lemmas

Peter Gammie peteg42 at gmail.com
Mon Nov 16 17:26:23 CET 2015

```Can someone add these in at the obvious places?

thanks,
peter

lemma LeastI2_wellorder_ex:
assumes "\<exists>x::'a::wellorder. P x"
and "\<And>a. \<lbrakk> P a; \<forall>b. P b \<longrightarrow> a \<le> b \<rbrakk> \<Longrightarrow> Q a"
shows "Q (Least P)"
using assms by clarify (blast intro!: LeastI2_wellorder)

lemma fcomp_comp: "fcomp f g = comp g f" by (simp add: ext)

lemma drop_rev:
"drop n (rev xs) = rev (take (length xs - n) xs)"
by (cases "length xs < n") (auto simp: rev_take)

lemma take_rev:
"take n (rev xs) = rev (drop (length xs - n) xs)"
by (cases “length xs < n") (auto simp: rev_drop)

HOL/Library/Permutation:

lemma perm_finite[simp, intro!]:
"finite {B. B <~~> A}"
proof(rule finite_subset[where B="{xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"])
show "finite {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"
apply (cases A, simp)
apply (rule card_ge_0_finite)
apply (auto simp: card_lists_length_le)
done
next
show "{B. B <~~> A} \<subseteq> {xs. set xs \<subseteq> set A \<and> length xs \<le> length A}"
by (clarsimp simp add: perm_length perm_set_eq)
qed

lemma perm_swap:
assumes "i < length xs"
assumes "j < length xs"
shows "xs[i := xs ! j, j := xs ! i] <~~> xs"
using assms by (simp add: mset_eq_perm[symmetric] mset_swap)

--
http://peteg.org/

```