# HG changeset patch # User haftmann # Date 1333729036 -7200 # Node ID d654c73e4b123f6f66180c8d6b07177d11b3bfd8 # Parent a0f257197741840418f0de5b54195de9ad69692d no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code diff -r a0f257197741 -r d654c73e4b12 NEWS --- a/NEWS Fri Apr 06 14:40:00 2012 +0200 +++ b/NEWS Fri Apr 06 18:17:16 2012 +0200 @@ -208,10 +208,11 @@ SUPR_set_fold ~> SUP_set_fold INF_code ~> INF_set_foldr SUP_code ~> SUP_set_foldr - foldr.simps ~> foldr_Nil foldr_Cons (in point-free formulation) - foldl.simps ~> foldl_Nil foldl_Cons - foldr_fold_rev ~> foldr_def - foldl_fold ~> foldl_def + foldr.simps ~> foldr.simps (in point-free formulation) + foldr_fold_rev ~> foldr_conv_fold + foldl_fold ~> foldl_conv_fold + foldr_foldr ~> foldr_conv_foldl + foldl_foldr ~> foldl_conv_foldr INCOMPATIBILITY. @@ -220,11 +221,12 @@ rev_foldl_cons, fold_set_remdups, fold_set, fold_set1, concat_conv_foldl, foldl_weak_invariant, foldl_invariant, foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1, -listsum_conv_fold, listsum_foldl, sort_foldl_insort. INCOMPATIBILITY. -Prefer "List.fold" with canonical argument order, or boil down -"List.foldr" and "List.foldl" to "List.fold" by unfolding "foldr_def" -and "foldl_def". For the common phrases "%xs. List.foldr plus xs 0" -and "List.foldl plus 0", prefer "List.listsum". +listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc, +foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv. +INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0" +and "List.foldl plus 0", prefer "List.listsum". Otherwise it can +be useful to boil down "List.foldr" and "List.foldl" to "List.fold" +by unfolding "foldr_conv_fold" and "foldl_conv_fold". * Congruence rules Option.map_cong and Option.bind_cong for recursion through option types. diff -r a0f257197741 -r d654c73e4b12 src/HOL/Library/AList.thy --- a/src/HOL/Library/AList.thy Fri Apr 06 14:40:00 2012 +0200 +++ b/src/HOL/Library/AList.thy Fri Apr 06 18:17:16 2012 +0200 @@ -97,7 +97,7 @@ have "map_of \<circ> fold (prod_case update) (zip ks vs) = fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of" by (rule fold_commute) (auto simp add: fun_eq_iff update_conv') - then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_def split_def) + then show ?thesis by (auto simp add: updates_def fun_eq_iff map_upds_fold_map_upd foldl_conv_fold split_def) qed lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k" @@ -427,7 +427,7 @@ lemma merge_updates: "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs" - by (simp add: merge_def updates_def foldr_def zip_rev zip_map_fst_snd) + by (simp add: merge_def updates_def foldr_conv_fold zip_rev zip_map_fst_snd) lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys" by (induct ys arbitrary: xs) (auto simp add: dom_update) @@ -448,7 +448,7 @@ fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of" by (rule fold_commute) (simp add: update_conv' prod_case_beta split_def fun_eq_iff) then show ?thesis - by (simp add: merge_def map_add_map_of_foldr foldr_def fun_eq_iff) + by (simp add: merge_def map_add_map_of_foldr foldr_conv_fold fun_eq_iff) qed corollary merge_conv: diff -r a0f257197741 -r d654c73e4b12 src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Fri Apr 06 14:40:00 2012 +0200 +++ b/src/HOL/Library/RBT_Impl.thy Fri Apr 06 18:17:16 2012 +0200 @@ -1076,7 +1076,7 @@ from this Empty_is_rbt have "lookup (List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs" by (simp add: `ys = rev xs`) - then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_def) + then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_conv_fold) qed hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted diff -r a0f257197741 -r d654c73e4b12 src/HOL/List.thy --- a/src/HOL/List.thy Fri Apr 06 14:40:00 2012 +0200 +++ b/src/HOL/List.thy Fri Apr 06 18:17:16 2012 +0200 @@ -85,18 +85,20 @@ syntax (HTML output) "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])") -primrec -- {* canonical argument order *} - fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where - "fold f [] = id" - | "fold f (x # xs) = fold f xs \<circ> f x" - -definition - foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where - [code_abbrev]: "foldr f xs = fold f (rev xs)" - -definition - foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where - "foldl f s xs = fold (\<lambda>x s. f s x) xs s" +primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" +where + fold_Nil: "fold f [] = id" +| fold_Cons: "fold f (x # xs) = fold f xs \<circ> f x" -- {* natural argument order *} + +primrec foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" +where + foldr_Nil: "foldr f [] = id" +| foldr_Cons: "foldr f (x # xs) = f x \<circ> foldr f xs" -- {* natural argument order *} + +primrec foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" +where + foldl_Nil: "foldl f a [] = a" +| foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs" primrec concat:: "'a list list \<Rightarrow> 'a list" where @@ -250,8 +252,8 @@ @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\ @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\ @{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\ -@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by (simp add: foldr_def)}\\ -@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by (simp add: foldl_def)}\\ +@{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\ +@{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\ @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\ @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\ @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\ @@ -277,7 +279,7 @@ @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\ @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\ @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\ -@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def foldr_def)} +@{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)} \end{tabular}} \caption{Characteristic examples} \label{fig:Characteristic} @@ -2387,7 +2389,7 @@ by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong) -subsubsection {* @{const fold} with canonical argument order *} +subsubsection {* @{const fold} with natural argument order *} lemma fold_remove1_split: assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" @@ -2477,7 +2479,7 @@ qed qed -lemma union_set_fold: +lemma union_set_fold [code]: "set xs \<union> A = fold Set.insert xs A" proof - interpret comp_fun_idem Set.insert @@ -2485,7 +2487,11 @@ show ?thesis by (simp add: union_fold_insert fold_set_fold) qed -lemma minus_set_fold: +lemma union_coset_filter [code]: + "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)" + by auto + +lemma minus_set_fold [code]: "A - set xs = fold Set.remove xs A" proof - interpret comp_fun_idem Set.remove @@ -2494,6 +2500,18 @@ by (simp add: minus_fold_remove [of _ A] fold_set_fold) qed +lemma minus_coset_filter [code]: + "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)" + by auto + +lemma inter_set_filter [code]: + "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" + by auto + +lemma inter_coset_fold [code]: + "A \<inter> List.coset xs = fold Set.remove xs A" + by (simp add: Diff_eq [symmetric] minus_set_fold) + lemma (in lattice) Inf_fin_set_fold: "Inf_fin (set (x # xs)) = fold inf xs x" proof - @@ -2503,6 +2521,8 @@ by (simp add: Inf_fin_def fold1_set_fold del: set.simps) qed +declare Inf_fin_set_fold [code] + lemma (in lattice) Sup_fin_set_fold: "Sup_fin (set (x # xs)) = fold sup xs x" proof - @@ -2512,6 +2532,8 @@ by (simp add: Sup_fin_def fold1_set_fold del: set.simps) qed +declare Sup_fin_set_fold [code] + lemma (in linorder) Min_fin_set_fold: "Min (set (x # xs)) = fold min xs x" proof - @@ -2521,6 +2543,8 @@ by (simp add: Min_def fold1_set_fold del: set.simps) qed +declare Min_fin_set_fold [code] + lemma (in linorder) Max_fin_set_fold: "Max (set (x # xs)) = fold max xs x" proof - @@ -2530,6 +2554,8 @@ by (simp add: Max_def fold1_set_fold del: set.simps) qed +declare Max_fin_set_fold [code] + lemma (in complete_lattice) Inf_set_fold: "Inf (set xs) = fold inf xs top" proof - @@ -2538,6 +2564,8 @@ show ?thesis by (simp add: Inf_fold_inf fold_set_fold inf_commute) qed +declare Inf_set_fold [where 'a = "'a set", code] + lemma (in complete_lattice) Sup_set_fold: "Sup (set xs) = fold sup xs bot" proof - @@ -2546,73 +2574,74 @@ show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute) qed +declare Sup_set_fold [where 'a = "'a set", code] + lemma (in complete_lattice) INF_set_fold: "INFI (set xs) f = fold (inf \<circ> f) xs top" unfolding INF_def set_map [symmetric] Inf_set_fold fold_map .. +declare INF_set_fold [code] + lemma (in complete_lattice) SUP_set_fold: "SUPR (set xs) f = fold (sup \<circ> f) xs bot" unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map .. +declare SUP_set_fold [code] subsubsection {* Fold variants: @{const foldr} and @{const foldl} *} text {* Correspondence *} -lemma foldr_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *} +lemma foldr_conv_fold [code_abbrev]: + "foldr f xs = fold f (rev xs)" + by (induct xs) simp_all + +lemma foldl_conv_fold: + "foldl f s xs = fold (\<lambda>x s. f s x) xs s" + by (induct xs arbitrary: s) simp_all + +lemma foldr_conv_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *} "foldr f xs a = foldl (\<lambda>x y. f y x) a (rev xs)" - by (simp add: foldr_def foldl_def) - -lemma foldl_foldr: + by (simp add: foldr_conv_fold foldl_conv_fold) + +lemma foldl_conv_foldr: "foldl f a xs = foldr (\<lambda>x y. f y x) (rev xs) a" - by (simp add: foldr_def foldl_def) + by (simp add: foldr_conv_fold foldl_conv_fold) lemma foldr_fold: assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y" shows "foldr f xs = fold f xs" - using assms unfolding foldr_def by (rule fold_rev) - -lemma - foldr_Nil [code, simp]: "foldr f [] = id" - and foldr_Cons [code, simp]: "foldr f (x # xs) = f x \<circ> foldr f xs" - by (simp_all add: foldr_def) - -lemma - foldl_Nil [simp]: "foldl f a [] = a" - and foldl_Cons [simp]: "foldl f a (x # xs) = foldl f (f a x) xs" - by (simp_all add: foldl_def) + using assms unfolding foldr_conv_fold by (rule fold_rev) lemma foldr_cong [fundef_cong]: "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f x a = g x a) \<Longrightarrow> foldr f l a = foldr g k b" - by (auto simp add: foldr_def intro!: fold_cong) + by (auto simp add: foldr_conv_fold intro!: fold_cong) lemma foldl_cong [fundef_cong]: "a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f a x = g a x) \<Longrightarrow> foldl f a l = foldl g b k" - by (auto simp add: foldl_def intro!: fold_cong) + by (auto simp add: foldl_conv_fold intro!: fold_cong) lemma foldr_append [simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)" - by (simp add: foldr_def) + by (simp add: foldr_conv_fold) lemma foldl_append [simp]: "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" - by (simp add: foldl_def) + by (simp add: foldl_conv_fold) lemma foldr_map [code_unfold]: "foldr g (map f xs) a = foldr (g o f) xs a" - by (simp add: foldr_def fold_map rev_map) + by (simp add: foldr_conv_fold fold_map rev_map) lemma foldl_map [code_unfold]: "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs" - by (simp add: foldl_def fold_map comp_def) - -text {* Executing operations in terms of @{const foldr} -- tail-recursive! *} + by (simp add: foldl_conv_fold fold_map comp_def) lemma concat_conv_foldr [code]: "concat xss = foldr append xss []" - by (simp add: fold_append_concat_rev foldr_def) - -lemma minus_set_foldr [code]: + by (simp add: fold_append_concat_rev foldr_conv_fold) + +lemma minus_set_foldr: "A - set xs = foldr Set.remove xs A" proof - have "\<And>x y :: 'a. Set.remove y \<circ> Set.remove x = Set.remove x \<circ> Set.remove y" @@ -2620,11 +2649,7 @@ then show ?thesis by (simp add: minus_set_fold foldr_fold) qed -lemma subtract_coset_filter [code]: - "A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)" - by auto - -lemma union_set_foldr [code]: +lemma union_set_foldr: "set xs \<union> A = foldr Set.insert xs A" proof - have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y" @@ -2632,31 +2657,23 @@ then show ?thesis by (simp add: union_set_fold foldr_fold) qed -lemma union_coset_foldr [code]: - "List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)" - by auto - -lemma inter_set_filer [code]: - "A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)" - by auto - -lemma inter_coset_foldr [code]: +lemma inter_coset_foldr: "A \<inter> List.coset xs = foldr Set.remove xs A" by (simp add: Diff_eq [symmetric] minus_set_foldr) -lemma (in lattice) Inf_fin_set_foldr [code]: +lemma (in lattice) Inf_fin_set_foldr: "Inf_fin (set (x # xs)) = foldr inf xs x" by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) -lemma (in lattice) Sup_fin_set_foldr [code]: +lemma (in lattice) Sup_fin_set_foldr: "Sup_fin (set (x # xs)) = foldr sup xs x" by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) -lemma (in linorder) Min_fin_set_foldr [code]: +lemma (in linorder) Min_fin_set_foldr: "Min (set (x # xs)) = foldr min xs x" by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) -lemma (in linorder) Max_fin_set_foldr [code]: +lemma (in linorder) Max_fin_set_foldr: "Max (set (x # xs)) = foldr max xs x" by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) @@ -2668,13 +2685,11 @@ "Sup (set xs) = foldr sup xs bot" by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) -declare Inf_set_foldr [where 'a = "'a set", code] Sup_set_foldr [where 'a = "'a set", code] - -lemma (in complete_lattice) INF_set_foldr [code]: +lemma (in complete_lattice) INF_set_foldr: "INFI (set xs) f = foldr (inf \<circ> f) xs top" by (simp only: INF_def Inf_set_foldr foldr_map set_map [symmetric]) -lemma (in complete_lattice) SUP_set_foldr [code]: +lemma (in complete_lattice) SUP_set_foldr: "SUPR (set xs) f = foldr (sup \<circ> f) xs bot" by (simp only: SUP_def Sup_set_foldr foldr_map set_map [symmetric]) @@ -3108,7 +3123,7 @@ lemma (in comm_monoid_add) listsum_rev [simp]: "listsum (rev xs) = listsum xs" - by (simp add: listsum_def foldr_def fold_rev fun_eq_iff add_ac) + by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac) lemma (in monoid_add) fold_plus_listsum_rev: "fold plus xs = plus (listsum (rev xs))" @@ -3116,40 +3131,12 @@ fix x have "fold plus xs x = fold plus xs (x + 0)" by simp also have "\<dots> = fold plus (x # xs) 0" by simp - also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_def) + also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold) also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def) also have "\<dots> = listsum (rev xs) + listsum [x]" by simp finally show "fold plus xs x = listsum (rev xs) + x" by simp qed -lemma (in semigroup_add) foldl_assoc: - "foldl plus (x + y) zs = x + foldl plus y zs" - by (simp add: foldl_def fold_commute_apply [symmetric] fun_eq_iff add_assoc) - -lemma (in ab_semigroup_add) foldr_conv_foldl: - "foldr plus xs a = foldl plus a xs" - by (simp add: foldl_def foldr_fold fun_eq_iff add_ac) - -text {* - Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more - difficult to use because it requires an additional transitivity step. -*} - -lemma start_le_sum: - fixes m n :: nat - shows "m \<le> n \<Longrightarrow> m \<le> foldl plus n ns" - by (simp add: foldl_def add_commute fold_plus_listsum_rev) - -lemma elem_le_sum: - fixes m n :: nat - shows "n \<in> set ns \<Longrightarrow> n \<le> foldl plus 0 ns" - by (force intro: start_le_sum simp add: in_set_conv_decomp) - -lemma sum_eq_0_conv [iff]: - fixes m :: nat - shows "foldl plus m ns = 0 \<longleftrightarrow> m = 0 \<and> (\<forall>n \<in> set ns. n = 0)" - by (induct ns arbitrary: m) auto - text{* Some syntactic sugar for summing a function over a list: *} syntax @@ -3186,17 +3173,18 @@ lemma listsum_eq_0_nat_iff_nat [simp]: "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)" - by (simp add: listsum_def foldr_conv_foldl) + by (induct ns) simp_all + +lemma member_le_listsum_nat: + "(n :: nat) \<in> set ns \<Longrightarrow> n \<le> listsum ns" + by (induct ns) auto lemma elem_le_listsum_nat: "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)" -apply(induct ns arbitrary: k) - apply simp -apply(fastforce simp add:nth_Cons split: nat.split) -done + by (rule member_le_listsum_nat) simp lemma listsum_update_nat: - "k<size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k" + "k < size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k" apply(induct ns arbitrary:k) apply (auto split:nat.split) apply(drule elem_le_listsum_nat) @@ -4053,7 +4041,7 @@ show "(insort_key f y \<circ> insort_key f x) zs = (insort_key f x \<circ> insort_key f y) zs" by (induct zs) (auto intro: * simp add: **) qed - then show ?thesis by (simp add: sort_key_def foldr_def) + then show ?thesis by (simp add: sort_key_def foldr_conv_fold) qed lemma (in linorder) sort_conv_fold: @@ -4601,7 +4589,7 @@ lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)" proof (rule mono_inf [where f=listsp, THEN order_antisym]) show "mono listsp" by (simp add: mono_def listsp_mono) - show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I) + show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI) qed lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def] @@ -5756,3 +5744,4 @@ by (simp add: wf_iff_acyclic_if_finite) end + diff -r a0f257197741 -r d654c73e4b12 src/HOL/Nominal/Examples/Standardization.thy --- a/src/HOL/Nominal/Examples/Standardization.thy Fri Apr 06 14:40:00 2012 +0200 +++ b/src/HOL/Nominal/Examples/Standardization.thy Fri Apr 06 18:17:16 2012 +0200 @@ -213,7 +213,8 @@ prefer 2 apply (erule allE, erule impE, rule refl, erule spec) apply simp - apply (clarsimp simp add: foldr_conv_foldl [symmetric] foldr_def fold_plus_listsum_rev listsum_map_remove1) + apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev) + apply (fastforce simp add: listsum_map_remove1) apply clarify apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)") prefer 2 @@ -232,8 +233,10 @@ apply clarify apply (erule allE, erule impE) prefer 2 - apply blast - apply (force intro: le_imp_less_Suc trans_le_add1 trans_le_add2 elem_le_sum) + apply blast + apply simp + apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev) + apply (fastforce simp add: listsum_map_remove1) done theorem Apps_lam_induct: @@ -855,3 +858,4 @@ qed end + diff -r a0f257197741 -r d654c73e4b12 src/HOL/Proofs/Lambda/ListApplication.thy --- a/src/HOL/Proofs/Lambda/ListApplication.thy Fri Apr 06 14:40:00 2012 +0200 +++ b/src/HOL/Proofs/Lambda/ListApplication.thy Fri Apr 06 18:17:16 2012 +0200 @@ -110,10 +110,8 @@ prefer 2 apply (erule allE, erule mp, rule refl) apply simp - apply (rule lem0) - apply force - apply (rule elem_le_sum) - apply force + apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev) + apply (fastforce simp add: listsum_map_remove1) apply clarify apply (rule assms) apply (erule allE, erule impE) @@ -128,8 +126,8 @@ apply (rule le_imp_less_Suc) apply (rule trans_le_add1) apply (rule trans_le_add2) - apply (rule elem_le_sum) - apply force + apply (simp only: foldl_conv_fold add_commute fold_plus_listsum_rev) + apply (simp add: member_le_listsum_nat) done theorem Apps_dB_induct: @@ -143,3 +141,4 @@ done end +