src/HOL/Library/Permutations.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 41959 b460124855b8
     1.1 --- a/src/HOL/Library/Permutations.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Permutations.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
     1.7 -  by (auto simp add: ext_iff swap_def fun_upd_def)
     1.8 +  by (auto simp add: fun_eq_iff swap_def fun_upd_def)
     1.9  lemma swap_id_refl: "Fun.swap a a id = id" by simp
    1.10  lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
    1.11    by (rule ext, simp add: swap_def)
    1.12 @@ -25,7 +25,7 @@
    1.13  
    1.14  lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id"
    1.15    shows "inv f = g"
    1.16 -  using fg gf inv_equality[of g f] by (auto simp add: ext_iff)
    1.17 +  using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
    1.18  
    1.19  lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
    1.20    by (rule inv_unique_comp, simp_all)
    1.21 @@ -44,7 +44,7 @@
    1.22    using pS
    1.23    unfolding permutes_def
    1.24    apply -
    1.25 -  apply (rule set_ext)
    1.26 +  apply (rule set_eqI)
    1.27    apply (simp add: image_iff)
    1.28    apply metis
    1.29    done
    1.30 @@ -67,16 +67,16 @@
    1.31    assumes pS: "p permutes S"
    1.32    shows "p (inv p x) = x"
    1.33    and "inv p (p x) = x"
    1.34 -  using permutes_inv_o[OF pS, unfolded ext_iff o_def] by auto
    1.35 +  using permutes_inv_o[OF pS, unfolded fun_eq_iff o_def] by auto
    1.36  
    1.37  lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T ==> p permutes T"
    1.38    unfolding permutes_def by blast
    1.39  
    1.40  lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id"
    1.41 -  unfolding ext_iff permutes_def apply simp by metis
    1.42 +  unfolding fun_eq_iff permutes_def apply simp by metis
    1.43  
    1.44  lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id"
    1.45 -  unfolding ext_iff permutes_def apply simp by metis
    1.46 +  unfolding fun_eq_iff permutes_def apply simp by metis
    1.47  
    1.48  lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
    1.49    unfolding permutes_def by simp
    1.50 @@ -111,7 +111,7 @@
    1.51    using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis
    1.52  
    1.53  lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p"
    1.54 -  unfolding ext_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
    1.55 +  unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
    1.56    by blast
    1.57  
    1.58  (* ------------------------------------------------------------------------- *)
    1.59 @@ -136,7 +136,7 @@
    1.60      {assume pS: "p permutes insert a S"
    1.61        let ?b = "p a"
    1.62        let ?q = "Fun.swap a (p a) id o p"
    1.63 -      have th0: "p = Fun.swap a ?b id o ?q" unfolding ext_iff o_assoc by simp
    1.64 +      have th0: "p = Fun.swap a ?b id o ?q" unfolding fun_eq_iff o_assoc by simp
    1.65        have th1: "?b \<in> insert a S " unfolding permutes_in_image[OF pS] by simp
    1.66        from permutes_insert_lemma[OF pS] th0 th1
    1.67        have "\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S" by blast}
    1.68 @@ -180,11 +180,11 @@
    1.69            and eq: "?g (b,p) = ?g (c,q)"
    1.70          from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
    1.71          from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x" unfolding permutes_def
    1.72 -          by (auto simp add: swap_def fun_upd_def ext_iff)
    1.73 +          by (auto simp add: swap_def fun_upd_def fun_eq_iff)
    1.74          also have "\<dots> = ?g (c,q) x" using ths(5) `x \<notin> F` eq
    1.75 -          by (auto simp add: swap_def fun_upd_def ext_iff)
    1.76 +          by (auto simp add: swap_def fun_upd_def fun_eq_iff)
    1.77          also have "\<dots> = c"using ths(5) `x \<notin> F` unfolding permutes_def
    1.78 -          by (auto simp add: swap_def fun_upd_def ext_iff)
    1.79 +          by (auto simp add: swap_def fun_upd_def fun_eq_iff)
    1.80          finally have bc: "b = c" .
    1.81          hence "Fun.swap x b id = Fun.swap x c id" by simp
    1.82          with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
    1.83 @@ -251,12 +251,12 @@
    1.84  (* Various combinations of transpositions with 2, 1 and 0 common elements.   *)
    1.85  (* ------------------------------------------------------------------------- *)
    1.86  
    1.87 -lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>  Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: ext_iff swap_def)
    1.88 +lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>  Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
    1.89  
    1.90 -lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: ext_iff swap_def)
    1.91 +lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
    1.92  
    1.93  lemma swap_id_independent: "~(a = c) \<Longrightarrow> ~(a = d) \<Longrightarrow> ~(b = c) \<Longrightarrow> ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id"
    1.94 -  by (simp add: swap_def ext_iff)
    1.95 +  by (simp add: swap_def fun_eq_iff)
    1.96  
    1.97  (* ------------------------------------------------------------------------- *)
    1.98  (* Permutations as transposition sequences.                                  *)
    1.99 @@ -352,18 +352,18 @@
   1.100    apply (rule_tac x="b" in exI)
   1.101    apply (rule_tac x="d" in exI)
   1.102    apply (rule_tac x="b" in exI)
   1.103 -  apply (clarsimp simp add: ext_iff swap_def)
   1.104 +  apply (clarsimp simp add: fun_eq_iff swap_def)
   1.105    apply (case_tac "a \<noteq> c \<and> b = d")
   1.106    apply (rule disjI2)
   1.107    apply (rule_tac x="c" in exI)
   1.108    apply (rule_tac x="d" in exI)
   1.109    apply (rule_tac x="c" in exI)
   1.110 -  apply (clarsimp simp add: ext_iff swap_def)
   1.111 +  apply (clarsimp simp add: fun_eq_iff swap_def)
   1.112    apply (rule disjI2)
   1.113    apply (rule_tac x="c" in exI)
   1.114    apply (rule_tac x="d" in exI)
   1.115    apply (rule_tac x="b" in exI)
   1.116 -  apply (clarsimp simp add: ext_iff swap_def)
   1.117 +  apply (clarsimp simp add: fun_eq_iff swap_def)
   1.118    done
   1.119  with H show ?thesis by metis
   1.120  qed
   1.121 @@ -518,7 +518,7 @@
   1.122    from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
   1.123    from swapidseq_inverse_exists[OF n] obtain q where
   1.124      q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
   1.125 -  thus ?thesis unfolding bij_iff  apply (auto simp add: ext_iff) apply metis done
   1.126 +  thus ?thesis unfolding bij_iff  apply (auto simp add: fun_eq_iff) apply metis done
   1.127  qed
   1.128  
   1.129  lemma permutation_finite_support: assumes p: "permutation p"
   1.130 @@ -544,7 +544,7 @@
   1.131  lemma bij_swap_comp:
   1.132    assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p"
   1.133    using surj_f_inv_f[OF bij_is_surj[OF bp]]
   1.134 -  by (simp add: ext_iff swap_def bij_inv_eq_iff[OF bp])
   1.135 +  by (simp add: fun_eq_iff swap_def bij_inv_eq_iff[OF bp])
   1.136  
   1.137  lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id o p)"
   1.138  proof-
   1.139 @@ -688,7 +688,7 @@
   1.140          ultimately have "p n = n" by blast }
   1.141        ultimately show "p n = n"  by blast
   1.142      qed}
   1.143 -  thus ?thesis by (auto simp add: ext_iff)
   1.144 +  thus ?thesis by (auto simp add: fun_eq_iff)
   1.145  qed
   1.146  
   1.147  lemma permutes_natset_ge:
   1.148 @@ -709,7 +709,7 @@
   1.149  qed
   1.150  
   1.151  lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
   1.152 -apply (rule set_ext)
   1.153 +apply (rule set_eqI)
   1.154  apply auto
   1.155    using permutes_inv_inv permutes_inv apply auto
   1.156    apply (rule_tac x="inv x" in exI)
   1.157 @@ -718,7 +718,7 @@
   1.158  
   1.159  lemma image_compose_permutations_left:
   1.160    assumes q: "q permutes S" shows "{q o p | p. p permutes S} = {p . p permutes S}"
   1.161 -apply (rule set_ext)
   1.162 +apply (rule set_eqI)
   1.163  apply auto
   1.164  apply (rule permutes_compose)
   1.165  using q apply auto
   1.166 @@ -728,7 +728,7 @@
   1.167  lemma image_compose_permutations_right:
   1.168    assumes q: "q permutes S"
   1.169    shows "{p o q | p. p permutes S} = {p . p permutes S}"
   1.170 -apply (rule set_ext)
   1.171 +apply (rule set_eqI)
   1.172  apply auto
   1.173  apply (rule permutes_compose)
   1.174  using q apply auto
   1.175 @@ -811,7 +811,7 @@
   1.176    shows "setsum f {p. p permutes (insert a S)} = setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)"
   1.177  proof-
   1.178    have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id o p)) = f o (\<lambda>(b,p). Fun.swap a b id o p)"
   1.179 -    by (simp add: ext_iff)
   1.180 +    by (simp add: fun_eq_iff)
   1.181    have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}" by blast
   1.182    have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast
   1.183    show ?thesis