expand_fun_eq -> ext_iff
authornipkow
Tue Sep 07 10:05:19 2010 +0200 (2010-09-07)
changeset 39198f967a16dfcdd
parent 39166 19efc2af3e6c
child 39199 720112792ba0
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
src/HOL/Bali/Example.thy
src/HOL/Bali/Table.thy
src/HOL/Big_Operators.thy
src/HOL/Datatype.thy
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hoare/SchorrWaite.thy
src/HOL/IMP/Live.thy
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Import/HOL/bool.imp
src/HOL/Import/HOL/prob_extra.imp
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Library/AssocList.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Code_Char_chr.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Enum.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Fset.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Function_Algebras.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/More_List.thy
src/HOL/Library/More_Set.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Order_Relation.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Quotient_List.thy
src/HOL/Library/Quotient_Option.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Library/RBT.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Limits.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/MicroJava/Comp/AuxLemmas.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Determinants.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/NatStar.thy
src/HOL/NSA/Star.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/Nat_Transfer.thy
src/HOL/Nitpick.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nominal/Examples/Class1.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Predicate.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
src/HOL/Probability/Borel.thy
src/HOL/Probability/Euclidean_Lebesgue.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Positive_Infinite_Real.thy
src/HOL/Probability/Probability_Space.thy
src/HOL/Product_Type.thy
src/HOL/Quotient.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Random.thy
src/HOL/Recdef.thy
src/HOL/Set.thy
src/HOL/SetInterval.thy
src/HOL/String.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Sledgehammer/clausifier.ML
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Lift_prog.thy
src/HOL/Word/Word.thy
src/HOL/ZF/HOLZF.thy
src/HOL/ex/Execute_Choice.thy
src/HOL/ex/Landau.thy
src/HOL/ex/Summation.thy
     1.1 --- a/src/HOL/Bali/Example.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -792,7 +792,7 @@
     1.4  lemma Base_fields_accessible[simp]:
     1.5   "accfield tprg S Base 
     1.6    = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
     1.7 -apply (auto simp add: accfield_def expand_fun_eq Let_def 
     1.8 +apply (auto simp add: accfield_def ext_iff Let_def 
     1.9                        accessible_in_RefT_simp
    1.10                        is_public_def
    1.11                        BaseCl_def
    1.12 @@ -837,7 +837,7 @@
    1.13  lemma Ext_fields_accessible[simp]:
    1.14  "accfield tprg S Ext 
    1.15    = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
    1.16 -apply (auto simp add: accfield_def expand_fun_eq Let_def 
    1.17 +apply (auto simp add: accfield_def ext_iff Let_def 
    1.18                        accessible_in_RefT_simp
    1.19                        is_public_def
    1.20                        BaseCl_def
     2.1 --- a/src/HOL/Bali/Table.thy	Mon Sep 06 22:58:06 2010 +0200
     2.2 +++ b/src/HOL/Bali/Table.thy	Tue Sep 07 10:05:19 2010 +0200
     2.3 @@ -65,10 +65,10 @@
     2.4                                           else Some old_val))))"
     2.5  
     2.6  lemma cond_override_empty1[simp]: "cond_override c empty t = t"
     2.7 -by (simp add: cond_override_def expand_fun_eq)
     2.8 +by (simp add: cond_override_def ext_iff)
     2.9  
    2.10  lemma cond_override_empty2[simp]: "cond_override c t empty = t"
    2.11 -by (simp add: cond_override_def expand_fun_eq)
    2.12 +by (simp add: cond_override_def ext_iff)
    2.13  
    2.14  lemma cond_override_None[simp]:
    2.15   "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
    2.16 @@ -105,10 +105,10 @@
    2.17  by (simp add: filter_tab_def empty_def)
    2.18  
    2.19  lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
    2.20 -by (simp add: expand_fun_eq filter_tab_def)
    2.21 +by (simp add: ext_iff filter_tab_def)
    2.22  
    2.23  lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
    2.24 -by (simp add: expand_fun_eq filter_tab_def empty_def)
    2.25 +by (simp add: ext_iff filter_tab_def empty_def)
    2.26  
    2.27  lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
    2.28  by (auto simp add: filter_tab_def ran_def)
    2.29 @@ -134,26 +134,26 @@
    2.30  
    2.31  lemma filter_tab_all_True: 
    2.32   "\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t"
    2.33 -apply (auto simp add: filter_tab_def expand_fun_eq)
    2.34 +apply (auto simp add: filter_tab_def ext_iff)
    2.35  done
    2.36  
    2.37  lemma filter_tab_all_True_Some:
    2.38   "\<lbrakk>\<forall> k y. t k = Some y \<longrightarrow> p k y; t k = Some v\<rbrakk> \<Longrightarrow> filter_tab p t k = Some v"
    2.39 -by (auto simp add: filter_tab_def expand_fun_eq)
    2.40 +by (auto simp add: filter_tab_def ext_iff)
    2.41  
    2.42  lemma filter_tab_all_False: 
    2.43   "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
    2.44 -by (auto simp add: filter_tab_def expand_fun_eq)
    2.45 +by (auto simp add: filter_tab_def ext_iff)
    2.46  
    2.47  lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
    2.48 -apply (simp add: filter_tab_def expand_fun_eq)
    2.49 +apply (simp add: filter_tab_def ext_iff)
    2.50  done
    2.51  
    2.52  lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"
    2.53  by (auto simp add: filter_tab_def dom_def)
    2.54  
    2.55  lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b"
    2.56 -by (auto simp add: expand_fun_eq filter_tab_def)
    2.57 +by (auto simp add: ext_iff filter_tab_def)
    2.58  
    2.59  lemma finite_dom_filter_tab:
    2.60  "finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"
    2.61 @@ -175,7 +175,7 @@
    2.62     \<rbrakk> \<Longrightarrow>
    2.63      cond_override overC (filter_tab filterC t) (filter_tab filterC s) 
    2.64      = filter_tab filterC (cond_override overC t s)"
    2.65 -by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
    2.66 +by (auto simp add: ext_iff cond_override_def filter_tab_def )
    2.67  
    2.68  
    2.69  section {* Misc. *}
     3.1 --- a/src/HOL/Big_Operators.thy	Mon Sep 06 22:58:06 2010 +0200
     3.2 +++ b/src/HOL/Big_Operators.thy	Tue Sep 07 10:05:19 2010 +0200
     3.3 @@ -1504,11 +1504,11 @@
     3.4  
     3.5  lemma dual_max:
     3.6    "ord.max (op \<ge>) = min"
     3.7 -  by (auto simp add: ord.max_def_raw min_def expand_fun_eq)
     3.8 +  by (auto simp add: ord.max_def_raw min_def ext_iff)
     3.9  
    3.10  lemma dual_min:
    3.11    "ord.min (op \<ge>) = max"
    3.12 -  by (auto simp add: ord.min_def_raw max_def expand_fun_eq)
    3.13 +  by (auto simp add: ord.min_def_raw max_def ext_iff)
    3.14  
    3.15  lemma strict_below_fold1_iff:
    3.16    assumes "finite A" and "A \<noteq> {}"
     4.1 --- a/src/HOL/Datatype.thy	Mon Sep 06 22:58:06 2010 +0200
     4.2 +++ b/src/HOL/Datatype.thy	Tue Sep 07 10:05:19 2010 +0200
     4.3 @@ -109,12 +109,12 @@
     4.4  (** Push -- an injection, analogous to Cons on lists **)
     4.5  
     4.6  lemma Push_inject1: "Push i f = Push j g  ==> i=j"
     4.7 -apply (simp add: Push_def expand_fun_eq) 
     4.8 +apply (simp add: Push_def ext_iff) 
     4.9  apply (drule_tac x=0 in spec, simp) 
    4.10  done
    4.11  
    4.12  lemma Push_inject2: "Push i f = Push j g  ==> f=g"
    4.13 -apply (auto simp add: Push_def expand_fun_eq) 
    4.14 +apply (auto simp add: Push_def ext_iff) 
    4.15  apply (drule_tac x="Suc x" in spec, simp) 
    4.16  done
    4.17  
    4.18 @@ -123,7 +123,7 @@
    4.19  by (blast dest: Push_inject1 Push_inject2) 
    4.20  
    4.21  lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
    4.22 -by (auto simp add: Push_def expand_fun_eq split: nat.split_asm)
    4.23 +by (auto simp add: Push_def ext_iff split: nat.split_asm)
    4.24  
    4.25  lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard]
    4.26  
    4.27 @@ -399,7 +399,7 @@
    4.28  lemma ntrunc_o_equality: 
    4.29      "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2"
    4.30  apply (rule ntrunc_equality [THEN ext])
    4.31 -apply (simp add: expand_fun_eq) 
    4.32 +apply (simp add: ext_iff) 
    4.33  done
    4.34  
    4.35  
     5.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Mon Sep 06 22:58:06 2010 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Tue Sep 07 10:05:19 2010 +0200
     5.3 @@ -342,7 +342,7 @@
     5.4  
     5.5  lemma UNIV_nat_infinite: "\<not> finite (UNIV :: nat set)"
     5.6    unfolding finite_conv_nat_seg_image
     5.7 -proof(auto simp add: expand_set_eq image_iff)
     5.8 +proof(auto simp add: set_ext_iff image_iff)
     5.9    fix n::nat and f:: "nat \<Rightarrow> nat"
    5.10    let ?N = "{i. i < n}"
    5.11    let ?fN = "f ` ?N"
     6.1 --- a/src/HOL/Finite_Set.thy	Mon Sep 06 22:58:06 2010 +0200
     6.2 +++ b/src/HOL/Finite_Set.thy	Tue Sep 07 10:05:19 2010 +0200
     6.3 @@ -541,7 +541,7 @@
     6.4  qed (simp add: UNIV_option_conv)
     6.5  
     6.6  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
     6.7 -  by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq)
     6.8 +  by (rule inj_onI, auto simp add: set_ext_iff ext_iff)
     6.9  
    6.10  instance "fun" :: (finite, finite) finite
    6.11  proof
    6.12 @@ -576,7 +576,7 @@
    6.13  text{* On a functional level it looks much nicer: *}
    6.14  
    6.15  lemma fun_comp_comm:  "f x \<circ> f y = f y \<circ> f x"
    6.16 -by (simp add: fun_left_comm expand_fun_eq)
    6.17 +by (simp add: fun_left_comm ext_iff)
    6.18  
    6.19  end
    6.20  
    6.21 @@ -720,7 +720,7 @@
    6.22  
    6.23  text{* The nice version: *}
    6.24  lemma fun_comp_idem : "f x o f x = f x"
    6.25 -by (simp add: fun_left_idem expand_fun_eq)
    6.26 +by (simp add: fun_left_idem ext_iff)
    6.27  
    6.28  lemma fold_insert_idem:
    6.29    assumes fin: "finite A"
    6.30 @@ -1363,17 +1363,17 @@
    6.31  
    6.32  lemma empty [simp]:
    6.33    "F {} = id"
    6.34 -  by (simp add: eq_fold expand_fun_eq)
    6.35 +  by (simp add: eq_fold ext_iff)
    6.36  
    6.37  lemma insert [simp]:
    6.38    assumes "finite A" and "x \<notin> A"
    6.39    shows "F (insert x A) = F A \<circ> f x"
    6.40  proof -
    6.41    interpret fun_left_comm f proof
    6.42 -  qed (insert commute_comp, simp add: expand_fun_eq)
    6.43 +  qed (insert commute_comp, simp add: ext_iff)
    6.44    from fold_insert2 assms
    6.45    have "\<And>s. fold f s (insert x A) = fold f (f x s) A" .
    6.46 -  with `finite A` show ?thesis by (simp add: eq_fold expand_fun_eq)
    6.47 +  with `finite A` show ?thesis by (simp add: eq_fold ext_iff)
    6.48  qed
    6.49  
    6.50  lemma remove:
    6.51 @@ -1736,14 +1736,14 @@
    6.52    then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
    6.53    with `finite A` have "finite B" by simp
    6.54    interpret fold: folding "op *" "\<lambda>a b. fold (op *) b a" proof
    6.55 -  qed (simp_all add: expand_fun_eq ac_simps)
    6.56 -  thm fold.commute_comp' [of B b, simplified expand_fun_eq, simplified]
    6.57 +  qed (simp_all add: ext_iff ac_simps)
    6.58 +  thm fold.commute_comp' [of B b, simplified ext_iff, simplified]
    6.59    from `finite B` fold.commute_comp' [of B x]
    6.60      have "op * x \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> op * x" by simp
    6.61 -  then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: expand_fun_eq commute)
    6.62 +  then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: ext_iff commute)
    6.63    from `finite B` * fold.insert [of B b]
    6.64      have "(\<lambda>x. fold op * x (insert b B)) = (\<lambda>x. fold op * x B) \<circ> op * b" by simp
    6.65 -  then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: expand_fun_eq)
    6.66 +  then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: ext_iff)
    6.67    from A B assms * show ?thesis by (simp add: eq_fold' del: fold.insert)
    6.68  qed
    6.69  
     7.1 --- a/src/HOL/Fun.thy	Mon Sep 06 22:58:06 2010 +0200
     7.2 +++ b/src/HOL/Fun.thy	Tue Sep 07 10:05:19 2010 +0200
     7.3 @@ -11,7 +11,7 @@
     7.4  
     7.5  text{*As a simplification rule, it replaces all function equalities by
     7.6    first-order equalities.*}
     7.7 -lemma expand_fun_eq: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
     7.8 +lemma ext_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
     7.9  apply (rule iffI)
    7.10  apply (simp (no_asm_simp))
    7.11  apply (rule ext)
    7.12 @@ -163,7 +163,7 @@
    7.13    by (simp add: inj_on_def)
    7.14  
    7.15  lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
    7.16 -  by (simp add: inj_on_def expand_fun_eq)
    7.17 +  by (simp add: inj_on_def ext_iff)
    7.18  
    7.19  lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
    7.20  by (simp add: inj_on_eq_iff)
    7.21 @@ -463,7 +463,7 @@
    7.22  by simp
    7.23  
    7.24  lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)"
    7.25 -by (simp add: expand_fun_eq)
    7.26 +by (simp add: ext_iff)
    7.27  
    7.28  lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
    7.29  by (rule ext, auto)
    7.30 @@ -515,7 +515,7 @@
    7.31  lemma swap_triple:
    7.32    assumes "a \<noteq> c" and "b \<noteq> c"
    7.33    shows "swap a b (swap b c (swap a b f)) = swap a c f"
    7.34 -  using assms by (simp add: expand_fun_eq swap_def)
    7.35 +  using assms by (simp add: ext_iff swap_def)
    7.36  
    7.37  lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
    7.38  by (rule ext, simp add: fun_upd_def swap_def)
     8.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Sep 06 22:58:06 2010 +0200
     8.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Sep 07 10:05:19 2010 +0200
     8.3 @@ -138,7 +138,7 @@
     8.4  qed
     8.5  
     8.6  lemma inj_iff: "(inj f) = (inv f o f = id)"
     8.7 -apply (simp add: o_def expand_fun_eq)
     8.8 +apply (simp add: o_def ext_iff)
     8.9  apply (blast intro: inj_on_inverseI inv_into_f_f)
    8.10  done
    8.11  
    8.12 @@ -178,7 +178,7 @@
    8.13  by (simp add: inj_on_inv_into surj_range)
    8.14  
    8.15  lemma surj_iff: "(surj f) = (f o inv f = id)"
    8.16 -apply (simp add: o_def expand_fun_eq)
    8.17 +apply (simp add: o_def ext_iff)
    8.18  apply (blast intro: surjI surj_f_inv_f)
    8.19  done
    8.20  
     9.1 --- a/src/HOL/Hoare/SchorrWaite.thy	Mon Sep 06 22:58:06 2010 +0200
     9.2 +++ b/src/HOL/Hoare/SchorrWaite.thy	Tue Sep 07 10:05:19 2010 +0200
     9.3 @@ -239,7 +239,7 @@
     9.4      from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+
     9.5      from pNull i1 have stackEmpty: "stack = []" by simp
     9.6      from tDisj i4 have RisMarked[rule_format]: "\<forall>x.  x \<in> R \<longrightarrow> m x"  by(auto simp: reachable_def addrs_def stackEmpty)
     9.7 -    from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL"  by(auto simp: stackEmpty expand_fun_eq intro:RisMarked)
     9.8 +    from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL"  by(auto simp: stackEmpty ext_iff intro:RisMarked)
     9.9  
    9.10    next   
    9.11        fix c m l r t p q root
    10.1 --- a/src/HOL/IMP/Live.thy	Mon Sep 06 22:58:06 2010 +0200
    10.2 +++ b/src/HOL/IMP/Live.thy	Tue Sep 07 10:05:19 2010 +0200
    10.3 @@ -8,7 +8,7 @@
    10.4  consts Dep :: "((loc \<Rightarrow> 'a) \<Rightarrow> 'b) \<Rightarrow> loc set"
    10.5  specification (Dep)
    10.6  dep_on: "(\<forall>x\<in>Dep e. s x = t x) \<Longrightarrow> e s = e t"
    10.7 -by(rule_tac x="%x. UNIV" in exI)(simp add: expand_fun_eq[symmetric])
    10.8 +by(rule_tac x="%x. UNIV" in exI)(simp add: ext_iff[symmetric])
    10.9  
   10.10  text{* The following definition of @{const Dep} looks very tempting
   10.11  @{prop"Dep e = {a. EX s t. (ALL x. x\<noteq>a \<longrightarrow> s x = t x) \<and> e s \<noteq> e t}"}
    11.1 --- a/src/HOL/Imperative_HOL/Array.thy	Mon Sep 06 22:58:06 2010 +0200
    11.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Sep 07 10:05:19 2010 +0200
    11.3 @@ -99,7 +99,7 @@
    11.4  
    11.5  lemma set_set_swap:
    11.6    "r =!!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)"
    11.7 -  by (simp add: Let_def expand_fun_eq noteq_def set_def)
    11.8 +  by (simp add: Let_def ext_iff noteq_def set_def)
    11.9  
   11.10  lemma get_update_eq [simp]:
   11.11    "get (update a i v h) a = (get h a) [i := v]"
   11.12 @@ -115,7 +115,7 @@
   11.13  
   11.14  lemma length_update [simp]: 
   11.15    "length (update b i v h) = length h"
   11.16 -  by (simp add: update_def length_def set_def get_def expand_fun_eq)
   11.17 +  by (simp add: update_def length_def set_def get_def ext_iff)
   11.18  
   11.19  lemma update_swap_neq:
   11.20    "a =!!= a' \<Longrightarrow> 
   11.21 @@ -145,7 +145,7 @@
   11.22  
   11.23  lemma present_update [simp]: 
   11.24    "present (update b i v h) = present h"
   11.25 -  by (simp add: update_def present_def set_def get_def expand_fun_eq)
   11.26 +  by (simp add: update_def present_def set_def get_def ext_iff)
   11.27  
   11.28  lemma present_alloc [simp]:
   11.29    "present (snd (alloc xs h)) (fst (alloc xs h))"
    12.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Sep 06 22:58:06 2010 +0200
    12.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Sep 07 10:05:19 2010 +0200
    12.3 @@ -31,7 +31,7 @@
    12.4  
    12.5  lemma Heap_eqI:
    12.6    "(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"
    12.7 -    by (cases f, cases g) (auto simp: expand_fun_eq)
    12.8 +    by (cases f, cases g) (auto simp: ext_iff)
    12.9  
   12.10  ML {* structure Execute_Simps = Named_Thms(
   12.11    val name = "execute_simps"
    13.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Mon Sep 06 22:58:06 2010 +0200
    13.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Sep 07 10:05:19 2010 +0200
    13.3 @@ -98,7 +98,7 @@
    13.4  
    13.5  lemma set_set_swap:
    13.6    "r =!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)"
    13.7 -  by (simp add: noteq_def set_def expand_fun_eq)
    13.8 +  by (simp add: noteq_def set_def ext_iff)
    13.9  
   13.10  lemma alloc_set:
   13.11    "fst (alloc x (set r x' h)) = fst (alloc x h)"
   13.12 @@ -126,7 +126,7 @@
   13.13  
   13.14  lemma present_set [simp]:
   13.15    "present (set r v h) = present h"
   13.16 -  by (simp add: present_def expand_fun_eq)
   13.17 +  by (simp add: present_def ext_iff)
   13.18  
   13.19  lemma noteq_I:
   13.20    "present h r \<Longrightarrow> \<not> present h r' \<Longrightarrow> r =!= r'"
   13.21 @@ -220,7 +220,7 @@
   13.22  
   13.23  lemma array_get_set [simp]:
   13.24    "Array.get (set r v h) = Array.get h"
   13.25 -  by (simp add: Array.get_def set_def expand_fun_eq)
   13.26 +  by (simp add: Array.get_def set_def ext_iff)
   13.27  
   13.28  lemma get_update [simp]:
   13.29    "get (Array.update a i v h) r = get h r"
   13.30 @@ -240,15 +240,15 @@
   13.31  
   13.32  lemma array_get_alloc [simp]: 
   13.33    "Array.get (snd (alloc v h)) = Array.get h"
   13.34 -  by (simp add: Array.get_def alloc_def set_def Let_def expand_fun_eq)
   13.35 +  by (simp add: Array.get_def alloc_def set_def Let_def ext_iff)
   13.36  
   13.37  lemma present_update [simp]: 
   13.38    "present (Array.update a i v h) = present h"
   13.39 -  by (simp add: Array.update_def Array.set_def expand_fun_eq present_def)
   13.40 +  by (simp add: Array.update_def Array.set_def ext_iff present_def)
   13.41  
   13.42  lemma array_present_set [simp]:
   13.43    "Array.present (set r v h) = Array.present h"
   13.44 -  by (simp add: Array.present_def set_def expand_fun_eq)
   13.45 +  by (simp add: Array.present_def set_def ext_iff)
   13.46  
   13.47  lemma array_present_alloc [simp]:
   13.48    "Array.present h a \<Longrightarrow> Array.present (snd (alloc v h)) a"
    14.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Sep 06 22:58:06 2010 +0200
    14.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Tue Sep 07 10:05:19 2010 +0200
    14.3 @@ -550,7 +550,7 @@
    14.4    }"
    14.5    unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
    14.6  thm arg_cong2
    14.7 -  by (auto simp add: expand_fun_eq intro: arg_cong2[where f = bind] split: node.split)
    14.8 +  by (auto simp add: ext_iff intro: arg_cong2[where f = bind] split: node.split)
    14.9  
   14.10  primrec rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
   14.11  where
    15.1 --- a/src/HOL/Import/HOL/bool.imp	Mon Sep 06 22:58:06 2010 +0200
    15.2 +++ b/src/HOL/Import/HOL/bool.imp	Tue Sep 07 10:05:19 2010 +0200
    15.3 @@ -124,7 +124,7 @@
    15.4    "IMP_ANTISYM_AX" > "HOL4Setup.light_imp_as"
    15.5    "F_IMP" > "HOL4Base.bool.F_IMP"
    15.6    "F_DEF" > "HOL.False_def"
    15.7 -  "FUN_EQ_THM" > "Fun.expand_fun_eq"
    15.8 +  "FUN_EQ_THM" > "Fun.ext_iff"
    15.9    "FORALL_THM" > "HOL4Base.bool.FORALL_THM"
   15.10    "FORALL_SIMP" > "HOL.simp_thms_35"
   15.11    "FORALL_DEF" > "HOL.All_def"
    16.1 --- a/src/HOL/Import/HOL/prob_extra.imp	Mon Sep 06 22:58:06 2010 +0200
    16.2 +++ b/src/HOL/Import/HOL/prob_extra.imp	Tue Sep 07 10:05:19 2010 +0200
    16.3 @@ -73,7 +73,7 @@
    16.4    "EVEN_ODD_EXISTS_EQ" > "HOL4Prob.prob_extra.EVEN_ODD_EXISTS_EQ"
    16.5    "EVEN_ODD_BASIC" > "HOL4Prob.prob_extra.EVEN_ODD_BASIC"
    16.6    "EVEN_EXP_TWO" > "HOL4Prob.prob_extra.EVEN_EXP_TWO"
    16.7 -  "EQ_EXT_EQ" > "Fun.expand_fun_eq"
    16.8 +  "EQ_EXT_EQ" > "Fun.ext_iff"
    16.9    "DIV_TWO_UNIQUE" > "HOL4Prob.prob_extra.DIV_TWO_UNIQUE"
   16.10    "DIV_TWO_MONO_EVEN" > "HOL4Prob.prob_extra.DIV_TWO_MONO_EVEN"
   16.11    "DIV_TWO_MONO" > "HOL4Prob.prob_extra.DIV_TWO_MONO"
    17.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Mon Sep 06 22:58:06 2010 +0200
    17.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Tue Sep 07 10:05:19 2010 +0200
    17.3 @@ -1394,7 +1394,7 @@
    17.4    "GSPEC_def" > "HOLLight.hollight.GSPEC_def"
    17.5    "GEQ_def" > "HOLLight.hollight.GEQ_def"
    17.6    "GABS_def" > "HOLLight.hollight.GABS_def"
    17.7 -  "FUN_EQ_THM" > "Fun.expand_fun_eq"
    17.8 +  "FUN_EQ_THM" > "Fun.ext_iff"
    17.9    "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
   17.10    "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
   17.11    "FSTCART_PASTECART" > "HOLLight.hollight.FSTCART_PASTECART"
    18.1 --- a/src/HOL/Library/AssocList.thy	Mon Sep 06 22:58:06 2010 +0200
    18.2 +++ b/src/HOL/Library/AssocList.thy	Tue Sep 07 10:05:19 2010 +0200
    18.3 @@ -22,7 +22,7 @@
    18.4    | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    18.5  
    18.6  lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
    18.7 -  by (induct al) (auto simp add: expand_fun_eq)
    18.8 +  by (induct al) (auto simp add: ext_iff)
    18.9  
   18.10  corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\<mapsto>v)) k'"
   18.11    by (simp add: update_conv')
   18.12 @@ -67,7 +67,7 @@
   18.13          @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*}
   18.14  lemma update_swap: "k\<noteq>k' 
   18.15    \<Longrightarrow> map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))"
   18.16 -  by (simp add: update_conv' expand_fun_eq)
   18.17 +  by (simp add: update_conv' ext_iff)
   18.18  
   18.19  lemma update_Some_unfold: 
   18.20    "map_of (update k v al) x = Some y \<longleftrightarrow>
   18.21 @@ -96,8 +96,8 @@
   18.22  proof -
   18.23    have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
   18.24      More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> map_of"
   18.25 -    by (rule fold_apply) (auto simp add: expand_fun_eq update_conv')
   18.26 -  then show ?thesis by (auto simp add: updates_def expand_fun_eq map_upds_fold_map_upd foldl_fold split_def)
   18.27 +    by (rule fold_apply) (auto simp add: ext_iff update_conv')
   18.28 +  then show ?thesis by (auto simp add: updates_def ext_iff map_upds_fold_map_upd foldl_fold split_def)
   18.29  qed
   18.30  
   18.31  lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\<mapsto>]vs)) k"
   18.32 @@ -114,7 +114,7 @@
   18.33    moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
   18.34      More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> map fst"
   18.35      by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def)
   18.36 -  ultimately show ?thesis by (simp add: updates_def expand_fun_eq)
   18.37 +  ultimately show ?thesis by (simp add: updates_def ext_iff)
   18.38  qed
   18.39  
   18.40  lemma updates_append1[simp]: "size ks < size vs \<Longrightarrow>
   18.41 @@ -161,7 +161,7 @@
   18.42    by (auto simp add: delete_eq)
   18.43  
   18.44  lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)"
   18.45 -  by (induct al) (auto simp add: expand_fun_eq)
   18.46 +  by (induct al) (auto simp add: ext_iff)
   18.47  
   18.48  corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'"
   18.49    by (simp add: delete_conv')
   18.50 @@ -301,7 +301,7 @@
   18.51  lemma map_of_clearjunk:
   18.52    "map_of (clearjunk al) = map_of al"
   18.53    by (induct al rule: clearjunk.induct)
   18.54 -    (simp_all add: expand_fun_eq)
   18.55 +    (simp_all add: ext_iff)
   18.56  
   18.57  lemma clearjunk_keys_set:
   18.58    "set (map fst (clearjunk al)) = set (map fst al)"
   18.59 @@ -342,7 +342,7 @@
   18.60    have "clearjunk \<circ> More_List.fold (prod_case update) (zip ks vs) =
   18.61      More_List.fold (prod_case update) (zip ks vs) \<circ> clearjunk"
   18.62      by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def)
   18.63 -  then show ?thesis by (simp add: updates_def expand_fun_eq)
   18.64 +  then show ?thesis by (simp add: updates_def ext_iff)
   18.65  qed
   18.66  
   18.67  lemma clearjunk_delete:
   18.68 @@ -446,9 +446,9 @@
   18.69  proof -
   18.70    have "map_of \<circ> More_List.fold (prod_case update) (rev ys) =
   18.71      More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
   18.72 -    by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
   18.73 +    by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def ext_iff)
   18.74    then show ?thesis
   18.75 -    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq)
   18.76 +    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev ext_iff)
   18.77  qed
   18.78  
   18.79  corollary merge_conv:
   18.80 @@ -699,7 +699,7 @@
   18.81  
   18.82  lemma bulkload_Mapping [code]:
   18.83    "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
   18.84 -  by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
   18.85 +  by (rule mapping_eqI) (simp add: map_of_map_restrict ext_iff)
   18.86  
   18.87  lemma map_of_eqI: (*FIXME move to Map.thy*)
   18.88    assumes set_eq: "set (map fst xs) = set (map fst ys)"
    19.1 --- a/src/HOL/Library/Binomial.thy	Mon Sep 06 22:58:06 2010 +0200
    19.2 +++ b/src/HOL/Library/Binomial.thy	Tue Sep 07 10:05:19 2010 +0200
    19.3 @@ -236,7 +236,7 @@
    19.4      have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
    19.5        (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
    19.6        apply (rule setprod_reindex_cong [where f = Suc])
    19.7 -      using n0 by (auto simp add: expand_fun_eq field_simps)
    19.8 +      using n0 by (auto simp add: ext_iff field_simps)
    19.9      have ?thesis apply (simp add: pochhammer_def)
   19.10      unfolding setprod_insert[OF th0, unfolded eq]
   19.11      using th1 by (simp add: field_simps)}
   19.12 @@ -248,7 +248,7 @@
   19.13    
   19.14    apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod)
   19.15    apply (rule setprod_reindex_cong[where f=Suc])
   19.16 -  by (auto simp add: expand_fun_eq)
   19.17 +  by (auto simp add: ext_iff)
   19.18  
   19.19  lemma pochhammer_of_nat_eq_0_lemma: assumes kn: "k > n"
   19.20    shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
   19.21 @@ -315,7 +315,7 @@
   19.22        apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
   19.23        apply (auto simp add: inj_on_def image_def h )
   19.24        apply (rule_tac x="h - x" in bexI)
   19.25 -      by (auto simp add: expand_fun_eq h of_nat_diff)}
   19.26 +      by (auto simp add: ext_iff h of_nat_diff)}
   19.27    ultimately show ?thesis by (cases k, auto)
   19.28  qed
   19.29  
   19.30 @@ -410,11 +410,11 @@
   19.31      have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
   19.32        apply (rule strong_setprod_reindex_cong[where f="op - n"])
   19.33        using h kn 
   19.34 -      apply (simp_all add: inj_on_def image_iff Bex_def expand_set_eq)
   19.35 +      apply (simp_all add: inj_on_def image_iff Bex_def set_ext_iff)
   19.36        apply clarsimp
   19.37        apply (presburger)
   19.38        apply presburger
   19.39 -      by (simp add: expand_fun_eq field_simps of_nat_add[symmetric] del: of_nat_add)
   19.40 +      by (simp add: ext_iff field_simps of_nat_add[symmetric] del: of_nat_add)
   19.41      have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" 
   19.42  "{1..n - Suc h} \<inter> {n - h .. n} = {}" and eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}" using h kn by auto
   19.43      from eq[symmetric]
    20.1 --- a/src/HOL/Library/Code_Char_chr.thy	Mon Sep 06 22:58:06 2010 +0200
    20.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Tue Sep 07 10:05:19 2010 +0200
    20.3 @@ -13,14 +13,14 @@
    20.4  
    20.5  lemma [code]:
    20.6    "nat_of_char = nat o int_of_char"
    20.7 -  unfolding int_of_char_def by (simp add: expand_fun_eq)
    20.8 +  unfolding int_of_char_def by (simp add: ext_iff)
    20.9  
   20.10  definition
   20.11    "char_of_int = char_of_nat o nat"
   20.12  
   20.13  lemma [code]:
   20.14    "char_of_nat = char_of_int o int"
   20.15 -  unfolding char_of_int_def by (simp add: expand_fun_eq)
   20.16 +  unfolding char_of_int_def by (simp add: ext_iff)
   20.17  
   20.18  code_const int_of_char and char_of_int
   20.19    (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
    21.1 --- a/src/HOL/Library/Countable.thy	Mon Sep 06 22:58:06 2010 +0200
    21.2 +++ b/src/HOL/Library/Countable.thy	Tue Sep 07 10:05:19 2010 +0200
    21.3 @@ -139,7 +139,7 @@
    21.4    show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
    21.5    proof
    21.6      show "inj (\<lambda>f. to_nat (map f xs))"
    21.7 -      by (rule injI, simp add: xs expand_fun_eq)
    21.8 +      by (rule injI, simp add: xs ext_iff)
    21.9    qed
   21.10  qed
   21.11  
    22.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Sep 06 22:58:06 2010 +0200
    22.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Tue Sep 07 10:05:19 2010 +0200
    22.3 @@ -79,7 +79,7 @@
    22.4  
    22.5  lemma [code, code_unfold]:
    22.6    "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
    22.7 -  by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
    22.8 +  by (auto simp add: ext_iff dest!: gr0_implies_Suc)
    22.9  
   22.10  
   22.11  subsection {* Preprocessors *}
    23.1 --- a/src/HOL/Library/Enum.thy	Mon Sep 06 22:58:06 2010 +0200
    23.2 +++ b/src/HOL/Library/Enum.thy	Tue Sep 07 10:05:19 2010 +0200
    23.3 @@ -42,7 +42,7 @@
    23.4    "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
    23.5  
    23.6  instance proof
    23.7 -qed (simp_all add: equal_fun_def enum_all expand_fun_eq)
    23.8 +qed (simp_all add: equal_fun_def enum_all ext_iff)
    23.9  
   23.10  end
   23.11  
   23.12 @@ -54,7 +54,7 @@
   23.13    fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
   23.14    shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
   23.15      and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
   23.16 -  by (simp_all add: list_all_iff list_ex_iff enum_all expand_fun_eq le_fun_def order_less_le)
   23.17 +  by (simp_all add: list_all_iff list_ex_iff enum_all ext_iff le_fun_def order_less_le)
   23.18  
   23.19  
   23.20  subsection {* Quantifiers *}
   23.21 @@ -160,7 +160,7 @@
   23.22    proof (rule UNIV_eq_I)
   23.23      fix f :: "'a \<Rightarrow> 'b"
   23.24      have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
   23.25 -      by (auto simp add: map_of_zip_map expand_fun_eq)
   23.26 +      by (auto simp add: map_of_zip_map ext_iff)
   23.27      then show "f \<in> set enum"
   23.28        by (auto simp add: enum_fun_def set_n_lists)
   23.29    qed
    24.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon Sep 06 22:58:06 2010 +0200
    24.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Sep 07 10:05:19 2010 +0200
    24.3 @@ -18,7 +18,7 @@
    24.4  notation fps_nth (infixl "$" 75)
    24.5  
    24.6  lemma expand_fps_eq: "p = q \<longleftrightarrow> (\<forall>n. p $ n = q $ n)"
    24.7 -  by (simp add: fps_nth_inject [symmetric] expand_fun_eq)
    24.8 +  by (simp add: fps_nth_inject [symmetric] ext_iff)
    24.9  
   24.10  lemma fps_ext: "(\<And>n. p $ n = q $ n) \<Longrightarrow> p = q"
   24.11    by (simp add: expand_fps_eq)
   24.12 @@ -1244,7 +1244,7 @@
   24.13      {assume n0: "n \<noteq> 0"
   24.14        then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
   24.15          "{0..n - 1}\<union>{n} = {0..n}"
   24.16 -        by (auto simp: expand_set_eq)
   24.17 +        by (auto simp: set_ext_iff)
   24.18        have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
   24.19          "{0..n - 1}\<inter>{n} ={}" using n0 by simp_all
   24.20        have f: "finite {0}" "finite {1}" "finite {2 .. n}"
   24.21 @@ -1455,7 +1455,7 @@
   24.22    moreover
   24.23    {fix k assume k: "m = Suc k"
   24.24      have km: "k < m" using k by arith
   24.25 -    have u0: "{0 .. k} \<union> {m} = {0..m}" using k apply (simp add: expand_set_eq) by presburger
   24.26 +    have u0: "{0 .. k} \<union> {m} = {0..m}" using k apply (simp add: set_ext_iff) by presburger
   24.27      have f0: "finite {0 .. k}" "finite {m}" by auto
   24.28      have d0: "{0 .. k} \<inter> {m} = {}" using k by auto
   24.29      have "(setprod a {0 .. m}) $ n = (setprod a {0 .. k} * a m) $ n"
   24.30 @@ -1472,7 +1472,7 @@
   24.31        apply clarsimp
   24.32        apply (rule finite_imageI)
   24.33        apply (rule natpermute_finite)
   24.34 -      apply (clarsimp simp add: expand_set_eq)
   24.35 +      apply (clarsimp simp add: set_ext_iff)
   24.36        apply auto
   24.37        apply (rule setsum_cong2)
   24.38        unfolding setsum_left_distrib
   24.39 @@ -2153,7 +2153,7 @@
   24.40  qed
   24.41  
   24.42  lemma fps_inv_ginv: "fps_inv = fps_ginv X"
   24.43 -  apply (auto simp add: expand_fun_eq fps_eq_iff fps_inv_def fps_ginv_def)
   24.44 +  apply (auto simp add: ext_iff fps_eq_iff fps_inv_def fps_ginv_def)
   24.45    apply (induct_tac n rule: nat_less_induct, auto)
   24.46    apply (case_tac na)
   24.47    apply simp
   24.48 @@ -2192,7 +2192,7 @@
   24.49    "setsum (%i. a (i :: nat) * b (n - i)) {0 .. n} = setsum (%(i,j). a i * b j) {(i,j). i <= n \<and> j \<le> n \<and> i + j = n}"
   24.50    apply (rule setsum_reindex_cong[where f=fst])
   24.51    apply (clarsimp simp add: inj_on_def)
   24.52 -  apply (auto simp add: expand_set_eq image_iff)
   24.53 +  apply (auto simp add: set_ext_iff image_iff)
   24.54    apply (rule_tac x= "x" in exI)
   24.55    apply clarsimp
   24.56    apply (rule_tac x="n - x" in exI)
   24.57 @@ -2264,7 +2264,7 @@
   24.58    let ?KM=  "{(k,m). k + m \<le> n}"
   24.59    let ?f = "%s. UNION {(0::nat)..s} (%i. {(i,s - i)})"
   24.60    have th0: "?KM = UNION {0..n} ?f"
   24.61 -    apply (simp add: expand_set_eq)
   24.62 +    apply (simp add: set_ext_iff)
   24.63      apply arith (* FIXME: VERY slow! *)
   24.64      done
   24.65    show "?l = ?r "
   24.66 @@ -3312,10 +3312,10 @@
   24.67  
   24.68  lemma XDp_commute:
   24.69    shows "XDp b o XDp (c::'a::comm_ring_1) = XDp c o XDp b"
   24.70 -  by (auto simp add: XDp_def expand_fun_eq fps_eq_iff algebra_simps)
   24.71 +  by (auto simp add: XDp_def ext_iff fps_eq_iff algebra_simps)
   24.72  
   24.73  lemma XDp0[simp]: "XDp 0 = XD"
   24.74 -  by (simp add: expand_fun_eq fps_eq_iff)
   24.75 +  by (simp add: ext_iff fps_eq_iff)
   24.76  
   24.77  lemma XDp_fps_integral[simp]:"XDp 0 (fps_integral a c) = X * a"
   24.78    by (simp add: fps_eq_iff fps_integral_def)
    25.1 --- a/src/HOL/Library/FrechetDeriv.thy	Mon Sep 06 22:58:06 2010 +0200
    25.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Tue Sep 07 10:05:19 2010 +0200
    25.3 @@ -177,7 +177,7 @@
    25.4    hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)"
    25.5      by (rule FDERIV_zero_unique)
    25.6    thus "F = F'"
    25.7 -    unfolding expand_fun_eq right_minus_eq .
    25.8 +    unfolding ext_iff right_minus_eq .
    25.9  qed
   25.10  
   25.11  subsection {* Continuity *}
    26.1 --- a/src/HOL/Library/Fset.thy	Mon Sep 06 22:58:06 2010 +0200
    26.2 +++ b/src/HOL/Library/Fset.thy	Tue Sep 07 10:05:19 2010 +0200
    26.3 @@ -51,7 +51,7 @@
    26.4  lemma member_code [code]:
    26.5    "member (Set xs) = List.member xs"
    26.6    "member (Coset xs) = Not \<circ> List.member xs"
    26.7 -  by (simp_all add: expand_fun_eq member_def fun_Compl_def bool_Compl_def)
    26.8 +  by (simp_all add: ext_iff member_def fun_Compl_def bool_Compl_def)
    26.9  
   26.10  lemma member_image_UNIV [simp]:
   26.11    "member ` UNIV = UNIV"
   26.12 @@ -252,13 +252,13 @@
   26.13    show "inf A (Set xs) = Set (List.filter (member A) xs)"
   26.14      by (simp add: inter project_def Set_def)
   26.15    have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
   26.16 -    by (simp add: expand_fun_eq)
   26.17 +    by (simp add: ext_iff)
   26.18    have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
   26.19      fold More_Set.remove xs \<circ> member"
   26.20 -    by (rule fold_apply) (simp add: expand_fun_eq)
   26.21 +    by (rule fold_apply) (simp add: ext_iff)
   26.22    then have "fold More_Set.remove xs (member A) = 
   26.23      member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
   26.24 -    by (simp add: expand_fun_eq)
   26.25 +    by (simp add: ext_iff)
   26.26    then have "inf A (Coset xs) = fold remove xs A"
   26.27      by (simp add: Diff_eq [symmetric] minus_set *)
   26.28    moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
   26.29 @@ -277,13 +277,13 @@
   26.30    "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
   26.31  proof -
   26.32    have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
   26.33 -    by (simp add: expand_fun_eq)
   26.34 +    by (simp add: ext_iff)
   26.35    have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
   26.36      fold Set.insert xs \<circ> member"
   26.37 -    by (rule fold_apply) (simp add: expand_fun_eq)
   26.38 +    by (rule fold_apply) (simp add: ext_iff)
   26.39    then have "fold Set.insert xs (member A) =
   26.40      member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
   26.41 -    by (simp add: expand_fun_eq)
   26.42 +    by (simp add: ext_iff)
   26.43    then have "sup (Set xs) A = fold insert xs A"
   26.44      by (simp add: union_set *)
   26.45    moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
    27.1 --- a/src/HOL/Library/FuncSet.thy	Mon Sep 06 22:58:06 2010 +0200
    27.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Sep 07 10:05:19 2010 +0200
    27.3 @@ -128,7 +128,7 @@
    27.4  lemma compose_assoc:
    27.5      "[| f \<in> A -> B; g \<in> B -> C; h \<in> C -> D |]
    27.6        ==> compose A h (compose A g f) = compose A (compose B h g) f"
    27.7 -by (simp add: expand_fun_eq Pi_def compose_def restrict_def)
    27.8 +by (simp add: ext_iff Pi_def compose_def restrict_def)
    27.9  
   27.10  lemma compose_eq: "x \<in> A ==> compose A g f x = g(f(x))"
   27.11  by (simp add: compose_def restrict_def)
   27.12 @@ -151,18 +151,18 @@
   27.13  
   27.14  lemma restrict_ext:
   27.15      "(!!x. x \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>A. g x)"
   27.16 -  by (simp add: expand_fun_eq Pi_def restrict_def)
   27.17 +  by (simp add: ext_iff Pi_def restrict_def)
   27.18  
   27.19  lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A"
   27.20    by (simp add: inj_on_def restrict_def)
   27.21  
   27.22  lemma Id_compose:
   27.23      "[|f \<in> A -> B;  f \<in> extensional A|] ==> compose A (\<lambda>y\<in>B. y) f = f"
   27.24 -  by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
   27.25 +  by (auto simp add: ext_iff compose_def extensional_def Pi_def)
   27.26  
   27.27  lemma compose_Id:
   27.28      "[|g \<in> A -> B;  g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>A. x) = g"
   27.29 -  by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def)
   27.30 +  by (auto simp add: ext_iff compose_def extensional_def Pi_def)
   27.31  
   27.32  lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A"
   27.33    by (auto simp add: restrict_def)
   27.34 @@ -205,7 +205,7 @@
   27.35  lemma extensionalityI:
   27.36    "[| f \<in> extensional A; g \<in> extensional A;
   27.37        !!x. x\<in>A ==> f x = g x |] ==> f = g"
   27.38 -by (force simp add: expand_fun_eq extensional_def)
   27.39 +by (force simp add: ext_iff extensional_def)
   27.40  
   27.41  lemma inv_into_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
   27.42  by (unfold inv_into_def) (fast intro: someI2)
    28.1 --- a/src/HOL/Library/Function_Algebras.thy	Mon Sep 06 22:58:06 2010 +0200
    28.2 +++ b/src/HOL/Library/Function_Algebras.thy	Tue Sep 07 10:05:19 2010 +0200
    28.3 @@ -57,7 +57,7 @@
    28.4  qed (simp add: plus_fun_def add.assoc)
    28.5  
    28.6  instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
    28.7 -qed (simp_all add: plus_fun_def expand_fun_eq)
    28.8 +qed (simp_all add: plus_fun_def ext_iff)
    28.9  
   28.10  instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
   28.11  qed (simp add: plus_fun_def add.commute)
   28.12 @@ -106,7 +106,7 @@
   28.13  qed (simp_all add: zero_fun_def times_fun_def)
   28.14  
   28.15  instance "fun" :: (type, zero_neq_one) zero_neq_one proof
   28.16 -qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
   28.17 +qed (simp add: zero_fun_def one_fun_def ext_iff)
   28.18  
   28.19  
   28.20  text {* Ring structures *}
    29.1 --- a/src/HOL/Library/Inner_Product.thy	Mon Sep 06 22:58:06 2010 +0200
    29.2 +++ b/src/HOL/Library/Inner_Product.thy	Tue Sep 07 10:05:19 2010 +0200
    29.3 @@ -307,7 +307,7 @@
    29.4    have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
    29.5      by (intro inner.FDERIV FDERIV_ident)
    29.6    have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>h. inner h (scaleR 2 x))"
    29.7 -    by (simp add: expand_fun_eq inner_commute)
    29.8 +    by (simp add: ext_iff inner_commute)
    29.9    have "0 < inner x x" using `x \<noteq> 0` by simp
   29.10    then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
   29.11      by (rule DERIV_real_sqrt)
    30.1 --- a/src/HOL/Library/Mapping.thy	Mon Sep 06 22:58:06 2010 +0200
    30.2 +++ b/src/HOL/Library/Mapping.thy	Tue Sep 07 10:05:19 2010 +0200
    30.3 @@ -94,11 +94,11 @@
    30.4  
    30.5  lemma lookup_map_entry [simp]:
    30.6    "lookup (map_entry k f m) = (lookup m) (k := Option.map f (lookup m k))"
    30.7 -  by (cases "lookup m k") (simp_all add: map_entry_def expand_fun_eq)
    30.8 +  by (cases "lookup m k") (simp_all add: map_entry_def ext_iff)
    30.9  
   30.10  lemma lookup_tabulate [simp]:
   30.11    "lookup (tabulate ks f) = (Some o f) |` set ks"
   30.12 -  by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq)
   30.13 +  by (induct ks) (auto simp add: tabulate_def restrict_map_def ext_iff)
   30.14  
   30.15  lemma lookup_bulkload [simp]:
   30.16    "lookup (bulkload xs) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
   30.17 @@ -146,7 +146,7 @@
   30.18  
   30.19  lemma bulkload_tabulate:
   30.20    "bulkload xs = tabulate [0..<length xs] (nth xs)"
   30.21 -  by (rule mapping_eqI) (simp add: expand_fun_eq)
   30.22 +  by (rule mapping_eqI) (simp add: ext_iff)
   30.23  
   30.24  lemma is_empty_empty: (*FIXME*)
   30.25    "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
    31.1 --- a/src/HOL/Library/More_List.thy	Mon Sep 06 22:58:06 2010 +0200
    31.2 +++ b/src/HOL/Library/More_List.thy	Tue Sep 07 10:05:19 2010 +0200
    31.3 @@ -30,7 +30,7 @@
    31.4  
    31.5  lemma foldr_fold_rev:
    31.6    "foldr f xs = fold f (rev xs)"
    31.7 -  by (simp add: foldr_foldl foldl_fold expand_fun_eq)
    31.8 +  by (simp add: foldr_foldl foldl_fold ext_iff)
    31.9  
   31.10  lemma fold_rev_conv [code_unfold]:
   31.11    "fold f (rev xs) = foldr f xs"
   31.12 @@ -49,7 +49,7 @@
   31.13  lemma fold_apply:
   31.14    assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
   31.15    shows "h \<circ> fold g xs = fold f xs \<circ> h"
   31.16 -  using assms by (induct xs) (simp_all add: expand_fun_eq)
   31.17 +  using assms by (induct xs) (simp_all add: ext_iff)
   31.18  
   31.19  lemma fold_invariant: 
   31.20    assumes "\<And>x. x \<in> set xs \<Longrightarrow> Q x" and "P s"
   31.21 @@ -164,7 +164,7 @@
   31.22  
   31.23  lemma (in lattice) Inf_fin_set_foldr [code_unfold]:
   31.24    "Inf_fin (set (x # xs)) = foldr inf xs x"
   31.25 -  by (simp add: Inf_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
   31.26 +  by (simp add: Inf_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
   31.27  
   31.28  lemma (in lattice) Sup_fin_set_fold:
   31.29    "Sup_fin (set (x # xs)) = fold sup xs x"
   31.30 @@ -177,7 +177,7 @@
   31.31  
   31.32  lemma (in lattice) Sup_fin_set_foldr [code_unfold]:
   31.33    "Sup_fin (set (x # xs)) = foldr sup xs x"
   31.34 -  by (simp add: Sup_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
   31.35 +  by (simp add: Sup_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
   31.36  
   31.37  lemma (in linorder) Min_fin_set_fold:
   31.38    "Min (set (x # xs)) = fold min xs x"
   31.39 @@ -190,7 +190,7 @@
   31.40  
   31.41  lemma (in linorder) Min_fin_set_foldr [code_unfold]:
   31.42    "Min (set (x # xs)) = foldr min xs x"
   31.43 -  by (simp add: Min_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
   31.44 +  by (simp add: Min_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
   31.45  
   31.46  lemma (in linorder) Max_fin_set_fold:
   31.47    "Max (set (x # xs)) = fold max xs x"
   31.48 @@ -203,7 +203,7 @@
   31.49  
   31.50  lemma (in linorder) Max_fin_set_foldr [code_unfold]:
   31.51    "Max (set (x # xs)) = foldr max xs x"
   31.52 -  by (simp add: Max_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps)
   31.53 +  by (simp add: Max_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps)
   31.54  
   31.55  lemma (in complete_lattice) Inf_set_fold:
   31.56    "Inf (set xs) = fold inf xs top"
   31.57 @@ -215,7 +215,7 @@
   31.58  
   31.59  lemma (in complete_lattice) Inf_set_foldr [code_unfold]:
   31.60    "Inf (set xs) = foldr inf xs top"
   31.61 -  by (simp add: Inf_set_fold ac_simps foldr_fold expand_fun_eq)
   31.62 +  by (simp add: Inf_set_fold ac_simps foldr_fold ext_iff)
   31.63  
   31.64  lemma (in complete_lattice) Sup_set_fold:
   31.65    "Sup (set xs) = fold sup xs bot"
   31.66 @@ -227,7 +227,7 @@
   31.67  
   31.68  lemma (in complete_lattice) Sup_set_foldr [code_unfold]:
   31.69    "Sup (set xs) = foldr sup xs bot"
   31.70 -  by (simp add: Sup_set_fold ac_simps foldr_fold expand_fun_eq)
   31.71 +  by (simp add: Sup_set_fold ac_simps foldr_fold ext_iff)
   31.72  
   31.73  lemma (in complete_lattice) INFI_set_fold:
   31.74    "INFI (set xs) f = fold (inf \<circ> f) xs top"
    32.1 --- a/src/HOL/Library/More_Set.thy	Mon Sep 06 22:58:06 2010 +0200
    32.2 +++ b/src/HOL/Library/More_Set.thy	Tue Sep 07 10:05:19 2010 +0200
    32.3 @@ -18,7 +18,7 @@
    32.4  lemma fun_left_comm_idem_remove:
    32.5    "fun_left_comm_idem remove"
    32.6  proof -
    32.7 -  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
    32.8 +  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: ext_iff remove_def)
    32.9    show ?thesis by (simp only: fun_left_comm_idem_remove rem)
   32.10  qed
   32.11  
   32.12 @@ -26,7 +26,7 @@
   32.13    assumes "finite A"
   32.14    shows "B - A = Finite_Set.fold remove B A"
   32.15  proof -
   32.16 -  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def)
   32.17 +  have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: ext_iff remove_def)
   32.18    show ?thesis by (simp only: rem assms minus_fold_remove)
   32.19  qed
   32.20  
   32.21 @@ -124,6 +124,6 @@
   32.22  
   32.23  lemma not_set_compl:
   32.24    "Not \<circ> set xs = - set xs"
   32.25 -  by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq)
   32.26 +  by (simp add: fun_Compl_def bool_Compl_def comp_def ext_iff)
   32.27  
   32.28  end
    33.1 --- a/src/HOL/Library/Multiset.thy	Mon Sep 06 22:58:06 2010 +0200
    33.2 +++ b/src/HOL/Library/Multiset.thy	Tue Sep 07 10:05:19 2010 +0200
    33.3 @@ -26,7 +26,7 @@
    33.4  
    33.5  lemma multiset_ext_iff:
    33.6    "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
    33.7 -  by (simp only: count_inject [symmetric] expand_fun_eq)
    33.8 +  by (simp only: count_inject [symmetric] ext_iff)
    33.9  
   33.10  lemma multiset_ext:
   33.11    "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
   33.12 @@ -581,7 +581,7 @@
   33.13       apply (rule empty [unfolded defns])
   33.14      apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))")
   33.15       prefer 2
   33.16 -     apply (simp add: expand_fun_eq)
   33.17 +     apply (simp add: ext_iff)
   33.18      apply (erule ssubst)
   33.19      apply (erule Abs_multiset_inverse [THEN subst])
   33.20      apply (drule add')
   33.21 @@ -883,13 +883,13 @@
   33.22    with finite_dom_map_of [of xs] have "finite ?A"
   33.23      by (auto intro: finite_subset)
   33.24    then show ?thesis
   33.25 -    by (simp add: count_of_def expand_fun_eq multiset_def)
   33.26 +    by (simp add: count_of_def ext_iff multiset_def)
   33.27  qed
   33.28  
   33.29  lemma count_simps [simp]:
   33.30    "count_of [] = (\<lambda>_. 0)"
   33.31    "count_of ((x, n) # xs) = (\<lambda>y. if x = y then n else count_of xs y)"
   33.32 -  by (simp_all add: count_of_def expand_fun_eq)
   33.33 +  by (simp_all add: count_of_def ext_iff)
   33.34  
   33.35  lemma count_of_empty:
   33.36    "x \<notin> fst ` set xs \<Longrightarrow> count_of xs x = 0"
    34.1 --- a/src/HOL/Library/Order_Relation.thy	Mon Sep 06 22:58:06 2010 +0200
    34.2 +++ b/src/HOL/Library/Order_Relation.thy	Tue Sep 07 10:05:19 2010 +0200
    34.3 @@ -81,7 +81,7 @@
    34.4  
    34.5  lemma Refl_antisym_eq_Image1_Image1_iff:
    34.6    "\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
    34.7 -by(simp add: expand_set_eq antisym_def refl_on_def) metis
    34.8 +by(simp add: set_ext_iff antisym_def refl_on_def) metis
    34.9  
   34.10  lemma Partial_order_eq_Image1_Image1_iff:
   34.11    "\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
    35.1 --- a/src/HOL/Library/Permutations.thy	Mon Sep 06 22:58:06 2010 +0200
    35.2 +++ b/src/HOL/Library/Permutations.thy	Tue Sep 07 10:05:19 2010 +0200
    35.3 @@ -16,7 +16,7 @@
    35.4  (* ------------------------------------------------------------------------- *)
    35.5  
    35.6  lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
    35.7 -  by (auto simp add: expand_fun_eq swap_def fun_upd_def)
    35.8 +  by (auto simp add: ext_iff swap_def fun_upd_def)
    35.9  lemma swap_id_refl: "Fun.swap a a id = id" by simp
   35.10  lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
   35.11    by (rule ext, simp add: swap_def)
   35.12 @@ -25,7 +25,7 @@
   35.13  
   35.14  lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id"
   35.15    shows "inv f = g"
   35.16 -  using fg gf inv_equality[of g f] by (auto simp add: expand_fun_eq)
   35.17 +  using fg gf inv_equality[of g f] by (auto simp add: ext_iff)
   35.18  
   35.19  lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
   35.20    by (rule inv_unique_comp, simp_all)
   35.21 @@ -67,16 +67,16 @@
   35.22    assumes pS: "p permutes S"
   35.23    shows "p (inv p x) = x"
   35.24    and "inv p (p x) = x"
   35.25 -  using permutes_inv_o[OF pS, unfolded expand_fun_eq o_def] by auto
   35.26 +  using permutes_inv_o[OF pS, unfolded ext_iff o_def] by auto
   35.27  
   35.28  lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T ==> p permutes T"
   35.29    unfolding permutes_def by blast
   35.30  
   35.31  lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id"
   35.32 -  unfolding expand_fun_eq permutes_def apply simp by metis
   35.33 +  unfolding ext_iff permutes_def apply simp by metis
   35.34  
   35.35  lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id"
   35.36 -  unfolding expand_fun_eq permutes_def apply simp by metis
   35.37 +  unfolding ext_iff permutes_def apply simp by metis
   35.38  
   35.39  lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
   35.40    unfolding permutes_def by simp
   35.41 @@ -111,7 +111,7 @@
   35.42    using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis
   35.43  
   35.44  lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p"
   35.45 -  unfolding expand_fun_eq permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
   35.46 +  unfolding ext_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
   35.47    by blast
   35.48  
   35.49  (* ------------------------------------------------------------------------- *)
   35.50 @@ -136,7 +136,7 @@
   35.51      {assume pS: "p permutes insert a S"
   35.52        let ?b = "p a"
   35.53        let ?q = "Fun.swap a (p a) id o p"
   35.54 -      have th0: "p = Fun.swap a ?b id o ?q" unfolding expand_fun_eq o_assoc by simp
   35.55 +      have th0: "p = Fun.swap a ?b id o ?q" unfolding ext_iff o_assoc by simp
   35.56        have th1: "?b \<in> insert a S " unfolding permutes_in_image[OF pS] by simp
   35.57        from permutes_insert_lemma[OF pS] th0 th1
   35.58        have "\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S" by blast}
   35.59 @@ -180,11 +180,11 @@
   35.60            and eq: "?g (b,p) = ?g (c,q)"
   35.61          from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
   35.62          from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x" unfolding permutes_def
   35.63 -          by (auto simp add: swap_def fun_upd_def expand_fun_eq)
   35.64 +          by (auto simp add: swap_def fun_upd_def ext_iff)
   35.65          also have "\<dots> = ?g (c,q) x" using ths(5) `x \<notin> F` eq
   35.66 -          by (auto simp add: swap_def fun_upd_def expand_fun_eq)
   35.67 +          by (auto simp add: swap_def fun_upd_def ext_iff)
   35.68          also have "\<dots> = c"using ths(5) `x \<notin> F` unfolding permutes_def
   35.69 -          by (auto simp add: swap_def fun_upd_def expand_fun_eq)
   35.70 +          by (auto simp add: swap_def fun_upd_def ext_iff)
   35.71          finally have bc: "b = c" .
   35.72          hence "Fun.swap x b id = Fun.swap x c id" by simp
   35.73          with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
   35.74 @@ -251,12 +251,12 @@
   35.75  (* Various combinations of transpositions with 2, 1 and 0 common elements.   *)
   35.76  (* ------------------------------------------------------------------------- *)
   35.77  
   35.78 -lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>  Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: expand_fun_eq swap_def)
   35.79 +lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>  Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: ext_iff swap_def)
   35.80  
   35.81 -lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: expand_fun_eq swap_def)
   35.82 +lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: ext_iff swap_def)
   35.83  
   35.84  lemma swap_id_independent: "~(a = c) \<Longrightarrow> ~(a = d) \<Longrightarrow> ~(b = c) \<Longrightarrow> ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id"
   35.85 -  by (simp add: swap_def expand_fun_eq)
   35.86 +  by (simp add: swap_def ext_iff)
   35.87  
   35.88  (* ------------------------------------------------------------------------- *)
   35.89  (* Permutations as transposition sequences.                                  *)
   35.90 @@ -352,18 +352,18 @@
   35.91    apply (rule_tac x="b" in exI)
   35.92    apply (rule_tac x="d" in exI)
   35.93    apply (rule_tac x="b" in exI)
   35.94 -  apply (clarsimp simp add: expand_fun_eq swap_def)
   35.95 +  apply (clarsimp simp add: ext_iff swap_def)
   35.96    apply (case_tac "a \<noteq> c \<and> b = d")
   35.97    apply (rule disjI2)
   35.98    apply (rule_tac x="c" in exI)
   35.99    apply (rule_tac x="d" in exI)
  35.100    apply (rule_tac x="c" in exI)
  35.101 -  apply (clarsimp simp add: expand_fun_eq swap_def)
  35.102 +  apply (clarsimp simp add: ext_iff swap_def)
  35.103    apply (rule disjI2)
  35.104    apply (rule_tac x="c" in exI)
  35.105    apply (rule_tac x="d" in exI)
  35.106    apply (rule_tac x="b" in exI)
  35.107 -  apply (clarsimp simp add: expand_fun_eq swap_def)
  35.108 +  apply (clarsimp simp add: ext_iff swap_def)
  35.109    done
  35.110  with H show ?thesis by metis
  35.111  qed
  35.112 @@ -518,7 +518,7 @@
  35.113    from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
  35.114    from swapidseq_inverse_exists[OF n] obtain q where
  35.115      q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
  35.116 -  thus ?thesis unfolding bij_iff  apply (auto simp add: expand_fun_eq) apply metis done
  35.117 +  thus ?thesis unfolding bij_iff  apply (auto simp add: ext_iff) apply metis done
  35.118  qed
  35.119  
  35.120  lemma permutation_finite_support: assumes p: "permutation p"
  35.121 @@ -544,7 +544,7 @@
  35.122  lemma bij_swap_comp:
  35.123    assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p"
  35.124    using surj_f_inv_f[OF bij_is_surj[OF bp]]
  35.125 -  by (simp add: expand_fun_eq swap_def bij_inv_eq_iff[OF bp])
  35.126 +  by (simp add: ext_iff swap_def bij_inv_eq_iff[OF bp])
  35.127  
  35.128  lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id o p)"
  35.129  proof-
  35.130 @@ -688,7 +688,7 @@
  35.131          ultimately have "p n = n" by blast }
  35.132        ultimately show "p n = n"  by blast
  35.133      qed}
  35.134 -  thus ?thesis by (auto simp add: expand_fun_eq)
  35.135 +  thus ?thesis by (auto simp add: ext_iff)
  35.136  qed
  35.137  
  35.138  lemma permutes_natset_ge:
  35.139 @@ -811,7 +811,7 @@
  35.140    shows "setsum f {p. p permutes (insert a S)} = setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)"
  35.141  proof-
  35.142    have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id o p)) = f o (\<lambda>(b,p). Fun.swap a b id o p)"
  35.143 -    by (simp add: expand_fun_eq)
  35.144 +    by (simp add: ext_iff)
  35.145    have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}" by blast
  35.146    have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast
  35.147    show ?thesis
    36.1 --- a/src/HOL/Library/Polynomial.thy	Mon Sep 06 22:58:06 2010 +0200
    36.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Sep 07 10:05:19 2010 +0200
    36.3 @@ -16,7 +16,7 @@
    36.4    by auto
    36.5  
    36.6  lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
    36.7 -by (simp add: coeff_inject [symmetric] expand_fun_eq)
    36.8 +by (simp add: coeff_inject [symmetric] ext_iff)
    36.9  
   36.10  lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
   36.11  by (simp add: expand_poly_eq)
   36.12 @@ -1403,7 +1403,7 @@
   36.13    fixes p q :: "'a::{idom,ring_char_0} poly"
   36.14    shows "poly p = poly q \<longleftrightarrow> p = q"
   36.15    using poly_zero [of "p - q"]
   36.16 -  by (simp add: expand_fun_eq)
   36.17 +  by (simp add: ext_iff)
   36.18  
   36.19  
   36.20  subsection {* Composition of polynomials *}
    37.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Sep 06 22:58:06 2010 +0200
    37.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Sep 07 10:05:19 2010 +0200
    37.3 @@ -12,7 +12,7 @@
    37.4  declare le_bool_def_raw[code_pred_inline]
    37.5  
    37.6  lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
    37.7 -by (rule eq_reflection) (auto simp add: expand_fun_eq min_def le_bool_def)
    37.8 +by (rule eq_reflection) (auto simp add: ext_iff min_def le_bool_def)
    37.9  
   37.10  setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
   37.11  
    38.1 --- a/src/HOL/Library/Quotient_List.thy	Mon Sep 06 22:58:06 2010 +0200
    38.2 +++ b/src/HOL/Library/Quotient_List.thy	Tue Sep 07 10:05:19 2010 +0200
    38.3 @@ -19,7 +19,7 @@
    38.4  
    38.5  lemma map_id[id_simps]:
    38.6    shows "map id = id"
    38.7 -  apply(simp add: expand_fun_eq)
    38.8 +  apply(simp add: ext_iff)
    38.9    apply(rule allI)
   38.10    apply(induct_tac x)
   38.11    apply(simp_all)
   38.12 @@ -92,7 +92,7 @@
   38.13  lemma cons_prs[quot_preserve]:
   38.14    assumes q: "Quotient R Abs Rep"
   38.15    shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
   38.16 -  by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q])
   38.17 +  by (simp only: ext_iff fun_map_def cons_prs_aux[OF q])
   38.18       (simp)
   38.19  
   38.20  lemma cons_rsp[quot_respect]:
   38.21 @@ -122,7 +122,7 @@
   38.22    and     b: "Quotient R2 abs2 rep2"
   38.23    shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
   38.24    and   "((abs1 ---> id) ---> map rep1 ---> id) map = map"
   38.25 -  by (simp_all only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
   38.26 +  by (simp_all only: ext_iff fun_map_def map_prs_aux[OF a b])
   38.27       (simp_all add: Quotient_abs_rep[OF a])
   38.28  
   38.29  lemma map_rsp[quot_respect]:
   38.30 @@ -148,7 +148,7 @@
   38.31    assumes a: "Quotient R1 abs1 rep1"
   38.32    and     b: "Quotient R2 abs2 rep2"
   38.33    shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
   38.34 -  by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b])
   38.35 +  by (simp only: ext_iff fun_map_def foldr_prs_aux[OF a b])
   38.36       (simp)
   38.37  
   38.38  lemma foldl_prs_aux:
   38.39 @@ -162,7 +162,7 @@
   38.40    assumes a: "Quotient R1 abs1 rep1"
   38.41    and     b: "Quotient R2 abs2 rep2"
   38.42    shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
   38.43 -  by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b])
   38.44 +  by (simp only: ext_iff fun_map_def foldl_prs_aux[OF a b])
   38.45       (simp)
   38.46  
   38.47  lemma list_all2_empty:
   38.48 @@ -231,7 +231,7 @@
   38.49  lemma[quot_preserve]:
   38.50    assumes a: "Quotient R abs1 rep1"
   38.51    shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2"
   38.52 -  apply (simp add: expand_fun_eq)
   38.53 +  apply (simp add: ext_iff)
   38.54    apply clarify
   38.55    apply (induct_tac xa xb rule: list_induct2')
   38.56    apply (simp_all add: Quotient_abs_rep[OF a])
   38.57 @@ -244,7 +244,7 @@
   38.58  
   38.59  lemma list_all2_eq[id_simps]:
   38.60    shows "(list_all2 (op =)) = (op =)"
   38.61 -  unfolding expand_fun_eq
   38.62 +  unfolding ext_iff
   38.63    apply(rule allI)+
   38.64    apply(induct_tac x xa rule: list_induct2')
   38.65    apply(simp_all)
    39.1 --- a/src/HOL/Library/Quotient_Option.thy	Mon Sep 06 22:58:06 2010 +0200
    39.2 +++ b/src/HOL/Library/Quotient_Option.thy	Tue Sep 07 10:05:19 2010 +0200
    39.3 @@ -66,16 +66,16 @@
    39.4  lemma option_Some_prs[quot_preserve]:
    39.5    assumes q: "Quotient R Abs Rep"
    39.6    shows "(Rep ---> Option.map Abs) Some = Some"
    39.7 -  apply(simp add: expand_fun_eq)
    39.8 +  apply(simp add: ext_iff)
    39.9    apply(simp add: Quotient_abs_rep[OF q])
   39.10    done
   39.11  
   39.12  lemma option_map_id[id_simps]:
   39.13    shows "Option.map id = id"
   39.14 -  by (simp add: expand_fun_eq split_option_all)
   39.15 +  by (simp add: ext_iff split_option_all)
   39.16  
   39.17  lemma option_rel_eq[id_simps]:
   39.18    shows "option_rel (op =) = (op =)"
   39.19 -  by (simp add: expand_fun_eq split_option_all)
   39.20 +  by (simp add: ext_iff split_option_all)
   39.21  
   39.22  end
    40.1 --- a/src/HOL/Library/Quotient_Product.thy	Mon Sep 06 22:58:06 2010 +0200
    40.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Sep 07 10:05:19 2010 +0200
    40.3 @@ -51,7 +51,7 @@
    40.4    assumes q1: "Quotient R1 Abs1 Rep1"
    40.5    assumes q2: "Quotient R2 Abs2 Rep2"
    40.6    shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
    40.7 -  apply(simp add: expand_fun_eq)
    40.8 +  apply(simp add: ext_iff)
    40.9    apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   40.10    done
   40.11  
   40.12 @@ -65,7 +65,7 @@
   40.13    assumes q1: "Quotient R1 Abs1 Rep1"
   40.14    assumes q2: "Quotient R2 Abs2 Rep2"
   40.15    shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
   40.16 -  apply(simp add: expand_fun_eq)
   40.17 +  apply(simp add: ext_iff)
   40.18    apply(simp add: Quotient_abs_rep[OF q1])
   40.19    done
   40.20  
   40.21 @@ -79,7 +79,7 @@
   40.22    assumes q1: "Quotient R1 Abs1 Rep1"
   40.23    assumes q2: "Quotient R2 Abs2 Rep2"
   40.24    shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
   40.25 -  apply(simp add: expand_fun_eq)
   40.26 +  apply(simp add: ext_iff)
   40.27    apply(simp add: Quotient_abs_rep[OF q2])
   40.28    done
   40.29  
   40.30 @@ -91,7 +91,7 @@
   40.31    assumes q1: "Quotient R1 Abs1 Rep1"
   40.32    and     q2: "Quotient R2 Abs2 Rep2"
   40.33    shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
   40.34 -  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   40.35 +  by (simp add: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   40.36  
   40.37  lemma [quot_respect]:
   40.38    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
   40.39 @@ -103,7 +103,7 @@
   40.40    and     q2: "Quotient R2 abs2 rep2"
   40.41    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
   40.42    prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel"
   40.43 -  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   40.44 +  by (simp add: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   40.45  
   40.46  lemma [quot_preserve]:
   40.47    shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
   40.48 @@ -118,6 +118,6 @@
   40.49  
   40.50  lemma prod_rel_eq[id_simps]:
   40.51    shows "prod_rel (op =) (op =) = (op =)"
   40.52 -  by (simp add: expand_fun_eq)
   40.53 +  by (simp add: ext_iff)
   40.54  
   40.55  end
    41.1 --- a/src/HOL/Library/Quotient_Sum.thy	Mon Sep 06 22:58:06 2010 +0200
    41.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Sep 07 10:05:19 2010 +0200
    41.3 @@ -74,7 +74,7 @@
    41.4    assumes q1: "Quotient R1 Abs1 Rep1"
    41.5    assumes q2: "Quotient R2 Abs2 Rep2"
    41.6    shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
    41.7 -  apply(simp add: expand_fun_eq)
    41.8 +  apply(simp add: ext_iff)
    41.9    apply(simp add: Quotient_abs_rep[OF q1])
   41.10    done
   41.11  
   41.12 @@ -82,16 +82,16 @@
   41.13    assumes q1: "Quotient R1 Abs1 Rep1"
   41.14    assumes q2: "Quotient R2 Abs2 Rep2"
   41.15    shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
   41.16 -  apply(simp add: expand_fun_eq)
   41.17 +  apply(simp add: ext_iff)
   41.18    apply(simp add: Quotient_abs_rep[OF q2])
   41.19    done
   41.20  
   41.21  lemma sum_map_id[id_simps]:
   41.22    shows "sum_map id id = id"
   41.23 -  by (simp add: expand_fun_eq split_sum_all)
   41.24 +  by (simp add: ext_iff split_sum_all)
   41.25  
   41.26  lemma sum_rel_eq[id_simps]:
   41.27    shows "sum_rel (op =) (op =) = (op =)"
   41.28 -  by (simp add: expand_fun_eq split_sum_all)
   41.29 +  by (simp add: ext_iff split_sum_all)
   41.30  
   41.31  end
    42.1 --- a/src/HOL/Library/RBT.thy	Mon Sep 06 22:58:06 2010 +0200
    42.2 +++ b/src/HOL/Library/RBT.thy	Tue Sep 07 10:05:19 2010 +0200
    42.3 @@ -112,7 +112,7 @@
    42.4  
    42.5  lemma lookup_empty [simp]:
    42.6    "lookup empty = Map.empty"
    42.7 -  by (simp add: empty_def lookup_RBT expand_fun_eq)
    42.8 +  by (simp add: empty_def lookup_RBT ext_iff)
    42.9  
   42.10  lemma lookup_insert [simp]:
   42.11    "lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
   42.12 @@ -144,7 +144,7 @@
   42.13  
   42.14  lemma fold_fold:
   42.15    "fold f t = More_List.fold (prod_case f) (entries t)"
   42.16 -  by (simp add: fold_def expand_fun_eq RBT_Impl.fold_def entries_impl_of)
   42.17 +  by (simp add: fold_def ext_iff RBT_Impl.fold_def entries_impl_of)
   42.18  
   42.19  lemma is_empty_empty [simp]:
   42.20    "is_empty t \<longleftrightarrow> t = empty"
   42.21 @@ -152,7 +152,7 @@
   42.22  
   42.23  lemma RBT_lookup_empty [simp]: (*FIXME*)
   42.24    "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
   42.25 -  by (cases t) (auto simp add: expand_fun_eq)
   42.26 +  by (cases t) (auto simp add: ext_iff)
   42.27  
   42.28  lemma lookup_empty_empty [simp]:
   42.29    "lookup t = Map.empty \<longleftrightarrow> t = empty"
   42.30 @@ -220,7 +220,7 @@
   42.31  
   42.32  lemma bulkload_Mapping [code]:
   42.33    "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
   42.34 -  by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
   42.35 +  by (rule mapping_eqI) (simp add: map_of_map_restrict ext_iff)
   42.36  
   42.37  lemma equal_Mapping [code]:
   42.38    "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
    43.1 --- a/src/HOL/Library/RBT_Impl.thy	Mon Sep 06 22:58:06 2010 +0200
    43.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Sep 07 10:05:19 2010 +0200
    43.3 @@ -1019,7 +1019,7 @@
    43.4  
    43.5  theorem lookup_map_entry:
    43.6    "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
    43.7 -  by (induct t) (auto split: option.splits simp add: expand_fun_eq)
    43.8 +  by (induct t) (auto split: option.splits simp add: ext_iff)
    43.9  
   43.10  
   43.11  subsection {* Mapping all entries *}
   43.12 @@ -1054,7 +1054,7 @@
   43.13  lemma fold_simps [simp, code]:
   43.14    "fold f Empty = id"
   43.15    "fold f (Branch c lt k v rt) = fold f rt \<circ> f k v \<circ> fold f lt"
   43.16 -  by (simp_all add: fold_def expand_fun_eq)
   43.17 +  by (simp_all add: fold_def ext_iff)
   43.18  
   43.19  
   43.20  subsection {* Bulkloading a tree *}
    44.1 --- a/src/HOL/Library/Set_Algebras.thy	Mon Sep 06 22:58:06 2010 +0200
    44.2 +++ b/src/HOL/Library/Set_Algebras.thy	Tue Sep 07 10:05:19 2010 +0200
    44.3 @@ -72,7 +72,7 @@
    44.4    show "monoid_add.listsum set_plus {0::'a} = listsum_set"
    44.5      by (simp only: listsum_set_def)
    44.6    show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
    44.7 -    by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq)
    44.8 +    by (simp add: set_add.setsum_def setsum_set_def ext_iff)
    44.9  qed
   44.10  
   44.11  interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
   44.12 @@ -117,7 +117,7 @@
   44.13    show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
   44.14      by (simp add: power_set_def)
   44.15    show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
   44.16 -    by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq)
   44.17 +    by (simp add: set_mult.setprod_def setprod_set_def ext_iff)
   44.18  qed
   44.19  
   44.20  lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
    45.1 --- a/src/HOL/Library/Univ_Poly.thy	Mon Sep 06 22:58:06 2010 +0200
    45.2 +++ b/src/HOL/Library/Univ_Poly.thy	Tue Sep 07 10:05:19 2010 +0200
    45.3 @@ -382,7 +382,7 @@
    45.4  lemma (in idom_char_0) poly_entire:
    45.5    "poly (p *** q) = poly [] \<longleftrightarrow> poly p = poly [] \<or> poly q = poly []"
    45.6  using poly_entire_lemma2[of p q]
    45.7 -by (auto simp add: expand_fun_eq poly_mult)
    45.8 +by (auto simp add: ext_iff poly_mult)
    45.9  
   45.10  lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
   45.11  by (simp add: poly_entire)
   45.12 @@ -847,14 +847,14 @@
   45.13    assume eq: ?lhs
   45.14    hence "\<And>x. poly ((c#cs) +++ -- (d#ds)) x = 0"
   45.15      by (simp only: poly_minus poly_add algebra_simps) simp
   45.16 -  hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add:expand_fun_eq)
   45.17 +  hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add: ext_iff)
   45.18    hence "c = d \<and> list_all (\<lambda>x. x=0) ((cs +++ -- ds))"
   45.19      unfolding poly_zero by (simp add: poly_minus_def algebra_simps)
   45.20    hence "c = d \<and> (\<forall>x. poly (cs +++ -- ds) x = 0)"
   45.21      unfolding poly_zero[symmetric] by simp
   45.22 -  thus ?rhs  by (simp add: poly_minus poly_add algebra_simps expand_fun_eq)
   45.23 +  thus ?rhs  by (simp add: poly_minus poly_add algebra_simps ext_iff)
   45.24  next
   45.25 -  assume ?rhs then show ?lhs by(simp add:expand_fun_eq)
   45.26 +  assume ?rhs then show ?lhs by(simp add:ext_iff)
   45.27  qed
   45.28  
   45.29  lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \<Longrightarrow> pnormalize p = pnormalize q"
    46.1 --- a/src/HOL/Limits.thy	Mon Sep 06 22:58:06 2010 +0200
    46.2 +++ b/src/HOL/Limits.thy	Tue Sep 07 10:05:19 2010 +0200
    46.3 @@ -46,7 +46,7 @@
    46.4  
    46.5  lemma expand_net_eq:
    46.6    shows "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
    46.7 -unfolding Rep_net_inject [symmetric] expand_fun_eq eventually_def ..
    46.8 +unfolding Rep_net_inject [symmetric] ext_iff eventually_def ..
    46.9  
   46.10  lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
   46.11  unfolding eventually_def
    47.1 --- a/src/HOL/List.thy	Mon Sep 06 22:58:06 2010 +0200
    47.2 +++ b/src/HOL/List.thy	Tue Sep 07 10:05:19 2010 +0200
    47.3 @@ -2317,7 +2317,7 @@
    47.4  lemma foldl_apply:
    47.5    assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
    47.6    shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
    47.7 -  by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: expand_fun_eq)
    47.8 +  by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: ext_iff)
    47.9  
   47.10  lemma foldl_cong [fundef_cong, recdef_cong]:
   47.11    "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
   47.12 @@ -4564,7 +4564,7 @@
   47.13  
   47.14  lemma member_set:
   47.15    "member = set"
   47.16 -  by (simp add: expand_fun_eq member_def mem_def)
   47.17 +  by (simp add: ext_iff member_def mem_def)
   47.18  
   47.19  lemma member_rec [code]:
   47.20    "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
    48.1 --- a/src/HOL/Map.thy	Mon Sep 06 22:58:06 2010 +0200
    48.2 +++ b/src/HOL/Map.thy	Tue Sep 07 10:05:19 2010 +0200
    48.3 @@ -218,7 +218,7 @@
    48.4  
    48.5  lemma map_of_zip_map:
    48.6    "map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
    48.7 -  by (induct xs) (simp_all add: expand_fun_eq)
    48.8 +  by (induct xs) (simp_all add: ext_iff)
    48.9  
   48.10  lemma finite_range_map_of: "finite (range (map_of xys))"
   48.11  apply (induct xys)
   48.12 @@ -245,7 +245,7 @@
   48.13  
   48.14  lemma map_of_map:
   48.15    "map_of (map (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
   48.16 -  by (induct xs) (auto simp add: expand_fun_eq)
   48.17 +  by (induct xs) (auto simp add: ext_iff)
   48.18  
   48.19  lemma dom_option_map:
   48.20    "dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
   48.21 @@ -347,7 +347,7 @@
   48.22  
   48.23  lemma map_add_map_of_foldr:
   48.24    "m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m"
   48.25 -  by (induct ps) (auto simp add: expand_fun_eq map_add_def)
   48.26 +  by (induct ps) (auto simp add: ext_iff map_add_def)
   48.27  
   48.28  
   48.29  subsection {* @{term [source] restrict_map} *}
   48.30 @@ -381,26 +381,26 @@
   48.31  
   48.32  lemma restrict_fun_upd [simp]:
   48.33    "m(x := y)|`D = (if x \<in> D then (m|`(D-{x}))(x := y) else m|`D)"
   48.34 -by (simp add: restrict_map_def expand_fun_eq)
   48.35 +by (simp add: restrict_map_def ext_iff)
   48.36  
   48.37  lemma fun_upd_None_restrict [simp]:
   48.38    "(m|`D)(x := None) = (if x:D then m|`(D - {x}) else m|`D)"
   48.39 -by (simp add: restrict_map_def expand_fun_eq)
   48.40 +by (simp add: restrict_map_def ext_iff)
   48.41  
   48.42  lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
   48.43 -by (simp add: restrict_map_def expand_fun_eq)
   48.44 +by (simp add: restrict_map_def ext_iff)
   48.45  
   48.46  lemma fun_upd_restrict_conv [simp]:
   48.47    "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
   48.48 -by (simp add: restrict_map_def expand_fun_eq)
   48.49 +by (simp add: restrict_map_def ext_iff)
   48.50  
   48.51  lemma map_of_map_restrict:
   48.52    "map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
   48.53 -  by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
   48.54 +  by (induct ks) (simp_all add: ext_iff restrict_map_insert)
   48.55  
   48.56  lemma restrict_complement_singleton_eq:
   48.57    "f |` (- {x}) = f(x := None)"
   48.58 -  by (simp add: restrict_map_def expand_fun_eq)
   48.59 +  by (simp add: restrict_map_def ext_iff)
   48.60  
   48.61  
   48.62  subsection {* @{term [source] map_upds} *}
   48.63 @@ -641,7 +641,7 @@
   48.64  by (fastsimp simp add: map_le_def)
   48.65  
   48.66  lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
   48.67 -by(fastsimp simp: map_add_def map_le_def expand_fun_eq split: option.splits)
   48.68 +by(fastsimp simp: map_add_def map_le_def ext_iff split: option.splits)
   48.69  
   48.70  lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
   48.71  by (fastsimp simp add: map_le_def map_add_def dom_def)
    49.1 --- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Mon Sep 06 22:58:06 2010 +0200
    49.2 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Tue Sep 07 10:05:19 2010 +0200
    49.3 @@ -68,7 +68,7 @@
    49.4  (**********************************************************************)
    49.5  
    49.6  lemma the_map_upd: "(the \<circ> f(x\<mapsto>v)) = (the \<circ> f)(x:=v)"
    49.7 -by (simp add: expand_fun_eq)
    49.8 +by (simp add: ext_iff)
    49.9  
   49.10  lemma map_of_in_set: 
   49.11    "(map_of xs x = None) = (x \<notin> set (map fst xs))"
    50.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Mon Sep 06 22:58:06 2010 +0200
    50.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Tue Sep 07 10:05:19 2010 +0200
    50.3 @@ -113,7 +113,7 @@
    50.4  by (auto simp add: subcls1_def2 comp_classname comp_is_class)
    50.5  
    50.6  lemma comp_widen: "widen (comp G) = widen G"
    50.7 -  apply (simp add: expand_fun_eq)
    50.8 +  apply (simp add: ext_iff)
    50.9    apply (intro allI iffI)
   50.10    apply (erule widen.cases) 
   50.11    apply (simp_all add: comp_subcls1 widen.null)
   50.12 @@ -122,7 +122,7 @@
   50.13    done
   50.14  
   50.15  lemma comp_cast: "cast (comp G) = cast G"
   50.16 -  apply (simp add: expand_fun_eq)
   50.17 +  apply (simp add: ext_iff)
   50.18    apply (intro allI iffI)
   50.19    apply (erule cast.cases) 
   50.20    apply (simp_all add: comp_subcls1 cast.widen cast.subcls)
   50.21 @@ -133,7 +133,7 @@
   50.22    done
   50.23  
   50.24  lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G"
   50.25 -  by (simp add: expand_fun_eq cast_ok_def comp_widen)
   50.26 +  by (simp add: ext_iff cast_ok_def comp_widen)
   50.27  
   50.28  
   50.29  lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)"
   50.30 @@ -171,7 +171,7 @@
   50.31  apply (subgoal_tac "(Fun.comp fst (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
   50.32    (C, cno, fdls, map (compMethod G C) jmdls))) = fst")
   50.33  apply (simp del: image_compose)
   50.34 -apply (simp add: expand_fun_eq split_beta)
   50.35 +apply (simp add: ext_iff split_beta)
   50.36  done
   50.37  
   50.38  
   50.39 @@ -322,7 +322,7 @@
   50.40    = (\<lambda>x. (fst x, Object, fst (snd x),
   50.41                          snd (snd (compMethod G Object (S, snd x)))))")
   50.42  apply (simp only:)
   50.43 -apply (simp add: expand_fun_eq)
   50.44 +apply (simp add: ext_iff)
   50.45  apply (intro strip)
   50.46  apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)")
   50.47  apply (simp only:)
    51.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Mon Sep 06 22:58:06 2010 +0200
    51.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Sep 07 10:05:19 2010 +0200
    51.3 @@ -725,7 +725,7 @@
    51.4  	    hence "a_max = a'" using a' min_max by auto
    51.5  	    thus False unfolding True using min_max by auto qed qed
    51.6  	hence "\<forall>i. a_max i = a1 i" by auto
    51.7 -	hence "a' = a" unfolding True `a=a0` apply-apply(subst expand_fun_eq,rule)
    51.8 +	hence "a' = a" unfolding True `a=a0` apply-apply(subst ext_iff,rule)
    51.9  	  apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
   51.10  	proof- case goal1 thus ?case apply(cases "x\<in>{1..n}") by auto qed
   51.11  	hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` by auto
   51.12 @@ -738,7 +738,7 @@
   51.13  	  have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto
   51.14  	  hence "a2 \<in> s - {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[THEN sym] by auto qed
   51.15  	hence "\<forall>i. a_min i = a2 i" by auto
   51.16 -	hence "a' = a3" unfolding as `a=a0` apply-apply(subst expand_fun_eq,rule)
   51.17 +	hence "a' = a3" unfolding as `a=a0` apply-apply(subst ext_iff,rule)
   51.18  	  apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format]
   51.19  	  unfolding a3_def k(2)[rule_format] unfolding a0a1(5)[rule_format] proof- case goal1
   51.20  	  show ?case unfolding goal1 apply(cases "x\<in>{1..n}") defer apply(cases "x=k")
   51.21 @@ -834,7 +834,7 @@
   51.22  	proof- case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed
   51.23  	have "\<forall>i. a_min i = a3 i" using a_max apply-apply(rule,erule_tac x=i in allE)
   51.24  	  unfolding min_max(5)[rule_format] *[rule_format] proof- case goal1
   51.25 -	  thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding expand_fun_eq .
   51.26 +	  thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding ext_iff .
   51.27  	hence "s' = insert a3 (s - {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next
   51.28  	case False hence as:"a'=a_max" using ** by auto
   51.29  	have "a_min = a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule)
   51.30 @@ -843,7 +843,7 @@
   51.31  	  thus "a_min \<in> s" by auto have "a0 \<in> s - {a1}" using a0a1(1-3) by auto thus "a0 \<in> s'"
   51.32  	    unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed
   51.33  	hence "\<forall>i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto
   51.34 -	hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding expand_fun_eq by auto
   51.35 +	hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding ext_iff by auto
   51.36  	thus ?thesis by auto qed qed 
   51.37      ultimately have *:"?A = {s, insert a3 (s - {a1})}" by blast
   51.38      have "s \<noteq> insert a3 (s - {a1})" using `a3\<notin>s` by auto
   51.39 @@ -863,7 +863,7 @@
   51.40        thus False using ksimplexD(6)[OF assms(1),rule_format,OF u v] unfolding kle_def
   51.41  	unfolding l(2) k(2) `k=l` apply-apply(erule disjE)apply(erule_tac[!] exE conjE)+
   51.42  	apply(erule_tac[!] x=l in allE)+ by(auto simp add: *) qed
   51.43 -    hence aa':"a'\<noteq>a" apply-apply rule unfolding expand_fun_eq unfolding a'_def k(2)
   51.44 +    hence aa':"a'\<noteq>a" apply-apply rule unfolding ext_iff unfolding a'_def k(2)
   51.45        apply(erule_tac x=l in allE) by auto
   51.46      have "a' \<notin> s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`]) proof(cases "kle n a a'")
   51.47        case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise)
   51.48 @@ -877,22 +877,22 @@
   51.49      have uxv:"\<And>x. kle n u x \<Longrightarrow> kle n x v \<Longrightarrow> (x = u) \<or> (x = a) \<or> (x = a') \<or> (x = v)"
   51.50      proof- case goal1 thus ?case proof(cases "x k = u k", case_tac[!] "x l = u l")
   51.51        assume as:"x l = u l" "x k = u k"
   51.52 -      have "x = u" unfolding expand_fun_eq
   51.53 +      have "x = u" unfolding ext_iff
   51.54  	using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2) apply-
   51.55  	using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
   51.56  	thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
   51.57        assume as:"x l \<noteq> u l" "x k = u k"
   51.58 -      have "x = a'" unfolding expand_fun_eq unfolding a'_def
   51.59 +      have "x = a'" unfolding ext_iff unfolding a'_def
   51.60  	using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
   51.61  	using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
   51.62  	thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
   51.63        assume as:"x l = u l" "x k \<noteq> u k"
   51.64 -      have "x = a" unfolding expand_fun_eq
   51.65 +      have "x = a" unfolding ext_iff
   51.66  	using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
   51.67  	using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
   51.68  	thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next
   51.69        assume as:"x l \<noteq> u l" "x k \<noteq> u k"
   51.70 -      have "x = v" unfolding expand_fun_eq
   51.71 +      have "x = v" unfolding ext_iff
   51.72  	using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply-
   51.73  	using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1
   51.74  	thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\<noteq>l` by auto qed thus ?case by auto qed qed
   51.75 @@ -935,9 +935,9 @@
   51.76      moreover have "?A \<subseteq> {s, insert a' (s - {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)
   51.77        fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
   51.78        from this(2) guess a'' .. note a''=this
   51.79 -      have "u\<noteq>v" unfolding expand_fun_eq unfolding l(2) k(2) by auto
   51.80 +      have "u\<noteq>v" unfolding ext_iff unfolding l(2) k(2) by auto
   51.81        hence uv':"\<not> kle n v u" using uv using kle_antisym by auto
   51.82 -      have "u\<noteq>a" "v\<noteq>a" unfolding expand_fun_eq k(2) l(2) by auto 
   51.83 +      have "u\<noteq>a" "v\<noteq>a" unfolding ext_iff k(2) l(2) by auto 
   51.84        hence uvs':"u\<in>s'" "v\<in>s'" using `u\<in>s` `v\<in>s` using a'' by auto
   51.85        have lem6:"a \<in> s' \<or> a' \<in> s'" proof(cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
   51.86  	case False then guess w unfolding ball_simps .. note w=this
    52.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Sep 06 22:58:06 2010 +0200
    52.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Sep 07 10:05:19 2010 +0200
    52.3 @@ -1440,12 +1440,12 @@
    52.4  lemma interval_cart: fixes a :: "'a::ord^'n" shows
    52.5    "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
    52.6    "{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
    52.7 -  by (auto simp add: expand_set_eq vector_less_def vector_le_def)
    52.8 +  by (auto simp add: set_ext_iff vector_less_def vector_le_def)
    52.9  
   52.10  lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows
   52.11    "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
   52.12    "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
   52.13 -  using interval_cart[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def)
   52.14 +  using interval_cart[of a b] by(auto simp add: set_ext_iff vector_less_def vector_le_def)
   52.15  
   52.16  lemma interval_eq_empty_cart: fixes a :: "real^'n" shows
   52.17   "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
   52.18 @@ -1498,7 +1498,7 @@
   52.19  
   52.20  lemma interval_sing: fixes a :: "'a::linorder^'n" shows
   52.21   "{a .. a} = {a} \<and> {a<..<a} = {}"
   52.22 -apply(auto simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
   52.23 +apply(auto simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
   52.24  apply (simp add: order_eq_iff)
   52.25  apply (auto simp add: not_less less_imp_le)
   52.26  done
   52.27 @@ -1511,17 +1511,17 @@
   52.28    { fix i
   52.29      have "a $ i \<le> x $ i"
   52.30        using x order_less_imp_le[of "a$i" "x$i"]
   52.31 -      by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
   52.32 +      by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
   52.33    }
   52.34    moreover
   52.35    { fix i
   52.36      have "x $ i \<le> b $ i"
   52.37        using x order_less_imp_le[of "x$i" "b$i"]
   52.38 -      by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
   52.39 +      by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
   52.40    }
   52.41    ultimately
   52.42    show "a \<le> x \<and> x \<le> b"
   52.43 -    by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
   52.44 +    by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
   52.45  qed
   52.46  
   52.47  lemma subset_interval_cart: fixes a :: "real^'n" shows
   52.48 @@ -1540,7 +1540,7 @@
   52.49  
   52.50  lemma inter_interval_cart: fixes a :: "'a::linorder^'n" shows
   52.51   "{a .. b} \<inter> {c .. d} =  {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
   52.52 -  unfolding expand_set_eq and Int_iff and mem_interval_cart
   52.53 +  unfolding set_ext_iff and Int_iff and mem_interval_cart
   52.54    by auto
   52.55  
   52.56  lemma closed_interval_left_cart: fixes b::"real^'n"
   52.57 @@ -1656,7 +1656,7 @@
   52.58    shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
   52.59    "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
   52.60    using m0
   52.61 -apply (auto simp add: expand_fun_eq vector_add_ldistrib)
   52.62 +apply (auto simp add: ext_iff vector_add_ldistrib)
   52.63  by (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])
   52.64  
   52.65  lemma vector_affinity_eq:
   52.66 @@ -2119,10 +2119,10 @@
   52.67  
   52.68  lemma open_closed_interval_1: fixes a :: "real^1" shows
   52.69   "{a<..<b} = {a .. b} - {a, b}"
   52.70 -  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
   52.71 +  unfolding set_ext_iff apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
   52.72  
   52.73  lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
   52.74 -  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
   52.75 +  unfolding set_ext_iff apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
   52.76  
   52.77  lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
   52.78    "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
    53.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Sep 06 22:58:06 2010 +0200
    53.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Sep 07 10:05:19 2010 +0200
    53.3 @@ -191,7 +191,7 @@
    53.4  lemma affine_hull_finite:
    53.5    assumes "finite s"
    53.6    shows "affine hull s = {y. \<exists>u. setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
    53.7 -  unfolding affine_hull_explicit and expand_set_eq and mem_Collect_eq apply (rule,rule)
    53.8 +  unfolding affine_hull_explicit and set_ext_iff and mem_Collect_eq apply (rule,rule)
    53.9    apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof-
   53.10    fix x u assume "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
   53.11    thus "\<exists>sa u. finite sa \<and> \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x"
   53.12 @@ -709,7 +709,7 @@
   53.13      ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
   53.14        apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastsimp
   53.15      hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto  }
   53.16 -  ultimately show ?thesis unfolding expand_set_eq by blast
   53.17 +  ultimately show ?thesis unfolding set_ext_iff by blast
   53.18  qed
   53.19  
   53.20  subsection {* A stepping theorem for that expansion. *}
   53.21 @@ -882,7 +882,7 @@
   53.22  lemma convex_hull_caratheodory: fixes p::"('a::euclidean_space) set"
   53.23    shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
   53.24    (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
   53.25 -  unfolding convex_hull_explicit expand_set_eq mem_Collect_eq
   53.26 +  unfolding convex_hull_explicit set_ext_iff mem_Collect_eq
   53.27  proof(rule,rule)
   53.28    fix y let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
   53.29    assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
   53.30 @@ -939,7 +939,7 @@
   53.31  lemma caratheodory:
   53.32   "convex hull p = {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
   53.33        card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
   53.34 -  unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof-
   53.35 +  unfolding set_ext_iff apply(rule, rule) unfolding mem_Collect_eq proof-
   53.36    fix x assume "x \<in> convex hull p"
   53.37    then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
   53.38       "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"unfolding convex_hull_caratheodory by auto
   53.39 @@ -1029,7 +1029,7 @@
   53.40      case (Suc n)
   53.41      show ?case proof(cases "n=0")
   53.42        case True have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} = s"
   53.43 -        unfolding expand_set_eq and mem_Collect_eq proof(rule, rule)
   53.44 +        unfolding set_ext_iff and mem_Collect_eq proof(rule, rule)
   53.45          fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
   53.46          then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
   53.47          show "x\<in>s" proof(cases "card t = 0")
   53.48 @@ -1048,7 +1048,7 @@
   53.49        case False have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} =
   53.50          { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 
   53.51          0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> {x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> x \<in> convex hull t}}"
   53.52 -        unfolding expand_set_eq and mem_Collect_eq proof(rule,rule)
   53.53 +        unfolding set_ext_iff and mem_Collect_eq proof(rule,rule)
   53.54          fix x assume "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
   53.55            0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)"
   53.56          then obtain u v c t where obt:"x = (1 - c) *\<^sub>R u + c *\<^sub>R v"
    54.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Sep 06 22:58:06 2010 +0200
    54.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Sep 07 10:05:19 2010 +0200
    54.3 @@ -665,7 +665,7 @@
    54.4    have "\<forall>i<DIM('a). f' (basis i) = 0"
    54.5      by (simp add: euclidean_eq[of _ "0::'a"])
    54.6    with derivative_is_linear[OF deriv, THEN linear_componentwise, of _ 0]
    54.7 -  show ?thesis by (simp add: expand_fun_eq)
    54.8 +  show ?thesis by (simp add: ext_iff)
    54.9  qed
   54.10  
   54.11  lemma rolle: fixes f::"real\<Rightarrow>real"
   54.12 @@ -948,13 +948,13 @@
   54.13     assumes lf: "linear f" and gf: "f o g = id"
   54.14     shows "linear g"
   54.15   proof-
   54.16 -   from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def expand_fun_eq)
   54.17 +   from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def ext_iff)
   54.18       by metis 
   54.19     from linear_surjective_isomorphism[OF lf fi]
   54.20     obtain h:: "'a => 'a" where
   54.21       h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" by blast
   54.22     have "h = g" apply (rule ext) using gf h(2,3)
   54.23 -     apply (simp add: o_def id_def expand_fun_eq)
   54.24 +     apply (simp add: o_def id_def ext_iff)
   54.25       by metis
   54.26     with h(1) show ?thesis by blast
   54.27   qed
   54.28 @@ -1268,7 +1268,7 @@
   54.29    have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
   54.30      using assms [unfolded has_vector_derivative_def]
   54.31      by (rule frechet_derivative_unique_at)
   54.32 -  thus ?thesis unfolding expand_fun_eq by auto
   54.33 +  thus ?thesis unfolding ext_iff by auto
   54.34  qed
   54.35  
   54.36  lemma vector_derivative_unique_within_closed_interval: fixes f::"real \<Rightarrow> 'n::ordered_euclidean_space"
   54.37 @@ -1279,7 +1279,7 @@
   54.38      apply(rule frechet_derivative_unique_within_closed_interval[of "a" "b"])
   54.39      using assms(3-)[unfolded has_vector_derivative_def] using assms(1-2) by auto
   54.40    show ?thesis proof(rule ccontr) assume "f' \<noteq> f''" moreover
   54.41 -    hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1" using * by (auto simp: expand_fun_eq)
   54.42 +    hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1" using * by (auto simp: ext_iff)
   54.43      ultimately show False unfolding o_def by auto qed qed
   54.44  
   54.45  lemma vector_derivative_at:
    55.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Mon Sep 06 22:58:06 2010 +0200
    55.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Sep 07 10:05:19 2010 +0200
    55.3 @@ -141,7 +141,7 @@
    55.4        {fix i assume i: "i \<in> ?U"
    55.5          from i permutes_inv_o[OF pU] permutes_in_image[OF pU]
    55.6          have "((\<lambda>i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)"
    55.7 -          unfolding transpose_def by (simp add: expand_fun_eq)}
    55.8 +          unfolding transpose_def by (simp add: ext_iff)}
    55.9        then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
   55.10      qed
   55.11      finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth
   55.12 @@ -207,7 +207,7 @@
   55.13    have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
   55.14    {fix p assume p: "p \<in> ?PU - {id}"
   55.15      then have "p \<noteq> id" by simp
   55.16 -    then obtain i where i: "p i \<noteq> i" unfolding expand_fun_eq by auto
   55.17 +    then obtain i where i: "p i \<noteq> i" unfolding ext_iff by auto
   55.18      from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast
   55.19      from setprod_zero [OF fU ex] have "?pp p = 0" by simp}
   55.20    then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"  by blast
    56.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Sep 06 22:58:06 2010 +0200
    56.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Sep 07 10:05:19 2010 +0200
    56.3 @@ -2363,7 +2363,7 @@
    56.4        apply (rule span_mul)
    56.5        by (rule span_superset)}
    56.6    then have SC: "span ?C = span (insert a B)"
    56.7 -    unfolding expand_set_eq span_breakdown_eq C(3)[symmetric] by auto
    56.8 +    unfolding set_ext_iff span_breakdown_eq C(3)[symmetric] by auto
    56.9    thm pairwise_def
   56.10    {fix x y assume xC: "x \<in> ?C" and yC: "y \<in> ?C" and xy: "x \<noteq> y"
   56.11      {assume xa: "x = ?a" and ya: "y = ?a"
   56.12 @@ -2826,7 +2826,7 @@
   56.13      " \<forall>x \<in> f ` basis ` {..<DIM('a)}. h x = inv f x" by blast
   56.14    from h(2)
   56.15    have th: "\<forall>i<DIM('a). (h \<circ> f) (basis i) = id (basis i)"
   56.16 -    using inv_o_cancel[OF fi, unfolded expand_fun_eq id_def o_def]
   56.17 +    using inv_o_cancel[OF fi, unfolded ext_iff id_def o_def]
   56.18      by auto
   56.19  
   56.20    from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th]
   56.21 @@ -2843,7 +2843,7 @@
   56.22      h: "linear h" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
   56.23    from h(2)
   56.24    have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
   56.25 -    using sf by(auto simp add: surj_iff o_def expand_fun_eq)
   56.26 +    using sf by(auto simp add: surj_iff o_def ext_iff)
   56.27    from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
   56.28    have "f o h = id" .
   56.29    then show ?thesis using h(1) by blast
   56.30 @@ -2970,7 +2970,7 @@
   56.31  
   56.32  lemma isomorphism_expand:
   56.33    "f o g = id \<and> g o f = id \<longleftrightarrow> (\<forall>x. f(g x) = x) \<and> (\<forall>x. g(f x) = x)"
   56.34 -  by (simp add: expand_fun_eq o_def id_def)
   56.35 +  by (simp add: ext_iff o_def id_def)
   56.36  
   56.37  lemma linear_injective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space"
   56.38    assumes lf: "linear f" and fi: "inj f"
   56.39 @@ -2995,10 +2995,10 @@
   56.40    {fix f f':: "'a => 'a"
   56.41      assume lf: "linear f" "linear f'" and f: "f o f' = id"
   56.42      from f have sf: "surj f"
   56.43 -      apply (auto simp add: o_def expand_fun_eq id_def surj_def)
   56.44 +      apply (auto simp add: o_def ext_iff id_def surj_def)
   56.45        by metis
   56.46      from linear_surjective_isomorphism[OF lf(1) sf] lf f
   56.47 -    have "f' o f = id" unfolding expand_fun_eq o_def id_def
   56.48 +    have "f' o f = id" unfolding ext_iff o_def id_def
   56.49        by metis}
   56.50    then show ?thesis using lf lf' by metis
   56.51  qed
   56.52 @@ -3009,13 +3009,13 @@
   56.53    assumes lf: "linear f" and gf: "g o f = id"
   56.54    shows "linear g"
   56.55  proof-
   56.56 -  from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def expand_fun_eq)
   56.57 +  from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def ext_iff)
   56.58      by metis
   56.59    from linear_injective_isomorphism[OF lf fi]
   56.60    obtain h:: "'a \<Rightarrow> 'a" where
   56.61      h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" by blast
   56.62    have "h = g" apply (rule ext) using gf h(2,3)
   56.63 -    apply (simp add: o_def id_def expand_fun_eq)
   56.64 +    apply (simp add: o_def id_def ext_iff)
   56.65      by metis
   56.66    with h(1) show ?thesis by blast
   56.67  qed
    57.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Sep 06 22:58:06 2010 +0200
    57.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue Sep 07 10:05:19 2010 +0200
    57.3 @@ -42,7 +42,7 @@
    57.4    by (auto intro: ext)
    57.5  
    57.6  lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
    57.7 -  by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)
    57.8 +  by (simp add: Cart_nth_inject [symmetric] ext_iff)
    57.9  
   57.10  lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i"
   57.11    by (simp add: Cart_lambda_inverse)
    58.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 06 22:58:06 2010 +0200
    58.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 07 10:05:19 2010 +0200
    58.3 @@ -253,10 +253,10 @@
    58.4  lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
    58.5  lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq)
    58.6  lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
    58.7 -  by (simp add: expand_set_eq) arith
    58.8 +  by (simp add: set_ext_iff) arith
    58.9  
   58.10  lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
   58.11 -  by (simp add: expand_set_eq)
   58.12 +  by (simp add: set_ext_iff)
   58.13  
   58.14  lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
   58.15    "(a::real) - b < 0 \<longleftrightarrow> a < b"
   58.16 @@ -289,7 +289,7 @@
   58.17    by (metis open_contains_ball subset_eq centre_in_ball)
   58.18  
   58.19  lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
   58.20 -  unfolding mem_ball expand_set_eq
   58.21 +  unfolding mem_ball set_ext_iff
   58.22    apply (simp add: not_less)
   58.23    by (metis zero_le_dist order_trans dist_self)
   58.24  
   58.25 @@ -447,7 +447,7 @@
   58.26    let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
   58.27    have "open ?T" by (simp add: open_Union)
   58.28    also have "?T = - {a}"
   58.29 -    by (simp add: expand_set_eq separation_t1, auto)
   58.30 +    by (simp add: set_ext_iff separation_t1, auto)
   58.31    finally show "closed {a}" unfolding closed_def .
   58.32  qed
   58.33  
   58.34 @@ -483,7 +483,7 @@
   58.35                 ==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
   58.36    have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}"
   58.37      using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute]
   58.38 -    by (auto simp add: expand_set_eq)
   58.39 +    by (auto simp add: set_ext_iff)
   58.40    then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
   58.41      by blast
   58.42  qed
   58.43 @@ -641,7 +641,7 @@
   58.44  definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
   58.45  
   58.46  lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
   58.47 -  apply (simp add: expand_set_eq interior_def)
   58.48 +  apply (simp add: set_ext_iff interior_def)
   58.49    apply (subst (2) open_subopen) by (safe, blast+)
   58.50  
   58.51  lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
   58.52 @@ -706,7 +706,7 @@
   58.53      proof (rule ccontr)
   58.54        assume "x \<notin> interior S"
   58.55        with `x \<in> R` `open R` obtain y where "y \<in> R - S"
   58.56 -        unfolding interior_def expand_set_eq by fast
   58.57 +        unfolding interior_def set_ext_iff by fast
   58.58        from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
   58.59        from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
   58.60        from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
   58.61 @@ -1006,7 +1006,7 @@
   58.62      unfolding trivial_limit_def
   58.63      unfolding eventually_within eventually_at_topological
   58.64      unfolding islimpt_def
   58.65 -    apply (clarsimp simp add: expand_set_eq)
   58.66 +    apply (clarsimp simp add: set_ext_iff)
   58.67      apply (rename_tac T, rule_tac x=T in exI)
   58.68      apply (clarsimp, drule_tac x=y in bspec, simp_all)
   58.69      done
   58.70 @@ -1904,18 +1904,18 @@
   58.71    fixes a :: "'a::real_normed_vector"
   58.72    shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}"
   58.73    apply (simp add: frontier_def closure_ball interior_open order_less_imp_le)
   58.74 -  apply (simp add: expand_set_eq)
   58.75 +  apply (simp add: set_ext_iff)
   58.76    by arith
   58.77  
   58.78  lemma frontier_cball:
   58.79    fixes a :: "'a::{real_normed_vector, perfect_space}"
   58.80    shows "frontier(cball a e) = {x. dist a x = e}"
   58.81    apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le)
   58.82 -  apply (simp add: expand_set_eq)
   58.83 +  apply (simp add: set_ext_iff)
   58.84    by arith
   58.85  
   58.86  lemma cball_eq_empty: "(cball x e = {}) \<longleftrightarrow> e < 0"
   58.87 -  apply (simp add: expand_set_eq not_le)
   58.88 +  apply (simp add: set_ext_iff not_le)
   58.89    by (metis zero_le_dist dist_self order_less_le_trans)
   58.90  lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty)
   58.91  
   58.92 @@ -1927,13 +1927,13 @@
   58.93    obtain a where "a \<noteq> x" "dist a x < e"
   58.94      using perfect_choose_dist [OF e] by auto
   58.95    hence "a \<noteq> x" "dist x a \<le> e" by (auto simp add: dist_commute)
   58.96 -  with e show ?thesis by (auto simp add: expand_set_eq)
   58.97 +  with e show ?thesis by (auto simp add: set_ext_iff)
   58.98  qed auto
   58.99  
  58.100  lemma cball_sing:
  58.101    fixes x :: "'a::metric_space"
  58.102    shows "e = 0 ==> cball x e = {x}"
  58.103 -  by (auto simp add: expand_set_eq)
  58.104 +  by (auto simp add: set_ext_iff)
  58.105  
  58.106  text{* For points in the interior, localization of limits makes no difference.   *}
  58.107  
  58.108 @@ -4615,12 +4615,12 @@
  58.109  lemma interval: fixes a :: "'a::ordered_euclidean_space" shows
  58.110    "{a <..< b} = {x::'a. \<forall>i<DIM('a). a$$i < x$$i \<and> x$$i < b$$i}" and
  58.111    "{a .. b} = {x::'a. \<forall>i<DIM('a). a$$i \<le> x$$i \<and> x$$i \<le> b$$i}"
  58.112 -  by(auto simp add:expand_set_eq eucl_le[where 'a='a] eucl_less[where 'a='a])
  58.113 +  by(auto simp add:set_ext_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
  58.114  
  58.115  lemma mem_interval: fixes a :: "'a::ordered_euclidean_space" shows
  58.116    "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < x$$i \<and> x$$i < b$$i)"
  58.117    "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i \<le> x$$i \<and> x$$i \<le> b$$i)"
  58.118 -  using interval[of a b] by(auto simp add: expand_set_eq eucl_le[where 'a='a] eucl_less[where 'a='a])
  58.119 +  using interval[of a b] by(auto simp add: set_ext_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
  58.120  
  58.121  lemma interval_eq_empty: fixes a :: "'a::ordered_euclidean_space" shows
  58.122   "({a <..< b} = {} \<longleftrightarrow> (\<exists>i<DIM('a). b$$i \<le> a$$i))" (is ?th1) and
  58.123 @@ -4662,7 +4662,7 @@
  58.124  
  58.125  lemma interval_sing: fixes a :: "'a::ordered_euclidean_space" shows
  58.126   "{a .. a} = {a}" "{a<..<a} = {}"
  58.127 -  apply(auto simp add: expand_set_eq euclidean_eq[where 'a='a] eucl_less[where 'a='a] eucl_le[where 'a='a])
  58.128 +  apply(auto simp add: set_ext_iff euclidean_eq[where 'a='a] eucl_less[where 'a='a] eucl_le[where 'a='a])
  58.129    apply (simp add: order_eq_iff) apply(rule_tac x=0 in exI) by (auto simp add: not_less less_imp_le)
  58.130  
  58.131  lemma subset_interval_imp: fixes a :: "'a::ordered_euclidean_space" shows
  58.132 @@ -4681,17 +4681,17 @@
  58.133    { fix i assume "i<DIM('a)"
  58.134      hence "a $$ i \<le> x $$ i"
  58.135        using x order_less_imp_le[of "a$$i" "x$$i"] 
  58.136 -      by(simp add: expand_set_eq eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
  58.137 +      by(simp add: set_ext_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
  58.138    }
  58.139    moreover
  58.140    { fix i assume "i<DIM('a)"
  58.141      hence "x $$ i \<le> b $$ i"
  58.142        using x order_less_imp_le[of "x$$i" "b$$i"]
  58.143 -      by(simp add: expand_set_eq eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
  58.144 +      by(simp add: set_ext_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
  58.145    }
  58.146    ultimately
  58.147    show "a \<le> x \<and> x \<le> b"
  58.148 -    by(simp add: expand_set_eq eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
  58.149 +    by(simp add: set_ext_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
  58.150  qed
  58.151  
  58.152  lemma subset_interval: fixes a :: "'a::ordered_euclidean_space" shows
  58.153 @@ -4757,7 +4757,7 @@
  58.154    "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i<DIM('a). (b$$i \<le> a$$i \<or> d$$i \<le> c$$i \<or> b$$i \<le> c$$i \<or> d$$i \<le> a$$i))" (is ?th4)
  58.155  proof-
  58.156    let ?z = "(\<chi>\<chi> i. ((max (a$$i) (c$$i)) + (min (b$$i) (d$$i))) / 2)::'a"
  58.157 -  note * = expand_set_eq Int_iff empty_iff mem_interval all_conj_distrib[THEN sym] eq_False
  58.158 +  note * = set_ext_iff Int_iff empty_iff mem_interval all_conj_distrib[THEN sym] eq_False
  58.159    show ?th1 unfolding * apply safe apply(erule_tac x="?z" in allE)
  58.160      unfolding not_all apply(erule exE,rule_tac x=x in exI) apply(erule_tac[2-] x=i in allE) by auto
  58.161    show ?th2 unfolding * apply safe apply(erule_tac x="?z" in allE)
  58.162 @@ -4770,7 +4770,7 @@
  58.163  
  58.164  lemma inter_interval: fixes a :: "'a::ordered_euclidean_space" shows
  58.165   "{a .. b} \<inter> {c .. d} =  {(\<chi>\<chi> i. max (a$$i) (c$$i)) .. (\<chi>\<chi> i. min (b$$i) (d$$i))}"
  58.166 -  unfolding expand_set_eq and Int_iff and mem_interval
  58.167 +  unfolding set_ext_iff and Int_iff and mem_interval
  58.168    by auto
  58.169  
  58.170  (* Moved interval_open_subset_closed a bit upwards *)
  58.171 @@ -5440,7 +5440,7 @@
  58.172      then obtain x where "\<forall>n. x n \<in> s \<and> g n = f (x n)" 
  58.173        using choice[of "\<lambda> n xa. xa \<in> s \<and> g n = f xa"] by auto
  58.174      hence x:"\<forall>n. x n \<in> s"  "\<forall>n. g n = f (x n)" by auto
  58.175 -    hence "f \<circ> x = g" unfolding expand_fun_eq by auto
  58.176 +    hence "f \<circ> x = g" unfolding ext_iff by auto
  58.177      then obtain l where "l\<in>s" and l:"(x ---> l) sequentially"
  58.178        using cs[unfolded complete_def, THEN spec[where x="x"]]
  58.179        using cauchy_isometric[OF `0<e` s f normf] and cfg and x(1) by auto
    59.1 --- a/src/HOL/NSA/NatStar.thy	Mon Sep 06 22:58:06 2010 +0200
    59.2 +++ b/src/HOL/NSA/NatStar.thy	Tue Sep 07 10:05:19 2010 +0200
    59.3 @@ -115,7 +115,7 @@
    59.4    @{term real_of_nat} *}
    59.5  
    59.6  lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
    59.7 -by transfer (simp add: expand_fun_eq real_of_nat_def)
    59.8 +by transfer (simp add: ext_iff real_of_nat_def)
    59.9  
   59.10  lemma starfun_inverse_real_of_nat_eq:
   59.11       "N \<in> HNatInfinite
    60.1 --- a/src/HOL/NSA/Star.thy	Mon Sep 06 22:58:06 2010 +0200
    60.2 +++ b/src/HOL/NSA/Star.thy	Tue Sep 07 10:05:19 2010 +0200
    60.3 @@ -87,7 +87,7 @@
    60.4     sequence) as a special case of an internal set*}
    60.5  
    60.6  lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
    60.7 -apply (drule expand_fun_eq [THEN iffD2])
    60.8 +apply (drule ext_iff [THEN iffD2])
    60.9  apply (simp add: starset_n_def starset_def star_of_def)
   60.10  done
   60.11  
   60.12 @@ -102,7 +102,7 @@
   60.13  (*----------------------------------------------------------------*)
   60.14  
   60.15  lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f"
   60.16 -apply (drule expand_fun_eq [THEN iffD2])
   60.17 +apply (drule ext_iff [THEN iffD2])
   60.18  apply (simp add: starfun_n_def starfun_def star_of_def)
   60.19  done
   60.20  
    61.1 --- a/src/HOL/NSA/StarDef.thy	Mon Sep 06 22:58:06 2010 +0200
    61.2 +++ b/src/HOL/NSA/StarDef.thy	Tue Sep 07 10:05:19 2010 +0200
    61.3 @@ -145,7 +145,7 @@
    61.4    "\<lbrakk>\<And>X. f (star_n X) = g (star_n X) 
    61.5      \<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
    61.6        \<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
    61.7 -by (simp only: expand_fun_eq transfer_all)
    61.8 +by (simp only: ext_iff transfer_all)
    61.9  
   61.10  lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
   61.11  by (rule reflexive)
   61.12 @@ -351,12 +351,12 @@
   61.13  lemma transfer_Collect [transfer_intro]:
   61.14    "\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
   61.15      \<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
   61.16 -by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n)
   61.17 +by (simp add: atomize_eq set_ext_iff all_star_eq Iset_star_n)
   61.18  
   61.19  lemma transfer_set_eq [transfer_intro]:
   61.20    "\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
   61.21      \<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
   61.22 -by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem)
   61.23 +by (simp only: set_ext_iff transfer_all transfer_iff transfer_mem)
   61.24  
   61.25  lemma transfer_ball [transfer_intro]:
   61.26    "\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
    62.1 --- a/src/HOL/Nat.thy	Mon Sep 06 22:58:06 2010 +0200
    62.2 +++ b/src/HOL/Nat.thy	Tue Sep 07 10:05:19 2010 +0200
    62.3 @@ -1360,7 +1360,7 @@
    62.4    by (induct n) simp_all
    62.5  
    62.6  lemma of_nat_eq_id [simp]: "of_nat = id"
    62.7 -  by (auto simp add: expand_fun_eq)
    62.8 +  by (auto simp add: ext_iff)
    62.9  
   62.10  
   62.11  subsection {* The Set of Natural Numbers *}
    63.1 --- a/src/HOL/Nat_Transfer.thy	Mon Sep 06 22:58:06 2010 +0200
    63.2 +++ b/src/HOL/Nat_Transfer.thy	Tue Sep 07 10:05:19 2010 +0200
    63.3 @@ -170,7 +170,7 @@
    63.4    apply (rule iffI)
    63.5    apply (erule finite_imageI)
    63.6    apply (erule finite_imageD)
    63.7 -  apply (auto simp add: image_def expand_set_eq inj_on_def)
    63.8 +  apply (auto simp add: image_def set_ext_iff inj_on_def)
    63.9    apply (drule_tac x = "int x" in spec, auto)
   63.10    apply (drule_tac x = "int x" in spec, auto)
   63.11    apply (drule_tac x = "int x" in spec, auto)
    64.1 --- a/src/HOL/Nitpick.thy	Mon Sep 06 22:58:06 2010 +0200
    64.2 +++ b/src/HOL/Nitpick.thy	Tue Sep 07 10:05:19 2010 +0200
    64.3 @@ -59,7 +59,7 @@
    64.4  lemma Ex1_def [nitpick_def, no_atp]:
    64.5  "Ex1 P \<equiv> \<exists>x. P = {x}"
    64.6  apply (rule eq_reflection)
    64.7 -apply (simp add: Ex1_def expand_set_eq)
    64.8 +apply (simp add: Ex1_def set_ext_iff)
    64.9  apply (rule iffI)
   64.10   apply (erule exE)
   64.11   apply (erule conjE)
    65.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Sep 06 22:58:06 2010 +0200
    65.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 07 10:05:19 2010 +0200
    65.3 @@ -110,7 +110,7 @@
    65.4  "my_int_rel (x, y) (u, v) = (x + v = u + y)"
    65.5  
    65.6  quotient_type my_int = "nat \<times> nat" / my_int_rel
    65.7 -by (auto simp add: equivp_def expand_fun_eq)
    65.8 +by (auto simp add: equivp_def ext_iff)
    65.9  
   65.10  definition add_raw where
   65.11  "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
    66.1 --- a/src/HOL/Nominal/Examples/Class1.thy	Mon Sep 06 22:58:06 2010 +0200
    66.2 +++ b/src/HOL/Nominal/Examples/Class1.thy	Tue Sep 07 10:05:19 2010 +0200
    66.3 @@ -2167,7 +2167,7 @@
    66.4  apply(auto simp add: fresh_left calc_atm forget)
    66.5  apply(generate_fresh "coname")
    66.6  apply(rule_tac f="fresh_fun" in arg_cong)
    66.7 -apply(simp add:  expand_fun_eq)
    66.8 +apply(simp add:  ext_iff)
    66.9  apply(rule allI)
   66.10  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.11  apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto)
   66.12 @@ -2183,7 +2183,7 @@
   66.13  apply(auto simp add: fresh_left calc_atm forget)
   66.14  apply(generate_fresh "name")
   66.15  apply(rule_tac f="fresh_fun" in arg_cong)
   66.16 -apply(simp add:  expand_fun_eq)
   66.17 +apply(simp add:  ext_iff)
   66.18  apply(rule allI)
   66.19  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.20  apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto)
   66.21 @@ -2199,13 +2199,13 @@
   66.22  apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
   66.23  apply(generate_fresh "name")
   66.24  apply(rule_tac f="fresh_fun" in arg_cong)
   66.25 -apply(simp add:  expand_fun_eq)
   66.26 +apply(simp add:  ext_iff)
   66.27  apply(rule allI)
   66.28  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.29  apply(rule forget)
   66.30  apply(simp add: fresh_left calc_atm)
   66.31  apply(rule_tac f="fresh_fun" in arg_cong)
   66.32 -apply(simp add:  expand_fun_eq)
   66.33 +apply(simp add:  ext_iff)
   66.34  apply(rule allI)
   66.35  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.36  apply(rule forget)
   66.37 @@ -2224,13 +2224,13 @@
   66.38  apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
   66.39  apply(generate_fresh "name")
   66.40  apply(rule_tac f="fresh_fun" in arg_cong)
   66.41 -apply(simp add:  expand_fun_eq)
   66.42 +apply(simp add:  ext_iff)
   66.43  apply(rule allI)
   66.44  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.45  apply(rule forget)
   66.46  apply(simp add: fresh_left calc_atm)
   66.47  apply(rule_tac f="fresh_fun" in arg_cong)
   66.48 -apply(simp add:  expand_fun_eq)
   66.49 +apply(simp add:  ext_iff)
   66.50  apply(rule allI)
   66.51  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.52  apply(rule forget)
   66.53 @@ -2255,7 +2255,7 @@
   66.54  apply(auto simp add: fresh_prod fresh_atm)[1]
   66.55  apply(simp)
   66.56  apply(rule_tac f="fresh_fun" in arg_cong)
   66.57 -apply(simp add:  expand_fun_eq)
   66.58 +apply(simp add:  ext_iff)
   66.59  apply(rule allI)
   66.60  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.61  apply(rule conjI)
   66.62 @@ -2283,7 +2283,7 @@
   66.63  apply(auto simp add: fresh_prod fresh_atm)[1]
   66.64  apply(simp)
   66.65  apply(rule_tac f="fresh_fun" in arg_cong)
   66.66 -apply(simp add:  expand_fun_eq)
   66.67 +apply(simp add:  ext_iff)
   66.68  apply(rule allI)
   66.69  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.70  apply(rule conjI)
   66.71 @@ -2304,13 +2304,13 @@
   66.72  apply(subgoal_tac "OrR1 <a>.M d = OrR1 <c>.([(c,a)]\<bullet>M) d")
   66.73  apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
   66.74  apply(rule_tac f="fresh_fun" in arg_cong)
   66.75 -apply(simp add:  expand_fun_eq)
   66.76 +apply(simp add:  ext_iff)
   66.77  apply(rule allI)
   66.78  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.79  apply(rule forget)
   66.80  apply(simp add: fresh_left calc_atm)
   66.81  apply(rule_tac f="fresh_fun" in arg_cong)
   66.82 -apply(simp add:  expand_fun_eq)
   66.83 +apply(simp add:  ext_iff)
   66.84  apply(rule allI)
   66.85  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.86  apply(rule forget)
   66.87 @@ -2328,13 +2328,13 @@
   66.88  apply(subgoal_tac "OrR2 <a>.M d = OrR2 <c>.([(c,a)]\<bullet>M) d")
   66.89  apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
   66.90  apply(rule_tac f="fresh_fun" in arg_cong)
   66.91 -apply(simp add:  expand_fun_eq)
   66.92 +apply(simp add:  ext_iff)
   66.93  apply(rule allI)
   66.94  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
   66.95  apply(rule forget)
   66.96  apply(simp add: fresh_left calc_atm)
   66.97  apply(rule_tac f="fresh_fun" in arg_cong)
   66.98 -apply(simp add:  expand_fun_eq)
   66.99 +apply(simp add:  ext_iff)
  66.100  apply(rule allI)
  66.101  apply(simp add: trm.inject alpha fresh_prod fresh_atm)
  66.102  apply(rule forget)
  66.103 @@ -2353,13 +2353,13 @@
  66.104  apply(subgoal_tac "ImpR (x).<a>.M d = ImpR (ca).<c>.([(c,a)]\<bullet>[(ca,x)]\<bullet>M) d")
  66.105  apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
  66.106  apply(rule_tac f="fresh_fun" in arg_cong)
  66.107 -apply(simp add:  expand_fun_eq)
  66.108 +apply(simp add:  ext_iff)
  66.109  apply(rule allI)
  66.110  apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
  66.111  apply(rule forget)
  66.112  apply(simp add: fresh_left calc_atm)
  66.113  apply(rule_tac f="fresh_fun" in arg_cong)
  66.114 -apply(simp add:  expand_fun_eq)
  66.115 +apply(simp add:  ext_iff)
  66.116  apply(rule allI)
  66.117  apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh)
  66.118  apply(rule forget)
  66.119 @@ -2378,7 +2378,7 @@
  66.120  apply(subgoal_tac "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]\<bullet>M) (caa).([(caa,x)]\<bullet>N) y")
  66.121  apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
  66.122  apply(rule_tac f="fresh_fun" in arg_cong)
  66.123 -apply(simp add:  expand_fun_eq)
  66.124 +apply(simp add:  ext_iff)
  66.125  apply(rule allI)
  66.126  apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
  66.127  apply(rule forget)
    67.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Sep 06 22:58:06 2010 +0200
    67.2 +++ b/src/HOL/Nominal/Nominal.thy	Tue Sep 07 10:05:19 2010 +0200
    67.3 @@ -148,11 +148,11 @@
    67.4  (* permutation on sets *)
    67.5  lemma empty_eqvt:
    67.6    shows "pi\<bullet>{} = {}"
    67.7 -  by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] expand_fun_eq)
    67.8 +  by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] ext_iff)
    67.9  
   67.10  lemma union_eqvt:
   67.11    shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
   67.12 -  by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] expand_fun_eq)
   67.13 +  by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] ext_iff)
   67.14  
   67.15  (* permutations on products *)
   67.16  lemma fst_eqvt:
   67.17 @@ -2069,7 +2069,7 @@
   67.18    show "?LHS"
   67.19    proof (rule ccontr)
   67.20      assume "(pi\<bullet>f) \<noteq> f"
   67.21 -    hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: expand_fun_eq)
   67.22 +    hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: ext_iff)
   67.23      then obtain x where b1: "(pi\<bullet>f) x \<noteq> f x" by force
   67.24      from b have "pi\<bullet>(f ((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" by force
   67.25      hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" 
   67.26 @@ -2763,7 +2763,7 @@
   67.27    and     at: "at TYPE ('x)"
   67.28    shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
   67.29  using c1 c2
   67.30 -apply(auto simp add: cp_def perm_fun_def expand_fun_eq)
   67.31 +apply(auto simp add: cp_def perm_fun_def ext_iff)
   67.32  apply(simp add: rev_eqvt[symmetric])
   67.33  apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at])
   67.34  done
   67.35 @@ -2988,7 +2988,7 @@
   67.36    and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
   67.37    shows "pi\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
   67.38    apply(simp add: abs_fun_def perm_fun_def abs_fun_if)
   67.39 -  apply(simp only: expand_fun_eq)
   67.40 +  apply(simp only: ext_iff)
   67.41    apply(rule allI)
   67.42    apply(subgoal_tac "(((rev pi)\<bullet>(xa::'y)) = (a::'y)) = (xa = pi\<bullet>a)")(*A*)
   67.43    apply(subgoal_tac "(((rev pi)\<bullet>xa)\<sharp>x) = (xa\<sharp>(pi\<bullet>x))")(*B*)
   67.44 @@ -3029,7 +3029,7 @@
   67.45    and   a  :: "'x"
   67.46    shows "([a].x = [a].y) = (x = y)"
   67.47  apply(auto simp add: abs_fun_def)
   67.48 -apply(auto simp add: expand_fun_eq)
   67.49 +apply(auto simp add: ext_iff)
   67.50  apply(drule_tac x="a" in spec)
   67.51  apply(simp)
   67.52  done
   67.53 @@ -3045,7 +3045,7 @@
   67.54        and a2: "[a].x = [b].y" 
   67.55    shows "x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
   67.56  proof -
   67.57 -  from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: expand_fun_eq)
   67.58 +  from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: ext_iff)
   67.59    hence "([a].x) a = ([b].y) a" by simp
   67.60    hence a3: "nSome(x) = ([b].y) a" by (simp add: abs_fun_def)
   67.61    show "x=[(a,b)]\<bullet>y \<and> a\<sharp>y"
   67.62 @@ -3076,7 +3076,7 @@
   67.63    shows "[a].x =[b].y"
   67.64  proof -
   67.65    show ?thesis 
   67.66 -  proof (simp only: abs_fun_def expand_fun_eq, intro strip)
   67.67 +  proof (simp only: abs_fun_def ext_iff, intro strip)
   67.68      fix c::"'x"
   67.69      let ?LHS = "if c=a then nSome(x) else if c\<sharp>x then nSome([(a,c)]\<bullet>x) else nNone"
   67.70      and ?RHS = "if c=b then nSome(y) else if c\<sharp>y then nSome([(b,c)]\<bullet>y) else nNone"
    68.1 --- a/src/HOL/Predicate.thy	Mon Sep 06 22:58:06 2010 +0200
    68.2 +++ b/src/HOL/Predicate.thy	Tue Sep 07 10:05:19 2010 +0200
    68.3 @@ -72,7 +72,7 @@
    68.4    by (simp add: mem_def)
    68.5  
    68.6  lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
    68.7 -  by (simp add: expand_fun_eq mem_def)
    68.8 +  by (simp add: ext_iff mem_def)
    68.9  
   68.10  
   68.11  subsubsection {* Order relation *}
   68.12 @@ -99,10 +99,10 @@
   68.13    by (simp add: bot_fun_eq bot_bool_eq)
   68.14  
   68.15  lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
   68.16 -  by (auto simp add: expand_fun_eq)
   68.17 +  by (auto simp add: ext_iff)
   68.18  
   68.19  lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
   68.20 -  by (auto simp add: expand_fun_eq)
   68.21 +  by (auto simp add: ext_iff)
   68.22  
   68.23  
   68.24  subsubsection {* Binary union *}
   68.25 @@ -197,10 +197,10 @@
   68.26    by (auto simp add: SUP2_iff)
   68.27  
   68.28  lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
   68.29 -  by (simp add: SUP1_iff expand_fun_eq)
   68.30 +  by (simp add: SUP1_iff ext_iff)
   68.31  
   68.32  lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
   68.33 -  by (simp add: SUP2_iff expand_fun_eq)
   68.34 +  by (simp add: SUP2_iff ext_iff)
   68.35  
   68.36  
   68.37  subsubsection {* Intersections of families *}
   68.38 @@ -230,10 +230,10 @@
   68.39    by (auto simp add: INF2_iff)
   68.40  
   68.41  lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
   68.42 -  by (simp add: INF1_iff expand_fun_eq)
   68.43 +  by (simp add: INF1_iff ext_iff)
   68.44  
   68.45  lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
   68.46 -  by (simp add: INF2_iff expand_fun_eq)
   68.47 +  by (simp add: INF2_iff ext_iff)
   68.48  
   68.49  
   68.50  subsection {* Predicates as relations *}
   68.51 @@ -251,7 +251,7 @@
   68.52  
   68.53  lemma pred_comp_rel_comp_eq [pred_set_conv]:
   68.54    "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
   68.55 -  by (auto simp add: expand_fun_eq elim: pred_compE)
   68.56 +  by (auto simp add: ext_iff elim: pred_compE)
   68.57  
   68.58  
   68.59  subsubsection {* Converse *}
   68.60 @@ -276,7 +276,7 @@
   68.61  
   68.62  lemma conversep_converse_eq [pred_set_conv]:
   68.63    "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
   68.64 -  by (auto simp add: expand_fun_eq)
   68.65 +  by (auto simp add: ext_iff)
   68.66  
   68.67  lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
   68.68    by (iprover intro: order_antisym conversepI dest: conversepD)
   68.69 @@ -294,10 +294,10 @@
   68.70      (iprover intro: conversepI ext dest: conversepD)
   68.71  
   68.72  lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
   68.73 -  by (auto simp add: expand_fun_eq)
   68.74 +  by (auto simp add: ext_iff)
   68.75  
   68.76  lemma conversep_eq [simp]: "(op =)^--1 = op ="
   68.77 -  by (auto simp add: expand_fun_eq)
   68.78 +  by (auto simp add: ext_iff)
   68.79  
   68.80  
   68.81  subsubsection {* Domain *}
   68.82 @@ -347,7 +347,7 @@
   68.83    "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
   68.84  
   68.85  lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
   68.86 -  by (auto simp add: Powp_def expand_fun_eq)
   68.87 +  by (auto simp add: Powp_def ext_iff)
   68.88  
   68.89  lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]
   68.90  
   68.91 @@ -430,7 +430,7 @@
   68.92  
   68.93  lemma bind_bind:
   68.94    "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
   68.95 -  by (auto simp add: bind_def expand_fun_eq)
   68.96 +  by (auto simp add: bind_def ext_iff)
   68.97  
   68.98  lemma bind_single:
   68.99    "P \<guillemotright>= single = P"
  68.100 @@ -442,14 +442,14 @@
  68.101  
  68.102  lemma bottom_bind:
  68.103    "\<bottom> \<guillemotright>= P = \<bottom>"
  68.104 -  by (auto simp add: bot_pred_def bind_def expand_fun_eq)
  68.105 +  by (auto simp add: bot_pred_def bind_def ext_iff)
  68.106  
  68.107  lemma sup_bind:
  68.108    "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
  68.109 -  by (auto simp add: bind_def sup_pred_def expand_fun_eq)
  68.110 +  by (auto simp add: bind_def sup_pred_def ext_iff)
  68.111  
  68.112  lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
  68.113 -  by (auto simp add: bind_def Sup_pred_def SUP1_iff expand_fun_eq)
  68.114 +  by (auto simp add: bind_def Sup_pred_def SUP1_iff ext_iff)
  68.115  
  68.116  lemma pred_iffI:
  68.117    assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
  68.118 @@ -457,7 +457,7 @@
  68.119    shows "A = B"
  68.120  proof -
  68.121    from assms have "\<And>x. eval A x \<longleftrightarrow> eval B x" by blast
  68.122 -  then show ?thesis by (cases A, cases B) (simp add: expand_fun_eq)
  68.123 +  then show ?thesis by (cases A, cases B) (simp add: ext_iff)
  68.124  qed
  68.125    
  68.126  lemma singleI: "eval (single x) x"
  68.127 @@ -492,7 +492,7 @@
  68.128  
  68.129  lemma single_not_bot [simp]:
  68.130    "single x \<noteq> \<bottom>"
  68.131 -  by (auto simp add: single_def bot_pred_def expand_fun_eq)
  68.132 +  by (auto simp add: single_def bot_pred_def ext_iff)
  68.133  
  68.134  lemma not_bot:
  68.135    assumes "A \<noteq> \<bottom>"
  68.136 @@ -512,7 +512,7 @@
  68.137  
  68.138  lemma not_is_empty_single:
  68.139    "\<not> is_empty (single x)"
  68.140 -  by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq)
  68.141 +  by (auto simp add: is_empty_def single_def bot_pred_def ext_iff)
  68.142  
  68.143  lemma is_empty_sup:
  68.144    "is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
  68.145 @@ -543,7 +543,7 @@
  68.146    moreover from assm have "\<And>x. eval A x \<Longrightarrow> singleton dfault A = x"
  68.147      by (rule singleton_eqI)
  68.148    ultimately have "eval (single (singleton dfault A)) = eval A"
  68.149 -    by (simp (no_asm_use) add: single_def expand_fun_eq) blast
  68.150 +    by (simp (no_asm_use) add: single_def ext_iff) blast
  68.151    then show ?thesis by (simp add: eval_inject)
  68.152  qed
  68.153  
  68.154 @@ -714,13 +714,13 @@
  68.155    "member xq = eval (pred_of_seq xq)"
  68.156  proof (induct xq)
  68.157    case Empty show ?case
  68.158 -  by (auto simp add: expand_fun_eq elim: botE)
  68.159 +  by (auto simp add: ext_iff elim: botE)
  68.160  next
  68.161    case Insert show ?case
  68.162 -  by (auto simp add: expand_fun_eq elim: supE singleE intro: supI1 supI2 singleI)
  68.163 +  by (auto simp add: ext_iff elim: supE singleE intro: supI1 supI2 singleI)
  68.164  next
  68.165    case Join then show ?case
  68.166 -  by (auto simp add: expand_fun_eq elim: supE intro: supI1 supI2)
  68.167 +  by (auto simp add: ext_iff elim: supE intro: supI1 supI2)
  68.168  qed
  68.169  
  68.170  lemma eval_code [code]: "eval (Seq f) = member (f ())"
    69.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Mon Sep 06 22:58:06 2010 +0200
    69.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Tue Sep 07 10:05:19 2010 +0200
    69.3 @@ -79,10 +79,10 @@
    69.4  declare Let_def[code_pred_inline]
    69.5  
    69.6  lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
    69.7 -by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
    69.8 +by (auto simp add: insert_iff[unfolded mem_def] ext_iff intro!: eq_reflection)
    69.9  
   69.10  lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
   69.11 -by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection)
   69.12 +by (auto simp add: Diff_iff[unfolded mem_def] ext_iff intro!: eq_reflection)
   69.13  
   69.14  setup {* Code_Prolog.map_code_options (K
   69.15    {ensure_groundness = true,
    70.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Sep 06 22:58:06 2010 +0200
    70.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 07 10:05:19 2010 +0200
    70.3 @@ -31,7 +31,7 @@
    70.4  
    70.5  lemma [code_pred_inline]:
    70.6    "max = max_nat"
    70.7 -by (simp add: expand_fun_eq max_def max_nat_def)
    70.8 +by (simp add: ext_iff max_def max_nat_def)
    70.9  
   70.10  definition
   70.11    "max_of_my_Suc x = max x (Suc x)"
    71.1 --- a/src/HOL/Probability/Borel.thy	Mon Sep 06 22:58:06 2010 +0200
    71.2 +++ b/src/HOL/Probability/Borel.thy	Tue Sep 07 10:05:19 2010 +0200
    71.3 @@ -1031,7 +1031,7 @@
    71.4    have "f -` {\<omega>} \<inter> space M = {x\<in>space M. f x = \<omega>}" by auto
    71.5    with * have **: "{x\<in>space M. f x = \<omega>} \<in> sets M" by simp
    71.6    have f: "f = (\<lambda>x. if f x = \<omega> then \<omega> else Real (real (f x)))"
    71.7 -    by (simp add: expand_fun_eq Real_real)
    71.8 +    by (simp add: ext_iff Real_real)
    71.9    show "f \<in> borel_measurable M"
   71.10      apply (subst f)
   71.11      apply (rule measurable_If)
   71.12 @@ -1264,7 +1264,7 @@
   71.13  proof -
   71.14    have *: "(\<lambda>x. f x + g x) =
   71.15       (\<lambda>x. if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else Real (real (f x) + real (g x)))"
   71.16 -     by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex)
   71.17 +     by (auto simp: ext_iff pinfreal_noteq_omega_Ex)
   71.18    show ?thesis using assms unfolding *
   71.19      by (auto intro!: measurable_If)
   71.20  qed
   71.21 @@ -1276,7 +1276,7 @@
   71.22    have *: "(\<lambda>x. f x * g x) =
   71.23       (\<lambda>x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else
   71.24        Real (real (f x) * real (g x)))"
   71.25 -     by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex)
   71.26 +     by (auto simp: ext_iff pinfreal_noteq_omega_Ex)
   71.27    show ?thesis using assms unfolding *
   71.28      by (auto intro!: measurable_If)
   71.29  qed
    72.1 --- a/src/HOL/Probability/Euclidean_Lebesgue.thy	Mon Sep 06 22:58:06 2010 +0200
    72.2 +++ b/src/HOL/Probability/Euclidean_Lebesgue.thy	Tue Sep 07 10:05:19 2010 +0200
    72.3 @@ -104,7 +104,7 @@
    72.4    from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u]
    72.5    show ?ilim using mono lim i by auto
    72.6    have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal
    72.7 -    unfolding expand_fun_eq SUPR_fun_expand mono_def by auto
    72.8 +    unfolding ext_iff SUPR_fun_expand mono_def by auto
    72.9    moreover have "(SUP i. f i) \<in> borel_measurable M"
   72.10      using i by (rule borel_measurable_SUP)
   72.11    ultimately show "u \<in> borel_measurable M" by simp
    73.1 --- a/src/HOL/Probability/Information.thy	Mon Sep 06 22:58:06 2010 +0200
    73.2 +++ b/src/HOL/Probability/Information.thy	Tue Sep 07 10:05:19 2010 +0200
    73.3 @@ -505,7 +505,7 @@
    73.4      by auto
    73.5    also have "\<dots> = log b (\<Sum>x\<in>X`space M. if ?d x \<noteq> 0 then 1 else 0)"
    73.6      apply (rule arg_cong[where f="\<lambda>f. log b (\<Sum>x\<in>X`space M. f x)"])
    73.7 -    using distribution_finite[of X] by (auto simp: expand_fun_eq real_of_pinfreal_eq_0)
    73.8 +    using distribution_finite[of X] by (auto simp: ext_iff real_of_pinfreal_eq_0)
    73.9    finally show ?thesis
   73.10      using finite_space by (auto simp: setsum_cases real_eq_of_nat)
   73.11  qed
   73.12 @@ -645,7 +645,7 @@
   73.13    let "?dZ A" = "real (distribution Z A)"
   73.14    let ?M = "X ` space M \<times> Y ` space M \<times> Z ` space M"
   73.15  
   73.16 -  have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: expand_fun_eq)
   73.17 +  have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: ext_iff)
   73.18  
   73.19    have "- (\<Sum>(x, y, z) \<in> ?M. ?dXYZ {(x, y, z)} *
   73.20      log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})))
    74.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Mon Sep 06 22:58:06 2010 +0200
    74.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Sep 07 10:05:19 2010 +0200
    74.3 @@ -1106,7 +1106,7 @@
    74.4      by (rule positive_integral_isoton)
    74.5         (auto intro!: borel_measurable_pinfreal_setsum assms positive_integral_mono
    74.6                       arg_cong[where f=Sup]
    74.7 -             simp: isoton_def le_fun_def psuminf_def expand_fun_eq SUPR_def Sup_fun_def)
    74.8 +             simp: isoton_def le_fun_def psuminf_def ext_iff SUPR_def Sup_fun_def)
    74.9    thus ?thesis
   74.10      by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms])
   74.11  qed
   74.12 @@ -1365,7 +1365,7 @@
   74.13      then have *: "(\<lambda>x. g x * indicator A x) = g"
   74.14        "\<And>x. g x * indicator A x = g x"
   74.15        "\<And>x. g x \<le> f x"
   74.16 -      by (auto simp: le_fun_def expand_fun_eq indicator_def split: split_if_asm)
   74.17 +      by (auto simp: le_fun_def ext_iff indicator_def split: split_if_asm)
   74.18      from g show "\<exists>x. simple_function (\<lambda>xa. x xa * indicator A xa) \<and> x \<le> f \<and> (\<forall>xa\<in>A. \<omega> \<noteq> x xa) \<and>
   74.19        simple_integral g = simple_integral (\<lambda>xa. x xa * indicator A xa)"
   74.20        using `A \<in> sets M`[THEN sets_into_space]
    75.1 --- a/src/HOL/Probability/Positive_Infinite_Real.thy	Mon Sep 06 22:58:06 2010 +0200
    75.2 +++ b/src/HOL/Probability/Positive_Infinite_Real.thy	Tue Sep 07 10:05:19 2010 +0200
    75.3 @@ -1036,7 +1036,7 @@
    75.4    qed
    75.5    from choice[OF this] obtain r where f: "f = (\<lambda>i. Real (r i))"
    75.6      and pos: "\<forall>i. 0 \<le> r i"
    75.7 -    by (auto simp: expand_fun_eq)
    75.8 +    by (auto simp: ext_iff)
    75.9    hence [simp]: "\<And>i. real (f i) = r i" by auto
   75.10  
   75.11    have "mono (\<lambda>n. setsum r {..<n})" (is "mono ?S")
   75.12 @@ -1156,7 +1156,7 @@
   75.13  lemma psuminf_0: "psuminf f = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
   75.14  proof safe
   75.15    assume "\<forall>i. f i = 0"
   75.16 -  hence "f = (\<lambda>i. 0)" by (simp add: expand_fun_eq)
   75.17 +  hence "f = (\<lambda>i. 0)" by (simp add: ext_iff)
   75.18    thus "psuminf f = 0" using psuminf_const by simp
   75.19  next
   75.20    fix i assume "psuminf f = 0"
    76.1 --- a/src/HOL/Probability/Probability_Space.thy	Mon Sep 06 22:58:06 2010 +0200
    76.2 +++ b/src/HOL/Probability/Probability_Space.thy	Tue Sep 07 10:05:19 2010 +0200
    76.3 @@ -34,14 +34,14 @@
    76.4  lemma (in prob_space) distribution_cong:
    76.5    assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x"
    76.6    shows "distribution X = distribution Y"
    76.7 -  unfolding distribution_def expand_fun_eq
    76.8 +  unfolding distribution_def ext_iff
    76.9    using assms by (auto intro!: arg_cong[where f="\<mu>"])
   76.10  
   76.11  lemma (in prob_space) joint_distribution_cong:
   76.12    assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"
   76.13    assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"
   76.14    shows "joint_distribution X Y = joint_distribution X' Y'"
   76.15 -  unfolding distribution_def expand_fun_eq
   76.16 +  unfolding distribution_def ext_iff
   76.17    using assms by (auto intro!: arg_cong[where f="\<mu>"])
   76.18  
   76.19  lemma prob_space: "prob (space M) = 1"
    77.1 --- a/src/HOL/Product_Type.thy	Mon Sep 06 22:58:06 2010 +0200
    77.2 +++ b/src/HOL/Product_Type.thy	Tue Sep 07 10:05:19 2010 +0200
    77.3 @@ -151,7 +151,7 @@
    77.4  next
    77.5    fix a c :: 'a and b d :: 'b
    77.6    have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
    77.7 -    by (auto simp add: Pair_Rep_def expand_fun_eq)
    77.8 +    by (auto simp add: Pair_Rep_def ext_iff)
    77.9    moreover have "Pair_Rep a b \<in> prod" and "Pair_Rep c d \<in> prod"
   77.10      by (auto simp add: prod_def)
   77.11    ultimately show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> b = d"
   77.12 @@ -394,7 +394,7 @@
   77.13    (Haskell "fst" and "snd")
   77.14  
   77.15  lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))"
   77.16 -  by (simp add: expand_fun_eq split: prod.split)
   77.17 +  by (simp add: ext_iff split: prod.split)
   77.18  
   77.19  lemma fst_eqD: "fst (x, y) = a ==> x = a"
   77.20    by simp
   77.21 @@ -423,11 +423,11 @@
   77.22    by (rule split_conv [THEN iffD1])
   77.23  
   77.24  lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
   77.25 -  by (simp add: expand_fun_eq split: prod.split)
   77.26 +  by (simp add: ext_iff split: prod.split)
   77.27  
   77.28  lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
   77.29    -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
   77.30 -  by (simp add: expand_fun_eq split: prod.split)
   77.31 +  by (simp add: ext_iff split: prod.split)
   77.32  
   77.33  lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
   77.34    by (cases x) simp
   77.35 @@ -797,25 +797,25 @@
   77.36    "f \<circ>\<rightarrow> g = (\<lambda>x. prod_case g (f x))"
   77.37  
   77.38  lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
   77.39 -  by (simp add: expand_fun_eq scomp_def prod_case_unfold)
   77.40 +  by (simp add: ext_iff scomp_def prod_case_unfold)
   77.41  
   77.42  lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = prod_case g (f x)"
   77.43    by (simp add: scomp_unfold prod_case_unfold)
   77.44  
   77.45  lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
   77.46 -  by (simp add: expand_fun_eq scomp_apply)
   77.47 +  by (simp add: ext_iff scomp_apply)
   77.48  
   77.49  lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
   77.50 -  by (simp add: expand_fun_eq scomp_apply)
   77.51 +  by (simp add: ext_iff scomp_apply)
   77.52  
   77.53  lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
   77.54 -  by (simp add: expand_fun_eq scomp_unfold)
   77.55 +  by (simp add: ext_iff scomp_unfold)
   77.56  
   77.57  lemma scomp_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
   77.58 -  by (simp add: expand_fun_eq scomp_unfold fcomp_def)
   77.59 +  by (simp add: ext_iff scomp_unfold fcomp_def)
   77.60  
   77.61  lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
   77.62 -  by (simp add: expand_fun_eq scomp_unfold fcomp_apply)
   77.63 +  by (simp add: ext_iff scomp_unfold fcomp_apply)
   77.64  
   77.65  code_const scomp
   77.66    (Eval infixl 3 "#->")
   77.67 @@ -919,11 +919,11 @@
   77.68  
   77.69  lemma apfst_id [simp] :
   77.70    "apfst id = id"
   77.71 -  by (simp add: expand_fun_eq)
   77.72 +  by (simp add: ext_iff)
   77.73  
   77.74  lemma apsnd_id [simp] :
   77.75    "apsnd id = id"
   77.76 -  by (simp add: expand_fun_eq)
   77.77 +  by (simp add: ext_iff)
   77.78  
   77.79  lemma apfst_eq_conv [simp]:
   77.80    "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)"
    78.1 --- a/src/HOL/Quotient.thy	Mon Sep 06 22:58:06 2010 +0200
    78.2 +++ b/src/HOL/Quotient.thy	Tue Sep 07 10:05:19 2010 +0200
    78.3 @@ -34,7 +34,7 @@
    78.4  
    78.5  lemma equivp_reflp_symp_transp:
    78.6    shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
    78.7 -  unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
    78.8 +  unfolding equivp_def reflp_def symp_def transp_def ext_iff
    78.9    by blast
   78.10  
   78.11  lemma equivp_reflp:
   78.12 @@ -97,7 +97,7 @@
   78.13  
   78.14  lemma eq_comp_r:
   78.15    shows "((op =) OOO R) = R"
   78.16 -  by (auto simp add: expand_fun_eq)
   78.17 +  by (auto simp add: ext_iff)
   78.18  
   78.19  subsection {* Respects predicate *}
   78.20  
   78.21 @@ -130,11 +130,11 @@
   78.22  
   78.23  lemma fun_map_id:
   78.24    shows "(id ---> id) = id"
   78.25 -  by (simp add: expand_fun_eq id_def)
   78.26 +  by (simp add: ext_iff id_def)
   78.27  
   78.28  lemma fun_rel_eq:
   78.29    shows "((op =) ===> (op =)) = (op =)"
   78.30 -  by (simp add: expand_fun_eq)
   78.31 +  by (simp add: ext_iff)
   78.32  
   78.33  
   78.34  subsection {* Quotient Predicate *}
   78.35 @@ -209,7 +209,7 @@
   78.36    have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
   78.37      using q1 q2
   78.38      unfolding Quotient_def
   78.39 -    unfolding expand_fun_eq
   78.40 +    unfolding ext_iff
   78.41      by simp
   78.42    moreover
   78.43    have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
   78.44 @@ -219,7 +219,7 @@
   78.45    moreover
   78.46    have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   78.47          (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
   78.48 -    unfolding expand_fun_eq
   78.49 +    unfolding ext_iff
   78.50      apply(auto)
   78.51      using q1 q2 unfolding Quotient_def
   78.52      apply(metis)
   78.53 @@ -238,7 +238,7 @@
   78.54  lemma abs_o_rep:
   78.55    assumes a: "Quotient R Abs Rep"
   78.56    shows "Abs o Rep = id"
   78.57 -  unfolding expand_fun_eq
   78.58 +  unfolding ext_iff
   78.59    by (simp add: Quotient_abs_rep[OF a])
   78.60  
   78.61  lemma equals_rsp:
   78.62 @@ -253,7 +253,7 @@
   78.63    assumes q1: "Quotient R1 Abs1 Rep1"
   78.64    and     q2: "Quotient R2 Abs2 Rep2"
   78.65    shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   78.66 -  unfolding expand_fun_eq
   78.67 +  unfolding ext_iff
   78.68    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   78.69    by simp
   78.70  
   78.71 @@ -261,7 +261,7 @@
   78.72    assumes q1: "Quotient R1 Abs1 Rep1"
   78.73    and     q2: "Quotient R2 Abs2 Rep2"
   78.74    shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   78.75 -  unfolding expand_fun_eq
   78.76 +  unfolding ext_iff
   78.77    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   78.78    by simp
   78.79  
   78.80 @@ -445,7 +445,7 @@
   78.81     is an equivalence this may be useful in regularising *)
   78.82  lemma babs_reg_eqv:
   78.83    shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
   78.84 -  by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
   78.85 +  by (simp add: ext_iff Babs_def in_respects equivp_reflp)
   78.86  
   78.87  
   78.88  (* 3 lemmas needed for proving repabs_inj *)
   78.89 @@ -617,12 +617,12 @@
   78.90    shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
   78.91    and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
   78.92    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
   78.93 -  unfolding o_def expand_fun_eq by simp_all
   78.94 +  unfolding o_def ext_iff by simp_all
   78.95  
   78.96  lemma o_rsp:
   78.97    "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
   78.98    "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
   78.99 -  unfolding fun_rel_def o_def expand_fun_eq by auto
  78.100 +  unfolding fun_rel_def o_def ext_iff by auto
  78.101  
  78.102  lemma cond_prs:
  78.103    assumes a: "Quotient R absf repf"
  78.104 @@ -633,7 +633,7 @@
  78.105    assumes q: "Quotient R Abs Rep"
  78.106    shows "(id ---> Rep ---> Rep ---> Abs) If = If"
  78.107    using Quotient_abs_rep[OF q]
  78.108 -  by (auto simp add: expand_fun_eq)
  78.109 +  by (auto simp add: ext_iff)
  78.110  
  78.111  lemma if_rsp:
  78.112    assumes q: "Quotient R Abs Rep"
  78.113 @@ -645,7 +645,7 @@
  78.114    and     q2: "Quotient R2 Abs2 Rep2"
  78.115    shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
  78.116    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
  78.117 -  by (auto simp add: expand_fun_eq)
  78.118 +  by (auto simp add: ext_iff)
  78.119  
  78.120  lemma let_rsp:
  78.121    shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
  78.122 @@ -659,7 +659,7 @@
  78.123    assumes a1: "Quotient R1 Abs1 Rep1"
  78.124    and     a2: "Quotient R2 Abs2 Rep2"
  78.125    shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
  78.126 -  by (simp add: expand_fun_eq mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
  78.127 +  by (simp add: ext_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
  78.128  
  78.129  locale quot_type =
  78.130    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    79.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Mon Sep 06 22:58:06 2010 +0200
    79.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Sep 07 10:05:19 2010 +0200
    79.3 @@ -563,12 +563,12 @@
    79.4  
    79.5  lemma [quot_preserve]:
    79.6    "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
    79.7 -  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
    79.8 +  by (simp add: ext_iff Quotient_abs_rep[OF Quotient_fset]
    79.9        abs_o_rep[OF Quotient_fset] map_id finsert_def)
   79.10  
   79.11  lemma [quot_preserve]:
   79.12    "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
   79.13 -  by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]
   79.14 +  by (simp add: ext_iff Quotient_abs_rep[OF Quotient_fset]
   79.15        abs_o_rep[OF Quotient_fset] map_id sup_fset_def)
   79.16  
   79.17  lemma list_all2_app_l:
   79.18 @@ -771,7 +771,7 @@
   79.19  
   79.20  lemma inj_map_eq_iff:
   79.21    "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
   79.22 -  by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
   79.23 +  by (simp add: set_ext_iff[symmetric] inj_image_eq_iff)
   79.24  
   79.25  text {* alternate formulation with a different decomposition principle
   79.26    and a proof of equivalence *}
    80.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Mon Sep 06 22:58:06 2010 +0200
    80.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Tue Sep 07 10:05:19 2010 +0200
    80.3 @@ -14,7 +14,7 @@
    80.4    "intrel (x, y) (u, v) = (x + v = u + y)"
    80.5  
    80.6  quotient_type int = "nat \<times> nat" / intrel
    80.7 -  by (auto simp add: equivp_def expand_fun_eq)
    80.8 +  by (auto simp add: equivp_def ext_iff)
    80.9  
   80.10  instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
   80.11  begin
    81.1 --- a/src/HOL/Random.thy	Mon Sep 06 22:58:06 2010 +0200
    81.2 +++ b/src/HOL/Random.thy	Tue Sep 07 10:05:19 2010 +0200
    81.3 @@ -85,7 +85,7 @@
    81.4  
    81.5  lemma pick_drop_zero:
    81.6    "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
    81.7 -  by (induct xs) (auto simp add: expand_fun_eq)
    81.8 +  by (induct xs) (auto simp add: ext_iff)
    81.9  
   81.10  lemma pick_same:
   81.11    "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l"
   81.12 @@ -132,7 +132,7 @@
   81.13      by (induct xs) simp_all
   81.14    ultimately show ?thesis
   81.15      by (auto simp add: select_weight_def select_def scomp_def split_def
   81.16 -      expand_fun_eq pick_same [symmetric])
   81.17 +      ext_iff pick_same [symmetric])
   81.18  qed
   81.19  
   81.20  
    82.1 --- a/src/HOL/Recdef.thy	Mon Sep 06 22:58:06 2010 +0200
    82.2 +++ b/src/HOL/Recdef.thy	Tue Sep 07 10:05:19 2010 +0200
    82.3 @@ -45,7 +45,7 @@
    82.4  text{*cut*}
    82.5  
    82.6  lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
    82.7 -by (simp add: expand_fun_eq cut_def)
    82.8 +by (simp add: ext_iff cut_def)
    82.9  
   82.10  lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
   82.11  by (simp add: cut_def)
    83.1 --- a/src/HOL/Set.thy	Mon Sep 06 22:58:06 2010 +0200
    83.2 +++ b/src/HOL/Set.thy	Tue Sep 07 10:05:19 2010 +0200
    83.3 @@ -495,7 +495,7 @@
    83.4    apply (rule Collect_mem_eq)
    83.5    done
    83.6  
    83.7 -lemma expand_set_eq [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
    83.8 +lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
    83.9  by(auto intro:set_ext)
   83.10  
   83.11  lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
    84.1 --- a/src/HOL/SetInterval.thy	Mon Sep 06 22:58:06 2010 +0200
    84.2 +++ b/src/HOL/SetInterval.thy	Tue Sep 07 10:05:19 2010 +0200
    84.3 @@ -241,7 +241,7 @@
    84.4  lemma atLeastatMost_psubset_iff:
    84.5    "{a..b} < {c..d} \<longleftrightarrow>
    84.6     ((~ a <= b) | c <= a & b <= d & (c < a | b < d))  &  c <= d"
    84.7 -by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans)
    84.8 +by(simp add: psubset_eq set_ext_iff less_le_not_le)(blast intro: order_trans)
    84.9  
   84.10  lemma atLeastAtMost_singleton_iff[simp]:
   84.11    "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
    85.1 --- a/src/HOL/String.thy	Mon Sep 06 22:58:06 2010 +0200
    85.2 +++ b/src/HOL/String.thy	Tue Sep 07 10:05:19 2010 +0200
    85.3 @@ -60,12 +60,12 @@
    85.4  
    85.5  lemma char_case_nibble_pair [code, code_unfold]:
    85.6    "char_case f = split f o nibble_pair_of_char"
    85.7 -  by (simp add: expand_fun_eq split: char.split)
    85.8 +  by (simp add: ext_iff split: char.split)
    85.9  
   85.10  lemma char_rec_nibble_pair [code, code_unfold]:
   85.11    "char_rec f = split f o nibble_pair_of_char"
   85.12    unfolding char_case_nibble_pair [symmetric]
   85.13 -  by (simp add: expand_fun_eq split: char.split)
   85.14 +  by (simp add: ext_iff split: char.split)
   85.15  
   85.16  syntax
   85.17    "_Char" :: "xstr => char"    ("CHR _")
    86.1 --- a/src/HOL/Sum_Type.thy	Mon Sep 06 22:58:06 2010 +0200
    86.2 +++ b/src/HOL/Sum_Type.thy	Tue Sep 07 10:05:19 2010 +0200
    86.3 @@ -32,17 +32,17 @@
    86.4  lemma Inl_Rep_inject: "inj_on Inl_Rep A"
    86.5  proof (rule inj_onI)
    86.6    show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c"
    86.7 -    by (auto simp add: Inl_Rep_def expand_fun_eq)
    86.8 +    by (auto simp add: Inl_Rep_def ext_iff)
    86.9  qed
   86.10  
   86.11  lemma Inr_Rep_inject: "inj_on Inr_Rep A"
   86.12  proof (rule inj_onI)
   86.13    show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d"
   86.14 -    by (auto simp add: Inr_Rep_def expand_fun_eq)
   86.15 +    by (auto simp add: Inr_Rep_def ext_iff)
   86.16  qed
   86.17  
   86.18  lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b"
   86.19 -  by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq)
   86.20 +  by (auto simp add: Inl_Rep_def Inr_Rep_def ext_iff)
   86.21  
   86.22  definition Inl :: "'a \<Rightarrow> 'a + 'b" where
   86.23    "Inl = Abs_sum \<circ> Inl_Rep"
    87.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 06 22:58:06 2010 +0200
    87.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Sep 07 10:05:19 2010 +0200
    87.3 @@ -483,7 +483,7 @@
    87.4             [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
    87.5              REPEAT (rtac TrueI 1),
    87.6              rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
    87.7 -              Thm.symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
    87.8 +              Thm.symmetric (mk_meta_eq @{thm ext_iff}) :: range_eqs),
    87.9              rewrite_goals_tac (map Thm.symmetric range_eqs),
   87.10              REPEAT (EVERY
   87.11                [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
    88.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Sep 06 22:58:06 2010 +0200
    88.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Sep 07 10:05:19 2010 +0200
    88.3 @@ -78,7 +78,7 @@
    88.4  
    88.5  (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    88.6  
    88.7 -val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
    88.8 +val fun_cong_all = @{thm ext_iff [THEN iffD1]}
    88.9  
   88.10  (* Removes the lambdas from an equation of the form "t = (%x. u)".
   88.11     (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
    89.1 --- a/src/HOL/Transitive_Closure.thy	Mon Sep 06 22:58:06 2010 +0200
    89.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Sep 07 10:05:19 2010 +0200
    89.3 @@ -82,7 +82,7 @@
    89.4  subsection {* Reflexive-transitive closure *}
    89.5  
    89.6  lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
    89.7 -  by (auto simp add: expand_fun_eq)
    89.8 +  by (auto simp add: ext_iff)
    89.9  
   89.10  lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
   89.11    -- {* @{text rtrancl} of @{text r} contains @{text r} *}
   89.12 @@ -487,7 +487,7 @@
   89.13  lemmas trancl_converseD = tranclp_converseD [to_set]
   89.14  
   89.15  lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1"
   89.16 -  by (fastsimp simp add: expand_fun_eq
   89.17 +  by (fastsimp simp add: ext_iff
   89.18      intro!: tranclp_converseI dest!: tranclp_converseD)
   89.19  
   89.20  lemmas trancl_converse = tranclp_converse [to_set]
    90.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Mon Sep 06 22:58:06 2010 +0200
    90.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Tue Sep 07 10:05:19 2010 +0200
    90.3 @@ -358,7 +358,7 @@
    90.4    done
    90.5  
    90.6  lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
    90.7 -  apply (simp add: surj_iff expand_fun_eq o_apply)
    90.8 +  apply (simp add: surj_iff ext_iff o_apply)
    90.9    apply record_auto
   90.10    done
   90.11  
   90.12 @@ -386,7 +386,7 @@
   90.13    done
   90.14  
   90.15  lemma surj_sysOfClient [iff]: "surj sysOfClient"
   90.16 -  apply (simp add: surj_iff expand_fun_eq o_apply)
   90.17 +  apply (simp add: surj_iff ext_iff o_apply)
   90.18    apply record_auto
   90.19    done
   90.20  
   90.21 @@ -410,7 +410,7 @@
   90.22    done
   90.23  
   90.24  lemma surj_client_map [iff]: "surj client_map"
   90.25 -  apply (simp add: surj_iff expand_fun_eq o_apply)
   90.26 +  apply (simp add: surj_iff ext_iff o_apply)
   90.27    apply record_auto
   90.28    done
   90.29  
    91.1 --- a/src/HOL/UNITY/Lift_prog.thy	Mon Sep 06 22:58:06 2010 +0200
    91.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Tue Sep 07 10:05:19 2010 +0200
    91.3 @@ -337,10 +337,10 @@
    91.4  
    91.5  (*Lets us prove one version of a theorem and store others*)
    91.6  lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
    91.7 -by (simp add: expand_fun_eq o_def)
    91.8 +by (simp add: ext_iff o_def)
    91.9  
   91.10  lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x"
   91.11 -by (simp add: expand_fun_eq o_def)
   91.12 +by (simp add: ext_iff o_def)
   91.13  
   91.14  lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
   91.15  apply (rule ext)
    92.1 --- a/src/HOL/Word/Word.thy	Mon Sep 06 22:58:06 2010 +0200
    92.2 +++ b/src/HOL/Word/Word.thy	Tue Sep 07 10:05:19 2010 +0200
    92.3 @@ -4695,7 +4695,7 @@
    92.4  apply simp
    92.5  apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
    92.6         in subst)
    92.7 - apply (clarsimp simp add: expand_fun_eq)
    92.8 + apply (clarsimp simp add: ext_iff)
    92.9   apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
   92.10    apply simp
   92.11   apply (rule refl)
    93.1 --- a/src/HOL/ZF/HOLZF.thy	Mon Sep 06 22:58:06 2010 +0200
    93.2 +++ b/src/HOL/ZF/HOLZF.thy	Tue Sep 07 10:05:19 2010 +0200
    93.3 @@ -155,7 +155,7 @@
    93.4    by (auto simp add: explode_def)
    93.5  
    93.6  lemma explode_CartProd_eq: "explode (CartProd a b) = (% (x,y). Opair x y) ` ((explode a) \<times> (explode b))"
    93.7 -  by (simp add: explode_def expand_set_eq CartProd image_def)
    93.8 +  by (simp add: explode_def set_ext_iff CartProd image_def)
    93.9  
   93.10  lemma explode_Repl_eq: "explode (Repl A f) = image f (explode A)"
   93.11    by (simp add: explode_def Repl image_def)
    94.1 --- a/src/HOL/ex/Execute_Choice.thy	Mon Sep 06 22:58:06 2010 +0200
    94.2 +++ b/src/HOL/ex/Execute_Choice.thy	Tue Sep 07 10:05:19 2010 +0200
    94.3 @@ -26,7 +26,7 @@
    94.4    case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def)
    94.5  next
    94.6    case False
    94.7 -  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def expand_fun_eq mem_def keys_def)
    94.8 +  then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def ext_iff mem_def keys_def)
    94.9    then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
   94.10       the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
   94.11         (\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
    95.1 --- a/src/HOL/ex/Landau.thy	Mon Sep 06 22:58:06 2010 +0200
    95.2 +++ b/src/HOL/ex/Landau.thy	Tue Sep 07 10:05:19 2010 +0200
    95.3 @@ -189,7 +189,7 @@
    95.4    qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans)
    95.5    show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms .
    95.6    show "preorder_equiv.equiv less_eq_fun = equiv_fun"
    95.7 -    by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun)
    95.8 +    by (simp add: ext_iff equiv_def equiv_fun_less_eq_fun)
    95.9  qed
   95.10  
   95.11  
    96.1 --- a/src/HOL/ex/Summation.thy	Mon Sep 06 22:58:06 2010 +0200
    96.2 +++ b/src/HOL/ex/Summation.thy	Tue Sep 07 10:05:19 2010 +0200
    96.3 @@ -24,7 +24,7 @@
    96.4  
    96.5  lemma \<Delta>_shift:
    96.6    "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
    96.7 -  by (simp add: \<Delta>_def expand_fun_eq)
    96.8 +  by (simp add: \<Delta>_def ext_iff)
    96.9  
   96.10  lemma \<Delta>_same_shift:
   96.11    assumes "\<Delta> f = \<Delta> g"
   96.12 @@ -100,7 +100,7 @@
   96.13  proof -
   96.14    from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
   96.15    then obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
   96.16 -  then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: expand_fun_eq)
   96.17 +  then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: ext_iff)
   96.18    then show ?thesis by simp
   96.19  qed
   96.20