added lemmas
authornipkow
Mon Nov 05 08:31:12 2007 +0100 (2007-11-05)
changeset 2527795128fcdd7e8
parent 25276 f9237f6f3a8d
child 25278 3026df96941d
added lemmas
src/HOL/Library/Permutation.thy
src/HOL/List.thy
     1.1 --- a/src/HOL/Library/Permutation.thy	Sun Nov 04 19:17:13 2007 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Mon Nov 05 08:31:12 2007 +0100
     1.3 @@ -46,9 +46,6 @@
     1.4  lemma perm_sym: "xs <~~> ys ==> ys <~~> xs"
     1.5    by (erule perm.induct) auto
     1.6  
     1.7 -lemma perm_mem [rule_format]: "xs <~~> ys ==> x mem xs --> x mem ys"
     1.8 -  by (erule perm.induct) auto
     1.9 -
    1.10  
    1.11  subsection {* Ways of making new permutations *}
    1.12  
    1.13 @@ -172,4 +169,14 @@
    1.14    apply (blast intro: sym)+
    1.15    done
    1.16  
    1.17 +lemma perm_set_eq: "xs <~~> ys ==> set xs = set ys"
    1.18 +by (metis multiset_of_eq_perm multiset_of_eq_setD)
    1.19 +
    1.20 +lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
    1.21 +apply(induct rule:perm.induct)
    1.22 +   apply simp_all
    1.23 + apply fastsimp
    1.24 +apply (metis perm_set_eq)
    1.25 +done
    1.26 +
    1.27  end
     2.1 --- a/src/HOL/List.thy	Sun Nov 04 19:17:13 2007 +0100
     2.2 +++ b/src/HOL/List.thy	Mon Nov 05 08:31:12 2007 +0100
     2.3 @@ -2581,6 +2581,9 @@
     2.4  
     2.5  end
     2.6  
     2.7 +lemma sorted_upt[simp]: "sorted[i..<j]"
     2.8 +by (induct j) (simp_all add:sorted_append)
     2.9 +
    2.10  
    2.11  subsubsection {* @{text sorted_list_of_set} *}
    2.12