modernized primrec
authorhaftmann
Sat Nov 07 08:17:52 2009 +0100 (2009-11-07)
changeset 33498318acc1c9399
parent 33469 0183f9545fa2
child 33499 30e6e070bdb6
modernized primrec
src/HOL/Library/Permutation.thy
     1.1 --- a/src/HOL/Library/Permutation.thy	Fri Nov 06 13:42:29 2009 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Sat Nov 07 08:17:52 2009 +0100
     1.3 @@ -93,11 +93,9 @@
     1.4  
     1.5  subsection {* Removing elements *}
     1.6  
     1.7 -consts
     1.8 -  remove :: "'a => 'a list => 'a list"
     1.9 -primrec
    1.10 -  "remove x [] = []"
    1.11 -  "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
    1.12 +primrec remove :: "'a => 'a list => 'a list" where
    1.13 +    "remove x [] = []"
    1.14 +  | "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
    1.15  
    1.16  lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
    1.17    by (induct ys) auto
    1.18 @@ -156,7 +154,7 @@
    1.19    done
    1.20  
    1.21  lemma multiset_of_le_perm_append:
    1.22 -    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)";
    1.23 +    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)"
    1.24    apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
    1.25    apply (insert surj_multiset_of, drule surjD)
    1.26    apply (blast intro: sym)+