src/HOL/Library/Permutation.thy
changeset 53238 01ef0a103fc9
parent 51542 738598beeb26
child 55584 a879f14b6f95
equal deleted inserted replaced
53237:6bfe54791591 53238:01ef0a103fc9
     6 
     6 
     7 theory Permutation
     7 theory Permutation
     8 imports Multiset
     8 imports Multiset
     9 begin
     9 begin
    10 
    10 
    11 inductive
    11 inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  ("_ <~~> _"  [50, 50] 50)  (* FIXME proper infix, without ambiguity!? *)
    12   perm :: "'a list => 'a list => bool"  ("_ <~~> _"  [50, 50] 50)
    12 where
    13   where
    13   Nil [intro!]: "[] <~~> []"
    14     Nil  [intro!]: "[] <~~> []"
    14 | swap [intro!]: "y # x # l <~~> x # y # l"
    15   | swap [intro!]: "y # x # l <~~> x # y # l"
    15 | Cons [intro!]: "xs <~~> ys \<Longrightarrow> z # xs <~~> z # ys"
    16   | Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
    16 | trans [intro]: "xs <~~> ys \<Longrightarrow> ys <~~> zs \<Longrightarrow> xs <~~> zs"
    17   | trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
       
    18 
    17 
    19 lemma perm_refl [iff]: "l <~~> l"
    18 lemma perm_refl [iff]: "l <~~> l"
    20   by (induct l) auto
    19   by (induct l) auto
    21 
    20 
    22 
    21 
    23 subsection {* Some examples of rule induction on permutations *}
    22 subsection {* Some examples of rule induction on permutations *}
    24 
    23 
    25 lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
    24 lemma xperm_empty_imp: "[] <~~> ys \<Longrightarrow> ys = []"
    26   by (induct xs == "[]::'a list" ys pred: perm) simp_all
    25   by (induct xs == "[]::'a list" ys pred: perm) simp_all
    27 
    26 
    28 
    27 
    29 text {*
    28 text {*
    30   \medskip This more general theorem is easier to understand!
    29   \medskip This more general theorem is easier to understand!
    31   *}
    30   *}
    32 
    31 
    33 lemma perm_length: "xs <~~> ys ==> length xs = length ys"
    32 lemma perm_length: "xs <~~> ys \<Longrightarrow> length xs = length ys"
    34   by (induct pred: perm) simp_all
    33   by (induct pred: perm) simp_all
    35 
    34 
    36 lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
    35 lemma perm_empty_imp: "[] <~~> xs \<Longrightarrow> xs = []"
    37   by (drule perm_length) auto
    36   by (drule perm_length) auto
    38 
    37 
    39 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
    38 lemma perm_sym: "xs <~~> ys \<Longrightarrow> ys <~~> xs"
    40   by (induct pred: perm) auto
    39   by (induct pred: perm) auto
    41 
    40 
    42 
    41 
    43 subsection {* Ways of making new permutations *}
    42 subsection {* Ways of making new permutations *}
    44 
    43 
    62   apply (induct xs)
    61   apply (induct xs)
    63    apply simp_all
    62    apply simp_all
    64   apply (blast intro!: perm_append_single intro: perm_sym)
    63   apply (blast intro!: perm_append_single intro: perm_sym)
    65   done
    64   done
    66 
    65 
    67 lemma perm_append1: "xs <~~> ys ==> l @ xs <~~> l @ ys"
    66 lemma perm_append1: "xs <~~> ys \<Longrightarrow> l @ xs <~~> l @ ys"
    68   by (induct l) auto
    67   by (induct l) auto
    69 
    68 
    70 lemma perm_append2: "xs <~~> ys ==> xs @ l <~~> ys @ l"
    69 lemma perm_append2: "xs <~~> ys \<Longrightarrow> xs @ l <~~> ys @ l"
    71   by (blast intro!: perm_append_swap perm_append1)
    70   by (blast intro!: perm_append_swap perm_append1)
    72 
    71 
    73 
    72 
    74 subsection {* Further results *}
    73 subsection {* Further results *}
    75 
    74 
    79 lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
    78 lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
    80   apply auto
    79   apply auto
    81   apply (erule perm_sym [THEN perm_empty_imp])
    80   apply (erule perm_sym [THEN perm_empty_imp])
    82   done
    81   done
    83 
    82 
    84 lemma perm_sing_imp: "ys <~~> xs ==> xs = [y] ==> ys = [y]"
    83 lemma perm_sing_imp: "ys <~~> xs \<Longrightarrow> xs = [y] \<Longrightarrow> ys = [y]"
    85   by (induct pred: perm) auto
    84   by (induct pred: perm) auto
    86 
    85 
    87 lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
    86 lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
    88   by (blast intro: perm_sing_imp)
    87   by (blast intro: perm_sing_imp)
    89 
    88 
    91   by (blast dest: perm_sym)
    90   by (blast dest: perm_sym)
    92 
    91 
    93 
    92 
    94 subsection {* Removing elements *}
    93 subsection {* Removing elements *}
    95 
    94 
    96 lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove1 x ys"
    95 lemma perm_remove: "x \<in> set ys \<Longrightarrow> ys <~~> x # remove1 x ys"
    97   by (induct ys) auto
    96   by (induct ys) auto
    98 
    97 
    99 
    98 
   100 text {* \medskip Congruence rule *}
    99 text {* \medskip Congruence rule *}
   101 
   100 
   102 lemma perm_remove_perm: "xs <~~> ys ==> remove1 z xs <~~> remove1 z ys"
   101 lemma perm_remove_perm: "xs <~~> ys \<Longrightarrow> remove1 z xs <~~> remove1 z ys"
   103   by (induct pred: perm) auto
   102   by (induct pred: perm) auto
   104 
   103 
   105 lemma remove_hd [simp]: "remove1 z (z # xs) = xs"
   104 lemma remove_hd [simp]: "remove1 z (z # xs) = xs"
   106   by auto
   105   by auto
   107 
   106 
   108 lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
   107 lemma cons_perm_imp_perm: "z # xs <~~> z # ys \<Longrightarrow> xs <~~> ys"
   109   by (drule_tac z = z in perm_remove_perm) auto
   108   by (drule_tac z = z in perm_remove_perm) auto
   110 
   109 
   111 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
   110 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
   112   by (blast intro: cons_perm_imp_perm)
   111   by (blast intro: cons_perm_imp_perm)
   113 
   112 
   114 lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys ==> xs <~~> ys"
   113 lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys \<Longrightarrow> xs <~~> ys"
   115   apply (induct zs arbitrary: xs ys rule: rev_induct)
   114   by (induct zs arbitrary: xs ys rule: rev_induct) auto
   116    apply (simp_all (no_asm_use))
       
   117   apply blast
       
   118   done
       
   119 
   115 
   120 lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
   116 lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
   121   by (blast intro: append_perm_imp_perm perm_append1)
   117   by (blast intro: append_perm_imp_perm perm_append1)
   122 
   118 
   123 lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)"
   119 lemma perm_append2_eq [iff]: "(xs @ zs <~~> ys @ zs) = (xs <~~> ys)"
   133   apply (erule_tac [2] perm.induct, simp_all add: union_ac)
   129   apply (erule_tac [2] perm.induct, simp_all add: union_ac)
   134   apply (erule rev_mp, rule_tac x=ys in spec)
   130   apply (erule rev_mp, rule_tac x=ys in spec)
   135   apply (induct_tac xs, auto)
   131   apply (induct_tac xs, auto)
   136   apply (erule_tac x = "remove1 a x" in allE, drule sym, simp)
   132   apply (erule_tac x = "remove1 a x" in allE, drule sym, simp)
   137   apply (subgoal_tac "a \<in> set x")
   133   apply (subgoal_tac "a \<in> set x")
   138   apply (drule_tac z=a in perm.Cons)
   134   apply (drule_tac z = a in perm.Cons)
   139   apply (erule perm.trans, rule perm_sym, erule perm_remove)
   135   apply (erule perm.trans, rule perm_sym, erule perm_remove)
   140   apply (drule_tac f=set_of in arg_cong, simp)
   136   apply (drule_tac f=set_of in arg_cong, simp)
   141   done
   137   done
   142 
   138 
   143 lemma multiset_of_le_perm_append:
   139 lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
   144     "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
       
   145   apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   140   apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   146   apply (insert surj_multiset_of, drule surjD)
   141   apply (insert surj_multiset_of, drule surjD)
   147   apply (blast intro: sym)+
   142   apply (blast intro: sym)+
   148   done
   143   done
   149 
   144 
   150 lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
   145 lemma perm_set_eq: "xs <~~> ys \<Longrightarrow> set xs = set ys"
   151   by (metis multiset_of_eq_perm multiset_of_eq_setD)
   146   by (metis multiset_of_eq_perm multiset_of_eq_setD)
   152 
   147 
   153 lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
   148 lemma perm_distinct_iff: "xs <~~> ys \<Longrightarrow> distinct xs = distinct ys"
   154   apply (induct pred: perm)
   149   apply (induct pred: perm)
   155      apply simp_all
   150      apply simp_all
   156    apply fastforce
   151    apply fastforce
   157   apply (metis perm_set_eq)
   152   apply (metis perm_set_eq)
   158   done
   153   done
   159 
   154 
   160 lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
   155 lemma eq_set_perm_remdups: "set xs = set ys \<Longrightarrow> remdups xs <~~> remdups ys"
   161   apply (induct xs arbitrary: ys rule: length_induct)
   156   apply (induct xs arbitrary: ys rule: length_induct)
   162   apply (case_tac "remdups xs", simp, simp)
   157   apply (case_tac "remdups xs")
   163   apply (subgoal_tac "a : set (remdups ys)")
   158    apply simp_all
       
   159   apply (subgoal_tac "a \<in> set (remdups ys)")
   164    prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
   160    prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
   165   apply (drule split_list) apply(elim exE conjE)
   161   apply (drule split_list) apply(elim exE conjE)
   166   apply (drule_tac x=list in spec) apply(erule impE) prefer 2
   162   apply (drule_tac x=list in spec) apply(erule impE) prefer 2
   167    apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
   163    apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
   168     apply simp
   164     apply simp
   169     apply (subgoal_tac "a#list <~~> a#ysa@zs")
   165     apply (subgoal_tac "a # list <~~> a # ysa @ zs")
   170      apply (metis Cons_eq_appendI perm_append_Cons trans)
   166      apply (metis Cons_eq_appendI perm_append_Cons trans)
   171     apply (metis Cons Cons_eq_appendI distinct.simps(2)
   167     apply (metis Cons Cons_eq_appendI distinct.simps(2)
   172       distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
   168       distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
   173    apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
   169    apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
   174     apply (fastforce simp add: insert_ident)
   170     apply (fastforce simp add: insert_ident)
   178    apply (subgoal_tac "length (remdups xs) \<le> length xs")
   174    apply (subgoal_tac "length (remdups xs) \<le> length xs")
   179    apply simp
   175    apply simp
   180    apply (rule length_remdups_leq)
   176    apply (rule length_remdups_leq)
   181   done
   177   done
   182 
   178 
   183 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
   179 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y \<longleftrightarrow> (set x = set y)"
   184   by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
   180   by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
   185 
   181 
   186 lemma permutation_Ex_bij:
   182 lemma permutation_Ex_bij:
   187   assumes "xs <~~> ys"
   183   assumes "xs <~~> ys"
   188   shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
   184   shows "\<exists>f. bij_betw f {..<length xs} {..<length ys} \<and> (\<forall>i<length xs. xs ! i = ys ! (f i))"
   189 using assms proof induct
   185 using assms proof induct
   190   case Nil then show ?case unfolding bij_betw_def by simp
   186   case Nil
       
   187   then show ?case unfolding bij_betw_def by simp
   191 next
   188 next
   192   case (swap y x l)
   189   case (swap y x l)
   193   show ?case
   190   show ?case
   194   proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
   191   proof (intro exI[of _ "Fun.swap 0 1 id"] conjI allI impI)
   195     show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
   192     show "bij_betw (Fun.swap 0 1 id) {..<length (y # x # l)} {..<length (x # y # l)}"
   196       by (auto simp: bij_betw_def)
   193       by (auto simp: bij_betw_def)
   197     fix i assume "i < length(y#x#l)"
   194     fix i
       
   195     assume "i < length(y#x#l)"
   198     show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
   196     show "(y # x # l) ! i = (x # y # l) ! (Fun.swap 0 1 id) i"
   199       by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
   197       by (cases i) (auto simp: Fun.swap_def gr0_conv_Suc)
   200   qed
   198   qed
   201 next
   199 next
   202   case (Cons xs ys z)
   200   case (Cons xs ys z)
   203   then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
   201   then obtain f where bij: "bij_betw f {..<length xs} {..<length ys}" and
   204     perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
   202     perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" by blast
   205   let "?f i" = "case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
   203   let ?f = "\<lambda>i. case i of Suc n \<Rightarrow> Suc (f n) | 0 \<Rightarrow> 0"
   206   show ?case
   204   show ?case
   207   proof (intro exI[of _ ?f] allI conjI impI)
   205   proof (intro exI[of _ ?f] allI conjI impI)
   208     have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
   206     have *: "{..<length (z#xs)} = {0} \<union> Suc ` {..<length xs}"
   209             "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
   207             "{..<length (z#ys)} = {0} \<union> Suc ` {..<length ys}"
   210       by (simp_all add: lessThan_Suc_eq_insert_0)
   208       by (simp_all add: lessThan_Suc_eq_insert_0)
   211     show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}" unfolding *
   209     show "bij_betw ?f {..<length (z#xs)} {..<length (z#ys)}"
       
   210       unfolding *
   212     proof (rule bij_betw_combine)
   211     proof (rule bij_betw_combine)
   213       show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
   212       show "bij_betw ?f (Suc ` {..<length xs}) (Suc ` {..<length ys})"
   214         using bij unfolding bij_betw_def
   213         using bij unfolding bij_betw_def
   215         by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
   214         by (auto intro!: inj_onI imageI dest: inj_onD simp: image_compose[symmetric] comp_def)
   216     qed (auto simp: bij_betw_def)
   215     qed (auto simp: bij_betw_def)
   217     fix i assume "i < length (z#xs)"
   216     fix i
       
   217     assume "i < length (z#xs)"
   218     then show "(z # xs) ! i = (z # ys) ! (?f i)"
   218     then show "(z # xs) ! i = (z # ys) ! (?f i)"
   219       using perm by (cases i) auto
   219       using perm by (cases i) auto
   220   qed
   220   qed
   221 next
   221 next
   222   case (trans xs ys zs)
   222   case (trans xs ys zs)
   223   then obtain f g where
   223   then obtain f g where
   224     bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
   224     bij: "bij_betw f {..<length xs} {..<length ys}" "bij_betw g {..<length ys} {..<length zs}" and
   225     perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
   225     perm: "\<forall>i<length xs. xs ! i = ys ! (f i)" "\<forall>i<length ys. ys ! i = zs ! (g i)" by blast
   226   show ?case
   226   show ?case
   227   proof (intro exI[of _ "g\<circ>f"] conjI allI impI)
   227   proof (intro exI[of _ "g \<circ> f"] conjI allI impI)
   228     show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
   228     show "bij_betw (g \<circ> f) {..<length xs} {..<length zs}"
   229       using bij by (rule bij_betw_trans)
   229       using bij by (rule bij_betw_trans)
   230     fix i assume "i < length xs"
   230     fix i assume "i < length xs"
   231     with bij have "f i < length ys" unfolding bij_betw_def by force
   231     with bij have "f i < length ys" unfolding bij_betw_def by force
   232     with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
   232     with `i < length xs` show "xs ! i = zs ! (g \<circ> f) i"
   233       using trans(1,3)[THEN perm_length] perm by force
   233       using trans(1,3)[THEN perm_length] perm by auto
   234   qed
   234   qed
   235 qed
   235 qed
   236 
   236 
   237 end
   237 end