# HG changeset patch # User nipkow # Date 1284369195 -7200 # Node ID d7728f65b353a6cd277dcd6501adf89bea9d0518 # Parent e1bd8a54c40fd07cdade100f6fca1020be052dfc renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI diff -r e1bd8a54c40f -r d7728f65b353 NEWS --- a/NEWS Mon Sep 13 08:43:48 2010 +0200 +++ b/NEWS Mon Sep 13 11:13:15 2010 +0200 @@ -73,7 +73,10 @@ * String.literal is a type, but not a datatype. INCOMPATIBILITY. -* Renamed lemmas: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff +* Renamed lemmas: + expand_fun_eq -> fun_eq_iff + expand_set_eq -> set_eq_iff + set_ext -> set_eqI * Renamed class eq and constant eq (for code generation) to class equal and constant equal, plus renaming of related facts and various tuning. diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Mon Sep 13 11:13:15 2010 +0200 @@ -2193,7 +2193,7 @@ from csmset msubset have "fmset G bs = fmset G as + fmset G cs" - by (simp add: multiset_ext_iff mset_le_def) + by (simp add: multiset_eq_iff mset_le_def) hence basc: "b \ a \ c" by (rule fmset_wfactors_mult) fact+ diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Bali/Example.thy Mon Sep 13 11:13:15 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 ext_iff Let_def +apply (auto simp add: accfield_def fun_eq_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 ext_iff Let_def +apply (auto simp add: accfield_def fun_eq_iff Let_def accessible_in_RefT_simp is_public_def BaseCl_def diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Bali/Table.thy --- a/src/HOL/Bali/Table.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Bali/Table.thy Mon Sep 13 11:13:15 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 ext_iff) +by (simp add: cond_override_def fun_eq_iff) lemma cond_override_empty2[simp]: "cond_override c t empty = t" -by (simp add: cond_override_def ext_iff) +by (simp add: cond_override_def fun_eq_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: ext_iff filter_tab_def) +by (simp add: fun_eq_iff filter_tab_def) lemma filter_tab_False[simp]: "filter_tab (\x y. False) t = empty" -by (simp add: ext_iff filter_tab_def empty_def) +by (simp add: fun_eq_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 ext_iff) +apply (auto simp add: filter_tab_def fun_eq_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 ext_iff) +by (auto simp add: filter_tab_def fun_eq_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 ext_iff) +by (auto simp add: filter_tab_def fun_eq_iff) lemma filter_tab_None: "t k = None \ filter_tab p t k = None" -apply (simp add: filter_tab_def ext_iff) +apply (simp add: filter_tab_def fun_eq_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: ext_iff filter_tab_def) +by (auto simp add: fun_eq_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: ext_iff cond_override_def filter_tab_def ) +by (auto simp add: fun_eq_iff cond_override_def filter_tab_def ) section {* Misc. *} diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Big_Operators.thy Mon Sep 13 11:13:15 2010 +0200 @@ -1504,11 +1504,11 @@ lemma dual_max: "ord.max (op \) = min" - by (auto simp add: ord.max_def_raw min_def ext_iff) + by (auto simp add: ord.max_def_raw min_def fun_eq_iff) lemma dual_min: "ord.min (op \) = max" - by (auto simp add: ord.min_def_raw max_def ext_iff) + by (auto simp add: ord.min_def_raw max_def fun_eq_iff) lemma strict_below_fold1_iff: assumes "finite A" and "A \ {}" diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Complete_Lattice.thy Mon Sep 13 11:13:15 2010 +0200 @@ -272,7 +272,7 @@ lemma Union_eq: "\A = {x. \B \ A. x \ B}" -proof (rule set_ext) +proof (rule set_eqI) fix x have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)" by auto @@ -508,7 +508,7 @@ lemma Inter_eq: "\A = {x. \B \ A. x \ B}" -proof (rule set_ext) +proof (rule set_eqI) fix x have "(\Q\{P. \B\A. P \ x \ B}. Q) \ (\B\A. x \ B)" by auto diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Datatype.thy Mon Sep 13 11:13:15 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 ext_iff) +apply (simp add: Push_def fun_eq_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 ext_iff) +apply (auto simp add: Push_def fun_eq_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 ext_iff split: nat.split_asm) +by (auto simp add: Push_def fun_eq_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: ext_iff) +apply (simp add: fun_eq_iff) done diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Decision_Procs/Polynomial_List.thy --- a/src/HOL/Decision_Procs/Polynomial_List.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy Mon Sep 13 11:13:15 2010 +0200 @@ -334,7 +334,7 @@ lemma UNIV_nat_infinite: "\ finite (UNIV :: nat set)" unfolding finite_conv_nat_seg_image -proof(auto simp add: set_ext_iff image_iff) +proof(auto simp add: set_eq_iff image_iff) fix n::nat and f:: "nat \ nat" let ?N = "{i. i < n}" let ?fN = "f ` ?N" diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Finite_Set.thy Mon Sep 13 11:13:15 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: set_ext_iff ext_iff) + by (rule inj_onI, auto simp add: set_eq_iff fun_eq_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 ext_iff) +by (simp add: fun_left_comm fun_eq_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 ext_iff) +by (simp add: fun_left_idem fun_eq_iff) lemma fold_insert_idem: assumes fin: "finite A" @@ -1363,17 +1363,17 @@ lemma empty [simp]: "F {} = id" - by (simp add: eq_fold ext_iff) + by (simp add: eq_fold fun_eq_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: ext_iff) + qed (insert commute_comp, simp add: fun_eq_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 ext_iff) + with `finite A` show ?thesis by (simp add: eq_fold fun_eq_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: ext_iff ac_simps) - thm fold.commute_comp' [of B b, simplified ext_iff, simplified] + qed (simp_all add: fun_eq_iff ac_simps) + thm fold.commute_comp' [of B b, simplified fun_eq_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: ext_iff commute) + then have A: "x * fold op * b B = fold op * (b * x) B" by (simp add: fun_eq_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: ext_iff) + then have B: "fold op * x (insert b B) = fold op * (b * x) B" by (simp add: fun_eq_iff) from A B assms * show ?thesis by (simp add: eq_fold' del: fold.insert) qed diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Fun.thy Mon Sep 13 11:13:15 2010 +0200 @@ -11,15 +11,13 @@ text{*As a simplification rule, it replaces all function equalities by first-order equalities.*} -lemma ext_iff: "f = g \ (\x. f x = g x)" +lemma fun_eq_iff: "f = g \ (\x. f x = g x)" apply (rule iffI) apply (simp (no_asm_simp)) apply (rule ext) apply (simp (no_asm_simp)) done -lemmas expand_fun_eq = ext_iff - lemma apply_inverse: "f x = u \ (\x. P x \ g (f x) = x) \ P x \ x = g u" by auto @@ -165,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 ext_iff) + by (simp add: inj_on_def fun_eq_iff) lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)" by (simp add: inj_on_eq_iff) @@ -465,7 +463,7 @@ by simp lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)" -by (simp add: ext_iff) +by (simp add: fun_eq_iff) lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)" by (rule ext, auto) @@ -517,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: ext_iff swap_def) + using assms by (simp add: fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Hilbert_Choice.thy Mon Sep 13 11:13:15 2010 +0200 @@ -138,7 +138,7 @@ qed lemma inj_iff: "(inj f) = (inv f o f = id)" -apply (simp add: o_def ext_iff) +apply (simp add: o_def fun_eq_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 ext_iff) +apply (simp add: o_def fun_eq_iff) apply (blast intro: surjI surj_f_inv_f) done diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Hoare/SchorrWaite.thy --- a/src/HOL/Hoare/SchorrWaite.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Hoare/SchorrWaite.thy Mon Sep 13 11:13:15 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 ext_iff intro:RisMarked) + from i5 i6 show "(\x.(x \ R) = m x) \ r = iR \ l = iL" by(auto simp: stackEmpty fun_eq_iff intro:RisMarked) next fix c m l r t p q root diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/IMP/Live.thy --- a/src/HOL/IMP/Live.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/IMP/Live.thy Mon Sep 13 11:13:15 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: ext_iff[symmetric]) +by(rule_tac x="%x. UNIV" in exI)(simp add: fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Imperative_HOL/Array.thy Mon Sep 13 11:13:15 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 ext_iff noteq_def set_def) + by (simp add: Let_def fun_eq_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 ext_iff) + by (simp add: update_def length_def set_def get_def fun_eq_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 ext_iff) + by (simp add: update_def present_def set_def get_def fun_eq_iff) lemma present_alloc [simp]: "present (snd (alloc xs h)) (fst (alloc xs h))" diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Sep 13 11:13:15 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: ext_iff) + by (cases f, cases g) (auto simp: fun_eq_iff) ML {* structure Execute_Simps = Named_Thms( val name = "execute_simps" diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Imperative_HOL/Ref.thy --- a/src/HOL/Imperative_HOL/Ref.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Imperative_HOL/Ref.thy Mon Sep 13 11:13:15 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 ext_iff) + by (simp add: noteq_def set_def fun_eq_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 ext_iff) + by (simp add: present_def fun_eq_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 ext_iff) + by (simp add: Array.get_def set_def fun_eq_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 ext_iff) + by (simp add: Array.get_def alloc_def set_def Let_def fun_eq_iff) lemma present_update [simp]: "present (Array.update a i v h) = present h" - by (simp add: Array.update_def Array.set_def ext_iff present_def) + by (simp add: Array.update_def Array.set_def fun_eq_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 ext_iff) + by (simp add: Array.present_def set_def fun_eq_iff) lemma array_present_alloc [simp]: "Array.present h a \ Array.present (snd (alloc v h)) a" diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Sep 13 11:13:15 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: ext_iff intro: arg_cong2[where f = bind] split: node.split) + by (auto simp add: fun_eq_iff intro: arg_cong2[where f = bind] split: node.split) primrec rev :: "('a:: heap) node \ 'a node Heap" where diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Import/HOL/bool.imp --- a/src/HOL/Import/HOL/bool.imp Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Import/HOL/bool.imp Mon Sep 13 11:13:15 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.ext_iff" + "FUN_EQ_THM" > "Fun.fun_eq_iff" "FORALL_THM" > "HOL4Base.bool.FORALL_THM" "FORALL_SIMP" > "HOL.simp_thms_35" "FORALL_DEF" > "HOL.All_def" diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Import/HOL/prob_extra.imp --- a/src/HOL/Import/HOL/prob_extra.imp Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Import/HOL/prob_extra.imp Mon Sep 13 11:13:15 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.ext_iff" + "EQ_EXT_EQ" > "Fun.fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Import/HOLLight/hollight.imp --- a/src/HOL/Import/HOLLight/hollight.imp Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Import/HOLLight/hollight.imp Mon Sep 13 11:13:15 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.ext_iff" + "FUN_EQ_THM" > "Fun.fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Library/AssocList.thy --- a/src/HOL/Library/AssocList.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/AssocList.thy Mon Sep 13 11:13:15 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: ext_iff) + by (induct al) (auto simp add: fun_eq_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' ext_iff) + by (simp add: update_conv' fun_eq_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: ext_iff update_conv') - then show ?thesis by (auto simp add: updates_def ext_iff map_upds_fold_map_upd foldl_fold split_def) + by (rule fold_apply) (auto simp add: fun_eq_iff update_conv') + then show ?thesis by (auto simp add: updates_def fun_eq_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 ext_iff) + ultimately show ?thesis by (simp add: updates_def fun_eq_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: ext_iff) + by (induct al) (auto simp add: fun_eq_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: ext_iff) + (simp_all add: fun_eq_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 ext_iff) + then show ?thesis by (simp add: updates_def fun_eq_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 ext_iff) + by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def fun_eq_iff) then show ?thesis - by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev ext_iff) + by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev fun_eq_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: ext_iff field_simps) + using n0 by (auto simp add: fun_eq_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: ext_iff) + by (auto simp add: fun_eq_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: ext_iff h of_nat_diff)} + by (auto simp add: fun_eq_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 set_ext_iff) + apply (simp_all add: inj_on_def image_iff Bex_def set_eq_iff) apply clarsimp apply (presburger) apply presburger - by (simp add: ext_iff field_simps of_nat_add[symmetric] del: of_nat_add) + by (simp add: fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Code_Char_chr.thy --- a/src/HOL/Library/Code_Char_chr.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Code_Char_chr.thy Mon Sep 13 11:13:15 2010 +0200 @@ -13,14 +13,14 @@ lemma [code]: "nat_of_char = nat o int_of_char" - unfolding int_of_char_def by (simp add: ext_iff) + unfolding int_of_char_def by (simp add: fun_eq_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: ext_iff) + unfolding char_of_int_def by (simp add: fun_eq_iff) code_const int_of_char and char_of_int (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Countable.thy Mon Sep 13 11:13:15 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 ext_iff) + by (rule injI, simp add: xs fun_eq_iff) qed qed diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Mon Sep 13 11:13:15 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: ext_iff dest!: gr0_implies_Suc) + by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc) subsection {* Preprocessors *} diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Enum.thy Mon Sep 13 11:13:15 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 ext_iff) +qed (simp_all add: equal_fun_def enum_all fun_eq_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 ext_iff le_fun_def order_less_le) + by (simp_all add: list_all_iff list_ex_iff enum_all fun_eq_iff le_fun_def order_less_le) subsection {* Quantifiers *} @@ -82,7 +82,7 @@ by (induct n arbitrary: ys) auto lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \ set ys \ set xs}" -proof (rule set_ext) +proof (rule set_eqI) fix ys :: "'a list" show "ys \ set (n_lists n xs) \ ys \ {ys. length ys = n \ set ys \ set xs}" proof - @@ -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 ext_iff) + by (auto simp add: map_of_zip_map fun_eq_iff) then show "f \ set enum" by (auto simp add: enum_fun_def set_n_lists) qed diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Mon Sep 13 11:13:15 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] ext_iff) + by (simp add: fps_nth_inject [symmetric] fun_eq_iff) lemma fps_ext: "(\n. p $ n = q $ n) \ p = q" by (simp add: expand_fps_eq) @@ -791,14 +791,14 @@ apply (rule setsum_reindex_cong[where f="\i. n + 1 - i"]) apply (simp add: inj_on_def Ball_def) apply presburger - apply (rule set_ext) + apply (rule set_eqI) apply (presburger add: image_iff) by simp have s1: "setsum (\i. f $ i * g $ (n + 1 - i)) ?Zn1 = setsum (\i. f $ (n + 1 - i) * g $ i) ?Zn1" apply (rule setsum_reindex_cong[where f="\i. n + 1 - i"]) apply (simp add: inj_on_def Ball_def) apply presburger - apply (rule set_ext) + apply (rule set_eqI) apply (presburger add: image_iff) by simp have "(f * ?D g + ?D f * g)$n = (?D g * f + ?D f * g)$n" by (simp only: mult_commute) @@ -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: set_ext_iff) + by (auto simp: set_eq_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: set_ext_iff) by presburger + have u0: "{0 .. k} \ {m} = {0..m}" using k apply (simp add: set_eq_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: set_ext_iff) + apply (clarsimp simp add: set_eq_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: ext_iff fps_eq_iff fps_inv_def fps_ginv_def) + apply (auto simp add: fun_eq_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: set_ext_iff image_iff) + apply (auto simp add: set_eq_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: set_ext_iff) + apply (simp add: set_eq_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 ext_iff fps_eq_iff algebra_simps) + by (auto simp add: XDp_def fun_eq_iff fps_eq_iff algebra_simps) lemma XDp0[simp]: "XDp 0 = XD" - by (simp add: ext_iff fps_eq_iff) + by (simp add: fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Library/FrechetDeriv.thy --- a/src/HOL/Library/FrechetDeriv.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/FrechetDeriv.thy Mon Sep 13 11:13:15 2010 +0200 @@ -177,7 +177,7 @@ hence "(\h. F h - F' h) = (\h. 0)" by (rule FDERIV_zero_unique) thus "F = F'" - unfolding ext_iff right_minus_eq . + unfolding fun_eq_iff right_minus_eq . qed subsection {* Continuity *} diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Fset.thy Mon Sep 13 11:13:15 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: ext_iff member_def fun_Compl_def bool_Compl_def) + by (simp_all add: fun_eq_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: ext_iff) + by (simp add: fun_eq_iff) have "member \ fold (\x. Fset \ More_Set.remove x \ member) xs = fold More_Set.remove xs \ member" - by (rule fold_apply) (simp add: ext_iff) + by (rule fold_apply) (simp add: fun_eq_iff) then have "fold More_Set.remove xs (member A) = member (fold (\x. Fset \ More_Set.remove x \ member) xs A)" - by (simp add: ext_iff) + by (simp add: fun_eq_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: ext_iff) + by (simp add: fun_eq_iff) have "member \ fold (\x. Fset \ Set.insert x \ member) xs = fold Set.insert xs \ member" - by (rule fold_apply) (simp add: ext_iff) + by (rule fold_apply) (simp add: fun_eq_iff) then have "fold Set.insert xs (member A) = member (fold (\x. Fset \ Set.insert x \ member) xs A)" - by (simp add: ext_iff) + by (simp add: fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/FuncSet.thy Mon Sep 13 11:13:15 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: ext_iff Pi_def compose_def restrict_def) +by (simp add: fun_eq_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: ext_iff Pi_def restrict_def) + by (simp add: fun_eq_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: ext_iff compose_def extensional_def Pi_def) + by (auto simp add: fun_eq_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: ext_iff compose_def extensional_def Pi_def) + by (auto simp add: fun_eq_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: ext_iff extensional_def) +by (force simp add: fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Function_Algebras.thy --- a/src/HOL/Library/Function_Algebras.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Function_Algebras.thy Mon Sep 13 11:13:15 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 ext_iff) +qed (simp_all add: plus_fun_def fun_eq_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 ext_iff) +qed (simp add: zero_fun_def one_fun_def fun_eq_iff) text {* Ring structures *} diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Inner_Product.thy --- a/src/HOL/Library/Inner_Product.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Inner_Product.thy Mon Sep 13 11:13:15 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: ext_iff inner_commute) + by (simp add: fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Mapping.thy Mon Sep 13 11:13:15 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 ext_iff) + by (cases "lookup m k") (simp_all add: map_entry_def fun_eq_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 ext_iff) + by (induct ks) (auto simp add: tabulate_def restrict_map_def fun_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Library/More_List.thy --- a/src/HOL/Library/More_List.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/More_List.thy Mon Sep 13 11:13:15 2010 +0200 @@ -30,7 +30,7 @@ lemma foldr_fold_rev: "foldr f xs = fold f (rev xs)" - by (simp add: foldr_foldl foldl_fold ext_iff) + by (simp add: foldr_foldl foldl_fold fun_eq_iff) lemma fold_rev_conv [code_unfold]: "fold f (rev xs) = foldr f xs" @@ -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: ext_iff) + using assms by (induct xs) (simp_all add: fun_eq_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 ext_iff del: set.simps) + by (simp add: Inf_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) lemma (in lattice) Sup_fin_set_fold: "Sup_fin (set (x # xs)) = fold sup xs x" @@ -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 ext_iff del: set.simps) + by (simp add: Sup_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) lemma (in linorder) Min_fin_set_fold: "Min (set (x # xs)) = fold min xs x" @@ -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 ext_iff del: set.simps) + by (simp add: Min_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) lemma (in linorder) Max_fin_set_fold: "Max (set (x # xs)) = fold max xs x" @@ -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 ext_iff del: set.simps) + by (simp add: Max_fin_set_fold ac_simps foldr_fold fun_eq_iff del: set.simps) lemma (in complete_lattice) Inf_set_fold: "Inf (set xs) = fold inf xs top" @@ -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 ext_iff) + by (simp add: Inf_set_fold ac_simps foldr_fold fun_eq_iff) lemma (in complete_lattice) Sup_set_fold: "Sup (set xs) = fold sup xs bot" @@ -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 ext_iff) + by (simp add: Sup_set_fold ac_simps foldr_fold fun_eq_iff) lemma (in complete_lattice) INFI_set_fold: "INFI (set xs) f = fold (inf \ f) xs top" diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/More_Set.thy --- a/src/HOL/Library/More_Set.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/More_Set.thy Mon Sep 13 11:13:15 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: ext_iff remove_def) + have rem: "remove = (\x A. A - {x})" by (simp add: fun_eq_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: ext_iff remove_def) + have rem: "remove = (\x A. A - {x})" by (simp add: fun_eq_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 ext_iff) + by (simp add: fun_Compl_def bool_Compl_def comp_def fun_eq_iff) end diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Mon Sep 13 11:13:15 2010 +0200 @@ -24,13 +24,13 @@ notation (xsymbols) Melem (infix "\#" 50) -lemma multiset_ext_iff: +lemma multiset_eq_iff: "M = N \ (\a. count M a = count N a)" - by (simp only: count_inject [symmetric] ext_iff) + by (simp only: count_inject [symmetric] fun_eq_iff) -lemma multiset_ext: +lemma multiset_eqI: "(\x. count A x = count B x) \ A = B" - using multiset_ext_iff by auto + using multiset_eq_iff by auto text {* \medskip Preservation of the representing set @{term multiset}. @@ -127,7 +127,7 @@ by (simp add: union_def in_multiset multiset_typedef) instance multiset :: (type) cancel_comm_monoid_add proof -qed (simp_all add: multiset_ext_iff) +qed (simp_all add: multiset_eq_iff) subsubsection {* Difference *} @@ -146,62 +146,62 @@ by (simp add: diff_def in_multiset multiset_typedef) lemma diff_empty [simp]: "M - {#} = M \ {#} - M = {#}" -by(simp add: multiset_ext_iff) +by(simp add: multiset_eq_iff) lemma diff_cancel[simp]: "A - A = {#}" -by (rule multiset_ext) simp +by (rule multiset_eqI) simp lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)" -by(simp add: multiset_ext_iff) +by(simp add: multiset_eq_iff) lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)" -by(simp add: multiset_ext_iff) +by(simp add: multiset_eq_iff) lemma insert_DiffM: "x \# M \ {#x#} + (M - {#x#}) = M" - by (clarsimp simp: multiset_ext_iff) + by (clarsimp simp: multiset_eq_iff) lemma insert_DiffM2 [simp]: "x \# M \ M - {#x#} + {#x#} = M" - by (clarsimp simp: multiset_ext_iff) + by (clarsimp simp: multiset_eq_iff) lemma diff_right_commute: "(M::'a multiset) - N - Q = M - Q - N" - by (auto simp add: multiset_ext_iff) + by (auto simp add: multiset_eq_iff) lemma diff_add: "(M::'a multiset) - (N + Q) = M - N - Q" -by (simp add: multiset_ext_iff) +by (simp add: multiset_eq_iff) lemma diff_union_swap: "a \ b \ M - {#a#} + {#b#} = M + {#b#} - {#a#}" - by (auto simp add: multiset_ext_iff) + by (auto simp add: multiset_eq_iff) lemma diff_union_single_conv: "a \# J \ I + J - {#a#} = I + (J - {#a#})" - by (simp add: multiset_ext_iff) + by (simp add: multiset_eq_iff) subsubsection {* Equality of multisets *} lemma single_not_empty [simp]: "{#a#} \ {#} \ {#} \ {#a#}" - by (simp add: multiset_ext_iff) + by (simp add: multiset_eq_iff) lemma single_eq_single [simp]: "{#a#} = {#b#} \ a = b" - by (auto simp add: multiset_ext_iff) + by (auto simp add: multiset_eq_iff) lemma union_eq_empty [iff]: "M + N = {#} \ M = {#} \ N = {#}" - by (auto simp add: multiset_ext_iff) + by (auto simp add: multiset_eq_iff) lemma empty_eq_union [iff]: "{#} = M + N \ M = {#} \ N = {#}" - by (auto simp add: multiset_ext_iff) + by (auto simp add: multiset_eq_iff) lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \ False" - by (auto simp add: multiset_ext_iff) + by (auto simp add: multiset_eq_iff) lemma diff_single_trivial: "\ x \# M \ M - {#x#} = M" - by (auto simp add: multiset_ext_iff) + by (auto simp add: multiset_eq_iff) lemma diff_single_eq_union: "x \# M \ M - {#x#} = N \ M = N + {#x#}" @@ -220,7 +220,7 @@ assume ?rhs then show ?lhs by auto next assume ?lhs thus ?rhs - by(simp add: multiset_ext_iff split:if_splits) (metis add_is_1) + by(simp add: multiset_eq_iff split:if_splits) (metis add_is_1) qed lemma single_is_union: @@ -229,7 +229,7 @@ lemma add_eq_conv_diff: "M + {#a#} = N + {#b#} \ M = N \ a = b \ M = N - {#a#} + {#b#} \ N = M - {#b#} + {#a#}" (is "?lhs = ?rhs") -(* shorter: by (simp add: multiset_ext_iff) fastsimp *) +(* shorter: by (simp add: multiset_eq_iff) fastsimp *) proof assume ?rhs then show ?lhs by (auto simp add: add_assoc add_commute [of "{#b#}"]) @@ -278,7 +278,7 @@ mset_less_def: "(A::'a multiset) < B \ A \ B \ A \ B" instance proof -qed (auto simp add: mset_le_def mset_less_def multiset_ext_iff intro: order_trans antisym) +qed (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym) end @@ -289,7 +289,7 @@ lemma mset_le_exists_conv: "(A::'a multiset) \ B \ (\C. B = A + C)" apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI) -apply (auto intro: multiset_ext_iff [THEN iffD2]) +apply (auto intro: multiset_eq_iff [THEN iffD2]) done lemma mset_le_mono_add_right_cancel [simp]: @@ -318,11 +318,11 @@ lemma multiset_diff_union_assoc: "C \ B \ (A::'a multiset) + B - C = A + (B - C)" - by (simp add: multiset_ext_iff mset_le_def) + by (simp add: multiset_eq_iff mset_le_def) lemma mset_le_multiset_union_diff_commute: "B \ A \ (A::'a multiset) - B + C = A + C - B" -by (simp add: multiset_ext_iff mset_le_def) +by (simp add: multiset_eq_iff mset_le_def) lemma diff_le_self[simp]: "(M::'a multiset) - N \ M" by(simp add: mset_le_def) @@ -355,7 +355,7 @@ done lemma mset_less_of_empty[simp]: "A < {#} \ False" - by (auto simp add: mset_less_def mset_le_def multiset_ext_iff) + by (auto simp add: mset_less_def mset_le_def multiset_eq_iff) lemma multi_psub_of_add_self[simp]: "A < A + {#x#}" by (auto simp: mset_le_def mset_less_def) @@ -373,7 +373,7 @@ lemma mset_less_diff_self: "c \# B \ B - {#c#} < B" - by (auto simp: mset_le_def mset_less_def multiset_ext_iff) + by (auto simp: mset_le_def mset_less_def multiset_eq_iff) subsubsection {* Intersection *} @@ -400,15 +400,15 @@ by (simp add: multiset_inter_def multiset_typedef) lemma multiset_inter_single: "a \ b \ {#a#} #\ {#b#} = {#}" - by (rule multiset_ext) (auto simp add: multiset_inter_count) + by (rule multiset_eqI) (auto simp add: multiset_inter_count) lemma multiset_union_diff_commute: assumes "B #\ C = {#}" shows "A + B - C = A - C + B" -proof (rule multiset_ext) +proof (rule multiset_eqI) fix x from assms have "min (count B x) (count C x) = 0" - by (auto simp add: multiset_inter_count multiset_ext_iff) + by (auto simp add: multiset_inter_count multiset_eq_iff) then have "count B x = 0 \ count C x = 0" by auto then show "count (A + B - C) x = count (A - C + B) x" @@ -423,15 +423,15 @@ by (simp add: MCollect_def in_multiset multiset_typedef) lemma MCollect_empty [simp]: "MCollect {#} P = {#}" - by (rule multiset_ext) simp + by (rule multiset_eqI) simp lemma MCollect_single [simp]: "MCollect {#x#} P = (if P x then {#x#} else {#})" - by (rule multiset_ext) simp + by (rule multiset_eqI) simp lemma MCollect_union [simp]: "MCollect (M + N) f = MCollect M f + MCollect N f" - by (rule multiset_ext) simp + by (rule multiset_eqI) simp subsubsection {* Set of elements *} @@ -449,7 +449,7 @@ by (auto simp add: set_of_def) lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" -by (auto simp add: set_of_def multiset_ext_iff) +by (auto simp add: set_of_def multiset_eq_iff) lemma mem_set_of_iff [simp]: "(x \ set_of M) = (x :# M)" by (auto simp add: set_of_def) @@ -497,7 +497,7 @@ done lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" -by (auto simp add: size_def multiset_ext_iff) +by (auto simp add: size_def multiset_eq_iff) lemma nonempty_has_size: "(S \ {#}) = (0 < size S)" by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) @@ -584,7 +584,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: ext_iff) + apply (simp add: fun_eq_iff) apply (erule ssubst) apply (erule Abs_multiset_inverse [THEN subst]) apply (drule add') @@ -618,7 +618,7 @@ by (cases "B = {#}") (auto dest: multi_member_split) lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \ P x #}" -apply (subst multiset_ext_iff) +apply (subst multiset_eq_iff) apply auto done @@ -758,12 +758,12 @@ lemma multiset_of_eq_setD: "multiset_of xs = multiset_of ys \ set xs = set ys" -by (rule) (auto simp add:multiset_ext_iff set_count_greater_0) +by (rule) (auto simp add:multiset_eq_iff set_count_greater_0) lemma set_eq_iff_multiset_of_eq_distinct: "distinct x \ distinct y \ (set x = set y) = (multiset_of x = multiset_of y)" -by (auto simp: multiset_ext_iff distinct_count_atmost_1) +by (auto simp: multiset_eq_iff distinct_count_atmost_1) lemma set_eq_iff_multiset_of_remdups_eq: "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))" @@ -791,7 +791,7 @@ lemma multiset_of_remove1[simp]: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}" -by (induct xs) (auto simp add: multiset_ext_iff) +by (induct xs) (auto simp add: multiset_eq_iff) lemma multiset_of_eq_length: assumes "multiset_of xs = multiset_of ys" @@ -886,13 +886,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 ext_iff multiset_def) + by (simp add: count_of_def fun_eq_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 ext_iff) + by (simp_all add: count_of_def fun_eq_iff) lemma count_of_empty: "x \ fst ` set xs \ count_of xs x = 0" @@ -913,15 +913,15 @@ lemma Mempty_Bag [code]: "{#} = Bag []" - by (simp add: multiset_ext_iff) + by (simp add: multiset_eq_iff) lemma single_Bag [code]: "{#x#} = Bag [(x, 1)]" - by (simp add: multiset_ext_iff) + by (simp add: multiset_eq_iff) lemma MCollect_Bag [code]: "MCollect (Bag xs) P = Bag (filter (P \ fst) xs)" - by (simp add: multiset_ext_iff count_of_filter) + by (simp add: multiset_eq_iff count_of_filter) lemma mset_less_eq_Bag [code]: "Bag xs \ A \ (\(x, n) \ set xs. count_of xs x \ count A x)" @@ -1132,10 +1132,10 @@ apply (rule_tac x = "J + {#a#}" in exI) apply (rule_tac x = "K + Ka" in exI) apply (rule conjI) - apply (simp add: multiset_ext_iff split: nat_diff_split) + apply (simp add: multiset_eq_iff split: nat_diff_split) apply (rule conjI) apply (drule_tac f = "\M. M - {#a#}" in arg_cong, simp) - apply (simp add: multiset_ext_iff split: nat_diff_split) + apply (simp add: multiset_eq_iff split: nat_diff_split) apply (simp (no_asm_use) add: trans_def) apply blast apply (subgoal_tac "a :# (M0 + {#a#})") @@ -1650,7 +1650,7 @@ subsection {* Legacy theorem bindings *} -lemmas multi_count_eq = multiset_ext_iff [symmetric] +lemmas multi_count_eq = multiset_eq_iff [symmetric] lemma union_commute: "M + N = N + (M::'a multiset)" by (fact add_commute) diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Nat_Bijection.thy --- a/src/HOL/Library/Nat_Bijection.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Nat_Bijection.thy Mon Sep 13 11:13:15 2010 +0200 @@ -333,8 +333,8 @@ lemma set_decode_plus_power_2: "n \ set_decode z \ set_decode (2 ^ n + z) = insert n (set_decode z)" apply (induct n arbitrary: z, simp_all) - apply (rule set_ext, induct_tac x, simp, simp add: even_nat_Suc_div_2) - apply (rule set_ext, induct_tac x, simp, simp add: add_commute) + apply (rule set_eqI, induct_tac x, simp, simp add: even_nat_Suc_div_2) + apply (rule set_eqI, induct_tac x, simp, simp add: add_commute) done lemma finite_set_decode [simp]: "finite (set_decode n)" diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Order_Relation.thy --- a/src/HOL/Library/Order_Relation.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Order_Relation.thy Mon Sep 13 11:13:15 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: set_ext_iff antisym_def refl_on_def) metis +by(simp add: set_eq_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 e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Library/Permutations.thy Mon Sep 13 11:13:15 2010 +0200 @@ -16,7 +16,7 @@ (* ------------------------------------------------------------------------- *) lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" - by (auto simp add: ext_iff swap_def fun_upd_def) + by (auto simp add: fun_eq_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: ext_iff) + using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff) lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id" by (rule inv_unique_comp, simp_all) @@ -44,7 +44,7 @@ using pS unfolding permutes_def apply - - apply (rule set_ext) + apply (rule set_eqI) apply (simp add: image_iff) apply metis done @@ -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 ext_iff o_def] by auto + using permutes_inv_o[OF pS, unfolded fun_eq_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 ext_iff permutes_def apply simp by metis + unfolding fun_eq_iff permutes_def apply simp by metis lemma permutes_sing[simp]: "p permutes {a} \ p = id" - unfolding ext_iff permutes_def apply simp by metis + unfolding fun_eq_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 ext_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]] + unfolding fun_eq_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 ext_iff o_assoc by simp + have th0: "p = Fun.swap a ?b id o ?q" unfolding fun_eq_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 ext_iff) + by (auto simp add: swap_def fun_upd_def fun_eq_iff) also have "\ = ?g (c,q) x" using ths(5) `x \ F` eq - by (auto simp add: swap_def fun_upd_def ext_iff) + by (auto simp add: swap_def fun_upd_def fun_eq_iff) also have "\ = c"using ths(5) `x \ F` unfolding permutes_def - by (auto simp add: swap_def fun_upd_def ext_iff) + by (auto simp add: swap_def fun_upd_def fun_eq_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: ext_iff 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: fun_eq_iff swap_def) -lemma swap_id_common': "~(a = b) \ ~(a = c) \