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/
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
