added lemmas
authornipkow
Mon Nov 05 18:18:39 2007 +0100 (2007-11-05)
changeset 25287094dab519ff5
parent 25286 35e954ff67f8
child 25288 6e0c8dd213df
added lemmas
src/HOL/Library/Permutation.thy
src/HOL/List.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Library/Permutation.thy	Mon Nov 05 17:48:51 2007 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Mon Nov 05 18:18:39 2007 +0100
     1.3 @@ -179,4 +179,25 @@
     1.4  apply (metis perm_set_eq)
     1.5  done
     1.6  
     1.7 +lemma eq_set_perm_remdups: "set xs = set ys ==> remdups xs <~~> remdups ys"
     1.8 +apply(induct xs arbitrary: ys rule:length_induct)
     1.9 +apply (case_tac "remdups xs", simp, simp)
    1.10 +apply(subgoal_tac "a : set (remdups ys)")
    1.11 + prefer 2 apply (metis set.simps(2) insert_iff set_remdups)
    1.12 +apply(drule split_list) apply(elim exE conjE)
    1.13 +apply(drule_tac x=list in spec) apply(erule impE) prefer 2
    1.14 + apply(drule_tac x="ysa@zs" in spec) apply(erule impE) prefer 2
    1.15 +  apply simp
    1.16 +  apply(subgoal_tac "a#list <~~> a#ysa@zs")
    1.17 +   apply (metis Cons_eq_appendI perm_append_Cons trans)
    1.18 +  apply (metis Cons Cons_eq_appendI distinct.simps(2) distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
    1.19 + apply(subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
    1.20 +  apply(fastsimp simp add: insert_ident)
    1.21 + apply (metis distinct_remdups set_remdups)
    1.22 +apply (metis Nat.le_less_trans Suc_length_conv le_def length_remdups_leq less_Suc_eq)
    1.23 +done
    1.24 +
    1.25 +lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"
    1.26 +by (metis List.set_remdups perm_set_eq eq_set_perm_remdups)
    1.27 +
    1.28  end
     2.1 --- a/src/HOL/List.thy	Mon Nov 05 17:48:51 2007 +0100
     2.2 +++ b/src/HOL/List.thy	Mon Nov 05 18:18:39 2007 +0100
     2.3 @@ -2069,6 +2069,12 @@
     2.4  lemma distinct_remdups [iff]: "distinct (remdups xs)"
     2.5  by (induct xs) auto
     2.6  
     2.7 +lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
     2.8 +by (induct xs, auto)
     2.9 +
    2.10 +lemma remdups_id_iff_distinct[simp]: "(remdups xs = xs) = distinct xs"
    2.11 +by(metis distinct_remdups distinct_remdups_id)
    2.12 +
    2.13  lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
    2.14  by (metis distinct_remdups finite_list set_remdups)
    2.15  
    2.16 @@ -2184,6 +2190,12 @@
    2.17    qed
    2.18  qed
    2.19  
    2.20 +lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
    2.21 +apply (induct n == "length ws" arbitrary:ws) apply simp
    2.22 +apply(case_tac ws) apply simp
    2.23 +apply (simp split:split_if_asm)
    2.24 +apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
    2.25 +done
    2.26  
    2.27  lemma length_remdups_concat:
    2.28   "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
     3.1 --- a/src/HOL/Set.thy	Mon Nov 05 17:48:51 2007 +0100
     3.2 +++ b/src/HOL/Set.thy	Mon Nov 05 18:18:39 2007 +0100
     3.3 @@ -780,6 +780,8 @@
     3.4    show "x \<notin> A - {x}" by blast
     3.5  qed
     3.6  
     3.7 +lemma insert_ident: "x ~: A ==> x ~: B ==> (insert x A = insert x B) = (A = B)"
     3.8 +by auto
     3.9  
    3.10  subsubsection {* Singletons, using insert *}
    3.11