[isabelle-dev] extra lemmas

[Peter Gammie]

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/