src/HOL/Library/More_List.thy

   "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
   by (induct xs arbitrary: s) simp_all
 
 lemma foldr_fold_rev:
   "foldr f xs = fold f (rev xs)"
-  by (simp add: foldr_foldl foldl_fold ext_iff)
+  by (simp add: foldr_foldl foldl_fold fun_eq_iff)
 
 lemma fold_rev_conv [code_unfold]:
   "fold f (rev xs) = foldr f xs"
   by (simp add: foldr_fold_rev)
   

   using assms by (induct xs) simp_all
 
 lemma fold_apply:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   shows "h \<circ> fold g xs = fold f xs \<circ> h"
-  using assms by (induct xs) (simp_all add: ext_iff)
+  using assms by (induct xs) (simp_all add: fun_eq_iff)
 
 lemma fold_invariant: 
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
     and "\<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s)"
   shows "P (fold f xs s)"

     by (simp add: Inf_fin_def fold1_set del: set.simps)
 qed
 
 lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
   "Inf_fin (set (x # xs)) = foldr inf xs x"
-  by (simp add: Inf_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
+  by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
 
 lemma (in lattice) Sup_fin_set_fold:
   "Sup_fin (set (x # xs)) = fold sup xs x"
 proof -
   interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

     by (simp add: Sup_fin_def fold1_set del: set.simps)
 qed
 
 lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
   "Sup_fin (set (x # xs)) = foldr sup xs x"
-  by (simp add: Sup_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
+  by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
 
 lemma (in linorder) Min_fin_set_fold:
   "Min (set (x # xs)) = fold min xs x"
 proof -
   interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

     by (simp add: Min_def fold1_set del: set.simps)
 qed
 
 lemma (in linorder) Min_fin_set_foldr [code_unfold]:
   "Min (set (x # xs)) = foldr min xs x"
-  by (simp add: Min_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
+  by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
 
 lemma (in linorder) Max_fin_set_fold:
   "Max (set (x # xs)) = fold max xs x"
 proof -
   interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

     by (simp add: Max_def fold1_set del: set.simps)
 qed
 
 lemma (in linorder) Max_fin_set_foldr [code_unfold]:
   "Max (set (x # xs)) = foldr max xs x"
-  by (simp add: Max_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
+  by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps)
 
 lemma (in complete_lattice) Inf_set_fold:
   "Inf (set xs) = fold inf xs top"
 proof -
   interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

   show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
 qed
 
 lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
   "Inf (set xs) = foldr inf xs top"
-  by (simp add: Inf_set_fold ac_simps foldr_fold ext_iff)
+  by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff)
 
 lemma (in complete_lattice) Sup_set_fold:
   "Sup (set xs) = fold sup xs bot"
 proof -
   interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

   show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
 qed
 
 lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
   "Sup (set xs) = foldr sup xs bot"
-  by (simp add: Sup_set_fold ac_simps foldr_fold ext_iff)
+  by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff)
 
 lemma (in complete_lattice) INFI_set_fold:
   "INFI (set xs) f = fold (inf \<circ> f) xs top"
   unfolding INFI_def set_map [symmetric] Inf_set_fold fold_map ..