remove typo in bij_swap_compose_bij theorem name; tune proof
authorbulwahn
Thu Dec 08 17:22:51 2016 +0100 (2016-12-08)
changeset 645436b13586ef1a2
parent 64542 c7d76708379f
child 64544 d23b7c9b9dd4
remove typo in bij_swap_compose_bij theorem name; tune proof
NEWS
src/HOL/Library/Permutations.thy
     1.1 --- a/NEWS	Thu Dec 08 15:21:18 2016 +0100
     1.2 +++ b/NEWS	Thu Dec 08 17:22:51 2016 +0100
     1.3 @@ -11,7 +11,9 @@
     1.4      with type class annotations. As a result, the tactic that derives
     1.5      it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
     1.6  
     1.7 -
     1.8 +* The theorem in Permutations has been renamed:
     1.9 +  bij_swap_ompose_bij ~> bij_swap_compose_bij
    1.10 + 
    1.11  
    1.12  New in Isabelle2016-1 (December 2016)
    1.13  -------------------------------------
     2.1 --- a/src/HOL/Library/Permutations.thy	Thu Dec 08 15:21:18 2016 +0100
     2.2 +++ b/src/HOL/Library/Permutations.thy	Thu Dec 08 17:22:51 2016 +0100
     2.3 @@ -31,7 +31,7 @@
     2.4    using surj_f_inv_f[OF bij_is_surj[OF bp]]
     2.5    by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp])
     2.6  
     2.7 -lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
     2.8 +lemma bij_swap_compose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
     2.9  proof -
    2.10    assume H: "bij p"
    2.11    show ?thesis
    2.12 @@ -756,18 +756,10 @@
    2.13    let ?q = "Fun.swap a (p a) id \<circ> ?r"
    2.14    have raa: "?r a = a"
    2.15      by (simp add: Fun.swap_def)
    2.16 -  from bij_swap_ompose_bij[OF insert(4)]
    2.17 -  have br: "bij ?r"  .
    2.18 -
    2.19 +  from bij_swap_compose_bij[OF insert(4)] have br: "bij ?r"  .
    2.20    from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x"
    2.21 -    apply (clarsimp simp add: Fun.swap_def)
    2.22 -    apply (erule_tac x="x" in allE)
    2.23 -    apply auto
    2.24 -    unfolding bij_iff
    2.25 -    apply metis
    2.26 -    done
    2.27 -  from insert(3)[OF br th]
    2.28 -  have rp: "permutation ?r" .
    2.29 +    by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3))    
    2.30 +  from insert(3)[OF br th] have rp: "permutation ?r" .
    2.31    have "permutation ?q"
    2.32      by (simp add: permutation_compose permutation_swap_id rp)
    2.33    then show ?case
    2.34 @@ -926,7 +918,7 @@
    2.35      using permutes_in_image[OF assms] by auto
    2.36    have "count (mset (permute_list f xs)) y =
    2.37            card ((\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs})"
    2.38 -    by (simp add: permute_list_def mset_map count_image_mset atLeast0LessThan)
    2.39 +    by (simp add: permute_list_def count_image_mset atLeast0LessThan)
    2.40    also have "(\<lambda>i. xs ! f i) -` {y} \<inter> {..<length xs} = f -` {i. i < length xs \<and> y = xs ! i}"
    2.41      by auto
    2.42    also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}"