src/HOL/List.thy
changeset 44013 5cfc1c36ae97
parent 43594 ef1ddc59b825
child 44510 5e580115dfcd
     1.1 --- a/src/HOL/List.thy	Tue Aug 02 10:03:14 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Aug 02 10:36:50 2011 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* The datatype of finite lists *}
     1.5  
     1.6  theory List
     1.7 -imports Plain Presburger Recdef Code_Numeral Quotient ATP
     1.8 +imports Plain Presburger Code_Numeral Quotient ATP
     1.9  uses
    1.10    ("Tools/list_code.ML")
    1.11    ("Tools/list_to_set_comprehension.ML")
    1.12 @@ -800,7 +800,7 @@
    1.13  lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
    1.14  by (induct xs) auto
    1.15  
    1.16 -lemma map_cong [fundef_cong, recdef_cong]:
    1.17 +lemma map_cong [fundef_cong]:
    1.18    "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys"
    1.19    by simp
    1.20  
    1.21 @@ -1237,7 +1237,7 @@
    1.22    (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
    1.23  by(auto dest:Cons_eq_filterD)
    1.24  
    1.25 -lemma filter_cong[fundef_cong, recdef_cong]:
    1.26 +lemma filter_cong[fundef_cong]:
    1.27   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
    1.28  apply simp
    1.29  apply(erule thin_rl)
    1.30 @@ -2003,12 +2003,12 @@
    1.31  apply(auto)
    1.32  done
    1.33  
    1.34 -lemma takeWhile_cong [fundef_cong, recdef_cong]:
    1.35 +lemma takeWhile_cong [fundef_cong]:
    1.36    "[| l = k; !!x. x : set l ==> P x = Q x |] 
    1.37    ==> takeWhile P l = takeWhile Q k"
    1.38  by (induct k arbitrary: l) (simp_all)
    1.39  
    1.40 -lemma dropWhile_cong [fundef_cong, recdef_cong]:
    1.41 +lemma dropWhile_cong [fundef_cong]:
    1.42    "[| l = k; !!x. x : set l ==> P x = Q x |] 
    1.43    ==> dropWhile P l = dropWhile Q k"
    1.44  by (induct k arbitrary: l, simp_all)
    1.45 @@ -2349,12 +2349,12 @@
    1.46    shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
    1.47    by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_iff)
    1.48  
    1.49 -lemma foldl_cong [fundef_cong, recdef_cong]:
    1.50 +lemma foldl_cong [fundef_cong]:
    1.51    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
    1.52    ==> foldl f a l = foldl g b k"
    1.53  by (induct k arbitrary: a b l) simp_all
    1.54  
    1.55 -lemma foldr_cong [fundef_cong, recdef_cong]:
    1.56 +lemma foldr_cong [fundef_cong]:
    1.57    "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
    1.58    ==> foldr f l a = foldr g k b"
    1.59  by (induct k arbitrary: a b l) simp_all
    1.60 @@ -4586,7 +4586,7 @@
    1.61  definition
    1.62    "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
    1.63  
    1.64 -lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
    1.65 +lemma wf_measures[simp]: "wf (measures fs)"
    1.66  unfolding measures_def
    1.67  by blast
    1.68