# HG changeset patch
# User wenzelm
# Date 1194716167 -3600
# Node ID 12bcf37252b1f0bfccdc297abb3f959949fceb3a
# Parent  dca6916104890747cc57d81ce3479e4f41480b9e
tuned proofs;
tuned document;

diff -r dca691610489 -r 12bcf37252b1 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Sat Nov 10 18:36:06 2007 +0100
+++ b/src/HOL/Library/Permutation.thy	Sat Nov 10 18:36:07 2007 +0100
@@ -22,15 +22,8 @@
 
 subsection {* Some examples of rule induction on permutations *}
 
-lemma xperm_empty_imp_aux: "xs <~~> ys ==> xs = [] --> ys = []"
-    -- {*the form of the premise lets the induction bind @{term xs}
-         and @{term ys} *}
-  apply (erule perm.induct)
-     apply (simp_all (no_asm_simp))
-  done
-
 lemma xperm_empty_imp: "[] <~~> ys ==> ys = []"
-  using xperm_empty_imp_aux by blast
+  by (induct xs == "[]::'a list" ys pred: perm) simp_all
 
 
 text {*
@@ -38,13 +31,13 @@
   *}
 
 lemma perm_length: "xs <~~> ys ==> length xs = length ys"
-  by (erule perm.induct) simp_all
+  by (induct pred: perm) simp_all
 
 lemma perm_empty_imp: "[] <~~> xs ==> xs = []"
   by (drule perm_length) auto
 
 lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
-  by (erule perm.induct) auto
+  by (induct pred: perm) auto
 
 
 subsection {* Ways of making new permutations *}
@@ -88,8 +81,8 @@
   apply (erule perm_sym [THEN perm_empty_imp])
   done
 
-lemma perm_sing_imp [rule_format]: "ys <~~> xs ==> xs = [y] --> ys = [y]"
-  by (erule perm.induct) auto
+lemma perm_sing_imp: "ys <~~> xs ==> xs = [y] ==> ys = [y]"
+  by (induct pred: perm) auto
 
 lemma perm_sing_eq [iff]: "(ys <~~> [y]) = (ys = [y])"
   by (blast intro: perm_sing_imp)
@@ -112,7 +105,7 @@
 lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
   by (induct l) auto
 
-lemma multiset_of_remove[simp]:
+lemma multiset_of_remove [simp]:
     "multiset_of (remove a x) = multiset_of x - {#a#}"
   apply (induct x)
    apply (auto simp: multiset_eq_conv_count_eq)
@@ -122,7 +115,7 @@
 text {* \medskip Congruence rule *}
 
 lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
-  by (erule perm.induct) auto
+  by (induct pred: perm) auto
 
 lemma remove_hd [simp]: "remove z (z # xs) = xs"
   by auto
@@ -133,8 +126,8 @@
 lemma cons_perm_eq [iff]: "(z#xs <~~> z#ys) = (xs <~~> ys)"
   by (blast intro: cons_perm_imp_perm)
 
-lemma append_perm_imp_perm: "!!xs ys. zs @ xs <~~> zs @ ys ==> xs <~~> ys"
-  apply (induct zs rule: rev_induct)
+lemma append_perm_imp_perm: "zs @ xs <~~> zs @ ys ==> xs <~~> ys"
+  apply (induct zs arbitrary: xs ys rule: rev_induct)
    apply (simp_all (no_asm_use))
   apply blast
   done
@@ -170,34 +163,35 @@
   done
 
 lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
-by (metis multiset_of_eq_perm multiset_of_eq_setD)
+  by (metis multiset_of_eq_perm multiset_of_eq_setD)
 
 lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
-apply(induct rule:perm.induct)
-   apply simp_all
- apply fastsimp
-apply (metis perm_set_eq)
-done
+  apply (induct pred: perm)
+     apply simp_all
+   apply fastsimp
+  apply (metis perm_set_eq)
+  done
 
 lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
-apply(induct xs arbitrary: ys rule:length_induct)
-apply (case_tac "remdups xs", simp, simp)
-apply(subgoal_tac "a : set (remdups ys)")
- prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
-apply(drule split_list) apply(elim exE conjE)
-apply(drule_tac x=list in spec) apply(erule impE) prefer 2
- apply(drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
-  apply simp
-  apply(subgoal_tac "a#list <~~> a#ysa@zs")
-   apply (metis Cons_eq_appendI perm_append_Cons trans)
-  apply (metis Cons Cons_eq_appendI distinct.simps(2) distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
- apply(subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
-  apply(fastsimp simp add: insert_ident)
- apply (metis distinct_remdups set_remdups)
-apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
-done
+  apply (induct xs arbitrary: ys rule: length_induct)
+  apply (case_tac "remdups xs", simp, simp)
+  apply (subgoal_tac "a : set (remdups ys)")
+   prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
+  apply (drule split_list) apply(elim exE conjE)
+  apply (drule_tac x=list in spec) apply(erule impE) prefer 2
+   apply (drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
+    apply simp
+    apply (subgoal_tac "a#list <~~> a#ysa@zs")
+     apply (metis Cons_eq_appendI perm_append_Cons trans)
+    apply (metis Cons Cons_eq_appendI distinct.simps(2)
+      distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
+   apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
+    apply (fastsimp simp add: insert_ident)
+   apply (metis distinct_remdups set_remdups)
+  apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
+  done
 
 lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
-by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
+  by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
 
 end