--- a/NEWS Thu Dec 08 15:21:18 2016 +0100
+++ b/NEWS Thu Dec 08 17:22:51 2016 +0100
@@ -11,7 +11,9 @@
with type class annotations. As a result, the tactic that derives
it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
-
+* The theorem in Permutations has been renamed:
+ bij_swap_ompose_bij ~> bij_swap_compose_bij
+
New in Isabelle2016-1 (December 2016)
-------------------------------------
--- a/src/HOL/Library/Permutations.thy Thu Dec 08 15:21:18 2016 +0100
+++ b/src/HOL/Library/Permutations.thy Thu Dec 08 17:22:51 2016 +0100
@@ -31,7 +31,7 @@
using surj_f_inv_f[OF bij_is_surj[OF bp]]
by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp])
-lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
+lemma bij_swap_compose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
proof -
assume H: "bij p"
show ?thesis
@@ -756,18 +756,10 @@
let ?q = "Fun.swap a (p a) id \<circ> ?r"
have raa: "?r a = a"
by (simp add: Fun.swap_def)
- from bij_swap_ompose_bij[OF insert(4)]
- have br: "bij ?r" .
-
+ from bij_swap_compose_bij[OF insert(4)] have br: "bij ?r" .
from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"
- apply (clarsimp simp add: Fun.swap_def)
- apply (erule_tac x="x" in allE)
- apply auto
- unfolding bij_iff
- apply metis
- done
- from insert(3)[OF br th]
- have rp: "permutation ?r" .
+ by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3))
+ from insert(3)[OF br th] have rp: "permutation ?r" .
have "permutation ?q"
by (simp add: permutation_compose permutation_swap_id rp)
then show ?case
@@ -926,7 +918,7 @@
using permutes_in_image[OF assms] by auto
have "count (mset (permute_list f xs)) y =
card ((\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs})"
- by (simp add: permute_list_def mset_map count_image_mset atLeast0LessThan)
+ by (simp add: permute_list_def count_image_mset atLeast0LessThan)
also have "(\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs} = f -` {i. i < length xs \<and> y = xs ! i}"
by auto
also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}"