src/HOL/Library/Permutation.thy
changeset 25379 12bcf37252b1
parent 25287 094dab519ff5
child 26072 f65a7fa2da6c
     1.1 --- a/src/HOL/Library/Permutation.thy	Sat Nov 10 18:36:06 2007 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Sat Nov 10 18:36:07 2007 +0100
     1.3 @@ -22,15 +22,8 @@
     1.4  
     1.5  subsection {* Some examples of rule induction on permutations *}
     1.6  
     1.7 -lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
     1.8 -    -- {*the form of the premise lets the induction bind @{term xs}
     1.9 -         and @{term ys} *}
    1.10 -  apply (erule perm.induct)
    1.11 -     apply (simp_all (no_asm_simp))
    1.12 -  done
    1.13 -
    1.14  lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
    1.15 -  using xperm_empty_imp_aux by blast
    1.16 +  by (induct xs == "[]::'a list" ys pred: perm) simp_all
    1.17  
    1.18  
    1.19  text {*
    1.20 @@ -38,13 +31,13 @@
    1.21    *}
    1.22  
    1.23  lemma perm_length: "xs <~~> ys ==> length xs = length ys"
    1.24 -  by (erule perm.induct) simp_all
    1.25 +  by (induct pred: perm) simp_all
    1.26  
    1.27  lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
    1.28    by (drule perm_length) auto
    1.29  
    1.30  lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
    1.31 -  by (erule perm.induct) auto
    1.32 +  by (induct pred: perm) auto
    1.33  
    1.34  
    1.35  subsection {* Ways of making new permutations *}
    1.36 @@ -88,8 +81,8 @@
    1.37    apply (erule perm_sym [THEN perm_empty_imp])
    1.38    done
    1.39  
    1.40 -lemma perm_sing_imp [rule_format]: "ys <~~> xs ==> xs = [y] --> ys = [y]"
    1.41 -  by (erule perm.induct) auto
    1.42 +lemma perm_sing_imp: "ys <~~> xs ==> xs = [y] ==> ys = [y]"
    1.43 +  by (induct pred: perm) auto
    1.44  
    1.45  lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
    1.46    by (blast intro: perm_sing_imp)
    1.47 @@ -112,7 +105,7 @@
    1.48  lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
    1.49    by (induct l) auto
    1.50  
    1.51 -lemma multiset_of_remove[simp]:
    1.52 +lemma multiset_of_remove [simp]:
    1.53      "multiset_of (remove a x) = multiset_of x - {#a#}"
    1.54    apply (induct x)
    1.55     apply (auto simp: multiset_eq_conv_count_eq)
    1.56 @@ -122,7 +115,7 @@
    1.57  text {* \medskip Congruence rule *}
    1.58  
    1.59  lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
    1.60 -  by (erule perm.induct) auto
    1.61 +  by (induct pred: perm) auto
    1.62  
    1.63  lemma remove_hd [simp]: "remove z (z # xs) = xs"
    1.64    by auto
    1.65 @@ -133,8 +126,8 @@
    1.66  lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
    1.67    by (blast intro: cons_perm_imp_perm)
    1.68  
    1.69 -lemma append_perm_imp_perm: "!!xs ys. zs @ xs <~~> zs @ ys ==> xs <~~> ys"
    1.70 -  apply (induct zs rule: rev_induct)
    1.71 +lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys ==> xs <~~> ys"
    1.72 +  apply (induct zs arbitrary: xs ys rule: rev_induct)
    1.73     apply (simp_all (no_asm_use))
    1.74    apply blast
    1.75    done
    1.76 @@ -170,34 +163,35 @@
    1.77    done
    1.78  
    1.79  lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
    1.80 -by (metis multiset_of_eq_perm multiset_of_eq_setD)
    1.81 +  by (metis multiset_of_eq_perm multiset_of_eq_setD)
    1.82  
    1.83  lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
    1.84 -apply(induct rule:perm.induct)
    1.85 -   apply simp_all
    1.86 - apply fastsimp
    1.87 -apply (metis perm_set_eq)
    1.88 -done
    1.89 +  apply (induct pred: perm)
    1.90 +     apply simp_all
    1.91 +   apply fastsimp
    1.92 +  apply (metis perm_set_eq)
    1.93 +  done
    1.94  
    1.95  lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
    1.96 -apply(induct xs arbitrary: ys rule:length_induct)
    1.97 -apply (case_tac "remdups xs", simp, simp)
    1.98 -apply(subgoal_tac "a : set (remdups ys)")
    1.99 - prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
   1.100 -apply(drule split_list) apply(elim exE conjE)
   1.101 -apply(drule_tac x=list in spec) apply(erule impE) prefer 2
   1.102 - apply(drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
   1.103 -  apply simp
   1.104 -  apply(subgoal_tac "a#list <~~> a#ysa@zs")
   1.105 -   apply (metis Cons_eq_appendI perm_append_Cons trans)
   1.106 -  apply (metis Cons Cons_eq_appendI distinct.simps(2) distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
   1.107 - apply(subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
   1.108 -  apply(fastsimp simp add: insert_ident)
   1.109 - apply (metis distinct_remdups set_remdups)
   1.110 -apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
   1.111 -done
   1.112 +  apply (induct xs arbitrary: ys rule: length_induct)
   1.113 +  apply (case_tac "remdups xs", simp, simp)
   1.114 +  apply (subgoal_tac "a : set (remdups ys)")
   1.115 +   prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
   1.116 +  apply (drule split_list) apply(elim exE conjE)
   1.117 +  apply (drule_tac x=list in spec) apply(erule impE) prefer 2
   1.118 +   apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
   1.119 +    apply simp
   1.120 +    apply (subgoal_tac "a#list <~~> a#ysa@zs")
   1.121 +     apply (metis Cons_eq_appendI perm_append_Cons trans)
   1.122 +    apply (metis Cons Cons_eq_appendI distinct.simps(2)
   1.123 +      distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
   1.124 +   apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
   1.125 +    apply (fastsimp simp add: insert_ident)
   1.126 +   apply (metis distinct_remdups set_remdups)
   1.127 +  apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
   1.128 +  done
   1.129  
   1.130  lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
   1.131 -by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
   1.132 +  by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
   1.133  
   1.134  end