src/HOL/Library/Permutation.thy
changeset 25379 12bcf37252b1
parent 25287 094dab519ff5
child 26072 f65a7fa2da6c
equal deleted inserted replaced
25378:dca691610489 25379:12bcf37252b1
    20   by (induct l) auto
    20   by (induct l) auto
    21 
    21 
    22 
    22 
    23 subsection {* Some examples of rule induction on permutations *}
    23 subsection {* Some examples of rule induction on permutations *}
    24 
    24 
    25 lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
       
    26     -- {*the form of the premise lets the induction bind @{term xs}
       
    27          and @{term ys} *}
       
    28   apply (erule perm.induct)
       
    29      apply (simp_all (no_asm_simp))
       
    30   done
       
    31 
       
    32 lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
    25 lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
    33   using xperm_empty_imp_aux by blast
    26   by (induct xs == "[]::'a list" ys pred: perm) simp_all
    34 
    27 
    35 
    28 
    36 text {*
    29 text {*
    37   \medskip This more general theorem is easier to understand!
    30   \medskip This more general theorem is easier to understand!
    38   *}
    31   *}
    39 
    32 
    40 lemma perm_length: "xs <~~> ys ==> length xs = length ys"
    33 lemma perm_length: "xs <~~> ys ==> length xs = length ys"
    41   by (erule perm.induct) simp_all
    34   by (induct pred: perm) simp_all
    42 
    35 
    43 lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
    36 lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
    44   by (drule perm_length) auto
    37   by (drule perm_length) auto
    45 
    38 
    46 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
    39 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
    47   by (erule perm.induct) auto
    40   by (induct pred: perm) auto
    48 
    41 
    49 
    42 
    50 subsection {* Ways of making new permutations *}
    43 subsection {* Ways of making new permutations *}
    51 
    44 
    52 text {*
    45 text {*
    86 lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
    79 lemma perm_empty2 [iff]: "(xs <~~> []) = (xs = [])"
    87   apply auto
    80   apply auto
    88   apply (erule perm_sym [THEN perm_empty_imp])
    81   apply (erule perm_sym [THEN perm_empty_imp])
    89   done
    82   done
    90 
    83 
    91 lemma perm_sing_imp [rule_format]: "ys <~~> xs ==> xs = [y] --> ys = [y]"
    84 lemma perm_sing_imp: "ys <~~> xs ==> xs = [y] ==> ys = [y]"
    92   by (erule perm.induct) auto
    85   by (induct pred: perm) auto
    93 
    86 
    94 lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
    87 lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
    95   by (blast intro: perm_sing_imp)
    88   by (blast intro: perm_sing_imp)
    96 
    89 
    97 lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
    90 lemma perm_sing_eq2 [iff]: "([y] <~~> ys) = (ys = [y])"
   110   by (induct ys) auto
   103   by (induct ys) auto
   111 
   104 
   112 lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
   105 lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
   113   by (induct l) auto
   106   by (induct l) auto
   114 
   107 
   115 lemma multiset_of_remove[simp]:
   108 lemma multiset_of_remove [simp]:
   116     "multiset_of (remove a x) = multiset_of x - {#a#}"
   109     "multiset_of (remove a x) = multiset_of x - {#a#}"
   117   apply (induct x)
   110   apply (induct x)
   118    apply (auto simp: multiset_eq_conv_count_eq)
   111    apply (auto simp: multiset_eq_conv_count_eq)
   119   done
   112   done
   120 
   113 
   121 
   114 
   122 text {* \medskip Congruence rule *}
   115 text {* \medskip Congruence rule *}
   123 
   116 
   124 lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
   117 lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
   125   by (erule perm.induct) auto
   118   by (induct pred: perm) auto
   126 
   119 
   127 lemma remove_hd [simp]: "remove z (z # xs) = xs"
   120 lemma remove_hd [simp]: "remove z (z # xs) = xs"
   128   by auto
   121   by auto
   129 
   122 
   130 lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
   123 lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
   131   by (drule_tac z = z in perm_remove_perm) auto
   124   by (drule_tac z = z in perm_remove_perm) auto
   132 
   125 
   133 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
   126 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
   134   by (blast intro: cons_perm_imp_perm)
   127   by (blast intro: cons_perm_imp_perm)
   135 
   128 
   136 lemma append_perm_imp_perm: "!!xs ys. zs @ xs <~~> zs @ ys ==> xs <~~> ys"
   129 lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys ==> xs <~~> ys"
   137   apply (induct zs rule: rev_induct)
   130   apply (induct zs arbitrary: xs ys rule: rev_induct)
   138    apply (simp_all (no_asm_use))
   131    apply (simp_all (no_asm_use))
   139   apply blast
   132   apply blast
   140   done
   133   done
   141 
   134 
   142 lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
   135 lemma perm_append1_eq [iff]: "(zs @ xs <~~> zs @ ys) = (xs <~~> ys)"
   168   apply (insert surj_multiset_of, drule surjD)
   161   apply (insert surj_multiset_of, drule surjD)
   169   apply (blast intro: sym)+
   162   apply (blast intro: sym)+
   170   done
   163   done
   171 
   164 
   172 lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
   165 lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
   173 by (metis multiset_of_eq_perm multiset_of_eq_setD)
   166   by (metis multiset_of_eq_perm multiset_of_eq_setD)
   174 
   167 
   175 lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
   168 lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
   176 apply(induct rule:perm.induct)
   169   apply (induct pred: perm)
   177    apply simp_all
   170      apply simp_all
   178  apply fastsimp
   171    apply fastsimp
   179 apply (metis perm_set_eq)
   172   apply (metis perm_set_eq)
   180 done
   173   done
   181 
   174 
   182 lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
   175 lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
   183 apply(induct xs arbitrary: ys rule:length_induct)
   176   apply (induct xs arbitrary: ys rule: length_induct)
   184 apply (case_tac "remdups xs", simp, simp)
   177   apply (case_tac "remdups xs", simp, simp)
   185 apply(subgoal_tac "a : set (remdups ys)")
   178   apply (subgoal_tac "a : set (remdups ys)")
   186  prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
   179    prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
   187 apply(drule split_list) apply(elim exE conjE)
   180   apply (drule split_list) apply(elim exE conjE)
   188 apply(drule_tac x=list in spec) apply(erule impE) prefer 2
   181   apply (drule_tac x=list in spec) apply(erule impE) prefer 2
   189  apply(drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
   182    apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
   190   apply simp
   183     apply simp
   191   apply(subgoal_tac "a#list <~~> a#ysa@zs")
   184     apply (subgoal_tac "a#list <~~> a#ysa@zs")
   192    apply (metis Cons_eq_appendI perm_append_Cons trans)
   185      apply (metis Cons_eq_appendI perm_append_Cons trans)
   193   apply (metis Cons Cons_eq_appendI distinct.simps(2) distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
   186     apply (metis Cons Cons_eq_appendI distinct.simps(2)
   194  apply(subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
   187       distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
   195   apply(fastsimp simp add: insert_ident)
   188    apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
   196  apply (metis distinct_remdups set_remdups)
   189     apply (fastsimp simp add: insert_ident)
   197 apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
   190    apply (metis distinct_remdups set_remdups)
   198 done
   191   apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
       
   192   done
   199 
   193 
   200 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
   194 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
   201 by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
   195   by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
   202 
   196 
   203 end
   197 end