# HG changeset patch # User nipkow # Date 1283846719 -7200 # Node ID f967a16dfcdda658afa03943d43bfd377f658012 # Parent 19efc2af3e6ca4ad797c26bcd3b733959790bc87 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Bali/Example.thy Tue Sep 07 10:05:19 2010 +0200 @@ -792,7 +792,7 @@ lemma Base_fields_accessible[simp]: "accfield tprg S Base = table_of((map (\((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))" -apply (auto simp add: accfield_def expand_fun_eq Let_def +apply (auto simp add: accfield_def ext_iff Let_def accessible_in_RefT_simp is_public_def BaseCl_def @@ -837,7 +837,7 @@ lemma Ext_fields_accessible[simp]: "accfield tprg S Ext = table_of((map (\((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))" -apply (auto simp add: accfield_def expand_fun_eq Let_def +apply (auto simp add: accfield_def ext_iff Let_def accessible_in_RefT_simp is_public_def BaseCl_def diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Bali/Table.thy --- a/src/HOL/Bali/Table.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Bali/Table.thy Tue Sep 07 10:05:19 2010 +0200 @@ -65,10 +65,10 @@ else Some old_val))))" lemma cond_override_empty1[simp]: "cond_override c empty t = t" -by (simp add: cond_override_def expand_fun_eq) +by (simp add: cond_override_def ext_iff) lemma cond_override_empty2[simp]: "cond_override c t empty = t" -by (simp add: cond_override_def expand_fun_eq) +by (simp add: cond_override_def ext_iff) lemma cond_override_None[simp]: "old k = None \ (cond_override c old new) k = new k" @@ -105,10 +105,10 @@ by (simp add: filter_tab_def empty_def) lemma filter_tab_True[simp]: "filter_tab (\x y. True) t = t" -by (simp add: expand_fun_eq filter_tab_def) +by (simp add: ext_iff filter_tab_def) lemma filter_tab_False[simp]: "filter_tab (\x y. False) t = empty" -by (simp add: expand_fun_eq filter_tab_def empty_def) +by (simp add: ext_iff filter_tab_def empty_def) lemma filter_tab_ran_subset: "ran (filter_tab c t) \ ran t" by (auto simp add: filter_tab_def ran_def) @@ -134,26 +134,26 @@ lemma filter_tab_all_True: "\ k y. t k = Some y \ p k y \filter_tab p t = t" -apply (auto simp add: filter_tab_def expand_fun_eq) +apply (auto simp add: filter_tab_def ext_iff) done lemma filter_tab_all_True_Some: "\\ k y. t k = Some y \ p k y; t k = Some v\ \ filter_tab p t k = Some v" -by (auto simp add: filter_tab_def expand_fun_eq) +by (auto simp add: filter_tab_def ext_iff) lemma filter_tab_all_False: "\ k y. t k = Some y \ \ p k y \filter_tab p t = empty" -by (auto simp add: filter_tab_def expand_fun_eq) +by (auto simp add: filter_tab_def ext_iff) lemma filter_tab_None: "t k = None \ filter_tab p t k = None" -apply (simp add: filter_tab_def expand_fun_eq) +apply (simp add: filter_tab_def ext_iff) done lemma filter_tab_dom_subset: "dom (filter_tab C t) \ dom t" by (auto simp add: filter_tab_def dom_def) lemma filter_tab_eq: "\a=b\ \ filter_tab C a = filter_tab C b" -by (auto simp add: expand_fun_eq filter_tab_def) +by (auto simp add: ext_iff filter_tab_def) lemma finite_dom_filter_tab: "finite (dom t) \ finite (dom (filter_tab C t))" @@ -175,7 +175,7 @@ \ \ cond_override overC (filter_tab filterC t) (filter_tab filterC s) = filter_tab filterC (cond_override overC t s)" -by (auto simp add: expand_fun_eq cond_override_def filter_tab_def ) +by (auto simp add: ext_iff cond_override_def filter_tab_def ) section {* Misc. *} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Big_Operators.thy Tue Sep 07 10:05:19 2010 +0200 @@ -1504,11 +1504,11 @@ lemma dual_max: "ord.max (op \) = min" - by (auto simp add: ord.max_def_raw min_def expand_fun_eq) + by (auto simp add: ord.max_def_raw min_def ext_iff) lemma dual_min: "ord.min (op \) = max" - by (auto simp add: ord.min_def_raw max_def expand_fun_eq) + by (auto simp add: ord.min_def_raw max_def ext_iff) lemma strict_below_fold1_iff: assumes "finite A" and "A \ {}" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Datatype.thy Tue Sep 07 10:05:19 2010 +0200 @@ -109,12 +109,12 @@ (** Push -- an injection, analogous to Cons on lists **) lemma Push_inject1: "Push i f = Push j g ==> i=j" -apply (simp add: Push_def expand_fun_eq) +apply (simp add: Push_def ext_iff) apply (drule_tac x=0 in spec, simp) done lemma Push_inject2: "Push i f = Push j g ==> f=g" -apply (auto simp add: Push_def expand_fun_eq) +apply (auto simp add: Push_def ext_iff) apply (drule_tac x="Suc x" in spec, simp) done @@ -123,7 +123,7 @@ by (blast dest: Push_inject1 Push_inject2) lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P" -by (auto simp add: Push_def expand_fun_eq split: nat.split_asm) +by (auto simp add: Push_def ext_iff split: nat.split_asm) lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard] @@ -399,7 +399,7 @@ lemma ntrunc_o_equality: "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2" apply (rule ntrunc_equality [THEN ext]) -apply (simp add: expand_fun_eq) +apply (simp add: ext_iff) done diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Decision_Procs/Polynomial_List.thy --- a/src/HOL/Decision_Procs/Polynomial_List.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy Tue Sep 07 10:05:19 2010 +0200 @@ -342,7 +342,7 @@ lemma UNIV_nat_infinite: "\ finite (UNIV :: nat set)" unfolding finite_conv_nat_seg_image -proof(auto simp add: expand_set_eq image_iff) +proof(auto simp add: set_ext_iff image_iff) fix n::nat and f:: "nat \ nat" let ?N = "{i. i < n}" let ?fN = "f ` ?N" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Finite_Set.thy Tue Sep 07 10:05:19 2010 +0200 @@ -541,7 +541,7 @@ qed (simp add: UNIV_option_conv) lemma inj_graph: "inj (%f. {(x, y). y = f x})" - by (rule inj_onI, auto simp add: expand_set_eq expand_fun_eq) + by (rule inj_onI, auto simp add: set_ext_iff ext_iff) instance "fun" :: (finite, finite) finite proof @@ -576,7 +576,7 @@ text{* On a functional level it looks much nicer: *} lemma fun_comp_comm: "f x \ f y = f y \ f x" -by (simp add: fun_left_comm expand_fun_eq) +by (simp add: fun_left_comm ext_iff) end @@ -720,7 +720,7 @@ text{* The nice version: *} lemma fun_comp_idem : "f x o f x = f x" -by (simp add: fun_left_idem expand_fun_eq) +by (simp add: fun_left_idem ext_iff) lemma fold_insert_idem: assumes fin: "finite A" @@ -1363,17 +1363,17 @@ lemma empty [simp]: "F {} = id" - by (simp add: eq_fold expand_fun_eq) + by (simp add: eq_fold ext_iff) lemma insert [simp]: assumes "finite A" and "x \ A" shows "F (insert x A) = F A \ f x" proof - interpret fun_left_comm f proof - qed (insert commute_comp, simp add: expand_fun_eq) + qed (insert commute_comp, simp add: ext_iff) from fold_insert2 assms have "\s. fold f s (insert x A) = fold f (f x s) A" . - with `finite A` show ?thesis by (simp add: eq_fold expand_fun_eq) + with `finite A` show ?thesis by (simp add: eq_fold ext_iff) qed lemma remove: @@ -1736,14 +1736,14 @@ then obtain B where *: "A = insert b B" "b \ B" by (blast dest: mk_disjoint_insert) with `finite A` have "finite B" by simp interpret fold: folding "op *" "\a b. fold (op *) b a" proof - qed (simp_all add: expand_fun_eq ac_simps) - thm fold.commute_comp' [of B b, simplified expand_fun_eq, simplified] + qed (simp_all add: ext_iff ac_simps) + thm fold.commute_comp' [of B b, simplified ext_iff, simplified] from `finite B` fold.commute_comp' [of B x] have "op * x \ (\b. fold op * b B) = (\b. fold op * b B) \ op * x" by simp - then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: expand_fun_eq commute) + then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: ext_iff commute) from `finite B` * fold.insert [of B b] have "(\x. fold op * x (insert b B)) = (\x. fold op * x B) \ op * b" by simp - then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: expand_fun_eq) + then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: ext_iff) from A B assms * show ?thesis by (simp add: eq_fold' del: fold.insert) qed diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Fun.thy --- a/src/HOL/Fun.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Fun.thy Tue Sep 07 10:05:19 2010 +0200 @@ -11,7 +11,7 @@ text{*As a simplification rule, it replaces all function equalities by first-order equalities.*} -lemma expand_fun_eq: "f = g \ (\x. f x = g x)" +lemma ext_iff: "f = g \ (\x. f x = g x)" apply (rule iffI) apply (simp (no_asm_simp)) apply (rule ext) @@ -163,7 +163,7 @@ by (simp add: inj_on_def) lemma inj_fun: "inj f \ inj (\x y. f x)" - by (simp add: inj_on_def expand_fun_eq) + by (simp add: inj_on_def ext_iff) lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)" by (simp add: inj_on_eq_iff) @@ -463,7 +463,7 @@ by simp lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)" -by (simp add: expand_fun_eq) +by (simp add: ext_iff) lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)" by (rule ext, auto) @@ -515,7 +515,7 @@ lemma swap_triple: assumes "a \ c" and "b \ c" shows "swap a b (swap b c (swap a b f)) = swap a c f" - using assms by (simp add: expand_fun_eq swap_def) + using assms by (simp add: ext_iff swap_def) lemma comp_swap: "f \ swap a b g = swap a b (f \ g)" by (rule ext, simp add: fun_upd_def swap_def) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Hilbert_Choice.thy Tue Sep 07 10:05:19 2010 +0200 @@ -138,7 +138,7 @@ qed lemma inj_iff: "(inj f) = (inv f o f = id)" -apply (simp add: o_def expand_fun_eq) +apply (simp add: o_def ext_iff) apply (blast intro: inj_on_inverseI inv_into_f_f) done @@ -178,7 +178,7 @@ by (simp add: inj_on_inv_into surj_range) lemma surj_iff: "(surj f) = (f o inv f = id)" -apply (simp add: o_def expand_fun_eq) +apply (simp add: o_def ext_iff) apply (blast intro: surjI surj_f_inv_f) done diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Hoare/SchorrWaite.thy --- a/src/HOL/Hoare/SchorrWaite.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Hoare/SchorrWaite.thy Tue Sep 07 10:05:19 2010 +0200 @@ -239,7 +239,7 @@ from inv have i1: "?I1" and i4: "?I4" and i5: "?I5" and i6: "?I6" by simp+ from pNull i1 have stackEmpty: "stack = []" by simp from tDisj i4 have RisMarked[rule_format]: "\x. x \ R \ m x" by(auto simp: reachable_def addrs_def stackEmpty) - from i5 i6 show "(\x.(x \ R) = m x) \ r = iR \ l = iL" by(auto simp: stackEmpty expand_fun_eq intro:RisMarked) + from i5 i6 show "(\x.(x \ R) = m x) \ r = iR \ l = iL" by(auto simp: stackEmpty ext_iff intro:RisMarked) next fix c m l r t p q root diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/IMP/Live.thy --- a/src/HOL/IMP/Live.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/IMP/Live.thy Tue Sep 07 10:05:19 2010 +0200 @@ -8,7 +8,7 @@ consts Dep :: "((loc \ 'a) \ 'b) \ loc set" specification (Dep) dep_on: "(\x\Dep e. s x = t x) \ e s = e t" -by(rule_tac x="%x. UNIV" in exI)(simp add: expand_fun_eq[symmetric]) +by(rule_tac x="%x. UNIV" in exI)(simp add: ext_iff[symmetric]) text{* The following definition of @{const Dep} looks very tempting @{prop"Dep e = {a. EX s t. (ALL x. x\a \ s x = t x) \ e s \ e t}"} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Imperative_HOL/Array.thy Tue Sep 07 10:05:19 2010 +0200 @@ -99,7 +99,7 @@ lemma set_set_swap: "r =!!= r' \ set r x (set r' x' h) = set r' x' (set r x h)" - by (simp add: Let_def expand_fun_eq noteq_def set_def) + by (simp add: Let_def ext_iff noteq_def set_def) lemma get_update_eq [simp]: "get (update a i v h) a = (get h a) [i := v]" @@ -115,7 +115,7 @@ lemma length_update [simp]: "length (update b i v h) = length h" - by (simp add: update_def length_def set_def get_def expand_fun_eq) + by (simp add: update_def length_def set_def get_def ext_iff) lemma update_swap_neq: "a =!!= a' \ @@ -145,7 +145,7 @@ lemma present_update [simp]: "present (update b i v h) = present h" - by (simp add: update_def present_def set_def get_def expand_fun_eq) + by (simp add: update_def present_def set_def get_def ext_iff) lemma present_alloc [simp]: "present (snd (alloc xs h)) (fst (alloc xs h))" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Sep 07 10:05:19 2010 +0200 @@ -31,7 +31,7 @@ lemma Heap_eqI: "(\h. execute f h = execute g h) \ f = g" - by (cases f, cases g) (auto simp: expand_fun_eq) + by (cases f, cases g) (auto simp: ext_iff) ML {* structure Execute_Simps = Named_Thms( val name = "execute_simps" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Imperative_HOL/Ref.thy --- a/src/HOL/Imperative_HOL/Ref.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Imperative_HOL/Ref.thy Tue Sep 07 10:05:19 2010 +0200 @@ -98,7 +98,7 @@ lemma set_set_swap: "r =!= r' \ set r x (set r' x' h) = set r' x' (set r x h)" - by (simp add: noteq_def set_def expand_fun_eq) + by (simp add: noteq_def set_def ext_iff) lemma alloc_set: "fst (alloc x (set r x' h)) = fst (alloc x h)" @@ -126,7 +126,7 @@ lemma present_set [simp]: "present (set r v h) = present h" - by (simp add: present_def expand_fun_eq) + by (simp add: present_def ext_iff) lemma noteq_I: "present h r \ \ present h r' \ r =!= r'" @@ -220,7 +220,7 @@ lemma array_get_set [simp]: "Array.get (set r v h) = Array.get h" - by (simp add: Array.get_def set_def expand_fun_eq) + by (simp add: Array.get_def set_def ext_iff) lemma get_update [simp]: "get (Array.update a i v h) r = get h r" @@ -240,15 +240,15 @@ lemma array_get_alloc [simp]: "Array.get (snd (alloc v h)) = Array.get h" - by (simp add: Array.get_def alloc_def set_def Let_def expand_fun_eq) + by (simp add: Array.get_def alloc_def set_def Let_def ext_iff) lemma present_update [simp]: "present (Array.update a i v h) = present h" - by (simp add: Array.update_def Array.set_def expand_fun_eq present_def) + by (simp add: Array.update_def Array.set_def ext_iff present_def) lemma array_present_set [simp]: "Array.present (set r v h) = Array.present h" - by (simp add: Array.present_def set_def expand_fun_eq) + by (simp add: Array.present_def set_def ext_iff) lemma array_present_alloc [simp]: "Array.present h a \ Array.present (snd (alloc v h)) a" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Tue Sep 07 10:05:19 2010 +0200 @@ -550,7 +550,7 @@ }" unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric] thm arg_cong2 - by (auto simp add: expand_fun_eq intro: arg_cong2[where f = bind] split: node.split) + by (auto simp add: ext_iff intro: arg_cong2[where f = bind] split: node.split) primrec rev :: "('a:: heap) node \ 'a node Heap" where diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Import/HOL/bool.imp --- a/src/HOL/Import/HOL/bool.imp Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Import/HOL/bool.imp Tue Sep 07 10:05:19 2010 +0200 @@ -124,7 +124,7 @@ "IMP_ANTISYM_AX" > "HOL4Setup.light_imp_as" "F_IMP" > "HOL4Base.bool.F_IMP" "F_DEF" > "HOL.False_def" - "FUN_EQ_THM" > "Fun.expand_fun_eq" + "FUN_EQ_THM" > "Fun.ext_iff" "FORALL_THM" > "HOL4Base.bool.FORALL_THM" "FORALL_SIMP" > "HOL.simp_thms_35" "FORALL_DEF" > "HOL.All_def" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Import/HOL/prob_extra.imp --- a/src/HOL/Import/HOL/prob_extra.imp Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Import/HOL/prob_extra.imp Tue Sep 07 10:05:19 2010 +0200 @@ -73,7 +73,7 @@ "EVEN_ODD_EXISTS_EQ" > "HOL4Prob.prob_extra.EVEN_ODD_EXISTS_EQ" "EVEN_ODD_BASIC" > "HOL4Prob.prob_extra.EVEN_ODD_BASIC" "EVEN_EXP_TWO" > "HOL4Prob.prob_extra.EVEN_EXP_TWO" - "EQ_EXT_EQ" > "Fun.expand_fun_eq" + "EQ_EXT_EQ" > "Fun.ext_iff" "DIV_TWO_UNIQUE" > "HOL4Prob.prob_extra.DIV_TWO_UNIQUE" "DIV_TWO_MONO_EVEN" > "HOL4Prob.prob_extra.DIV_TWO_MONO_EVEN" "DIV_TWO_MONO" > "HOL4Prob.prob_extra.DIV_TWO_MONO" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Import/HOLLight/hollight.imp --- a/src/HOL/Import/HOLLight/hollight.imp Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Import/HOLLight/hollight.imp Tue Sep 07 10:05:19 2010 +0200 @@ -1394,7 +1394,7 @@ "GSPEC_def" > "HOLLight.hollight.GSPEC_def" "GEQ_def" > "HOLLight.hollight.GEQ_def" "GABS_def" > "HOLLight.hollight.GABS_def" - "FUN_EQ_THM" > "Fun.expand_fun_eq" + "FUN_EQ_THM" > "Fun.ext_iff" "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT" "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT" "FSTCART_PASTECART" > "HOLLight.hollight.FSTCART_PASTECART" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/AssocList.thy --- a/src/HOL/Library/AssocList.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/AssocList.thy Tue Sep 07 10:05:19 2010 +0200 @@ -22,7 +22,7 @@ | "update k v (p#ps) = (if fst p = k then (k, v) # ps else p # update k v ps)" lemma update_conv': "map_of (update k v al) = (map_of al)(k\v)" - by (induct al) (auto simp add: expand_fun_eq) + by (induct al) (auto simp add: ext_iff) corollary update_conv: "map_of (update k v al) k' = ((map_of al)(k\v)) k'" by (simp add: update_conv') @@ -67,7 +67,7 @@ @{term "update k' v' (update k v []) = [(k, v), (k', v')]"}.*} lemma update_swap: "k\k' \ map_of (update k v (update k' v' al)) = map_of (update k' v' (update k v al))" - by (simp add: update_conv' expand_fun_eq) + by (simp add: update_conv' ext_iff) lemma update_Some_unfold: "map_of (update k v al) x = Some y \ @@ -96,8 +96,8 @@ proof - have "map_of \ More_List.fold (prod_case update) (zip ks vs) = More_List.fold (\(k, v) f. f(k \ v)) (zip ks vs) \ map_of" - by (rule fold_apply) (auto simp add: expand_fun_eq update_conv') - then show ?thesis by (auto simp add: updates_def expand_fun_eq map_upds_fold_map_upd foldl_fold split_def) + by (rule fold_apply) (auto simp add: ext_iff update_conv') + then show ?thesis by (auto simp add: updates_def ext_iff map_upds_fold_map_upd foldl_fold split_def) qed lemma updates_conv: "map_of (updates ks vs al) k = ((map_of al)(ks[\]vs)) k" @@ -114,7 +114,7 @@ moreover have "map fst \ More_List.fold (prod_case update) (zip ks vs) = More_List.fold (\(k, v) al. if k \ set al then al else al @ [k]) (zip ks vs) \ map fst" by (rule fold_apply) (simp add: update_keys split_def prod_case_beta comp_def) - ultimately show ?thesis by (simp add: updates_def expand_fun_eq) + ultimately show ?thesis by (simp add: updates_def ext_iff) qed lemma updates_append1[simp]: "size ks < size vs \ @@ -161,7 +161,7 @@ by (auto simp add: delete_eq) lemma delete_conv': "map_of (delete k al) = (map_of al)(k := None)" - by (induct al) (auto simp add: expand_fun_eq) + by (induct al) (auto simp add: ext_iff) corollary delete_conv: "map_of (delete k al) k' = ((map_of al)(k := None)) k'" by (simp add: delete_conv') @@ -301,7 +301,7 @@ lemma map_of_clearjunk: "map_of (clearjunk al) = map_of al" by (induct al rule: clearjunk.induct) - (simp_all add: expand_fun_eq) + (simp_all add: ext_iff) lemma clearjunk_keys_set: "set (map fst (clearjunk al)) = set (map fst al)" @@ -342,7 +342,7 @@ have "clearjunk \ More_List.fold (prod_case update) (zip ks vs) = More_List.fold (prod_case update) (zip ks vs) \ clearjunk" by (rule fold_apply) (simp add: clearjunk_update prod_case_beta o_def) - then show ?thesis by (simp add: updates_def expand_fun_eq) + then show ?thesis by (simp add: updates_def ext_iff) qed lemma clearjunk_delete: @@ -446,9 +446,9 @@ proof - have "map_of \ More_List.fold (prod_case update) (rev ys) = More_List.fold (\(k, v) m. m(k \ v)) (rev ys) \ map_of" - by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq) + by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def ext_iff) then show ?thesis - by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq) + by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev ext_iff) qed corollary merge_conv: @@ -699,7 +699,7 @@ lemma bulkload_Mapping [code]: "Mapping.bulkload vs = Mapping (map (\n. (n, vs ! n)) [0..n\{1\nat..n}. a + of_nat n) = (\n\{0\nat..n - 1}. a + 1 + of_nat n)" apply (rule setprod_reindex_cong [where f = Suc]) - using n0 by (auto simp add: expand_fun_eq field_simps) + using n0 by (auto simp add: ext_iff field_simps) have ?thesis apply (simp add: pochhammer_def) unfolding setprod_insert[OF th0, unfolded eq] using th1 by (simp add: field_simps)} @@ -248,7 +248,7 @@ apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod) apply (rule setprod_reindex_cong[where f=Suc]) - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) lemma pochhammer_of_nat_eq_0_lemma: assumes kn: "k > n" shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0" @@ -315,7 +315,7 @@ apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"]) apply (auto simp add: inj_on_def image_def h ) apply (rule_tac x="h - x" in bexI) - by (auto simp add: expand_fun_eq h of_nat_diff)} + by (auto simp add: ext_iff h of_nat_diff)} ultimately show ?thesis by (cases k, auto) qed @@ -410,11 +410,11 @@ have eq': "(\i\{0..h}. of_nat n + - (of_nat i :: 'a)) = (\i\{n - h..n}. of_nat i)" apply (rule strong_setprod_reindex_cong[where f="op - n"]) using h kn - apply (simp_all add: inj_on_def image_iff Bex_def expand_set_eq) + apply (simp_all add: inj_on_def image_iff Bex_def set_ext_iff) apply clarsimp apply (presburger) apply presburger - by (simp add: expand_fun_eq field_simps of_nat_add[symmetric] del: of_nat_add) + by (simp add: ext_iff field_simps of_nat_add[symmetric] del: of_nat_add) have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" "{1..n - Suc h} \ {n - h .. n} = {}" and eq3: "{1..n - Suc h} \ {n - h .. n} = {1..n}" using h kn by auto from eq[symmetric] diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Code_Char_chr.thy --- a/src/HOL/Library/Code_Char_chr.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Code_Char_chr.thy Tue Sep 07 10:05:19 2010 +0200 @@ -13,14 +13,14 @@ lemma [code]: "nat_of_char = nat o int_of_char" - unfolding int_of_char_def by (simp add: expand_fun_eq) + unfolding int_of_char_def by (simp add: ext_iff) definition "char_of_int = char_of_nat o nat" lemma [code]: "char_of_nat = char_of_int o int" - unfolding char_of_int_def by (simp add: expand_fun_eq) + unfolding char_of_int_def by (simp add: ext_iff) code_const int_of_char and char_of_int (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Countable.thy Tue Sep 07 10:05:19 2010 +0200 @@ -139,7 +139,7 @@ show "\to_nat::('a \ 'b) \ nat. inj to_nat" proof show "inj (\f. to_nat (map f xs))" - by (rule injI, simp add: xs expand_fun_eq) + by (rule injI, simp add: xs ext_iff) qed qed diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Tue Sep 07 10:05:19 2010 +0200 @@ -79,7 +79,7 @@ lemma [code, code_unfold]: "nat_case = (\f g n. if n = 0 then f else g (n - 1))" - by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc) + by (auto simp add: ext_iff dest!: gr0_implies_Suc) subsection {* Preprocessors *} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Enum.thy Tue Sep 07 10:05:19 2010 +0200 @@ -42,7 +42,7 @@ "HOL.equal f g \ (\x \ set enum. f x = g x)" instance proof -qed (simp_all add: equal_fun_def enum_all expand_fun_eq) +qed (simp_all add: equal_fun_def enum_all ext_iff) end @@ -54,7 +54,7 @@ fixes f g :: "'a\enum \ 'b\order" shows "f \ g \ list_all (\x. f x \ g x) enum" and "f < g \ f \ g \ list_ex (\x. f x \ g x) enum" - by (simp_all add: list_all_iff list_ex_iff enum_all expand_fun_eq le_fun_def order_less_le) + by (simp_all add: list_all_iff list_ex_iff enum_all ext_iff le_fun_def order_less_le) subsection {* Quantifiers *} @@ -160,7 +160,7 @@ proof (rule UNIV_eq_I) fix f :: "'a \ 'b" have "f = the \ map_of (zip (enum \ 'a\enum list) (map f enum))" - by (auto simp add: map_of_zip_map expand_fun_eq) + by (auto simp add: map_of_zip_map ext_iff) then show "f \ set enum" by (auto simp add: enum_fun_def set_n_lists) qed diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Tue Sep 07 10:05:19 2010 +0200 @@ -18,7 +18,7 @@ notation fps_nth (infixl "$" 75) lemma expand_fps_eq: "p = q \ (\n. p $ n = q $ n)" - by (simp add: fps_nth_inject [symmetric] expand_fun_eq) + by (simp add: fps_nth_inject [symmetric] ext_iff) lemma fps_ext: "(\n. p $ n = q $ n) \ p = q" by (simp add: expand_fps_eq) @@ -1244,7 +1244,7 @@ {assume n0: "n \ 0" then have u: "{0} \ ({1} \ {2..n}) = {0..n}" "{1}\{2..n} = {1..n}" "{0..n - 1}\{n} = {0..n}" - by (auto simp: expand_set_eq) + by (auto simp: set_ext_iff) have d: "{0} \ ({1} \ {2..n}) = {}" "{1} \ {2..n} = {}" "{0..n - 1}\{n} ={}" using n0 by simp_all have f: "finite {0}" "finite {1}" "finite {2 .. n}" @@ -1455,7 +1455,7 @@ moreover {fix k assume k: "m = Suc k" have km: "k < m" using k by arith - have u0: "{0 .. k} \ {m} = {0..m}" using k apply (simp add: expand_set_eq) by presburger + have u0: "{0 .. k} \ {m} = {0..m}" using k apply (simp add: set_ext_iff) by presburger have f0: "finite {0 .. k}" "finite {m}" by auto have d0: "{0 .. k} \ {m} = {}" using k by auto have "(setprod a {0 .. m}) $ n = (setprod a {0 .. k} * a m) $ n" @@ -1472,7 +1472,7 @@ apply clarsimp apply (rule finite_imageI) apply (rule natpermute_finite) - apply (clarsimp simp add: expand_set_eq) + apply (clarsimp simp add: set_ext_iff) apply auto apply (rule setsum_cong2) unfolding setsum_left_distrib @@ -2153,7 +2153,7 @@ qed lemma fps_inv_ginv: "fps_inv = fps_ginv X" - apply (auto simp add: expand_fun_eq fps_eq_iff fps_inv_def fps_ginv_def) + apply (auto simp add: ext_iff fps_eq_iff fps_inv_def fps_ginv_def) apply (induct_tac n rule: nat_less_induct, auto) apply (case_tac na) apply simp @@ -2192,7 +2192,7 @@ "setsum (%i. a (i :: nat) * b (n - i)) {0 .. n} = setsum (%(i,j). a i * b j) {(i,j). i <= n \ j \ n \ i + j = n}" apply (rule setsum_reindex_cong[where f=fst]) apply (clarsimp simp add: inj_on_def) - apply (auto simp add: expand_set_eq image_iff) + apply (auto simp add: set_ext_iff image_iff) apply (rule_tac x= "x" in exI) apply clarsimp apply (rule_tac x="n - x" in exI) @@ -2264,7 +2264,7 @@ let ?KM= "{(k,m). k + m \ n}" let ?f = "%s. UNION {(0::nat)..s} (%i. {(i,s - i)})" have th0: "?KM = UNION {0..n} ?f" - apply (simp add: expand_set_eq) + apply (simp add: set_ext_iff) apply arith (* FIXME: VERY slow! *) done show "?l = ?r " @@ -3312,10 +3312,10 @@ lemma XDp_commute: shows "XDp b o XDp (c::'a::comm_ring_1) = XDp c o XDp b" - by (auto simp add: XDp_def expand_fun_eq fps_eq_iff algebra_simps) + by (auto simp add: XDp_def ext_iff fps_eq_iff algebra_simps) lemma XDp0[simp]: "XDp 0 = XD" - by (simp add: expand_fun_eq fps_eq_iff) + by (simp add: ext_iff fps_eq_iff) lemma XDp_fps_integral[simp]:"XDp 0 (fps_integral a c) = X * a" by (simp add: fps_eq_iff fps_integral_def) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/FrechetDeriv.thy --- a/src/HOL/Library/FrechetDeriv.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/FrechetDeriv.thy Tue Sep 07 10:05:19 2010 +0200 @@ -177,7 +177,7 @@ hence "(\h. F h - F' h) = (\h. 0)" by (rule FDERIV_zero_unique) thus "F = F'" - unfolding expand_fun_eq right_minus_eq . + unfolding ext_iff right_minus_eq . qed subsection {* Continuity *} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Fset.thy Tue Sep 07 10:05:19 2010 +0200 @@ -51,7 +51,7 @@ lemma member_code [code]: "member (Set xs) = List.member xs" "member (Coset xs) = Not \ List.member xs" - by (simp_all add: expand_fun_eq member_def fun_Compl_def bool_Compl_def) + by (simp_all add: ext_iff member_def fun_Compl_def bool_Compl_def) lemma member_image_UNIV [simp]: "member ` UNIV = UNIV" @@ -252,13 +252,13 @@ show "inf A (Set xs) = Set (List.filter (member A) xs)" by (simp add: inter project_def Set_def) have *: "\x::'a. remove = (\x. Fset \ More_Set.remove x \ member)" - by (simp add: expand_fun_eq) + by (simp add: ext_iff) have "member \ fold (\x. Fset \ More_Set.remove x \ member) xs = fold More_Set.remove xs \ member" - by (rule fold_apply) (simp add: expand_fun_eq) + by (rule fold_apply) (simp add: ext_iff) then have "fold More_Set.remove xs (member A) = member (fold (\x. Fset \ More_Set.remove x \ member) xs A)" - by (simp add: expand_fun_eq) + by (simp add: ext_iff) then have "inf A (Coset xs) = fold remove xs A" by (simp add: Diff_eq [symmetric] minus_set *) moreover have "\x y :: 'a. Fset.remove y \ Fset.remove x = Fset.remove x \ Fset.remove y" @@ -277,13 +277,13 @@ "sup (Coset xs) A = Coset (List.filter (Not \ member A) xs)" proof - have *: "\x::'a. insert = (\x. Fset \ Set.insert x \ member)" - by (simp add: expand_fun_eq) + by (simp add: ext_iff) have "member \ fold (\x. Fset \ Set.insert x \ member) xs = fold Set.insert xs \ member" - by (rule fold_apply) (simp add: expand_fun_eq) + by (rule fold_apply) (simp add: ext_iff) then have "fold Set.insert xs (member A) = member (fold (\x. Fset \ Set.insert x \ member) xs A)" - by (simp add: expand_fun_eq) + by (simp add: ext_iff) then have "sup (Set xs) A = fold insert xs A" by (simp add: union_set *) moreover have "\x y :: 'a. Fset.insert y \ Fset.insert x = Fset.insert x \ Fset.insert y" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/FuncSet.thy Tue Sep 07 10:05:19 2010 +0200 @@ -128,7 +128,7 @@ lemma compose_assoc: "[| f \ A -> B; g \ B -> C; h \ C -> D |] ==> compose A h (compose A g f) = compose A (compose B h g) f" -by (simp add: expand_fun_eq Pi_def compose_def restrict_def) +by (simp add: ext_iff Pi_def compose_def restrict_def) lemma compose_eq: "x \ A ==> compose A g f x = g(f(x))" by (simp add: compose_def restrict_def) @@ -151,18 +151,18 @@ lemma restrict_ext: "(!!x. x \ A ==> f x = g x) ==> (\x\A. f x) = (\x\A. g x)" - by (simp add: expand_fun_eq Pi_def restrict_def) + by (simp add: ext_iff Pi_def restrict_def) lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A" by (simp add: inj_on_def restrict_def) lemma Id_compose: "[|f \ A -> B; f \ extensional A|] ==> compose A (\y\B. y) f = f" - by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) + by (auto simp add: ext_iff compose_def extensional_def Pi_def) lemma compose_Id: "[|g \ A -> B; g \ extensional A|] ==> compose A g (\x\A. x) = g" - by (auto simp add: expand_fun_eq compose_def extensional_def Pi_def) + by (auto simp add: ext_iff compose_def extensional_def Pi_def) lemma image_restrict_eq [simp]: "(restrict f A) ` A = f ` A" by (auto simp add: restrict_def) @@ -205,7 +205,7 @@ lemma extensionalityI: "[| f \ extensional A; g \ extensional A; !!x. x\A ==> f x = g x |] ==> f = g" -by (force simp add: expand_fun_eq extensional_def) +by (force simp add: ext_iff extensional_def) lemma inv_into_funcset: "f ` A = B ==> (\x\B. inv_into A f x) : B -> A" by (unfold inv_into_def) (fast intro: someI2) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Function_Algebras.thy --- a/src/HOL/Library/Function_Algebras.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Function_Algebras.thy Tue Sep 07 10:05:19 2010 +0200 @@ -57,7 +57,7 @@ qed (simp add: plus_fun_def add.assoc) instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof -qed (simp_all add: plus_fun_def expand_fun_eq) +qed (simp_all add: plus_fun_def ext_iff) instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof qed (simp add: plus_fun_def add.commute) @@ -106,7 +106,7 @@ qed (simp_all add: zero_fun_def times_fun_def) instance "fun" :: (type, zero_neq_one) zero_neq_one proof -qed (simp add: zero_fun_def one_fun_def expand_fun_eq) +qed (simp add: zero_fun_def one_fun_def ext_iff) text {* Ring structures *} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Inner_Product.thy --- a/src/HOL/Library/Inner_Product.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Inner_Product.thy Tue Sep 07 10:05:19 2010 +0200 @@ -307,7 +307,7 @@ have 1: "FDERIV (\x. inner x x) x :> (\h. inner x h + inner h x)" by (intro inner.FDERIV FDERIV_ident) have 2: "(\h. inner x h + inner h x) = (\h. inner h (scaleR 2 x))" - by (simp add: expand_fun_eq inner_commute) + by (simp add: ext_iff inner_commute) have "0 < inner x x" using `x \ 0` by simp then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)" by (rule DERIV_real_sqrt) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Mapping.thy Tue Sep 07 10:05:19 2010 +0200 @@ -94,11 +94,11 @@ lemma lookup_map_entry [simp]: "lookup (map_entry k f m) = (lookup m) (k := Option.map f (lookup m k))" - by (cases "lookup m k") (simp_all add: map_entry_def expand_fun_eq) + by (cases "lookup m k") (simp_all add: map_entry_def ext_iff) lemma lookup_tabulate [simp]: "lookup (tabulate ks f) = (Some o f) |` set ks" - by (induct ks) (auto simp add: tabulate_def restrict_map_def expand_fun_eq) + by (induct ks) (auto simp add: tabulate_def restrict_map_def ext_iff) lemma lookup_bulkload [simp]: "lookup (bulkload xs) = (\k. if k < length xs then Some (xs ! k) else None)" @@ -146,7 +146,7 @@ lemma bulkload_tabulate: "bulkload xs = tabulate [0.. m = Mapping Map.empty" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/More_List.thy --- a/src/HOL/Library/More_List.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/More_List.thy Tue Sep 07 10:05:19 2010 +0200 @@ -30,7 +30,7 @@ lemma foldr_fold_rev: "foldr f xs = fold f (rev xs)" - by (simp add: foldr_foldl foldl_fold expand_fun_eq) + by (simp add: foldr_foldl foldl_fold ext_iff) lemma fold_rev_conv [code_unfold]: "fold f (rev xs) = foldr f xs" @@ -49,7 +49,7 @@ lemma fold_apply: assumes "\x. x \ set xs \ h \ g x = f x \ h" shows "h \ fold g xs = fold f xs \ h" - using assms by (induct xs) (simp_all add: expand_fun_eq) + using assms by (induct xs) (simp_all add: ext_iff) lemma fold_invariant: assumes "\x. x \ set xs \ Q x" and "P s" @@ -164,7 +164,7 @@ lemma (in lattice) Inf_fin_set_foldr [code_unfold]: "Inf_fin (set (x # xs)) = foldr inf xs x" - by (simp add: Inf_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps) + by (simp add: Inf_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps) lemma (in lattice) Sup_fin_set_fold: "Sup_fin (set (x # xs)) = fold sup xs x" @@ -177,7 +177,7 @@ lemma (in lattice) Sup_fin_set_foldr [code_unfold]: "Sup_fin (set (x # xs)) = foldr sup xs x" - by (simp add: Sup_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps) + by (simp add: Sup_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps) lemma (in linorder) Min_fin_set_fold: "Min (set (x # xs)) = fold min xs x" @@ -190,7 +190,7 @@ lemma (in linorder) Min_fin_set_foldr [code_unfold]: "Min (set (x # xs)) = foldr min xs x" - by (simp add: Min_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps) + by (simp add: Min_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps) lemma (in linorder) Max_fin_set_fold: "Max (set (x # xs)) = fold max xs x" @@ -203,7 +203,7 @@ lemma (in linorder) Max_fin_set_foldr [code_unfold]: "Max (set (x # xs)) = foldr max xs x" - by (simp add: Max_fin_set_fold ac_simps foldr_fold expand_fun_eq del: set.simps) + by (simp add: Max_fin_set_fold ac_simps foldr_fold ext_iff del: set.simps) lemma (in complete_lattice) Inf_set_fold: "Inf (set xs) = fold inf xs top" @@ -215,7 +215,7 @@ lemma (in complete_lattice) Inf_set_foldr [code_unfold]: "Inf (set xs) = foldr inf xs top" - by (simp add: Inf_set_fold ac_simps foldr_fold expand_fun_eq) + by (simp add: Inf_set_fold ac_simps foldr_fold ext_iff) lemma (in complete_lattice) Sup_set_fold: "Sup (set xs) = fold sup xs bot" @@ -227,7 +227,7 @@ lemma (in complete_lattice) Sup_set_foldr [code_unfold]: "Sup (set xs) = foldr sup xs bot" - by (simp add: Sup_set_fold ac_simps foldr_fold expand_fun_eq) + by (simp add: Sup_set_fold ac_simps foldr_fold ext_iff) lemma (in complete_lattice) INFI_set_fold: "INFI (set xs) f = fold (inf \ f) xs top" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/More_Set.thy --- a/src/HOL/Library/More_Set.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/More_Set.thy Tue Sep 07 10:05:19 2010 +0200 @@ -18,7 +18,7 @@ lemma fun_left_comm_idem_remove: "fun_left_comm_idem remove" proof - - have rem: "remove = (\x A. A - {x})" by (simp add: expand_fun_eq remove_def) + have rem: "remove = (\x A. A - {x})" by (simp add: ext_iff remove_def) show ?thesis by (simp only: fun_left_comm_idem_remove rem) qed @@ -26,7 +26,7 @@ assumes "finite A" shows "B - A = Finite_Set.fold remove B A" proof - - have rem: "remove = (\x A. A - {x})" by (simp add: expand_fun_eq remove_def) + have rem: "remove = (\x A. A - {x})" by (simp add: ext_iff remove_def) show ?thesis by (simp only: rem assms minus_fold_remove) qed @@ -124,6 +124,6 @@ lemma not_set_compl: "Not \ set xs = - set xs" - by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq) + by (simp add: fun_Compl_def bool_Compl_def comp_def ext_iff) end diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Tue Sep 07 10:05:19 2010 +0200 @@ -26,7 +26,7 @@ lemma multiset_ext_iff: "M = N \ (\a. count M a = count N a)" - by (simp only: count_inject [symmetric] expand_fun_eq) + by (simp only: count_inject [symmetric] ext_iff) lemma multiset_ext: "(\x. count A x = count B x) \ A = B" @@ -581,7 +581,7 @@ apply (rule empty [unfolded defns]) apply (subgoal_tac "f(b := f b + 1) = (\a. f a + (if a=b then 1 else 0))") prefer 2 - apply (simp add: expand_fun_eq) + apply (simp add: ext_iff) apply (erule ssubst) apply (erule Abs_multiset_inverse [THEN subst]) apply (drule add') @@ -883,13 +883,13 @@ with finite_dom_map_of [of xs] have "finite ?A" by (auto intro: finite_subset) then show ?thesis - by (simp add: count_of_def expand_fun_eq multiset_def) + by (simp add: count_of_def ext_iff multiset_def) qed lemma count_simps [simp]: "count_of [] = (\_. 0)" "count_of ((x, n) # xs) = (\y. if x = y then n else count_of xs y)" - by (simp_all add: count_of_def expand_fun_eq) + by (simp_all add: count_of_def ext_iff) lemma count_of_empty: "x \ fst ` set xs \ count_of xs x = 0" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Order_Relation.thy --- a/src/HOL/Library/Order_Relation.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Order_Relation.thy Tue Sep 07 10:05:19 2010 +0200 @@ -81,7 +81,7 @@ lemma Refl_antisym_eq_Image1_Image1_iff: "\Refl r; antisym r; a:Field r; b:Field r\ \ r `` {a} = r `` {b} \ a=b" -by(simp add: expand_set_eq antisym_def refl_on_def) metis +by(simp add: set_ext_iff antisym_def refl_on_def) metis lemma Partial_order_eq_Image1_Image1_iff: "\Partial_order r; a:Field r; b:Field r\ \ r `` {a} = r `` {b} \ a=b" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Permutations.thy Tue Sep 07 10:05:19 2010 +0200 @@ -16,7 +16,7 @@ (* ------------------------------------------------------------------------- *) lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" - by (auto simp add: expand_fun_eq swap_def fun_upd_def) + by (auto simp add: ext_iff swap_def fun_upd_def) lemma swap_id_refl: "Fun.swap a a id = id" by simp lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id" by (rule ext, simp add: swap_def) @@ -25,7 +25,7 @@ lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id" shows "inv f = g" - using fg gf inv_equality[of g f] by (auto simp add: expand_fun_eq) + using fg gf inv_equality[of g f] by (auto simp add: ext_iff) lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id" by (rule inv_unique_comp, simp_all) @@ -67,16 +67,16 @@ assumes pS: "p permutes S" shows "p (inv p x) = x" and "inv p (p x) = x" - using permutes_inv_o[OF pS, unfolded expand_fun_eq o_def] by auto + using permutes_inv_o[OF pS, unfolded ext_iff o_def] by auto lemma permutes_subset: "p permutes S \ S \ T ==> p permutes T" unfolding permutes_def by blast lemma permutes_empty[simp]: "p permutes {} \ p = id" - unfolding expand_fun_eq permutes_def apply simp by metis + unfolding ext_iff permutes_def apply simp by metis lemma permutes_sing[simp]: "p permutes {a} \ p = id" - unfolding expand_fun_eq permutes_def apply simp by metis + unfolding ext_iff permutes_def apply simp by metis lemma permutes_univ: "p permutes UNIV \ (\y. \!x. p x = y)" unfolding permutes_def by simp @@ -111,7 +111,7 @@ using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p" - unfolding expand_fun_eq permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]] + unfolding ext_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]] by blast (* ------------------------------------------------------------------------- *) @@ -136,7 +136,7 @@ {assume pS: "p permutes insert a S" let ?b = "p a" let ?q = "Fun.swap a (p a) id o p" - have th0: "p = Fun.swap a ?b id o ?q" unfolding expand_fun_eq o_assoc by simp + have th0: "p = Fun.swap a ?b id o ?q" unfolding ext_iff o_assoc by simp have th1: "?b \ insert a S " unfolding permutes_in_image[OF pS] by simp from permutes_insert_lemma[OF pS] th0 th1 have "\ b q. p = Fun.swap a b id o q \ b \ insert a S \ q permutes S" by blast} @@ -180,11 +180,11 @@ and eq: "?g (b,p) = ?g (c,q)" from bp cq have ths: "b \ insert x F" "c \ insert x F" "x \ insert x F" "p permutes F" "q permutes F" by auto from ths(4) `x \ F` eq have "b = ?g (b,p) x" unfolding permutes_def - by (auto simp add: swap_def fun_upd_def expand_fun_eq) + by (auto simp add: swap_def fun_upd_def ext_iff) also have "\ = ?g (c,q) x" using ths(5) `x \ F` eq - by (auto simp add: swap_def fun_upd_def expand_fun_eq) + by (auto simp add: swap_def fun_upd_def ext_iff) also have "\ = c"using ths(5) `x \ F` unfolding permutes_def - by (auto simp add: swap_def fun_upd_def expand_fun_eq) + by (auto simp add: swap_def fun_upd_def ext_iff) finally have bc: "b = c" . hence "Fun.swap x b id = Fun.swap x c id" by simp with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp @@ -251,12 +251,12 @@ (* Various combinations of transpositions with 2, 1 and 0 common elements. *) (* ------------------------------------------------------------------------- *) -lemma swap_id_common:" a \ c \ b \ c \ 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) +lemma swap_id_common:" a \ c \ b \ c \ 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) -lemma swap_id_common': "~(a = b) \ ~(a = c) \ 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) +lemma swap_id_common': "~(a = b) \ ~(a = c) \ 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) lemma swap_id_independent: "~(a = c) \ ~(a = d) \ ~(b = c) \ ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id" - by (simp add: swap_def expand_fun_eq) + by (simp add: swap_def ext_iff) (* ------------------------------------------------------------------------- *) (* Permutations as transposition sequences. *) @@ -352,18 +352,18 @@ apply (rule_tac x="b" in exI) apply (rule_tac x="d" in exI) apply (rule_tac x="b" in exI) - apply (clarsimp simp add: expand_fun_eq swap_def) + apply (clarsimp simp add: ext_iff swap_def) apply (case_tac "a \ c \ b = d") apply (rule disjI2) apply (rule_tac x="c" in exI) apply (rule_tac x="d" in exI) apply (rule_tac x="c" in exI) - apply (clarsimp simp add: expand_fun_eq swap_def) + apply (clarsimp simp add: ext_iff swap_def) apply (rule disjI2) apply (rule_tac x="c" in exI) apply (rule_tac x="d" in exI) apply (rule_tac x="b" in exI) - apply (clarsimp simp add: expand_fun_eq swap_def) + apply (clarsimp simp add: ext_iff swap_def) done with H show ?thesis by metis qed @@ -518,7 +518,7 @@ from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast from swapidseq_inverse_exists[OF n] obtain q where q: "swapidseq n q" "p \ q = id" "q \ p = id" by blast - thus ?thesis unfolding bij_iff apply (auto simp add: expand_fun_eq) apply metis done + thus ?thesis unfolding bij_iff apply (auto simp add: ext_iff) apply metis done qed lemma permutation_finite_support: assumes p: "permutation p" @@ -544,7 +544,7 @@ lemma bij_swap_comp: assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p" using surj_f_inv_f[OF bij_is_surj[OF bp]] - by (simp add: expand_fun_eq swap_def bij_inv_eq_iff[OF bp]) + by (simp add: ext_iff swap_def bij_inv_eq_iff[OF bp]) lemma bij_swap_ompose_bij: "bij p \ bij (Fun.swap a b id o p)" proof- @@ -688,7 +688,7 @@ ultimately have "p n = n" by blast } ultimately show "p n = n" by blast qed} - thus ?thesis by (auto simp add: expand_fun_eq) + thus ?thesis by (auto simp add: ext_iff) qed lemma permutes_natset_ge: @@ -811,7 +811,7 @@ shows "setsum f {p. p permutes (insert a S)} = setsum (\b. setsum (\q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)" proof- have th0: "\f a b. (\(b,p). f (Fun.swap a b id o p)) = f o (\(b,p). Fun.swap a b id o p)" - by (simp add: expand_fun_eq) + by (simp add: ext_iff) have th1: "\P Q. P \ Q = {(a,b). a \ P \ b \ Q}" by blast have th2: "\P Q. P \ (P \ Q) \ P \ Q" by blast show ?thesis diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Polynomial.thy Tue Sep 07 10:05:19 2010 +0200 @@ -16,7 +16,7 @@ by auto lemma expand_poly_eq: "p = q \ (\n. coeff p n = coeff q n)" -by (simp add: coeff_inject [symmetric] expand_fun_eq) +by (simp add: coeff_inject [symmetric] ext_iff) lemma poly_ext: "(\n. coeff p n = coeff q n) \ p = q" by (simp add: expand_poly_eq) @@ -1403,7 +1403,7 @@ fixes p q :: "'a::{idom,ring_char_0} poly" shows "poly p = poly q \ p = q" using poly_zero [of "p - q"] - by (simp add: expand_fun_eq) + by (simp add: ext_iff) subsection {* Composition of polynomials *} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Sep 07 10:05:19 2010 +0200 @@ -12,7 +12,7 @@ declare le_bool_def_raw[code_pred_inline] lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)" -by (rule eq_reflection) (auto simp add: expand_fun_eq min_def le_bool_def) +by (rule eq_reflection) (auto simp add: ext_iff min_def le_bool_def) setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Quotient_List.thy --- a/src/HOL/Library/Quotient_List.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Quotient_List.thy Tue Sep 07 10:05:19 2010 +0200 @@ -19,7 +19,7 @@ lemma map_id[id_simps]: shows "map id = id" - apply(simp add: expand_fun_eq) + apply(simp add: ext_iff) apply(rule allI) apply(induct_tac x) apply(simp_all) @@ -92,7 +92,7 @@ lemma cons_prs[quot_preserve]: assumes q: "Quotient R Abs Rep" shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" - by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) + by (simp only: ext_iff fun_map_def cons_prs_aux[OF q]) (simp) lemma cons_rsp[quot_respect]: @@ -122,7 +122,7 @@ and b: "Quotient R2 abs2 rep2" shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" and "((abs1 ---> id) ---> map rep1 ---> id) map = map" - by (simp_all only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) + by (simp_all only: ext_iff fun_map_def map_prs_aux[OF a b]) (simp_all add: Quotient_abs_rep[OF a]) lemma map_rsp[quot_respect]: @@ -148,7 +148,7 @@ assumes a: "Quotient R1 abs1 rep1" and b: "Quotient R2 abs2 rep2" shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" - by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) + by (simp only: ext_iff fun_map_def foldr_prs_aux[OF a b]) (simp) lemma foldl_prs_aux: @@ -162,7 +162,7 @@ assumes a: "Quotient R1 abs1 rep1" and b: "Quotient R2 abs2 rep2" shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" - by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) + by (simp only: ext_iff fun_map_def foldl_prs_aux[OF a b]) (simp) lemma list_all2_empty: @@ -231,7 +231,7 @@ lemma[quot_preserve]: assumes a: "Quotient R abs1 rep1" shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2" - apply (simp add: expand_fun_eq) + apply (simp add: ext_iff) apply clarify apply (induct_tac xa xb rule: list_induct2') apply (simp_all add: Quotient_abs_rep[OF a]) @@ -244,7 +244,7 @@ lemma list_all2_eq[id_simps]: shows "(list_all2 (op =)) = (op =)" - unfolding expand_fun_eq + unfolding ext_iff apply(rule allI)+ apply(induct_tac x xa rule: list_induct2') apply(simp_all) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Quotient_Option.thy --- a/src/HOL/Library/Quotient_Option.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Quotient_Option.thy Tue Sep 07 10:05:19 2010 +0200 @@ -66,16 +66,16 @@ lemma option_Some_prs[quot_preserve]: assumes q: "Quotient R Abs Rep" shows "(Rep ---> Option.map Abs) Some = Some" - apply(simp add: expand_fun_eq) + apply(simp add: ext_iff) apply(simp add: Quotient_abs_rep[OF q]) done lemma option_map_id[id_simps]: shows "Option.map id = id" - by (simp add: expand_fun_eq split_option_all) + by (simp add: ext_iff split_option_all) lemma option_rel_eq[id_simps]: shows "option_rel (op =) = (op =)" - by (simp add: expand_fun_eq split_option_all) + by (simp add: ext_iff split_option_all) end diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Quotient_Product.thy Tue Sep 07 10:05:19 2010 +0200 @@ -51,7 +51,7 @@ assumes q1: "Quotient R1 Abs1 Rep1" assumes q2: "Quotient R2 Abs2 Rep2" shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" - apply(simp add: expand_fun_eq) + apply(simp add: ext_iff) apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) done @@ -65,7 +65,7 @@ assumes q1: "Quotient R1 Abs1 Rep1" assumes q2: "Quotient R2 Abs2 Rep2" shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" - apply(simp add: expand_fun_eq) + apply(simp add: ext_iff) apply(simp add: Quotient_abs_rep[OF q1]) done @@ -79,7 +79,7 @@ assumes q1: "Quotient R1 Abs1 Rep1" assumes q2: "Quotient R2 Abs2 Rep2" shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" - apply(simp add: expand_fun_eq) + apply(simp add: ext_iff) apply(simp add: Quotient_abs_rep[OF q2]) done @@ -91,7 +91,7 @@ assumes q1: "Quotient R1 Abs1 Rep1" and q2: "Quotient R2 Abs2 Rep2" shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split" - by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + by (simp add: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) lemma [quot_respect]: shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> @@ -103,7 +103,7 @@ and q2: "Quotient R2 abs2 rep2" shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel" - by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + by (simp add: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) lemma [quot_preserve]: shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2) @@ -118,6 +118,6 @@ lemma prod_rel_eq[id_simps]: shows "prod_rel (op =) (op =) = (op =)" - by (simp add: expand_fun_eq) + by (simp add: ext_iff) end diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Quotient_Sum.thy Tue Sep 07 10:05:19 2010 +0200 @@ -74,7 +74,7 @@ assumes q1: "Quotient R1 Abs1 Rep1" assumes q2: "Quotient R2 Abs2 Rep2" shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" - apply(simp add: expand_fun_eq) + apply(simp add: ext_iff) apply(simp add: Quotient_abs_rep[OF q1]) done @@ -82,16 +82,16 @@ assumes q1: "Quotient R1 Abs1 Rep1" assumes q2: "Quotient R2 Abs2 Rep2" shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" - apply(simp add: expand_fun_eq) + apply(simp add: ext_iff) apply(simp add: Quotient_abs_rep[OF q2]) done lemma sum_map_id[id_simps]: shows "sum_map id id = id" - by (simp add: expand_fun_eq split_sum_all) + by (simp add: ext_iff split_sum_all) lemma sum_rel_eq[id_simps]: shows "sum_rel (op =) (op =) = (op =)" - by (simp add: expand_fun_eq split_sum_all) + by (simp add: ext_iff split_sum_all) end diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/RBT.thy --- a/src/HOL/Library/RBT.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/RBT.thy Tue Sep 07 10:05:19 2010 +0200 @@ -112,7 +112,7 @@ lemma lookup_empty [simp]: "lookup empty = Map.empty" - by (simp add: empty_def lookup_RBT expand_fun_eq) + by (simp add: empty_def lookup_RBT ext_iff) lemma lookup_insert [simp]: "lookup (insert k v t) = (lookup t)(k \ v)" @@ -144,7 +144,7 @@ lemma fold_fold: "fold f t = More_List.fold (prod_case f) (entries t)" - by (simp add: fold_def expand_fun_eq RBT_Impl.fold_def entries_impl_of) + by (simp add: fold_def ext_iff RBT_Impl.fold_def entries_impl_of) lemma is_empty_empty [simp]: "is_empty t \ t = empty" @@ -152,7 +152,7 @@ lemma RBT_lookup_empty [simp]: (*FIXME*) "RBT_Impl.lookup t = Map.empty \ t = RBT_Impl.Empty" - by (cases t) (auto simp add: expand_fun_eq) + by (cases t) (auto simp add: ext_iff) lemma lookup_empty_empty [simp]: "lookup t = Map.empty \ t = empty" @@ -220,7 +220,7 @@ lemma bulkload_Mapping [code]: "Mapping.bulkload vs = Mapping (bulkload (List.map (\n. (n, vs ! n)) [0.. entries t1 = entries t2" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/RBT_Impl.thy Tue Sep 07 10:05:19 2010 +0200 @@ -1019,7 +1019,7 @@ theorem lookup_map_entry: "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))" - by (induct t) (auto split: option.splits simp add: expand_fun_eq) + by (induct t) (auto split: option.splits simp add: ext_iff) subsection {* Mapping all entries *} @@ -1054,7 +1054,7 @@ lemma fold_simps [simp, code]: "fold f Empty = id" "fold f (Branch c lt k v rt) = fold f rt \ f k v \ fold f lt" - by (simp_all add: fold_def expand_fun_eq) + by (simp_all add: fold_def ext_iff) subsection {* Bulkloading a tree *} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Set_Algebras.thy --- a/src/HOL/Library/Set_Algebras.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Set_Algebras.thy Tue Sep 07 10:05:19 2010 +0200 @@ -72,7 +72,7 @@ show "monoid_add.listsum set_plus {0::'a} = listsum_set" by (simp only: listsum_set_def) show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set" - by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq) + by (simp add: set_add.setsum_def setsum_set_def ext_iff) qed interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \ 'a set \ 'a set" proof @@ -117,7 +117,7 @@ show "power.power {1} set_times = (\A n. power_set n A)" by (simp add: power_set_def) show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set" - by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq) + by (simp add: set_mult.setprod_def setprod_set_def ext_iff) qed lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \ D" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Univ_Poly.thy --- a/src/HOL/Library/Univ_Poly.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Library/Univ_Poly.thy Tue Sep 07 10:05:19 2010 +0200 @@ -382,7 +382,7 @@ lemma (in idom_char_0) poly_entire: "poly (p *** q) = poly [] \ poly p = poly [] \ poly q = poly []" using poly_entire_lemma2[of p q] -by (auto simp add: expand_fun_eq poly_mult) +by (auto simp add: ext_iff poly_mult) lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \ poly []) = ((poly p \ poly []) & (poly q \ poly []))" by (simp add: poly_entire) @@ -847,14 +847,14 @@ assume eq: ?lhs hence "\x. poly ((c#cs) +++ -- (d#ds)) x = 0" by (simp only: poly_minus poly_add algebra_simps) simp - hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add:expand_fun_eq) + hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add: ext_iff) hence "c = d \ list_all (\x. x=0) ((cs +++ -- ds))" unfolding poly_zero by (simp add: poly_minus_def algebra_simps) hence "c = d \ (\x. poly (cs +++ -- ds) x = 0)" unfolding poly_zero[symmetric] by simp - thus ?rhs by (simp add: poly_minus poly_add algebra_simps expand_fun_eq) + thus ?rhs by (simp add: poly_minus poly_add algebra_simps ext_iff) next - assume ?rhs then show ?lhs by(simp add:expand_fun_eq) + assume ?rhs then show ?lhs by(simp add:ext_iff) qed lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \ pnormalize p = pnormalize q" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Limits.thy Tue Sep 07 10:05:19 2010 +0200 @@ -46,7 +46,7 @@ lemma expand_net_eq: shows "net = net' \ (\P. eventually P net = eventually P net')" -unfolding Rep_net_inject [symmetric] expand_fun_eq eventually_def .. +unfolding Rep_net_inject [symmetric] ext_iff eventually_def .. lemma eventually_True [simp]: "eventually (\x. True) net" unfolding eventually_def diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/List.thy --- a/src/HOL/List.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/List.thy Tue Sep 07 10:05:19 2010 +0200 @@ -2317,7 +2317,7 @@ lemma foldl_apply: assumes "\x. x \ set xs \ f x \ h = h \ g x" shows "foldl (\s x. f x s) (h s) xs = h (foldl (\s x. g x s) s xs)" - by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: expand_fun_eq) + by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: ext_iff) lemma foldl_cong [fundef_cong, recdef_cong]: "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] @@ -4564,7 +4564,7 @@ lemma member_set: "member = set" - by (simp add: expand_fun_eq member_def mem_def) + by (simp add: ext_iff member_def mem_def) lemma member_rec [code]: "member (x # xs) y \ x = y \ member xs y" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Map.thy --- a/src/HOL/Map.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Map.thy Tue Sep 07 10:05:19 2010 +0200 @@ -218,7 +218,7 @@ lemma map_of_zip_map: "map_of (zip xs (map f xs)) = (\x. if x \ set xs then Some (f x) else None)" - by (induct xs) (simp_all add: expand_fun_eq) + by (induct xs) (simp_all add: ext_iff) lemma finite_range_map_of: "finite (range (map_of xys))" apply (induct xys) @@ -245,7 +245,7 @@ lemma map_of_map: "map_of (map (\(k, v). (k, f v)) xs) = Option.map f \ map_of xs" - by (induct xs) (auto simp add: expand_fun_eq) + by (induct xs) (auto simp add: ext_iff) lemma dom_option_map: "dom (\k. Option.map (f k) (m k)) = dom m" @@ -347,7 +347,7 @@ lemma map_add_map_of_foldr: "m ++ map_of ps = foldr (\(k, v) m. m(k \ v)) ps m" - by (induct ps) (auto simp add: expand_fun_eq map_add_def) + by (induct ps) (auto simp add: ext_iff map_add_def) subsection {* @{term [source] restrict_map} *} @@ -381,26 +381,26 @@ lemma restrict_fun_upd [simp]: "m(x := y)|`D = (if x \ D then (m|`(D-{x}))(x := y) else m|`D)" -by (simp add: restrict_map_def expand_fun_eq) +by (simp add: restrict_map_def ext_iff) lemma fun_upd_None_restrict [simp]: "(m|`D)(x := None) = (if x:D then m|`(D - {x}) else m|`D)" -by (simp add: restrict_map_def expand_fun_eq) +by (simp add: restrict_map_def ext_iff) lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)" -by (simp add: restrict_map_def expand_fun_eq) +by (simp add: restrict_map_def ext_iff) lemma fun_upd_restrict_conv [simp]: "x \ D \ (m|`D)(x := y) = (m|`(D-{x}))(x := y)" -by (simp add: restrict_map_def expand_fun_eq) +by (simp add: restrict_map_def ext_iff) lemma map_of_map_restrict: "map_of (map (\k. (k, f k)) ks) = (Some \ f) |` set ks" - by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert) + by (induct ks) (simp_all add: ext_iff restrict_map_insert) lemma restrict_complement_singleton_eq: "f |` (- {x}) = f(x := None)" - by (simp add: restrict_map_def expand_fun_eq) + by (simp add: restrict_map_def ext_iff) subsection {* @{term [source] map_upds} *} @@ -641,7 +641,7 @@ by (fastsimp simp add: map_le_def) lemma map_le_iff_map_add_commute: "(f \\<^sub>m f ++ g) = (f++g = g++f)" -by(fastsimp simp: map_add_def map_le_def expand_fun_eq split: option.splits) +by(fastsimp simp: map_add_def map_le_def ext_iff split: option.splits) lemma map_add_le_mapE: "f++g \\<^sub>m h \ g \\<^sub>m h" by (fastsimp simp add: map_le_def map_add_def dom_def) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/MicroJava/Comp/AuxLemmas.thy --- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Tue Sep 07 10:05:19 2010 +0200 @@ -68,7 +68,7 @@ (**********************************************************************) lemma the_map_upd: "(the \ f(x\v)) = (the \ f)(x:=v)" -by (simp add: expand_fun_eq) +by (simp add: ext_iff) lemma map_of_in_set: "(map_of xs x = None) = (x \ set (map fst xs))" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/MicroJava/Comp/LemmasComp.thy --- a/src/HOL/MicroJava/Comp/LemmasComp.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Tue Sep 07 10:05:19 2010 +0200 @@ -113,7 +113,7 @@ by (auto simp add: subcls1_def2 comp_classname comp_is_class) lemma comp_widen: "widen (comp G) = widen G" - apply (simp add: expand_fun_eq) + apply (simp add: ext_iff) apply (intro allI iffI) apply (erule widen.cases) apply (simp_all add: comp_subcls1 widen.null) @@ -122,7 +122,7 @@ done lemma comp_cast: "cast (comp G) = cast G" - apply (simp add: expand_fun_eq) + apply (simp add: ext_iff) apply (intro allI iffI) apply (erule cast.cases) apply (simp_all add: comp_subcls1 cast.widen cast.subcls) @@ -133,7 +133,7 @@ done lemma comp_cast_ok: "cast_ok (comp G) = cast_ok G" - by (simp add: expand_fun_eq cast_ok_def comp_widen) + by (simp add: ext_iff cast_ok_def comp_widen) lemma compClass_fst [simp]: "(fst (compClass G C)) = (fst C)" @@ -171,7 +171,7 @@ apply (subgoal_tac "(Fun.comp fst (\(C, cno::cname, fdls::fdecl list, jmdls). (C, cno, fdls, map (compMethod G C) jmdls))) = fst") apply (simp del: image_compose) -apply (simp add: expand_fun_eq split_beta) +apply (simp add: ext_iff split_beta) done @@ -322,7 +322,7 @@ = (\x. (fst x, Object, fst (snd x), snd (snd (compMethod G Object (S, snd x)))))") apply (simp only:) -apply (simp add: expand_fun_eq) +apply (simp add: ext_iff) apply (intro strip) apply (subgoal_tac "(inv (\(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)") apply (simp only:) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Sep 07 10:05:19 2010 +0200 @@ -725,7 +725,7 @@ hence "a_max = a'" using a' min_max by auto thus False unfolding True using min_max by auto qed qed hence "\i. a_max i = a1 i" by auto - hence "a' = a" unfolding True `a=a0` apply-apply(subst expand_fun_eq,rule) + hence "a' = a" unfolding True `a=a0` apply-apply(subst ext_iff,rule) apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format] proof- case goal1 thus ?case apply(cases "x\{1..n}") by auto qed hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\s` `a'\s'` by auto @@ -738,7 +738,7 @@ have "a2 \ a" unfolding `a=a0` using k(2)[rule_format,of k] by auto hence "a2 \ s - {a}" using a2 by auto thus "a2 \ s'" unfolding a'(2)[THEN sym] by auto qed hence "\i. a_min i = a2 i" by auto - hence "a' = a3" unfolding as `a=a0` apply-apply(subst expand_fun_eq,rule) + hence "a' = a3" unfolding as `a=a0` apply-apply(subst ext_iff,rule) apply(erule_tac x=x in allE) unfolding a0a1(5)[rule_format] min_max(5)[rule_format] unfolding a3_def k(2)[rule_format] unfolding a0a1(5)[rule_format] proof- case goal1 show ?case unfolding goal1 apply(cases "x\{1..n}") defer apply(cases "x=k") @@ -834,7 +834,7 @@ proof- case goal1 thus ?case apply(cases "j\{1..n}",case_tac[!] "j=k") by auto qed have "\i. a_min i = a3 i" using a_max apply-apply(rule,erule_tac x=i in allE) unfolding min_max(5)[rule_format] *[rule_format] proof- case goal1 - thus ?case apply(cases "i\{1..n}") by auto qed hence "a_min = a3" unfolding expand_fun_eq . + thus ?case apply(cases "i\{1..n}") by auto qed hence "a_min = a3" unfolding ext_iff . hence "s' = insert a3 (s - {a1})" using a' unfolding `a=a1` True by auto thus ?thesis by auto next case False hence as:"a'=a_max" using ** by auto have "a_min = a0" unfolding kle_antisym[THEN sym,of _ _ n] apply(rule) @@ -843,7 +843,7 @@ thus "a_min \ s" by auto have "a0 \ s - {a1}" using a0a1(1-3) by auto thus "a0 \ s'" unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed hence "\i. a_max i = a1 i" unfolding a0a1(5)[rule_format] min_max(5)[rule_format] by auto - hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\s` `a'\s'` unfolding as `a=a1` unfolding expand_fun_eq by auto + hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\s` `a'\s'` unfolding as `a=a1` unfolding ext_iff by auto thus ?thesis by auto qed qed ultimately have *:"?A = {s, insert a3 (s - {a1})}" by blast have "s \ insert a3 (s - {a1})" using `a3\s` by auto @@ -863,7 +863,7 @@ thus False using ksimplexD(6)[OF assms(1),rule_format,OF u v] unfolding kle_def unfolding l(2) k(2) `k=l` apply-apply(erule disjE)apply(erule_tac[!] exE conjE)+ apply(erule_tac[!] x=l in allE)+ by(auto simp add: *) qed - hence aa':"a'\a" apply-apply rule unfolding expand_fun_eq unfolding a'_def k(2) + hence aa':"a'\a" apply-apply rule unfolding ext_iff unfolding a'_def k(2) apply(erule_tac x=l in allE) by auto have "a' \ s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\s`]) proof(cases "kle n a a'") case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise) @@ -877,22 +877,22 @@ have uxv:"\x. kle n u x \ kle n x v \ (x = u) \ (x = a) \ (x = a') \ (x = v)" proof- case goal1 thus ?case proof(cases "x k = u k", case_tac[!] "x l = u l") assume as:"x l = u l" "x k = u k" - have "x = u" unfolding expand_fun_eq + have "x = u" unfolding ext_iff using goal1(2)[THEN kle_imp_pointwise,unfolded l(2)] unfolding k(2) apply- using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next assume as:"x l \ u l" "x k = u k" - have "x = a'" unfolding expand_fun_eq unfolding a'_def + have "x = a'" unfolding ext_iff unfolding a'_def using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next assume as:"x l = u l" "x k \ u k" - have "x = a" unfolding expand_fun_eq + have "x = a" unfolding ext_iff using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as by auto qed thus ?case by auto next assume as:"x l \ u l" "x k \ u k" - have "x = v" unfolding expand_fun_eq + have "x = v" unfolding ext_iff using goal1(2)[THEN kle_imp_pointwise] unfolding l(2) k(2) apply- using goal1(1)[THEN kle_imp_pointwise] apply-apply rule apply(erule_tac x=xa in allE)+ proof- case goal1 thus ?case apply(cases "x=l") apply(case_tac[!] "x=k") using as `k\l` by auto qed thus ?case by auto qed qed @@ -935,9 +935,9 @@ moreover have "?A \ {s, insert a' (s - {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE) fix s' assume as:"ksimplex p n s'" and "\b\s'. s' - {b} = s - {a}" from this(2) guess a'' .. note a''=this - have "u\v" unfolding expand_fun_eq unfolding l(2) k(2) by auto + have "u\v" unfolding ext_iff unfolding l(2) k(2) by auto hence uv':"\ kle n v u" using uv using kle_antisym by auto - have "u\a" "v\a" unfolding expand_fun_eq k(2) l(2) by auto + have "u\a" "v\a" unfolding ext_iff k(2) l(2) by auto hence uvs':"u\s'" "v\s'" using `u\s` `v\s` using a'' by auto have lem6:"a \ s' \ a' \ s'" proof(cases "\x\s'. kle n x u \ kle n v x") case False then guess w unfolding ball_simps .. note w=this diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Sep 07 10:05:19 2010 +0200 @@ -1440,12 +1440,12 @@ lemma interval_cart: fixes a :: "'a::ord^'n" shows "{a <..< b} = {x::'a^'n. \i. a$i < x$i \ x$i < b$i}" and "{a .. b} = {x::'a^'n. \i. a$i \ x$i \ x$i \ b$i}" - by (auto simp add: expand_set_eq vector_less_def vector_le_def) + by (auto simp add: set_ext_iff vector_less_def vector_le_def) lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows "x \ {a<.. (\i. a$i < x$i \ x$i < b$i)" "x \ {a .. b} \ (\i. a$i \ x$i \ x$i \ b$i)" - using interval_cart[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def) + using interval_cart[of a b] by(auto simp add: set_ext_iff vector_less_def vector_le_def) lemma interval_eq_empty_cart: fixes a :: "real^'n" shows "({a <..< b} = {} \ (\i. b$i \ a$i))" (is ?th1) and @@ -1498,7 +1498,7 @@ lemma interval_sing: fixes a :: "'a::linorder^'n" shows "{a .. a} = {a} \ {a<.. x $ i" using x order_less_imp_le[of "a$i" "x$i"] - by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq) + by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq) } moreover { fix i have "x $ i \ b $ i" using x order_less_imp_le[of "x$i" "b$i"] - by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq) + by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq) } ultimately show "a \ x \ x \ b" - by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq) + by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq) qed lemma subset_interval_cart: fixes a :: "real^'n" shows @@ -1540,7 +1540,7 @@ lemma inter_interval_cart: fixes a :: "'a::linorder^'n" shows "{a .. b} \ {c .. d} = {(\ i. max (a$i) (c$i)) .. (\ i. min (b$i) (d$i))}" - unfolding expand_set_eq and Int_iff and mem_interval_cart + unfolding set_ext_iff and Int_iff and mem_interval_cart by auto lemma closed_interval_left_cart: fixes b::"real^'n" @@ -1656,7 +1656,7 @@ shows "(\x. m *s x + c) o (\x. inverse(m) *s x + (-(inverse(m) *s c))) = id" "(\x. inverse(m) *s x + (-(inverse(m) *s c))) o (\x. m *s x + c) = id" using m0 -apply (auto simp add: expand_fun_eq vector_add_ldistrib) +apply (auto simp add: ext_iff vector_add_ldistrib) by (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric]) lemma vector_affinity_eq: @@ -2119,10 +2119,10 @@ lemma open_closed_interval_1: fixes a :: "real^1" shows "{a<.. dest_vec1 b ==> {a .. b} = {a<.. {a,b}" - 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) + 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) lemma Lim_drop_le: fixes f :: "'a \ real^1" shows "(f ---> l) net \ ~(trivial_limit net) \ eventually (\x. dest_vec1 (f x) \ b) net ==> dest_vec1 l \ b" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Sep 07 10:05:19 2010 +0200 @@ -191,7 +191,7 @@ lemma affine_hull_finite: assumes "finite s" shows "affine hull s = {y. \u. setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" - unfolding affine_hull_explicit and expand_set_eq and mem_Collect_eq apply (rule,rule) + unfolding affine_hull_explicit and set_ext_iff and mem_Collect_eq apply (rule,rule) apply(erule exE)+ apply(erule conjE)+ defer apply(erule exE) apply(erule conjE) proof- fix x u assume "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = x" thus "\sa u. finite sa \ \ (\x. (x \ sa) = (x \ {})) \ sa \ s \ setsum u sa = 1 \ (\v\sa. u v *\<^sub>R v) = x" @@ -709,7 +709,7 @@ ultimately have "\k u x. (\i\{1..k}. 0 \ u i \ x i \ p) \ setsum u {1..k} = 1 \ (\i::nat = 1..k. u i *\<^sub>R x i) = y" apply(rule_tac x="card s" in exI) apply(rule_tac x="u \ f" in exI) apply(rule_tac x=f in exI) by fastsimp hence "y \ ?lhs" unfolding convex_hull_indexed by auto } - ultimately show ?thesis unfolding expand_set_eq by blast + ultimately show ?thesis unfolding set_ext_iff by blast qed subsection {* A stepping theorem for that expansion. *} @@ -882,7 +882,7 @@ lemma convex_hull_caratheodory: fixes p::"('a::euclidean_space) set" shows "convex hull p = {y. \s u. finite s \ s \ p \ card s \ DIM('a) + 1 \ (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" - unfolding convex_hull_explicit expand_set_eq mem_Collect_eq + unfolding convex_hull_explicit set_ext_iff mem_Collect_eq proof(rule,rule) fix y let ?P = "\n. \s u. finite s \ card s = n \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" assume "\s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = y" @@ -939,7 +939,7 @@ lemma caratheodory: "convex hull p = {x::'a::euclidean_space. \s. finite s \ s \ p \ card s \ DIM('a) + 1 \ x \ convex hull s}" - unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof- + unfolding set_ext_iff apply(rule, rule) unfolding mem_Collect_eq proof- fix x assume "x \ convex hull p" then obtain s u where "finite s" "s \ p" "card s \ DIM('a) + 1" "\x\s. 0 \ u x" "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = x"unfolding convex_hull_caratheodory by auto @@ -1029,7 +1029,7 @@ case (Suc n) show ?case proof(cases "n=0") case True have "{x. \t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t} = s" - unfolding expand_set_eq and mem_Collect_eq proof(rule, rule) + unfolding set_ext_iff and mem_Collect_eq proof(rule, rule) fix x assume "\t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t" then obtain t where t:"finite t" "t \ s" "card t \ Suc n" "x \ convex hull t" by auto show "x\s" proof(cases "card t = 0") @@ -1048,7 +1048,7 @@ case False have "{x. \t. finite t \ t \ s \ card t \ Suc n \ x \ convex hull t} = { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ s \ y \ {x. \t. finite t \ t \ s \ card t \ n \ x \ convex hull t}}" - unfolding expand_set_eq and mem_Collect_eq proof(rule,rule) + unfolding set_ext_iff and mem_Collect_eq proof(rule,rule) fix x assume "\u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \ 0 \ c \ c \ 1 \ u \ s \ (\t. finite t \ t \ s \ card t \ n \ v \ convex hull t)" then obtain u v c t where obt:"x = (1 - c) *\<^sub>R u + c *\<^sub>R v" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Sep 07 10:05:19 2010 +0200 @@ -665,7 +665,7 @@ have "\ireal" @@ -948,13 +948,13 @@ assumes lf: "linear f" and gf: "f o g = id" shows "linear g" proof- - from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def expand_fun_eq) + from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def ext_iff) by metis from linear_surjective_isomorphism[OF lf fi] obtain h:: "'a => 'a" where h: "linear h" "\x. h (f x) = x" "\x. f (h x) = x" by blast have "h = g" apply (rule ext) using gf h(2,3) - apply (simp add: o_def id_def expand_fun_eq) + apply (simp add: o_def id_def ext_iff) by metis with h(1) show ?thesis by blast qed @@ -1268,7 +1268,7 @@ have "(\x. x *\<^sub>R f') = (\x. x *\<^sub>R f'')" using assms [unfolded has_vector_derivative_def] by (rule frechet_derivative_unique_at) - thus ?thesis unfolding expand_fun_eq by auto + thus ?thesis unfolding ext_iff by auto qed lemma vector_derivative_unique_within_closed_interval: fixes f::"real \ 'n::ordered_euclidean_space" @@ -1279,7 +1279,7 @@ apply(rule frechet_derivative_unique_within_closed_interval[of "a" "b"]) using assms(3-)[unfolded has_vector_derivative_def] using assms(1-2) by auto show ?thesis proof(rule ccontr) assume "f' \ f''" moreover - hence "(\x. x *\<^sub>R f') 1 = (\x. x *\<^sub>R f'') 1" using * by (auto simp: expand_fun_eq) + hence "(\x. x *\<^sub>R f') 1 = (\x. x *\<^sub>R f'') 1" using * by (auto simp: ext_iff) ultimately show False unfolding o_def by auto qed qed lemma vector_derivative_at: diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Sep 07 10:05:19 2010 +0200 @@ -141,7 +141,7 @@ {fix i assume i: "i \ ?U" from i permutes_inv_o[OF pU] permutes_in_image[OF pU] have "((\i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)" - unfolding transpose_def by (simp add: expand_fun_eq)} + unfolding transpose_def by (simp add: ext_iff)} then show "setprod ((\i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) qed finally have "of_int (sign (inv p)) * (setprod (\i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" using sth @@ -207,7 +207,7 @@ have id0: "{id} \ ?PU" by (auto simp add: permutes_id) {fix p assume p: "p \ ?PU - {id}" then have "p \ id" by simp - then obtain i where i: "p i \ i" unfolding expand_fun_eq by auto + then obtain i where i: "p i \ i" unfolding ext_iff by auto from ld [OF i [symmetric]] have ex:"\i \ ?U. A$i$p i = 0" by blast from setprod_zero [OF fU ex] have "?pp p = 0" by simp} then have p0: "\p \ ?PU - {id}. ?pp p = 0" by blast diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Sep 07 10:05:19 2010 +0200 @@ -2363,7 +2363,7 @@ apply (rule span_mul) by (rule span_superset)} then have SC: "span ?C = span (insert a B)" - unfolding expand_set_eq span_breakdown_eq C(3)[symmetric] by auto + unfolding set_ext_iff span_breakdown_eq C(3)[symmetric] by auto thm pairwise_def {fix x y assume xC: "x \ ?C" and yC: "y \ ?C" and xy: "x \ y" {assume xa: "x = ?a" and ya: "y = ?a" @@ -2826,7 +2826,7 @@ " \x \ f ` basis ` {..i f) (basis i) = id (basis i)" - using inv_o_cancel[OF fi, unfolded expand_fun_eq id_def o_def] + using inv_o_cancel[OF fi, unfolded ext_iff id_def o_def] by auto from linear_eq_stdbasis[OF linear_compose[OF lf h(1)] linear_id th] @@ -2843,7 +2843,7 @@ h: "linear h" "\ x\ basis ` {..i g o f = id \ (\x. f(g x) = x) \ (\x. g(f x) = x)" - by (simp add: expand_fun_eq o_def id_def) + by (simp add: ext_iff o_def id_def) lemma linear_injective_isomorphism: fixes f::"'a::euclidean_space => 'a::euclidean_space" assumes lf: "linear f" and fi: "inj f" @@ -2995,10 +2995,10 @@ {fix f f':: "'a => 'a" assume lf: "linear f" "linear f'" and f: "f o f' = id" from f have sf: "surj f" - apply (auto simp add: o_def expand_fun_eq id_def surj_def) + apply (auto simp add: o_def ext_iff id_def surj_def) by metis from linear_surjective_isomorphism[OF lf(1) sf] lf f - have "f' o f = id" unfolding expand_fun_eq o_def id_def + have "f' o f = id" unfolding ext_iff o_def id_def by metis} then show ?thesis using lf lf' by metis qed @@ -3009,13 +3009,13 @@ assumes lf: "linear f" and gf: "g o f = id" shows "linear g" proof- - from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def expand_fun_eq) + from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def ext_iff) by metis from linear_injective_isomorphism[OF lf fi] obtain h:: "'a \ 'a" where h: "linear h" "\x. h (f x) = x" "\x. f (h x) = x" by blast have "h = g" apply (rule ext) using gf h(2,3) - apply (simp add: o_def id_def expand_fun_eq) + apply (simp add: o_def id_def ext_iff) by metis with h(1) show ?thesis by blast qed diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue Sep 07 10:05:19 2010 +0200 @@ -42,7 +42,7 @@ by (auto intro: ext) lemma Cart_eq: "(x = y) \ (\i. x$i = y$i)" - by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) + by (simp add: Cart_nth_inject [symmetric] ext_iff) lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" by (simp add: Cart_lambda_inverse) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 07 10:05:19 2010 +0200 @@ -253,10 +253,10 @@ lemma subset_ball[intro]: "d <= e ==> ball x d \ ball x e" by (simp add: subset_eq) lemma subset_cball[intro]: "d <= e ==> cball x d \ cball x e" by (simp add: subset_eq) lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s" - by (simp add: expand_set_eq) arith + by (simp add: set_ext_iff) arith lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s" - by (simp add: expand_set_eq) + by (simp add: set_ext_iff) lemma diff_less_iff: "(a::real) - b > 0 \ a > b" "(a::real) - b < 0 \ a < b" @@ -289,7 +289,7 @@ by (metis open_contains_ball subset_eq centre_in_ball) lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" - unfolding mem_ball expand_set_eq + unfolding mem_ball set_ext_iff apply (simp add: not_less) by (metis zero_le_dist order_trans dist_self) @@ -447,7 +447,7 @@ let ?T = "\{S. open S \ a \ S}" have "open ?T" by (simp add: open_Union) also have "?T = - {a}" - by (simp add: expand_set_eq separation_t1, auto) + by (simp add: set_ext_iff separation_t1, auto) finally show "closed {a}" unfolding closed_def . qed @@ -483,7 +483,7 @@ ==> ~(d x y * 2 < d x z \ d z y * 2 < d x z)" by arith have "open ?U \ open ?V \ x \ ?U \ y \ ?V \ ?U \ ?V = {}" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute] - by (auto simp add: expand_set_eq) + by (auto simp add: set_ext_iff) then show "\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}" by blast qed @@ -641,7 +641,7 @@ definition "interior S = {x. \T. open T \ x \ T \ T \ S}" lemma interior_eq: "interior S = S \ open S" - apply (simp add: expand_set_eq interior_def) + apply (simp add: set_ext_iff interior_def) apply (subst (2) open_subopen) by (safe, blast+) lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq) @@ -706,7 +706,7 @@ proof (rule ccontr) assume "x \ interior S" with `x \ R` `open R` obtain y where "y \ R - S" - unfolding interior_def expand_set_eq by fast + unfolding interior_def set_ext_iff by fast from `open R` `closed S` have "open (R - S)" by (rule open_Diff) from `R \ S \ T` have "R - S \ T" by fast from `y \ R - S` `open (R - S)` `R - S \ T` `interior T = {}` @@ -1006,7 +1006,7 @@ unfolding trivial_limit_def unfolding eventually_within eventually_at_topological unfolding islimpt_def - apply (clarsimp simp add: expand_set_eq) + apply (clarsimp simp add: set_ext_iff) apply (rename_tac T, rule_tac x=T in exI) apply (clarsimp, drule_tac x=y in bspec, simp_all) done @@ -1904,18 +1904,18 @@ fixes a :: "'a::real_normed_vector" shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}" apply (simp add: frontier_def closure_ball interior_open order_less_imp_le) - apply (simp add: expand_set_eq) + apply (simp add: set_ext_iff) by arith lemma frontier_cball: fixes a :: "'a::{real_normed_vector, perfect_space}" shows "frontier(cball a e) = {x. dist a x = e}" apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le) - apply (simp add: expand_set_eq) + apply (simp add: set_ext_iff) by arith lemma cball_eq_empty: "(cball x e = {}) \ e < 0" - apply (simp add: expand_set_eq not_le) + apply (simp add: set_ext_iff not_le) by (metis zero_le_dist dist_self order_less_le_trans) lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty) @@ -1927,13 +1927,13 @@ obtain a where "a \ x" "dist a x < e" using perfect_choose_dist [OF e] by auto hence "a \ x" "dist x a \ e" by (auto simp add: dist_commute) - with e show ?thesis by (auto simp add: expand_set_eq) + with e show ?thesis by (auto simp add: set_ext_iff) qed auto lemma cball_sing: fixes x :: "'a::metric_space" shows "e = 0 ==> cball x e = {x}" - by (auto simp add: expand_set_eq) + by (auto simp add: set_ext_iff) text{* For points in the interior, localization of limits makes no difference. *} @@ -4615,12 +4615,12 @@ lemma interval: fixes a :: "'a::ordered_euclidean_space" shows "{a <..< b} = {x::'a. \i x$$i < b$$i}" and "{a .. b} = {x::'a. \i x$$i \ x$$i \ b$$i}" - by(auto simp add:expand_set_eq eucl_le[where 'a='a] eucl_less[where 'a='a]) + by(auto simp add:set_ext_iff eucl_le[where 'a='a] eucl_less[where 'a='a]) lemma mem_interval: fixes a :: "'a::ordered_euclidean_space" shows "x \ {a<.. (\i x$$i < b$$i)" "x \ {a .. b} \ (\i x$$i \ x$$i \ b$$i)" - using interval[of a b] by(auto simp add: expand_set_eq eucl_le[where 'a='a] eucl_less[where 'a='a]) + using interval[of a b] by(auto simp add: set_ext_iff eucl_le[where 'a='a] eucl_less[where 'a='a]) lemma interval_eq_empty: fixes a :: "'a::ordered_euclidean_space" shows "({a <..< b} = {} \ (\i a$$i))" (is ?th1) and @@ -4662,7 +4662,7 @@ lemma interval_sing: fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}" "{a<.. x $$ i" using x order_less_imp_le[of "a$$i" "x$$i"] - by(simp add: expand_set_eq eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq) + by(simp add: set_ext_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq) } moreover { fix i assume "i b $$ i" using x order_less_imp_le[of "x$$i" "b$$i"] - by(simp add: expand_set_eq eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq) + by(simp add: set_ext_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq) } ultimately show "a \ x \ x \ b" - by(simp add: expand_set_eq eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq) + by(simp add: set_ext_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq) qed lemma subset_interval: fixes a :: "'a::ordered_euclidean_space" shows @@ -4757,7 +4757,7 @@ "{a<.. {c<.. (\i a$$i \ d$$i \ c$$i \ b$$i \ c$$i \ d$$i \ a$$i))" (is ?th4) proof- let ?z = "(\\ i. ((max (a$$i) (c$$i)) + (min (b$$i) (d$$i))) / 2)::'a" - note * = expand_set_eq Int_iff empty_iff mem_interval all_conj_distrib[THEN sym] eq_False + note * = set_ext_iff Int_iff empty_iff mem_interval all_conj_distrib[THEN sym] eq_False show ?th1 unfolding * apply safe apply(erule_tac x="?z" in allE) unfolding not_all apply(erule exE,rule_tac x=x in exI) apply(erule_tac[2-] x=i in allE) by auto show ?th2 unfolding * apply safe apply(erule_tac x="?z" in allE) @@ -4770,7 +4770,7 @@ lemma inter_interval: fixes a :: "'a::ordered_euclidean_space" shows "{a .. b} \ {c .. d} = {(\\ i. max (a$$i) (c$$i)) .. (\\ i. min (b$$i) (d$$i))}" - unfolding expand_set_eq and Int_iff and mem_interval + unfolding set_ext_iff and Int_iff and mem_interval by auto (* Moved interval_open_subset_closed a bit upwards *) @@ -5440,7 +5440,7 @@ then obtain x where "\n. x n \ s \ g n = f (x n)" using choice[of "\ n xa. xa \ s \ g n = f xa"] by auto hence x:"\n. x n \ s" "\n. g n = f (x n)" by auto - hence "f \ x = g" unfolding expand_fun_eq by auto + hence "f \ x = g" unfolding ext_iff by auto then obtain l where "l\s" and l:"(x ---> l) sequentially" using cs[unfolded complete_def, THEN spec[where x="x"]] using cauchy_isometric[OF `0 HNatInfinite diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/NSA/Star.thy --- a/src/HOL/NSA/Star.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/NSA/Star.thy Tue Sep 07 10:05:19 2010 +0200 @@ -87,7 +87,7 @@ sequence) as a special case of an internal set*} lemma starset_n_starset: "\n. (As n = A) ==> *sn* As = *s* A" -apply (drule expand_fun_eq [THEN iffD2]) +apply (drule ext_iff [THEN iffD2]) apply (simp add: starset_n_def starset_def star_of_def) done @@ -102,7 +102,7 @@ (*----------------------------------------------------------------*) lemma starfun_n_starfun: "\n. (F n = f) ==> *fn* F = *f* f" -apply (drule expand_fun_eq [THEN iffD2]) +apply (drule ext_iff [THEN iffD2]) apply (simp add: starfun_n_def starfun_def star_of_def) done diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/NSA/StarDef.thy Tue Sep 07 10:05:19 2010 +0200 @@ -145,7 +145,7 @@ "\\X. f (star_n X) = g (star_n X) \ {n. F n (X n) = G n (X n)} \ \\ \ f = g \ {n. F n = G n} \ \" -by (simp only: expand_fun_eq transfer_all) +by (simp only: ext_iff transfer_all) lemma transfer_star_n [transfer_intro]: "star_n X \ star_n (\n. X n)" by (rule reflexive) @@ -351,12 +351,12 @@ lemma transfer_Collect [transfer_intro]: "\\X. p (star_n X) \ {n. P n (X n)} \ \\ \ Collect p \ Iset (star_n (\n. Collect (P n)))" -by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n) +by (simp add: atomize_eq set_ext_iff all_star_eq Iset_star_n) lemma transfer_set_eq [transfer_intro]: "\a \ Iset (star_n A); b \ Iset (star_n B)\ \ a = b \ {n. A n = B n} \ \" -by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem) +by (simp only: set_ext_iff transfer_all transfer_iff transfer_mem) lemma transfer_ball [transfer_intro]: "\a \ Iset (star_n A); \X. p (star_n X) \ {n. P n (X n)} \ \\ diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Nat.thy --- a/src/HOL/Nat.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Nat.thy Tue Sep 07 10:05:19 2010 +0200 @@ -1360,7 +1360,7 @@ by (induct n) simp_all lemma of_nat_eq_id [simp]: "of_nat = id" - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) subsection {* The Set of Natural Numbers *} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Nat_Transfer.thy --- a/src/HOL/Nat_Transfer.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Nat_Transfer.thy Tue Sep 07 10:05:19 2010 +0200 @@ -170,7 +170,7 @@ apply (rule iffI) apply (erule finite_imageI) apply (erule finite_imageD) - apply (auto simp add: image_def expand_set_eq inj_on_def) + apply (auto simp add: image_def set_ext_iff inj_on_def) apply (drule_tac x = "int x" in spec, auto) apply (drule_tac x = "int x" in spec, auto) apply (drule_tac x = "int x" in spec, auto) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Nitpick.thy Tue Sep 07 10:05:19 2010 +0200 @@ -59,7 +59,7 @@ lemma Ex1_def [nitpick_def, no_atp]: "Ex1 P \ \x. P = {x}" apply (rule eq_reflection) -apply (simp add: Ex1_def expand_set_eq) +apply (simp add: Ex1_def set_ext_iff) apply (rule iffI) apply (erule exE) apply (erule conjE) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 07 10:05:19 2010 +0200 @@ -110,7 +110,7 @@ "my_int_rel (x, y) (u, v) = (x + v = u + y)" quotient_type my_int = "nat \ nat" / my_int_rel -by (auto simp add: equivp_def expand_fun_eq) +by (auto simp add: equivp_def ext_iff) definition add_raw where "add_raw \ \(x, y) (u, v). (x + (u\nat), y + (v\nat))" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Nominal/Examples/Class1.thy --- a/src/HOL/Nominal/Examples/Class1.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Nominal/Examples/Class1.thy Tue Sep 07 10:05:19 2010 +0200 @@ -2167,7 +2167,7 @@ apply(auto simp add: fresh_left calc_atm forget) apply(generate_fresh "coname") apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto) @@ -2183,7 +2183,7 @@ apply(auto simp add: fresh_left calc_atm forget) apply(generate_fresh "name") apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto) @@ -2199,13 +2199,13 @@ apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] apply(generate_fresh "name") apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule forget) apply(simp add: fresh_left calc_atm) apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule forget) @@ -2224,13 +2224,13 @@ apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] apply(generate_fresh "name") apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule forget) apply(simp add: fresh_left calc_atm) apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule forget) @@ -2255,7 +2255,7 @@ apply(auto simp add: fresh_prod fresh_atm)[1] apply(simp) apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule conjI) @@ -2283,7 +2283,7 @@ apply(auto simp add: fresh_prod fresh_atm)[1] apply(simp) apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule conjI) @@ -2304,13 +2304,13 @@ apply(subgoal_tac "OrR1 .M d = OrR1 .([(c,a)]\M) d") apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule forget) apply(simp add: fresh_left calc_atm) apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule forget) @@ -2328,13 +2328,13 @@ apply(subgoal_tac "OrR2 .M d = OrR2 .([(c,a)]\M) d") apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule forget) apply(simp add: fresh_left calc_atm) apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm) apply(rule forget) @@ -2353,13 +2353,13 @@ apply(subgoal_tac "ImpR (x)..M d = ImpR (ca)..([(c,a)]\[(ca,x)]\M) d") apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) apply(rule forget) apply(simp add: fresh_left calc_atm) apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh) apply(rule forget) @@ -2378,7 +2378,7 @@ apply(subgoal_tac "ImpL .M (x).N y = ImpL .([(ca,a)]\M) (caa).([(caa,x)]\N) y") apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1] apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: expand_fun_eq) +apply(simp add: ext_iff) apply(rule allI) apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) apply(rule forget) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Nominal/Nominal.thy Tue Sep 07 10:05:19 2010 +0200 @@ -148,11 +148,11 @@ (* permutation on sets *) lemma empty_eqvt: shows "pi\{} = {}" - by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] expand_fun_eq) + by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] ext_iff) lemma union_eqvt: shows "(pi\(X\Y)) = (pi\X) \ (pi\Y)" - by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] expand_fun_eq) + by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] ext_iff) (* permutations on products *) lemma fst_eqvt: @@ -2069,7 +2069,7 @@ show "?LHS" proof (rule ccontr) assume "(pi\f) \ f" - hence "\x. (pi\f) x \ f x" by (simp add: expand_fun_eq) + hence "\x. (pi\f) x \ f x" by (simp add: ext_iff) then obtain x where b1: "(pi\f) x \ f x" by force from b have "pi\(f ((rev pi)\x)) = f (pi\((rev pi)\x))" by force hence "(pi\f)(pi\((rev pi)\x)) = f (pi\((rev pi)\x))" @@ -2763,7 +2763,7 @@ and at: "at TYPE ('x)" shows "cp TYPE ('a\'b) TYPE('x) TYPE('y)" using c1 c2 -apply(auto simp add: cp_def perm_fun_def expand_fun_eq) +apply(auto simp add: cp_def perm_fun_def ext_iff) apply(simp add: rev_eqvt[symmetric]) apply(simp add: pt_rev_pi[OF pt_list_inst[OF pt_prod_inst[OF pt, OF pt]], OF at]) done @@ -2988,7 +2988,7 @@ and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "pi\([a].x) = [(pi\a)].(pi\x)" apply(simp add: abs_fun_def perm_fun_def abs_fun_if) - apply(simp only: expand_fun_eq) + apply(simp only: ext_iff) apply(rule allI) apply(subgoal_tac "(((rev pi)\(xa::'y)) = (a::'y)) = (xa = pi\a)")(*A*) apply(subgoal_tac "(((rev pi)\xa)\x) = (xa\(pi\x))")(*B*) @@ -3029,7 +3029,7 @@ and a :: "'x" shows "([a].x = [a].y) = (x = y)" apply(auto simp add: abs_fun_def) -apply(auto simp add: expand_fun_eq) +apply(auto simp add: ext_iff) apply(drule_tac x="a" in spec) apply(simp) done @@ -3045,7 +3045,7 @@ and a2: "[a].x = [b].y" shows "x=[(a,b)]\y \ a\y" proof - - from a2 have "\c::'x. ([a].x) c = ([b].y) c" by (force simp add: expand_fun_eq) + from a2 have "\c::'x. ([a].x) c = ([b].y) c" by (force simp add: ext_iff) hence "([a].x) a = ([b].y) a" by simp hence a3: "nSome(x) = ([b].y) a" by (simp add: abs_fun_def) show "x=[(a,b)]\y \ a\y" @@ -3076,7 +3076,7 @@ shows "[a].x =[b].y" proof - show ?thesis - proof (simp only: abs_fun_def expand_fun_eq, intro strip) + proof (simp only: abs_fun_def ext_iff, intro strip) fix c::"'x" let ?LHS = "if c=a then nSome(x) else if c\x then nSome([(a,c)]\x) else nNone" and ?RHS = "if c=b then nSome(y) else if c\y then nSome([(b,c)]\y) else nNone" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Predicate.thy Tue Sep 07 10:05:19 2010 +0200 @@ -72,7 +72,7 @@ by (simp add: mem_def) lemma pred_equals_eq2 [pred_set_conv]: "((\x y. (x, y) \ R) = (\x y. (x, y) \ S)) = (R = S)" - by (simp add: expand_fun_eq mem_def) + by (simp add: ext_iff mem_def) subsubsection {* Order relation *} @@ -99,10 +99,10 @@ by (simp add: bot_fun_eq bot_bool_eq) lemma bot_empty_eq: "bot = (\x. x \ {})" - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) lemma bot_empty_eq2: "bot = (\x y. (x, y) \ {})" - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) subsubsection {* Binary union *} @@ -197,10 +197,10 @@ by (auto simp add: SUP2_iff) lemma SUP_UN_eq: "(SUP i. (\x. x \ r i)) = (\x. x \ (UN i. r i))" - by (simp add: SUP1_iff expand_fun_eq) + by (simp add: SUP1_iff ext_iff) lemma SUP_UN_eq2: "(SUP i. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (UN i. r i))" - by (simp add: SUP2_iff expand_fun_eq) + by (simp add: SUP2_iff ext_iff) subsubsection {* Intersections of families *} @@ -230,10 +230,10 @@ by (auto simp add: INF2_iff) lemma INF_INT_eq: "(INF i. (\x. x \ r i)) = (\x. x \ (INT i. r i))" - by (simp add: INF1_iff expand_fun_eq) + by (simp add: INF1_iff ext_iff) lemma INF_INT_eq2: "(INF i. (\x y. (x, y) \ r i)) = (\x y. (x, y) \ (INT i. r i))" - by (simp add: INF2_iff expand_fun_eq) + by (simp add: INF2_iff ext_iff) subsection {* Predicates as relations *} @@ -251,7 +251,7 @@ lemma pred_comp_rel_comp_eq [pred_set_conv]: "((\x y. (x, y) \ r) OO (\x y. (x, y) \ s)) = (\x y. (x, y) \ r O s)" - by (auto simp add: expand_fun_eq elim: pred_compE) + by (auto simp add: ext_iff elim: pred_compE) subsubsection {* Converse *} @@ -276,7 +276,7 @@ lemma conversep_converse_eq [pred_set_conv]: "(\x y. (x, y) \ r)^--1 = (\x y. (x, y) \ r^-1)" - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) lemma conversep_conversep [simp]: "(r^--1)^--1 = r" by (iprover intro: order_antisym conversepI dest: conversepD) @@ -294,10 +294,10 @@ (iprover intro: conversepI ext dest: conversepD) lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~=" - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) lemma conversep_eq [simp]: "(op =)^--1 = op =" - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) subsubsection {* Domain *} @@ -347,7 +347,7 @@ "Powp A == \B. \x \ B. A x" lemma Powp_Pow_eq [pred_set_conv]: "Powp (\x. x \ A) = (\x. x \ Pow A)" - by (auto simp add: Powp_def expand_fun_eq) + by (auto simp add: Powp_def ext_iff) lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq] @@ -430,7 +430,7 @@ lemma bind_bind: "(P \= Q) \= R = P \= (\x. Q x \= R)" - by (auto simp add: bind_def expand_fun_eq) + by (auto simp add: bind_def ext_iff) lemma bind_single: "P \= single = P" @@ -442,14 +442,14 @@ lemma bottom_bind: "\ \= P = \" - by (auto simp add: bot_pred_def bind_def expand_fun_eq) + by (auto simp add: bot_pred_def bind_def ext_iff) lemma sup_bind: "(P \ Q) \= R = P \= R \ Q \= R" - by (auto simp add: bind_def sup_pred_def expand_fun_eq) + by (auto simp add: bind_def sup_pred_def ext_iff) lemma Sup_bind: "(\A \= f) = \((\x. x \= f) ` A)" - by (auto simp add: bind_def Sup_pred_def SUP1_iff expand_fun_eq) + by (auto simp add: bind_def Sup_pred_def SUP1_iff ext_iff) lemma pred_iffI: assumes "\x. eval A x \ eval B x" @@ -457,7 +457,7 @@ shows "A = B" proof - from assms have "\x. eval A x \ eval B x" by blast - then show ?thesis by (cases A, cases B) (simp add: expand_fun_eq) + then show ?thesis by (cases A, cases B) (simp add: ext_iff) qed lemma singleI: "eval (single x) x" @@ -492,7 +492,7 @@ lemma single_not_bot [simp]: "single x \ \" - by (auto simp add: single_def bot_pred_def expand_fun_eq) + by (auto simp add: single_def bot_pred_def ext_iff) lemma not_bot: assumes "A \ \" @@ -512,7 +512,7 @@ lemma not_is_empty_single: "\ is_empty (single x)" - by (auto simp add: is_empty_def single_def bot_pred_def expand_fun_eq) + by (auto simp add: is_empty_def single_def bot_pred_def ext_iff) lemma is_empty_sup: "is_empty (A \ B) \ is_empty A \ is_empty B" @@ -543,7 +543,7 @@ moreover from assm have "\x. eval A x \ singleton dfault A = x" by (rule singleton_eqI) ultimately have "eval (single (singleton dfault A)) = eval A" - by (simp (no_asm_use) add: single_def expand_fun_eq) blast + by (simp (no_asm_use) add: single_def ext_iff) blast then show ?thesis by (simp add: eval_inject) qed @@ -714,13 +714,13 @@ "member xq = eval (pred_of_seq xq)" proof (induct xq) case Empty show ?case - by (auto simp add: expand_fun_eq elim: botE) + by (auto simp add: ext_iff elim: botE) next case Insert show ?case - by (auto simp add: expand_fun_eq elim: supE singleE intro: supI1 supI2 singleI) + by (auto simp add: ext_iff elim: supE singleE intro: supI1 supI2 singleI) next case Join then show ?case - by (auto simp add: expand_fun_eq elim: supE intro: supI1 supI2) + by (auto simp add: ext_iff elim: supE intro: supI1 supI2) qed lemma eval_code [code]: "eval (Seq f) = member (f ())" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Sep 07 10:05:19 2010 +0200 @@ -79,10 +79,10 @@ declare Let_def[code_pred_inline] lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)" -by (auto simp add: insert_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) +by (auto simp add: insert_iff[unfolded mem_def] ext_iff intro!: eq_reflection) lemma [code_pred_inline]: "(op -) == (%A B x. A x \ \ B x)" -by (auto simp add: Diff_iff[unfolded mem_def] expand_fun_eq intro!: eq_reflection) +by (auto simp add: Diff_iff[unfolded mem_def] ext_iff intro!: eq_reflection) setup {* Code_Prolog.map_code_options (K {ensure_groundness = true, diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Tue Sep 07 10:05:19 2010 +0200 @@ -31,7 +31,7 @@ lemma [code_pred_inline]: "max = max_nat" -by (simp add: expand_fun_eq max_def max_nat_def) +by (simp add: ext_iff max_def max_nat_def) definition "max_of_my_Suc x = max x (Suc x)" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Probability/Borel.thy --- a/src/HOL/Probability/Borel.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Probability/Borel.thy Tue Sep 07 10:05:19 2010 +0200 @@ -1031,7 +1031,7 @@ have "f -` {\} \ space M = {x\space M. f x = \}" by auto with * have **: "{x\space M. f x = \} \ sets M" by simp have f: "f = (\x. if f x = \ then \ else Real (real (f x)))" - by (simp add: expand_fun_eq Real_real) + by (simp add: ext_iff Real_real) show "f \ borel_measurable M" apply (subst f) apply (rule measurable_If) @@ -1264,7 +1264,7 @@ proof - have *: "(\x. f x + g x) = (\x. if f x = \ then \ else if g x = \ then \ else Real (real (f x) + real (g x)))" - by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex) + by (auto simp: ext_iff pinfreal_noteq_omega_Ex) show ?thesis using assms unfolding * by (auto intro!: measurable_If) qed @@ -1276,7 +1276,7 @@ have *: "(\x. f x * g x) = (\x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \ then \ else if g x = \ then \ else Real (real (f x) * real (g x)))" - by (auto simp: expand_fun_eq pinfreal_noteq_omega_Ex) + by (auto simp: ext_iff pinfreal_noteq_omega_Ex) show ?thesis using assms unfolding * by (auto intro!: measurable_If) qed diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Probability/Euclidean_Lebesgue.thy --- a/src/HOL/Probability/Euclidean_Lebesgue.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Probability/Euclidean_Lebesgue.thy Tue Sep 07 10:05:19 2010 +0200 @@ -104,7 +104,7 @@ from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u] show ?ilim using mono lim i by auto have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal - unfolding expand_fun_eq SUPR_fun_expand mono_def by auto + unfolding ext_iff SUPR_fun_expand mono_def by auto moreover have "(SUP i. f i) \ borel_measurable M" using i by (rule borel_measurable_SUP) ultimately show "u \ borel_measurable M" by simp diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Probability/Information.thy Tue Sep 07 10:05:19 2010 +0200 @@ -505,7 +505,7 @@ by auto also have "\ = log b (\x\X`space M. if ?d x \ 0 then 1 else 0)" apply (rule arg_cong[where f="\f. log b (\x\X`space M. f x)"]) - using distribution_finite[of X] by (auto simp: expand_fun_eq real_of_pinfreal_eq_0) + using distribution_finite[of X] by (auto simp: ext_iff real_of_pinfreal_eq_0) finally show ?thesis using finite_space by (auto simp: setsum_cases real_eq_of_nat) qed @@ -645,7 +645,7 @@ let "?dZ A" = "real (distribution Z A)" let ?M = "X ` space M \ Y ` space M \ Z ` space M" - have split_beta: "\f. split f = (\x. f (fst x) (snd x))" by (simp add: expand_fun_eq) + have split_beta: "\f. split f = (\x. f (fst x) (snd x))" by (simp add: ext_iff) have "- (\(x, y, z) \ ?M. ?dXYZ {(x, y, z)} * log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z}))) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Probability/Lebesgue_Integration.thy --- a/src/HOL/Probability/Lebesgue_Integration.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Sep 07 10:05:19 2010 +0200 @@ -1106,7 +1106,7 @@ by (rule positive_integral_isoton) (auto intro!: borel_measurable_pinfreal_setsum assms positive_integral_mono arg_cong[where f=Sup] - simp: isoton_def le_fun_def psuminf_def expand_fun_eq SUPR_def Sup_fun_def) + simp: isoton_def le_fun_def psuminf_def ext_iff SUPR_def Sup_fun_def) thus ?thesis by (auto simp: isoton_def psuminf_def positive_integral_setsum[OF assms]) qed @@ -1365,7 +1365,7 @@ then have *: "(\x. g x * indicator A x) = g" "\x. g x * indicator A x = g x" "\x. g x \ f x" - by (auto simp: le_fun_def expand_fun_eq indicator_def split: split_if_asm) + by (auto simp: le_fun_def ext_iff indicator_def split: split_if_asm) from g show "\x. simple_function (\xa. x xa * indicator A xa) \ x \ f \ (\xa\A. \ \ x xa) \ simple_integral g = simple_integral (\xa. x xa * indicator A xa)" using `A \ sets M`[THEN sets_into_space] diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Probability/Positive_Infinite_Real.thy --- a/src/HOL/Probability/Positive_Infinite_Real.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Probability/Positive_Infinite_Real.thy Tue Sep 07 10:05:19 2010 +0200 @@ -1036,7 +1036,7 @@ qed from choice[OF this] obtain r where f: "f = (\i. Real (r i))" and pos: "\i. 0 \ r i" - by (auto simp: expand_fun_eq) + by (auto simp: ext_iff) hence [simp]: "\i. real (f i) = r i" by auto have "mono (\n. setsum r {.. (\i. f i = 0)" proof safe assume "\i. f i = 0" - hence "f = (\i. 0)" by (simp add: expand_fun_eq) + hence "f = (\i. 0)" by (simp add: ext_iff) thus "psuminf f = 0" using psuminf_const by simp next fix i assume "psuminf f = 0" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Probability/Probability_Space.thy --- a/src/HOL/Probability/Probability_Space.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Probability/Probability_Space.thy Tue Sep 07 10:05:19 2010 +0200 @@ -34,14 +34,14 @@ lemma (in prob_space) distribution_cong: assumes "\x. x \ space M \ X x = Y x" shows "distribution X = distribution Y" - unfolding distribution_def expand_fun_eq + unfolding distribution_def ext_iff using assms by (auto intro!: arg_cong[where f="\"]) lemma (in prob_space) joint_distribution_cong: assumes "\x. x \ space M \ X x = X' x" assumes "\x. x \ space M \ Y x = Y' x" shows "joint_distribution X Y = joint_distribution X' Y'" - unfolding distribution_def expand_fun_eq + unfolding distribution_def ext_iff using assms by (auto intro!: arg_cong[where f="\"]) lemma prob_space: "prob (space M) = 1" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Product_Type.thy Tue Sep 07 10:05:19 2010 +0200 @@ -151,7 +151,7 @@ next fix a c :: 'a and b d :: 'b have "Pair_Rep a b = Pair_Rep c d \ a = c \ b = d" - by (auto simp add: Pair_Rep_def expand_fun_eq) + by (auto simp add: Pair_Rep_def ext_iff) moreover have "Pair_Rep a b \ prod" and "Pair_Rep c d \ prod" by (auto simp add: prod_def) ultimately show "Pair a b = Pair c d \ a = c \ b = d" @@ -394,7 +394,7 @@ (Haskell "fst" and "snd") lemma prod_case_unfold [nitpick_def]: "prod_case = (%c p. c (fst p) (snd p))" - by (simp add: expand_fun_eq split: prod.split) + by (simp add: ext_iff split: prod.split) lemma fst_eqD: "fst (x, y) = a ==> x = a" by simp @@ -423,11 +423,11 @@ by (rule split_conv [THEN iffD1]) lemma split_Pair [simp]: "(\(x, y). (x, y)) = id" - by (simp add: expand_fun_eq split: prod.split) + by (simp add: ext_iff split: prod.split) lemma split_eta: "(\(x, y). f (x, y)) = f" -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *} - by (simp add: expand_fun_eq split: prod.split) + by (simp add: ext_iff split: prod.split) lemma split_comp: "split (f \ g) x = f (g (fst x)) (snd x)" by (cases x) simp @@ -797,25 +797,25 @@ "f \\ g = (\x. prod_case g (f x))" lemma scomp_unfold: "scomp = (\f g x. g (fst (f x)) (snd (f x)))" - by (simp add: expand_fun_eq scomp_def prod_case_unfold) + by (simp add: ext_iff scomp_def prod_case_unfold) lemma scomp_apply [simp]: "(f \\ g) x = prod_case g (f x)" by (simp add: scomp_unfold prod_case_unfold) lemma Pair_scomp: "Pair x \\ f = f x" - by (simp add: expand_fun_eq scomp_apply) + by (simp add: ext_iff scomp_apply) lemma scomp_Pair: "x \\ Pair = x" - by (simp add: expand_fun_eq scomp_apply) + by (simp add: ext_iff scomp_apply) lemma scomp_scomp: "(f \\ g) \\ h = f \\ (\x. g x \\ h)" - by (simp add: expand_fun_eq scomp_unfold) + by (simp add: ext_iff scomp_unfold) lemma scomp_fcomp: "(f \\ g) \> h = f \\ (\x. g x \> h)" - by (simp add: expand_fun_eq scomp_unfold fcomp_def) + by (simp add: ext_iff scomp_unfold fcomp_def) lemma fcomp_scomp: "(f \> g) \\ h = f \> (g \\ h)" - by (simp add: expand_fun_eq scomp_unfold fcomp_apply) + by (simp add: ext_iff scomp_unfold fcomp_apply) code_const scomp (Eval infixl 3 "#->") @@ -919,11 +919,11 @@ lemma apfst_id [simp] : "apfst id = id" - by (simp add: expand_fun_eq) + by (simp add: ext_iff) lemma apsnd_id [simp] : "apsnd id = id" - by (simp add: expand_fun_eq) + by (simp add: ext_iff) lemma apfst_eq_conv [simp]: "apfst f x = apfst g x \ f (fst x) = g (fst x)" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Quotient.thy Tue Sep 07 10:05:19 2010 +0200 @@ -34,7 +34,7 @@ lemma equivp_reflp_symp_transp: shows "equivp E = (reflp E \ symp E \ transp E)" - unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq + unfolding equivp_def reflp_def symp_def transp_def ext_iff by blast lemma equivp_reflp: @@ -97,7 +97,7 @@ lemma eq_comp_r: shows "((op =) OOO R) = R" - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) subsection {* Respects predicate *} @@ -130,11 +130,11 @@ lemma fun_map_id: shows "(id ---> id) = id" - by (simp add: expand_fun_eq id_def) + by (simp add: ext_iff id_def) lemma fun_rel_eq: shows "((op =) ===> (op =)) = (op =)" - by (simp add: expand_fun_eq) + by (simp add: ext_iff) subsection {* Quotient Predicate *} @@ -209,7 +209,7 @@ have "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" using q1 q2 unfolding Quotient_def - unfolding expand_fun_eq + unfolding ext_iff by simp moreover have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" @@ -219,7 +219,7 @@ moreover have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ (rep1 ---> abs2) r = (rep1 ---> abs2) s)" - unfolding expand_fun_eq + unfolding ext_iff apply(auto) using q1 q2 unfolding Quotient_def apply(metis) @@ -238,7 +238,7 @@ lemma abs_o_rep: assumes a: "Quotient R Abs Rep" shows "Abs o Rep = id" - unfolding expand_fun_eq + unfolding ext_iff by (simp add: Quotient_abs_rep[OF a]) lemma equals_rsp: @@ -253,7 +253,7 @@ assumes q1: "Quotient R1 Abs1 Rep1" and q2: "Quotient R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) = (\x. f x)" - unfolding expand_fun_eq + unfolding ext_iff using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by simp @@ -261,7 +261,7 @@ assumes q1: "Quotient R1 Abs1 Rep1" and q2: "Quotient R2 Abs2 Rep2" shows "(Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x) = (\x. f x)" - unfolding expand_fun_eq + unfolding ext_iff using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by simp @@ -445,7 +445,7 @@ is an equivalence this may be useful in regularising *) lemma babs_reg_eqv: shows "equivp R \ Babs (Respects R) P = P" - by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) + by (simp add: ext_iff Babs_def in_respects equivp_reflp) (* 3 lemmas needed for proving repabs_inj *) @@ -617,12 +617,12 @@ shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \ = op \" and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \ = op \" using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3] - unfolding o_def expand_fun_eq by simp_all + unfolding o_def ext_iff by simp_all lemma o_rsp: "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \ op \" "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \ op \" - unfolding fun_rel_def o_def expand_fun_eq by auto + unfolding fun_rel_def o_def ext_iff by auto lemma cond_prs: assumes a: "Quotient R absf repf" @@ -633,7 +633,7 @@ assumes q: "Quotient R Abs Rep" shows "(id ---> Rep ---> Rep ---> Abs) If = If" using Quotient_abs_rep[OF q] - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) lemma if_rsp: assumes q: "Quotient R Abs Rep" @@ -645,7 +645,7 @@ and q2: "Quotient R2 Abs2 Rep2" shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let" using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) lemma let_rsp: shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let" @@ -659,7 +659,7 @@ assumes a1: "Quotient R1 Abs1 Rep1" and a2: "Quotient R2 Abs2 Rep2" shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \ = op \" - by (simp add: expand_fun_eq mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2]) + by (simp add: ext_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2]) locale quot_type = fixes R :: "'a \ 'a \ bool" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Quotient_Examples/FSet.thy Tue Sep 07 10:05:19 2010 +0200 @@ -563,12 +563,12 @@ lemma [quot_preserve]: "(rep_fset ---> (map rep_fset \ rep_fset) ---> (abs_fset \ map abs_fset)) op # = finsert" - by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] + by (simp add: ext_iff Quotient_abs_rep[OF Quotient_fset] abs_o_rep[OF Quotient_fset] map_id finsert_def) lemma [quot_preserve]: "((map rep_fset \ rep_fset) ---> (map rep_fset \ rep_fset) ---> (abs_fset \ map abs_fset)) op @ = funion" - by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] + by (simp add: ext_iff Quotient_abs_rep[OF Quotient_fset] abs_o_rep[OF Quotient_fset] map_id sup_fset_def) lemma list_all2_app_l: @@ -771,7 +771,7 @@ lemma inj_map_eq_iff: "inj f \ (map f l \ map f m) = (l \ m)" - by (simp add: expand_set_eq[symmetric] inj_image_eq_iff) + by (simp add: set_ext_iff[symmetric] inj_image_eq_iff) text {* alternate formulation with a different decomposition principle and a proof of equivalence *} diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Quotient_Examples/Quotient_Int.thy --- a/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Sep 07 10:05:19 2010 +0200 @@ -14,7 +14,7 @@ "intrel (x, y) (u, v) = (x + v = u + y)" quotient_type int = "nat \ nat" / intrel - by (auto simp add: equivp_def expand_fun_eq) + by (auto simp add: equivp_def ext_iff) instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}" begin diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Random.thy --- a/src/HOL/Random.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Random.thy Tue Sep 07 10:05:19 2010 +0200 @@ -85,7 +85,7 @@ lemma pick_drop_zero: "pick (filter (\(k, _). k > 0) xs) = pick xs" - by (induct xs) (auto simp add: expand_fun_eq) + by (induct xs) (auto simp add: ext_iff) lemma pick_same: "l < length xs \ Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l" @@ -132,7 +132,7 @@ by (induct xs) simp_all ultimately show ?thesis by (auto simp add: select_weight_def select_def scomp_def split_def - expand_fun_eq pick_same [symmetric]) + ext_iff pick_same [symmetric]) qed diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Recdef.thy Tue Sep 07 10:05:19 2010 +0200 @@ -45,7 +45,7 @@ text{*cut*} lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))" -by (simp add: expand_fun_eq cut_def) +by (simp add: ext_iff cut_def) lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)" by (simp add: cut_def) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Set.thy --- a/src/HOL/Set.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Set.thy Tue Sep 07 10:05:19 2010 +0200 @@ -495,7 +495,7 @@ apply (rule Collect_mem_eq) done -lemma expand_set_eq [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))" +lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))" by(auto intro:set_ext) lemma subset_antisym [intro!]: "A \ B ==> B \ A ==> A = B" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/SetInterval.thy Tue Sep 07 10:05:19 2010 +0200 @@ -241,7 +241,7 @@ lemma atLeastatMost_psubset_iff: "{a..b} < {c..d} \ ((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d" -by(simp add: psubset_eq expand_set_eq less_le_not_le)(blast intro: order_trans) +by(simp add: psubset_eq set_ext_iff less_le_not_le)(blast intro: order_trans) lemma atLeastAtMost_singleton_iff[simp]: "{a .. b} = {c} \ a = b \ b = c" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/String.thy --- a/src/HOL/String.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/String.thy Tue Sep 07 10:05:19 2010 +0200 @@ -60,12 +60,12 @@ lemma char_case_nibble_pair [code, code_unfold]: "char_case f = split f o nibble_pair_of_char" - by (simp add: expand_fun_eq split: char.split) + by (simp add: ext_iff split: char.split) lemma char_rec_nibble_pair [code, code_unfold]: "char_rec f = split f o nibble_pair_of_char" unfolding char_case_nibble_pair [symmetric] - by (simp add: expand_fun_eq split: char.split) + by (simp add: ext_iff split: char.split) syntax "_Char" :: "xstr => char" ("CHR _") diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Sum_Type.thy Tue Sep 07 10:05:19 2010 +0200 @@ -32,17 +32,17 @@ lemma Inl_Rep_inject: "inj_on Inl_Rep A" proof (rule inj_onI) show "\a c. Inl_Rep a = Inl_Rep c \ a = c" - by (auto simp add: Inl_Rep_def expand_fun_eq) + by (auto simp add: Inl_Rep_def ext_iff) qed lemma Inr_Rep_inject: "inj_on Inr_Rep A" proof (rule inj_onI) show "\b d. Inr_Rep b = Inr_Rep d \ b = d" - by (auto simp add: Inr_Rep_def expand_fun_eq) + by (auto simp add: Inr_Rep_def ext_iff) qed lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \ Inr_Rep b" - by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq) + by (auto simp add: Inl_Rep_def Inr_Rep_def ext_iff) definition Inl :: "'a \ 'a + 'b" where "Inl = Abs_sum \ Inl_Rep" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Tue Sep 07 10:05:19 2010 +0200 @@ -483,7 +483,7 @@ [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1, REPEAT (rtac TrueI 1), rewrite_goals_tac (mk_meta_eq @{thm choice_eq} :: - Thm.symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs), + Thm.symmetric (mk_meta_eq @{thm ext_iff}) :: range_eqs), rewrite_goals_tac (map Thm.symmetric range_eqs), REPEAT (EVERY [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @ diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Tools/Sledgehammer/clausifier.ML --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Sep 07 10:05:19 2010 +0200 @@ -78,7 +78,7 @@ (**** REPLACING ABSTRACTIONS BY COMBINATORS ****) -val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]} +val fun_cong_all = @{thm ext_iff [THEN iffD1]} (* Removes the lambdas from an equation of the form "t = (%x. u)". (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Transitive_Closure.thy Tue Sep 07 10:05:19 2010 +0200 @@ -82,7 +82,7 @@ subsection {* Reflexive-transitive closure *} lemma reflcl_set_eq [pred_set_conv]: "(sup (\x y. (x, y) \ r) op =) = (\x y. (x, y) \ r \ Id)" - by (auto simp add: expand_fun_eq) + by (auto simp add: ext_iff) lemma r_into_rtrancl [intro]: "!!p. p \ r ==> p \ r^*" -- {* @{text rtrancl} of @{text r} contains @{text r} *} @@ -487,7 +487,7 @@ lemmas trancl_converseD = tranclp_converseD [to_set] lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1" - by (fastsimp simp add: expand_fun_eq + by (fastsimp simp add: ext_iff intro!: tranclp_converseI dest!: tranclp_converseD) lemmas trancl_converse = tranclp_converse [to_set] diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/UNITY/Comp/Alloc.thy Tue Sep 07 10:05:19 2010 +0200 @@ -358,7 +358,7 @@ done lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc" - apply (simp add: surj_iff expand_fun_eq o_apply) + apply (simp add: surj_iff ext_iff o_apply) apply record_auto done @@ -386,7 +386,7 @@ done lemma surj_sysOfClient [iff]: "surj sysOfClient" - apply (simp add: surj_iff expand_fun_eq o_apply) + apply (simp add: surj_iff ext_iff o_apply) apply record_auto done @@ -410,7 +410,7 @@ done lemma surj_client_map [iff]: "surj client_map" - apply (simp add: surj_iff expand_fun_eq o_apply) + apply (simp add: surj_iff ext_iff o_apply) apply record_auto done diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/UNITY/Lift_prog.thy --- a/src/HOL/UNITY/Lift_prog.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/UNITY/Lift_prog.thy Tue Sep 07 10:05:19 2010 +0200 @@ -337,10 +337,10 @@ (*Lets us prove one version of a theorem and store others*) lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h" -by (simp add: expand_fun_eq o_def) +by (simp add: ext_iff o_def) lemma o_equiv_apply: "f o g = h ==> \x. f(g x) = h x" -by (simp add: expand_fun_eq o_def) +by (simp add: ext_iff o_def) lemma fst_o_lift_map: "sub i o fst o lift_map i = fst" apply (rule ext) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/Word/Word.thy Tue Sep 07 10:05:19 2010 +0200 @@ -4695,7 +4695,7 @@ apply simp apply (rule_tac t="\a. x (1 + (n - m + a))" and s="\a. x (1 + (n - m) + a)" in subst) - apply (clarsimp simp add: expand_fun_eq) + apply (clarsimp simp add: ext_iff) apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst) apply simp apply (rule refl) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/ZF/HOLZF.thy --- a/src/HOL/ZF/HOLZF.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/ZF/HOLZF.thy Tue Sep 07 10:05:19 2010 +0200 @@ -155,7 +155,7 @@ by (auto simp add: explode_def) lemma explode_CartProd_eq: "explode (CartProd a b) = (% (x,y). Opair x y) ` ((explode a) \ (explode b))" - by (simp add: explode_def expand_set_eq CartProd image_def) + by (simp add: explode_def set_ext_iff CartProd image_def) lemma explode_Repl_eq: "explode (Repl A f) = image f (explode A)" by (simp add: explode_def Repl image_def) diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/ex/Execute_Choice.thy --- a/src/HOL/ex/Execute_Choice.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/ex/Execute_Choice.thy Tue Sep 07 10:05:19 2010 +0200 @@ -26,7 +26,7 @@ case True then show ?thesis by (simp add: is_empty_def keys_def valuesum_def) next case False - then have l: "\l. l \ dom (Mapping.lookup m)" by (auto simp add: is_empty_def expand_fun_eq mem_def keys_def) + then have l: "\l. l \ dom (Mapping.lookup m)" by (auto simp add: is_empty_def ext_iff mem_def keys_def) then have "(let l = SOME l. l \ dom (Mapping.lookup m) in the (Mapping.lookup m l) + (\k \ dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) = (\k \ dom (Mapping.lookup m). the (Mapping.lookup m k))" diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/ex/Landau.thy --- a/src/HOL/ex/Landau.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/ex/Landau.thy Tue Sep 07 10:05:19 2010 +0200 @@ -189,7 +189,7 @@ qed (simp_all add: less_fun_def less_eq_fun_refl, auto intro: less_eq_fun_trans) show "class.preorder_equiv less_eq_fun less_fun" using preorder_equiv_axioms . show "preorder_equiv.equiv less_eq_fun = equiv_fun" - by (simp add: expand_fun_eq equiv_def equiv_fun_less_eq_fun) + by (simp add: ext_iff equiv_def equiv_fun_less_eq_fun) qed diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/ex/Summation.thy --- a/src/HOL/ex/Summation.thy Mon Sep 06 22:58:06 2010 +0200 +++ b/src/HOL/ex/Summation.thy Tue Sep 07 10:05:19 2010 +0200 @@ -24,7 +24,7 @@ lemma \_shift: "\ (\k. l + f k) = \ f" - by (simp add: \_def expand_fun_eq) + by (simp add: \_def ext_iff) lemma \_same_shift: assumes "\ f = \ g" @@ -100,7 +100,7 @@ proof - from \_\ have "\ (\ (\ f) j) = \ f" . then obtain k where "plus k \ \ (\ f) j = f" by (blast dest: \_same_shift) - then have "\q. f q = k + \ (\ f) j q" by (simp add: expand_fun_eq) + then have "\q. f q = k + \ (\ f) j q" by (simp add: ext_iff) then show ?thesis by simp qed