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"
```