These look useful, thanks! I’ll take care of it.
Larry Paulson
> On 16 Nov 2015, at 16:26, Peter Gammie <pete...@gmail.com> wrote:
>
> 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
