[isabelle-dev] extra lemmas

[Lawrence Paulson]

These look useful, thanks! I’ll take care of it.
Larry Paulson


> On 16 Nov 2015, at 16:26, Peter Gammie <peteg42 at 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev