src/HOL/Library/Permutation.thy
 changeset 25379 12bcf37252b1 parent 25287 094dab519ff5 child 26072 f65a7fa2da6c
equal 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 `
`    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`