src/HOL/Library/More_List.thy
changeset 39198 f967a16dfcdd
parent 37028 a6e0696d7110
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Library/More_List.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Library/More_List.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  
     1.5  lemma foldr_fold_rev:
     1.6    "foldr f xs = fold f (rev xs)"
     1.7 -  by (simp add: foldr_foldl foldl_fold expand_fun_eq)
     1.8 +  by (simp add: foldr_foldl foldl_fold ext_iff)
     1.9  
    1.10  lemma fold_rev_conv [code_unfold]:
    1.11    "fold f (rev xs) = foldr f xs"
    1.12 @@ -49,7 +49,7 @@
    1.13  lemma fold_apply:
    1.14    assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
    1.15    shows "h \<circ> fold g xs = fold f xs \<circ> h"
    1.16 -  using assms by (induct xs) (simp_all add: expand_fun_eq)
    1.17 +  using assms by (induct xs) (simp_all add: ext_iff)
    1.18  
    1.19  lemma fold_invariant: 
    1.20    assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
    1.21 @@ -164,7 +164,7 @@
    1.22  
    1.23  lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
    1.24    "Inf_fin (set (x # xs)) = foldr inf xs x"
    1.25 -  by (simp add: Inf_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
    1.26 +  by (simp add: Inf_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
    1.27  
    1.28  lemma (in lattice) Sup_fin_set_fold:
    1.29    "Sup_fin (set (x # xs)) = fold sup xs x"
    1.30 @@ -177,7 +177,7 @@
    1.31  
    1.32  lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
    1.33    "Sup_fin (set (x # xs)) = foldr sup xs x"
    1.34 -  by (simp add: Sup_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
    1.35 +  by (simp add: Sup_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
    1.36  
    1.37  lemma (in linorder) Min_fin_set_fold:
    1.38    "Min (set (x # xs)) = fold min xs x"
    1.39 @@ -190,7 +190,7 @@
    1.40  
    1.41  lemma (in linorder) Min_fin_set_foldr [code_unfold]:
    1.42    "Min (set (x # xs)) = foldr min xs x"
    1.43 -  by (simp add: Min_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
    1.44 +  by (simp add: Min_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
    1.45  
    1.46  lemma (in linorder) Max_fin_set_fold:
    1.47    "Max (set (x # xs)) = fold max xs x"
    1.48 @@ -203,7 +203,7 @@
    1.49  
    1.50  lemma (in linorder) Max_fin_set_foldr [code_unfold]:
    1.51    "Max (set (x # xs)) = foldr max xs x"
    1.52 -  by (simp add: Max_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
    1.53 +  by (simp add: Max_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
    1.54  
    1.55  lemma (in complete_lattice) Inf_set_fold:
    1.56    "Inf (set xs) = fold inf xs top"
    1.57 @@ -215,7 +215,7 @@
    1.58  
    1.59  lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
    1.60    "Inf (set xs) = foldr inf xs top"
    1.61 -  by (simp add: Inf_set_fold ac_simps foldr_fold expand_fun_eq)
    1.62 +  by (simp add: Inf_set_fold ac_simps foldr_fold ext_iff)
    1.63  
    1.64  lemma (in complete_lattice) Sup_set_fold:
    1.65    "Sup (set xs) = fold sup xs bot"
    1.66 @@ -227,7 +227,7 @@
    1.67  
    1.68  lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
    1.69    "Sup (set xs) = foldr sup xs bot"
    1.70 -  by (simp add: Sup_set_fold ac_simps foldr_fold expand_fun_eq)
    1.71 +  by (simp add: Sup_set_fold ac_simps foldr_fold ext_iff)
    1.72  
    1.73  lemma (in complete_lattice) INFI_set_fold:
    1.74    "INFI (set xs) f = fold (inf \<circ> f) xs top"