--- a/NEWS Mon Sep 13 09:29:43 2010 +0200
+++ b/NEWS Mon Sep 13 11:13:25 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.
@@ -182,6 +185,8 @@
* List.thy: use various operations from the Haskell prelude when
generating Haskell code.
+* Multiset.thy: renamed empty_idemp -> empty_neutral
+
* code_simp.ML and method code_simp: simplification with rules determined
by code generator.
--- a/src/HOL/Algebra/Divisibility.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Mon Sep 13 11:13:25 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 \<sim> a \<otimes> c"
by (rule fmset_wfactors_mult) fact+
--- a/src/HOL/Bali/Example.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Bali/Example.thy Mon Sep 13 11:13:25 2010 +0200
@@ -792,7 +792,7 @@
lemma Base_fields_accessible[simp]:
"accfield tprg S Base
= table_of((map (\<lambda>((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 (\<lambda>((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
--- a/src/HOL/Bali/Table.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Bali/Table.thy Mon Sep 13 11:13:25 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 \<Longrightarrow> (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 (\<lambda>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 (\<lambda>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) \<subseteq> ran t"
by (auto simp add: filter_tab_def ran_def)
@@ -134,26 +134,26 @@
lemma filter_tab_all_True:
"\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>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:
"\<lbrakk>\<forall> k y. t k = Some y \<longrightarrow> p k y; t k = Some v\<rbrakk> \<Longrightarrow> filter_tab p t k = Some v"
-by (auto simp add: filter_tab_def ext_iff)
+by (auto simp add: filter_tab_def fun_eq_iff)
lemma filter_tab_all_False:
"\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>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 \<Longrightarrow> 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) \<subseteq> dom t"
by (auto simp add: filter_tab_def dom_def)
lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> 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) \<Longrightarrow> finite (dom (filter_tab C t))"
@@ -175,7 +175,7 @@
\<rbrakk> \<Longrightarrow>
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. *}
--- a/src/HOL/Big_Operators.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Big_Operators.thy Mon Sep 13 11:13:25 2010 +0200
@@ -1504,11 +1504,11 @@
lemma dual_max:
"ord.max (op \<ge>) = 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 \<ge>) = 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 \<noteq> {}"
--- a/src/HOL/Complete_Lattice.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy Mon Sep 13 11:13:25 2010 +0200
@@ -272,7 +272,7 @@
lemma Union_eq:
"\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
-proof (rule set_ext)
+proof (rule set_eqI)
fix x
have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
by auto
@@ -508,7 +508,7 @@
lemma Inter_eq:
"\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
-proof (rule set_ext)
+proof (rule set_eqI)
fix x
have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
by auto
--- a/src/HOL/Datatype.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Datatype.thy Mon Sep 13 11:13:25 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
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Mon Sep 13 11:13:25 2010 +0200
@@ -334,7 +334,7 @@
lemma UNIV_nat_infinite: "\<not> 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 \<Rightarrow> nat"
let ?N = "{i. i < n}"
let ?fN = "f ` ?N"
--- a/src/HOL/Finite_Set.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Finite_Set.thy Mon Sep 13 11:13:25 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 \<circ> f y = f y \<circ> 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 \<notin> A"
shows "F (insert x A) = F A \<circ> 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 "\<And>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 \<notin> B" by (blast dest: mk_disjoint_insert)
with `finite A` have "finite B" by simp
interpret fold: folding "op *" "\<lambda>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 \<circ> (\<lambda>b. fold op * b B) = (\<lambda>b. fold op * b B) \<circ> 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 "(\<lambda>x. fold op * x (insert b B)) = (\<lambda>x. fold op * x B) \<circ> 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
--- a/src/HOL/Fun.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Fun.thy Mon Sep 13 11:13:25 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 \<longleftrightarrow> (\<forall>x. f x = g x)"
+lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>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 \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
by auto
@@ -165,7 +163,7 @@
by (simp add: inj_on_def)
lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>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 \<noteq> c" and "b \<noteq> 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 \<circ> swap a b g = swap a b (f \<circ> g)"
by (rule ext, simp add: fun_upd_def swap_def)
--- a/src/HOL/Hilbert_Choice.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Sep 13 11:13:25 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
--- a/src/HOL/Hoare/SchorrWaite.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy Mon Sep 13 11:13:25 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]: "\<forall>x. x \<in> R \<longrightarrow> m x" by(auto simp: reachable_def addrs_def stackEmpty)
- from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL" by(auto simp: stackEmpty ext_iff intro:RisMarked)
+ from i5 i6 show "(\<forall>x.(x \<in> R) = m x) \<and> r = iR \<and> l = iL" by(auto simp: stackEmpty fun_eq_iff intro:RisMarked)
next
fix c m l r t p q root
--- a/src/HOL/IMP/Live.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/IMP/Live.thy Mon Sep 13 11:13:25 2010 +0200
@@ -8,7 +8,7 @@
consts Dep :: "((loc \<Rightarrow> 'a) \<Rightarrow> 'b) \<Rightarrow> loc set"
specification (Dep)
dep_on: "(\<forall>x\<in>Dep e. s x = t x) \<Longrightarrow> 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\<noteq>a \<longrightarrow> s x = t x) \<and> e s \<noteq> e t}"}
--- a/src/HOL/Imperative_HOL/Array.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Mon Sep 13 11:13:25 2010 +0200
@@ -99,7 +99,7 @@
lemma set_set_swap:
"r =!!= r' \<Longrightarrow> 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' \<Longrightarrow>
@@ -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))"
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Sep 13 11:13:25 2010 +0200
@@ -31,7 +31,7 @@
lemma Heap_eqI:
"(\<And>h. execute f h = execute g h) \<Longrightarrow> 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"
--- a/src/HOL/Imperative_HOL/Ref.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Mon Sep 13 11:13:25 2010 +0200
@@ -98,7 +98,7 @@
lemma set_set_swap:
"r =!= r' \<Longrightarrow> 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 \<Longrightarrow> \<not> present h r' \<Longrightarrow> 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 \<Longrightarrow> Array.present (snd (alloc v h)) a"
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Sep 13 11:13:25 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 \<Rightarrow> 'a node Heap"
where
--- a/src/HOL/Import/HOL/bool.imp Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp Mon Sep 13 11:13:25 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"
--- a/src/HOL/Import/HOL/prob_extra.imp Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Import/HOL/prob_extra.imp Mon Sep 13 11:13:25 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"
--- a/src/HOL/Import/HOLLight/hollight.imp Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Mon Sep 13 11:13:25 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"
--- a/src/HOL/Library/AssocList.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/AssocList.thy Mon Sep 13 11:13:25 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\<mapsto>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\<mapsto>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\<noteq>k'
\<Longrightarrow> 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 \<longleftrightarrow>
@@ -96,8 +96,8 @@
proof -
have "map_of \<circ> More_List.fold (prod_case update) (zip ks vs) =
More_List.fold (\<lambda>(k, v) f. f(k \<mapsto> v)) (zip ks vs) \<circ> 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[\<mapsto>]vs)) k"
@@ -114,7 +114,7 @@
moreover have "map fst \<circ> More_List.fold (prod_case update) (zip ks vs) =
More_List.fold (\<lambda>(k, v) al. if k \<in> set al then al else al @ [k]) (zip ks vs) \<circ> 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 \<Longrightarrow>
@@ -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 \<circ> More_List.fold (prod_case update) (zip ks vs) =
More_List.fold (prod_case update) (zip ks vs) \<circ> 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 \<circ> More_List.fold (prod_case update) (rev ys) =
More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> 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 (\<lambda>n. (n, vs ! n)) [0..<length vs])"
- by (rule mapping_eqI) (simp add: map_of_map_restrict ext_iff)
+ by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
lemma map_of_eqI: (*FIXME move to Map.thy*)
assumes set_eq: "set (map fst xs) = set (map fst ys)"
--- a/src/HOL/Library/Binomial.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Binomial.thy Mon Sep 13 11:13:25 2010 +0200
@@ -236,7 +236,7 @@
have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
(\<Prod>n\<in>{0\<Colon>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': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{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} \<inter> {n - h .. n} = {}" and eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}" using h kn by auto
from eq[symmetric]
--- a/src/HOL/Library/Code_Char_chr.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy Mon Sep 13 11:13:25 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)")
--- a/src/HOL/Library/Countable.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Countable.thy Mon Sep 13 11:13:25 2010 +0200
@@ -139,7 +139,7 @@
show "\<exists>to_nat::('a \<Rightarrow> 'b) \<Rightarrow> nat. inj to_nat"
proof
show "inj (\<lambda>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
--- a/src/HOL/Library/Efficient_Nat.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Mon Sep 13 11:13:25 2010 +0200
@@ -79,7 +79,7 @@
lemma [code, code_unfold]:
"nat_case = (\<lambda>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 *}
--- a/src/HOL/Library/Enum.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Enum.thy Mon Sep 13 11:13:25 2010 +0200
@@ -42,7 +42,7 @@
"HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> 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\<Colon>enum \<Rightarrow> 'b\<Colon>order"
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> 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 \<and> set ys \<subseteq> set xs}"
-proof (rule set_ext)
+proof (rule set_eqI)
fix ys :: "'a list"
show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
proof -
@@ -160,7 +160,7 @@
proof (rule UNIV_eq_I)
fix f :: "'a \<Rightarrow> 'b"
have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>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 \<in> set enum"
by (auto simp add: enum_fun_def set_n_lists)
qed
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Sep 13 11:13:25 2010 +0200
@@ -18,7 +18,7 @@
notation fps_nth (infixl "$" 75)
lemma expand_fps_eq: "p = q \<longleftrightarrow> (\<forall>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: "(\<And>n. p $ n = q $ n) \<Longrightarrow> p = q"
by (simp add: expand_fps_eq)
@@ -791,14 +791,14 @@
apply (rule setsum_reindex_cong[where f="\<lambda>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 (\<lambda>i. f $ i * g $ (n + 1 - i)) ?Zn1 = setsum (\<lambda>i. f $ (n + 1 - i) * g $ i) ?Zn1"
apply (rule setsum_reindex_cong[where f="\<lambda>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 \<noteq> 0"
then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
"{0..n - 1}\<union>{n} = {0..n}"
- by (auto simp: set_ext_iff)
+ by (auto simp: set_eq_iff)
have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
"{0..n - 1}\<inter>{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} \<union> {m} = {0..m}" using k apply (simp add: set_ext_iff) by presburger
+ have u0: "{0 .. k} \<union> {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} \<inter> {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 \<and> j \<le> n \<and> 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 \<le> 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)
--- a/src/HOL/Library/FrechetDeriv.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy Mon Sep 13 11:13:25 2010 +0200
@@ -177,7 +177,7 @@
hence "(\<lambda>h. F h - F' h) = (\<lambda>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 *}
--- a/src/HOL/Library/Fset.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Fset.thy Mon Sep 13 11:13:25 2010 +0200
@@ -51,7 +51,7 @@
lemma member_code [code]:
"member (Set xs) = List.member xs"
"member (Coset xs) = Not \<circ> 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 *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
- by (simp add: ext_iff)
+ by (simp add: fun_eq_iff)
have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
fold More_Set.remove xs \<circ> 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 (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> 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 "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
@@ -277,13 +277,13 @@
"sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
proof -
have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
- by (simp add: ext_iff)
+ by (simp add: fun_eq_iff)
have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
fold Set.insert xs \<circ> 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 (\<lambda>x. Fset \<circ> Set.insert x \<circ> 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 "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
--- a/src/HOL/Library/FuncSet.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/FuncSet.thy Mon Sep 13 11:13:25 2010 +0200
@@ -128,7 +128,7 @@
lemma compose_assoc:
"[| f \<in> A -> B; g \<in> B -> C; h \<in> 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 \<in> 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 \<in> A ==> f x = g x) ==> (\<lambda>x\<in>A. f x) = (\<lambda>x\<in>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 \<in> A -> B; f \<in> extensional A|] ==> compose A (\<lambda>y\<in>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 \<in> A -> B; g \<in> extensional A|] ==> compose A g (\<lambda>x\<in>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 \<in> extensional A; g \<in> extensional A;
!!x. x\<in>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 ==> (\<lambda>x\<in>B. inv_into A f x) : B -> A"
by (unfold inv_into_def) (fast intro: someI2)
--- a/src/HOL/Library/Function_Algebras.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Function_Algebras.thy Mon Sep 13 11:13:25 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 *}
--- a/src/HOL/Library/Inner_Product.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Inner_Product.thy Mon Sep 13 11:13:25 2010 +0200
@@ -307,7 +307,7 @@
have 1: "FDERIV (\<lambda>x. inner x x) x :> (\<lambda>h. inner x h + inner h x)"
by (intro inner.FDERIV FDERIV_ident)
have 2: "(\<lambda>h. inner x h + inner h x) = (\<lambda>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 \<noteq> 0` by simp
then have 3: "DERIV sqrt (inner x x) :> (inverse (sqrt (inner x x)) / 2)"
by (rule DERIV_real_sqrt)
--- a/src/HOL/Library/Mapping.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Mapping.thy Mon Sep 13 11:13:25 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) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)"
@@ -146,7 +146,7 @@
lemma bulkload_tabulate:
"bulkload xs = tabulate [0..<length xs] (nth xs)"
- by (rule mapping_eqI) (simp add: ext_iff)
+ by (rule mapping_eqI) (simp add: fun_eq_iff)
lemma is_empty_empty: (*FIXME*)
"is_empty m \<longleftrightarrow> m = Mapping Map.empty"
--- a/src/HOL/Library/More_List.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/More_List.thy Mon Sep 13 11:13:25 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 "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
shows "h \<circ> fold g xs = fold f xs \<circ> 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 "\<And>x. x \<in> set xs \<Longrightarrow> 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 \<circ> f) xs top"
--- a/src/HOL/Library/More_Set.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/More_Set.thy Mon Sep 13 11:13:25 2010 +0200
@@ -18,7 +18,7 @@
lemma fun_left_comm_idem_remove:
"fun_left_comm_idem remove"
proof -
- have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: ext_iff remove_def)
+ have rem: "remove = (\<lambda>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 = (\<lambda>x A. A - {x})" by (simp add: ext_iff remove_def)
+ have rem: "remove = (\<lambda>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 \<circ> 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
--- a/src/HOL/Library/Multiset.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 13 11:13:25 2010 +0200
@@ -24,13 +24,13 @@
notation (xsymbols)
Melem (infix "\<in>#" 50)
-lemma multiset_ext_iff:
+lemma multiset_eq_iff:
"M = N \<longleftrightarrow> (\<forall>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:
"(\<And>x. count A x = count B x) \<Longrightarrow> 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 \<and> {#} - 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 \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
- by (clarsimp simp: multiset_ext_iff)
+ by (clarsimp simp: multiset_eq_iff)
lemma insert_DiffM2 [simp]:
"x \<in># M \<Longrightarrow> 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 \<noteq> b \<Longrightarrow> 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 \<in># J \<Longrightarrow> 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#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
- by (simp add: multiset_ext_iff)
+ by (simp add: multiset_eq_iff)
lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
- by (auto simp add: multiset_ext_iff)
+ by (auto simp add: multiset_eq_iff)
lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
- by (auto simp add: multiset_ext_iff)
+ by (auto simp add: multiset_eq_iff)
lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> 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#} \<longleftrightarrow> False"
- by (auto simp add: multiset_ext_iff)
+ by (auto simp add: multiset_eq_iff)
lemma diff_single_trivial:
"\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
- by (auto simp add: multiset_ext_iff)
+ by (auto simp add: multiset_eq_iff)
lemma diff_single_eq_union:
"x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> 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#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> 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 \<longleftrightarrow> A \<le> B \<and> A \<noteq> 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) \<le> B \<longleftrightarrow> (\<exists>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,14 @@
lemma multiset_diff_union_assoc:
"C \<le> B \<Longrightarrow> (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 \<le> A \<Longrightarrow> (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 \<le> M"
+by(simp add: mset_le_def)
lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
apply (clarsimp simp: mset_le_def mset_less_def)
@@ -352,7 +355,7 @@
done
lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> 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)
@@ -370,7 +373,7 @@
lemma mset_less_diff_self:
"c \<in># B \<Longrightarrow> 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 *}
@@ -397,15 +400,15 @@
by (simp add: multiset_inter_def multiset_typedef)
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#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 #\<inter> 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 \<or> count C x = 0"
by auto
then show "count (A + B - C) x = count (A - C + B) x"
@@ -420,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 *}
@@ -446,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 \<in> set_of M) = (x :# M)"
by (auto simp add: set_of_def)
@@ -494,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 \<noteq> {#}) = (0 < size S)"
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
@@ -581,7 +584,7 @@
apply (rule empty [unfolded defns])
apply (subgoal_tac "f(b := f b + 1) = (\<lambda>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')
@@ -615,7 +618,7 @@
by (cases "B = {#}") (auto dest: multi_member_split)
lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
-apply (subst multiset_ext_iff)
+apply (subst multiset_eq_iff)
apply auto
done
@@ -755,12 +758,12 @@
lemma multiset_of_eq_setD:
"multiset_of xs = multiset_of ys \<Longrightarrow> 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 \<Longrightarrow> distinct y \<Longrightarrow>
(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))"
@@ -788,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"
@@ -883,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 [] = (\<lambda>_. 0)"
"count_of ((x, n) # xs) = (\<lambda>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 \<notin> fst ` set xs \<Longrightarrow> count_of xs x = 0"
@@ -910,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 \<circ> 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 \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
@@ -1129,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 = "\<lambda>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#})")
@@ -1597,7 +1600,7 @@
thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
qed
-lemma empty_idemp: "{#} + x = x" "x + {#} = x"
+lemma empty_neutral: "{#} + x = x" "x + {#} = x"
and nonempty_plus: "{# x #} + rs \<noteq> {#}"
and nonempty_single: "{# x #} \<noteq> {#}"
by auto
@@ -1623,7 +1626,7 @@
val regroup_munion_conv =
Function_Lib.regroup_conv @{const_abbrev Mempty} @{const_name plus}
- (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_idemp}))
+ (map (fn t => t RS eq_reflection) (@{thms add_ac} @ @{thms empty_neutral}))
fun unfold_pwleq_tac i =
(rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
@@ -1647,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)
--- a/src/HOL/Library/Nat_Bijection.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy Mon Sep 13 11:13:25 2010 +0200
@@ -333,8 +333,8 @@
lemma set_decode_plus_power_2:
"n \<notin> set_decode z \<Longrightarrow> 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)"
--- a/src/HOL/Library/Order_Relation.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Order_Relation.thy Mon Sep 13 11:13:25 2010 +0200
@@ -81,7 +81,7 @@
lemma Refl_antisym_eq_Image1_Image1_iff:
"\<lbrakk>Refl r; antisym r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> 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:
"\<lbrakk>Partial_order r; a:Field r; b:Field r\<rbrakk> \<Longrightarrow> r `` {a} = r `` {b} \<longleftrightarrow> a=b"
--- a/src/HOL/Library/Permutations.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Permutations.thy Mon Sep 13 11:13:25 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 \<Longrightarrow> S \<subseteq> T ==> p permutes T"
unfolding permutes_def by blast
lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> 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} \<longleftrightarrow> 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 \<longleftrightarrow> (\<forall>y. \<exists>!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 \<in> insert a S " unfolding permutes_in_image[OF pS] by simp
from permutes_insert_lemma[OF pS] th0 th1
have "\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S" by blast}
@@ -180,11 +180,11 @@
and eq: "?g (b,p) = ?g (c,q)"
from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
from ths(4) `x \<notin> 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 "\<dots> = ?g (c,q) x" using ths(5) `x \<notin> 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 "\<dots> = c"using ths(5) `x \<notin> 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 \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: ext_iff swap_def)
+lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
-lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: ext_iff swap_def)
+lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
lemma swap_id_independent: "~(a = c) \<Longrightarrow> ~(a = d) \<Longrightarrow> ~(b = c) \<Longrightarrow> ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id"
- by (simp add: swap_def ext_iff)
+ by (simp add: swap_def fun_eq_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: ext_iff swap_def)
+ apply (clarsimp simp add: fun_eq_iff swap_def)
apply (case_tac "a \<noteq> c \<and> 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: ext_iff swap_def)
+ apply (clarsimp simp add: fun_eq_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: ext_iff swap_def)
+ apply (clarsimp simp add: fun_eq_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 \<circ> q = id" "q \<circ> p = id" by blast
- thus ?thesis unfolding bij_iff apply (auto simp add: ext_iff) apply metis done
+ thus ?thesis unfolding bij_iff apply (auto simp add: fun_eq_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: ext_iff swap_def bij_inv_eq_iff[OF bp])
+ by (simp add: fun_eq_iff swap_def bij_inv_eq_iff[OF bp])
lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> 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: ext_iff)
+ thus ?thesis by (auto simp add: fun_eq_iff)
qed
lemma permutes_natset_ge:
@@ -709,7 +709,7 @@
qed
lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
-apply (rule set_ext)
+apply (rule set_eqI)
apply auto
using permutes_inv_inv permutes_inv apply auto
apply (rule_tac x="inv x" in exI)
@@ -718,7 +718,7 @@
lemma image_compose_permutations_left:
assumes q: "q permutes S" shows "{q o p | p. p permutes S} = {p . p permutes S}"
-apply (rule set_ext)
+apply (rule set_eqI)
apply auto
apply (rule permutes_compose)
using q apply auto
@@ -728,7 +728,7 @@
lemma image_compose_permutations_right:
assumes q: "q permutes S"
shows "{p o q | p. p permutes S} = {p . p permutes S}"
-apply (rule set_ext)
+apply (rule set_eqI)
apply auto
apply (rule permutes_compose)
using q apply auto
@@ -811,7 +811,7 @@
shows "setsum f {p. p permutes (insert a S)} = setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)"
proof-
have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id o p)) = f o (\<lambda>(b,p). Fun.swap a b id o p)"
- by (simp add: ext_iff)
+ by (simp add: fun_eq_iff)
have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}" by blast
have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast
show ?thesis
--- a/src/HOL/Library/Polynomial.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Sep 13 11:13:25 2010 +0200
@@ -16,7 +16,7 @@
by auto
lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
-by (simp add: coeff_inject [symmetric] ext_iff)
+by (simp add: coeff_inject [symmetric] fun_eq_iff)
lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> 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 \<longleftrightarrow> p = q"
using poly_zero [of "p - q"]
- by (simp add: ext_iff)
+ by (simp add: fun_eq_iff)
subsection {* Composition of polynomials *}
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Sep 13 11:13:25 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: ext_iff min_def le_bool_def)
+by (rule eq_reflection) (auto simp add: fun_eq_iff min_def le_bool_def)
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
--- a/src/HOL/Library/Quotient_List.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Quotient_List.thy Mon Sep 13 11:13:25 2010 +0200
@@ -19,7 +19,7 @@
lemma map_id[id_simps]:
shows "map id = id"
- apply(simp add: ext_iff)
+ apply(simp add: fun_eq_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: ext_iff fun_map_def cons_prs_aux[OF q])
+ by (simp only: fun_eq_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: ext_iff fun_map_def map_prs_aux[OF a b])
+ by (simp_all only: fun_eq_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: ext_iff fun_map_def foldr_prs_aux[OF a b])
+ by (simp only: fun_eq_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: ext_iff fun_map_def foldl_prs_aux[OF a b])
+ by (simp only: fun_eq_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: ext_iff)
+ apply (simp add: fun_eq_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 ext_iff
+ unfolding fun_eq_iff
apply(rule allI)+
apply(induct_tac x xa rule: list_induct2')
apply(simp_all)
--- a/src/HOL/Library/Quotient_Option.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Mon Sep 13 11:13:25 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: ext_iff)
+ apply(simp add: fun_eq_iff)
apply(simp add: Quotient_abs_rep[OF q])
done
lemma option_map_id[id_simps]:
shows "Option.map id = id"
- by (simp add: ext_iff split_option_all)
+ by (simp add: fun_eq_iff split_option_all)
lemma option_rel_eq[id_simps]:
shows "option_rel (op =) = (op =)"
- by (simp add: ext_iff split_option_all)
+ by (simp add: fun_eq_iff split_option_all)
end
--- a/src/HOL/Library/Quotient_Product.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Mon Sep 13 11:13:25 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: ext_iff)
+ apply(simp add: fun_eq_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: ext_iff)
+ apply(simp add: fun_eq_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: ext_iff)
+ apply(simp add: fun_eq_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: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ by (simp add: fun_eq_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: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ by (simp add: fun_eq_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: ext_iff)
+ by (simp add: fun_eq_iff)
end
--- a/src/HOL/Library/Quotient_Sum.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy Mon Sep 13 11:13:25 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: ext_iff)
+ apply(simp add: fun_eq_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: ext_iff)
+ apply(simp add: fun_eq_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: ext_iff split_sum_all)
+ by (simp add: fun_eq_iff split_sum_all)
lemma sum_rel_eq[id_simps]:
shows "sum_rel (op =) (op =) = (op =)"
- by (simp add: ext_iff split_sum_all)
+ by (simp add: fun_eq_iff split_sum_all)
end
--- a/src/HOL/Library/RBT.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/RBT.thy Mon Sep 13 11:13:25 2010 +0200
@@ -112,7 +112,7 @@
lemma lookup_empty [simp]:
"lookup empty = Map.empty"
- by (simp add: empty_def lookup_RBT ext_iff)
+ by (simp add: empty_def lookup_RBT fun_eq_iff)
lemma lookup_insert [simp]:
"lookup (insert k v t) = (lookup t)(k \<mapsto> v)"
@@ -144,7 +144,7 @@
lemma fold_fold:
"fold f t = More_List.fold (prod_case f) (entries t)"
- by (simp add: fold_def ext_iff RBT_Impl.fold_def entries_impl_of)
+ by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
lemma is_empty_empty [simp]:
"is_empty t \<longleftrightarrow> t = empty"
@@ -152,7 +152,7 @@
lemma RBT_lookup_empty [simp]: (*FIXME*)
"RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
- by (cases t) (auto simp add: ext_iff)
+ by (cases t) (auto simp add: fun_eq_iff)
lemma lookup_empty_empty [simp]:
"lookup t = Map.empty \<longleftrightarrow> t = empty"
@@ -220,7 +220,7 @@
lemma bulkload_Mapping [code]:
"Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
- by (rule mapping_eqI) (simp add: map_of_map_restrict ext_iff)
+ by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
lemma equal_Mapping [code]:
"HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
--- a/src/HOL/Library/RBT_Impl.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Mon Sep 13 11:13:25 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: ext_iff)
+ by (induct t) (auto split: option.splits simp add: fun_eq_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 \<circ> f k v \<circ> fold f lt"
- by (simp_all add: fold_def ext_iff)
+ by (simp_all add: fold_def fun_eq_iff)
subsection {* Bulkloading a tree *}
--- a/src/HOL/Library/Set_Algebras.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Set_Algebras.thy Mon Sep 13 11:13:25 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 ext_iff)
+ by (simp add: set_add.setsum_def setsum_set_def fun_eq_iff)
qed
interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
@@ -117,7 +117,7 @@
show "power.power {1} set_times = (\<lambda>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 ext_iff)
+ by (simp add: set_mult.setprod_def setprod_set_def fun_eq_iff)
qed
lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
--- a/src/HOL/Library/Univ_Poly.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Library/Univ_Poly.thy Mon Sep 13 11:13:25 2010 +0200
@@ -382,7 +382,7 @@
lemma (in idom_char_0) poly_entire:
"poly (p *** q) = poly [] \<longleftrightarrow> poly p = poly [] \<or> poly q = poly []"
using poly_entire_lemma2[of p q]
-by (auto simp add: ext_iff poly_mult)
+by (auto simp add: fun_eq_iff poly_mult)
lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
by (simp add: poly_entire)
@@ -847,14 +847,14 @@
assume eq: ?lhs
hence "\<And>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: ext_iff)
+ hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add: fun_eq_iff)
hence "c = d \<and> list_all (\<lambda>x. x=0) ((cs +++ -- ds))"
unfolding poly_zero by (simp add: poly_minus_def algebra_simps)
hence "c = d \<and> (\<forall>x. poly (cs +++ -- ds) x = 0)"
unfolding poly_zero[symmetric] by simp
- thus ?rhs by (simp add: poly_minus poly_add algebra_simps ext_iff)
+ thus ?rhs by (simp add: poly_minus poly_add algebra_simps fun_eq_iff)
next
- assume ?rhs then show ?lhs by(simp add:ext_iff)
+ assume ?rhs then show ?lhs by(simp add:fun_eq_iff)
qed
lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \<Longrightarrow> pnormalize p = pnormalize q"
--- a/src/HOL/Limits.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Limits.thy Mon Sep 13 11:13:25 2010 +0200
@@ -46,7 +46,7 @@
lemma expand_net_eq:
shows "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
-unfolding Rep_net_inject [symmetric] ext_iff eventually_def ..
+unfolding Rep_net_inject [symmetric] fun_eq_iff eventually_def ..
lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
unfolding eventually_def
--- a/src/HOL/List.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/List.thy Mon Sep 13 11:13:25 2010 +0200
@@ -2317,7 +2317,7 @@
lemma foldl_apply:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
- by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: ext_iff)
+ by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: fun_eq_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: ext_iff member_def mem_def)
+ by (simp add: fun_eq_iff member_def mem_def)
lemma member_rec [code]:
"member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
--- a/src/HOL/Map.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Map.thy Mon Sep 13 11:13:25 2010 +0200
@@ -218,7 +218,7 @@
lemma map_of_zip_map:
"map_of (zip xs (map f xs)) = (\<lambda>x. if x \<in> set xs then Some (f x) else None)"
- by (induct xs) (simp_all add: ext_iff)
+ by (induct xs) (simp_all add: fun_eq_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 (\<lambda>(k, v). (k, f v)) xs) = Option.map f \<circ> map_of xs"
- by (induct xs) (auto simp add: ext_iff)
+ by (induct xs) (auto simp add: fun_eq_iff)
lemma dom_option_map:
"dom (\<lambda>k. Option.map (f k) (m k)) = dom m"
@@ -347,7 +347,7 @@
lemma map_add_map_of_foldr:
"m ++ map_of ps = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) ps m"
- by (induct ps) (auto simp add: ext_iff map_add_def)
+ by (induct ps) (auto simp add: fun_eq_iff map_add_def)
subsection {* @{term [source] restrict_map} *}
@@ -381,26 +381,26 @@
lemma restrict_fun_upd [simp]:
"m(x := y)|`D = (if x \<in> D then (m|`(D-{x}))(x := y) else m|`D)"
-by (simp add: restrict_map_def ext_iff)
+by (simp add: restrict_map_def fun_eq_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 ext_iff)
+by (simp add: restrict_map_def fun_eq_iff)
lemma fun_upd_restrict: "(m|`D)(x := y) = (m|`(D-{x}))(x := y)"
-by (simp add: restrict_map_def ext_iff)
+by (simp add: restrict_map_def fun_eq_iff)
lemma fun_upd_restrict_conv [simp]:
"x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
-by (simp add: restrict_map_def ext_iff)
+by (simp add: restrict_map_def fun_eq_iff)
lemma map_of_map_restrict:
"map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
- by (induct ks) (simp_all add: ext_iff restrict_map_insert)
+ by (induct ks) (simp_all add: fun_eq_iff restrict_map_insert)
lemma restrict_complement_singleton_eq:
"f |` (- {x}) = f(x := None)"
- by (simp add: restrict_map_def ext_iff)
+ by (simp add: restrict_map_def fun_eq_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 \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
-by(fastsimp simp: map_add_def map_le_def ext_iff split: option.splits)
+by(fastsimp simp: map_add_def map_le_def fun_eq_iff split: option.splits)
lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
by (fastsimp simp add: map_le_def map_add_def dom_def)
--- a/src/HOL/Matrix/Matrix.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Matrix/Matrix.thy Mon Sep 13 11:13:25 2010 +0200
@@ -74,7 +74,7 @@
let ?B = "{pos. Rep_matrix x (fst pos) (snd pos) \<noteq> 0}"
have swap_image: "?swap`?A = ?B"
apply (simp add: image_def)
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (simp)
proof
fix y
@@ -208,7 +208,7 @@
apply (simp)
proof -
fix n
- have "{x. x < Suc n} = insert n {x. x < n}" by (rule set_ext, simp, arith)
+ have "{x. x < Suc n} = insert n {x. x < n}" by (rule set_eqI, simp, arith)
moreover assume "finite {x. x < n}"
ultimately show "finite {x. x < Suc n}" by (simp)
qed
@@ -225,11 +225,11 @@
have f1: "finite ?sd"
proof -
let ?f = "% x. (m, x)"
- have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_ext, simp add: image_def, auto)
+ have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_eqI, simp add: image_def, auto)
moreover have "finite {x. x < n}" by (simp add: finite_natarray1)
ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp)
qed
- have su: "?s0 \<union> ?sd = ?s1" by (rule set_ext, simp, arith)
+ have su: "?s0 \<union> ?sd = ?s1" by (rule set_eqI, simp, arith)
from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI)
with su show "finite ?s1" by (simp)
qed
@@ -247,7 +247,7 @@
have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)
from a b have "(?u \<inter> (-?v)) = {}"
apply (simp)
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (simp)
apply auto
by (rule c, auto)+
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy Mon Sep 13 11:13:25 2010 +0200
@@ -68,7 +68,7 @@
(**********************************************************************)
lemma the_map_upd: "(the \<circ> f(x\<mapsto>v)) = (the \<circ> f)(x:=v)"
-by (simp add: ext_iff)
+by (simp add: fun_eq_iff)
lemma map_of_in_set:
"(map_of xs x = None) = (x \<notin> set (map fst xs))"
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Mon Sep 13 11:13:25 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: ext_iff)
+ apply (simp add: fun_eq_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: ext_iff)
+ apply (simp add: fun_eq_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: ext_iff cast_ok_def comp_widen)
+ by (simp add: fun_eq_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 (\<lambda>(C, cno::cname, fdls::fdecl list, jmdls).
(C, cno, fdls, map (compMethod G C) jmdls))) = fst")
apply (simp del: image_compose)
-apply (simp add: ext_iff split_beta)
+apply (simp add: fun_eq_iff split_beta)
done
@@ -322,7 +322,7 @@
= (\<lambda>x. (fst x, Object, fst (snd x),
snd (snd (compMethod G Object (S, snd x)))))")
apply (simp only:)
-apply (simp add: ext_iff)
+apply (simp add: fun_eq_iff)
apply (intro strip)
apply (subgoal_tac "(inv (\<lambda>(s, m). (s, Object, m)) (S, Object, snd x)) = (S, snd x)")
apply (simp only:)
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Sep 13 11:13:25 2010 +0200
@@ -101,7 +101,7 @@
lemma card_1_exists: "card s = 1 \<longleftrightarrow> (\<exists>!x. x \<in> s)" unfolding One_nat_def
apply rule apply(drule card_eq_SucD) defer apply(erule ex1E) proof-
fix x assume as:"x \<in> s" "\<forall>y. y \<in> s \<longrightarrow> y = x"
- have *:"s = insert x {}" apply- apply(rule set_ext,rule) unfolding singleton_iff
+ have *:"s = insert x {}" apply- apply(rule set_eqI,rule) unfolding singleton_iff
apply(rule as(2)[rule_format]) using as(1) by auto
show "card s = Suc 0" unfolding * using card_insert by auto qed auto
@@ -122,7 +122,7 @@
shows "card {s'. \<exists>a\<in>s. s' = s - {a} \<and> f ` s' = t - {b}} = 1" proof-
obtain a where a:"b = f a" "a\<in>s" using assms(4-5) by auto
have inj:"inj_on f s" apply(rule eq_card_imp_inj_on) using assms(1-4) by auto
- have *:"{a \<in> s. f ` (s - {a}) = t - {b}} = {a}" apply(rule set_ext) unfolding singleton_iff
+ have *:"{a \<in> s. f ` (s - {a}) = t - {b}} = {a}" apply(rule set_eqI) unfolding singleton_iff
apply(rule,rule inj[unfolded inj_on_def,rule_format]) unfolding a using a(2) and assms and inj[unfolded inj_on_def] by auto
show ?thesis apply(rule image_lemma_0) unfolding * by auto qed
@@ -135,7 +135,7 @@
have "f a \<in> t - {b}" using a and assms by auto
hence "\<exists>c \<in> s - {a}. f a = f c" unfolding image_iff[symmetric] and a by auto
then obtain c where c:"c \<in> s" "a \<noteq> c" "f a = f c" by auto
- hence *:"f ` (s - {c}) = f ` (s - {a})" apply-apply(rule set_ext,rule) proof-
+ hence *:"f ` (s - {c}) = f ` (s - {a})" apply-apply(rule set_eqI,rule) proof-
fix x assume "x \<in> f ` (s - {a})" then obtain y where y:"f y = x" "y\<in>s- {a}" by auto
thus "x \<in> f ` (s - {c})" unfolding image_iff apply(rule_tac x="if y = c then a else y" in bexI) using c a by auto qed auto
have "c\<in>?M" unfolding mem_Collect_eq and * using a and c(1) by auto
@@ -165,7 +165,7 @@
(\<exists>a\<in>s. (f = s - {a})) \<and> P f \<longleftrightarrow> (\<exists>a\<in>s. (f = s - {a}) \<and> P f)" by auto
fix s assume s:"s\<in>simplices" let ?S = "{f \<in> {f. \<exists>s\<in>simplices. face f s}. face f s \<and> rl ` f = {0..n}}"
have "{0..n + 1} - {n + 1} = {0..n}" by auto
- hence S:"?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}" apply- apply(rule set_ext)
+ hence S:"?S = {s'. \<exists>a\<in>s. s' = s - {a} \<and> rl ` s' = {0..n + 1} - {n + 1}}" apply- apply(rule set_eqI)
unfolding assms(2)[rule_format] mem_Collect_eq and *[OF s, unfolded mem_Collect_eq, where P="\<lambda>x. rl ` x = {0..n}"] by auto
show "rl ` s = {0..n+1} \<Longrightarrow> card ?S = 1" "rl ` s \<noteq> {0..n+1} \<Longrightarrow> card ?S = 0 \<or> card ?S = 2" unfolding S
apply(rule_tac[!] image_lemma_1 image_lemma_2) using ** assms(4) and s by auto qed
@@ -493,13 +493,13 @@
lemma card_funspace': assumes "finite s" "finite t" "card s = m" "card t = n"
shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m" (is "card (?M s) = _")
using assms apply - proof(induct m arbitrary: s)
- have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" apply(rule set_ext,rule)unfolding mem_Collect_eq apply(rule,rule ext) by auto
+ have *:"{f. \<forall>x. f x = d} = {\<lambda>x. d}" apply(rule set_eqI,rule)unfolding mem_Collect_eq apply(rule,rule ext) by auto
case 0 thus ?case by(auto simp add: *) next
case (Suc m) guess a using card_eq_SucD[OF Suc(4)] .. then guess s0
apply(erule_tac exE) apply(erule conjE)+ . note as0 = this
have **:"card s0 = m" using as0 using Suc(2) Suc(4) by auto
let ?l = "(\<lambda>(b,g) x. if x = a then b else g x)" have *:"?M (insert a s0) = ?l ` {(b,g). b\<in>t \<and> g\<in>?M s0}"
- apply(rule set_ext,rule) unfolding mem_Collect_eq image_iff apply(erule conjE)
+ apply(rule set_eqI,rule) unfolding mem_Collect_eq image_iff apply(erule conjE)
apply(rule_tac x="(x a, \<lambda>y. if y\<in>s0 then x y else d)" in bexI) apply(rule ext) prefer 3 apply rule defer
apply(erule bexE,rule) unfolding mem_Collect_eq apply(erule splitE)+ apply(erule conjE)+ proof-
fix x xa xb xc y assume as:"x = (\<lambda>(b, g) x. if x = a then b else g x) xa" "xb \<in> UNIV - insert a s0" "xa = (xc, y)" "xc \<in> t"
@@ -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 "\<forall>i. a_max i = a1 i" by auto
- hence "a' = a" unfolding True `a=a0` apply-apply(subst ext_iff,rule)
+ hence "a' = a" unfolding True `a=a0` apply-apply(subst fun_eq_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\<in>{1..n}") by auto qed
hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` by auto
@@ -738,7 +738,7 @@
have "a2 \<noteq> a" unfolding `a=a0` using k(2)[rule_format,of k] by auto
hence "a2 \<in> s - {a}" using a2 by auto thus "a2 \<in> s'" unfolding a'(2)[THEN sym] by auto qed
hence "\<forall>i. a_min i = a2 i" by auto
- hence "a' = a3" unfolding as `a=a0` apply-apply(subst ext_iff,rule)
+ hence "a' = a3" unfolding as `a=a0` apply-apply(subst fun_eq_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\<in>{1..n}") defer apply(cases "x=k")
@@ -834,7 +834,7 @@
proof- case goal1 thus ?case apply(cases "j\<in>{1..n}",case_tac[!] "j=k") by auto qed
have "\<forall>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\<in>{1..n}") by auto qed hence "a_min = a3" unfolding ext_iff .
+ thus ?case apply(cases "i\<in>{1..n}") by auto qed hence "a_min = a3" unfolding fun_eq_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 \<in> s" by auto have "a0 \<in> s - {a1}" using a0a1(1-3) by auto thus "a0 \<in> s'"
unfolding a'(2)[THEN sym,unfolded `a=a1`] by auto qed
hence "\<forall>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\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding ext_iff by auto
+ hence "s' = s" apply-apply(rule lem1[OF a'(2)]) using `a\<in>s` `a'\<in>s'` unfolding as `a=a1` unfolding fun_eq_iff by auto
thus ?thesis by auto qed qed
ultimately have *:"?A = {s, insert a3 (s - {a1})}" by blast
have "s \<noteq> insert a3 (s - {a1})" using `a3\<notin>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'\<noteq>a" apply-apply rule unfolding ext_iff unfolding a'_def k(2)
+ hence aa':"a'\<noteq>a" apply-apply rule unfolding fun_eq_iff unfolding a'_def k(2)
apply(erule_tac x=l in allE) by auto
have "a' \<notin> s" apply(rule) apply(drule ksimplexD(6)[OF assms(1),rule_format,OF `a\<in>s`]) proof(cases "kle n a a'")
case goal2 hence "kle n a' a" by auto thus False apply(drule_tac kle_imp_pointwise)
@@ -877,22 +877,22 @@
have uxv:"\<And>x. kle n u x \<Longrightarrow> kle n x v \<Longrightarrow> (x = u) \<or> (x = a) \<or> (x = a') \<or> (x = v)"
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 ext_iff
+ have "x = u" unfolding fun_eq_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 \<noteq> u l" "x k = u k"
- have "x = a'" unfolding ext_iff unfolding a'_def
+ have "x = a'" unfolding fun_eq_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 \<noteq> u k"
- have "x = a" unfolding ext_iff
+ have "x = a" unfolding fun_eq_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 \<noteq> u l" "x k \<noteq> u k"
- have "x = v" unfolding ext_iff
+ have "x = v" unfolding fun_eq_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\<noteq>l` by auto qed thus ?case by auto qed qed
@@ -935,9 +935,9 @@
moreover have "?A \<subseteq> {s, insert a' (s - {a})}" apply(rule) unfolding mem_Collect_eq proof(erule conjE)
fix s' assume as:"ksimplex p n s'" and "\<exists>b\<in>s'. s' - {b} = s - {a}"
from this(2) guess a'' .. note a''=this
- have "u\<noteq>v" unfolding ext_iff unfolding l(2) k(2) by auto
+ have "u\<noteq>v" unfolding fun_eq_iff unfolding l(2) k(2) by auto
hence uv':"\<not> kle n v u" using uv using kle_antisym by auto
- have "u\<noteq>a" "v\<noteq>a" unfolding ext_iff k(2) l(2) by auto
+ have "u\<noteq>a" "v\<noteq>a" unfolding fun_eq_iff k(2) l(2) by auto
hence uvs':"u\<in>s'" "v\<in>s'" using `u\<in>s` `v\<in>s` using a'' by auto
have lem6:"a \<in> s' \<or> a' \<in> s'" proof(cases "\<forall>x\<in>s'. kle n x u \<or> kle n v x")
case False then guess w unfolding ball_simps .. note w=this
@@ -1052,7 +1052,7 @@
shows "odd (card {s. ksimplex p (n+1) s \<and>((reduced lab (n+1)) ` s = {0..n+1})})" proof-
have *:"\<And>s t. odd (card s) \<Longrightarrow> s = t \<Longrightarrow> odd (card t)" "\<And>s f. (\<And>x. f x \<le> n +1 ) \<Longrightarrow> f ` s \<subseteq> {0..n+1}" by auto
show ?thesis apply(rule kuhn_simplex_lemma[unfolded mem_Collect_eq]) apply(rule,rule,rule *,rule reduced_labelling)
- apply(rule *(1)[OF assms(4)]) apply(rule set_ext) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof-(*(rule,rule)*)
+ apply(rule *(1)[OF assms(4)]) apply(rule set_eqI) unfolding mem_Collect_eq apply(rule,erule conjE) defer apply(rule) proof-(*(rule,rule)*)
fix f assume as:"ksimplex p n f" "reduced lab n ` f = {0..n}"
have *:"\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = 0 \<longrightarrow> lab x j = 0" "\<forall>x\<in>f. \<forall>j\<in>{1..n + 1}. x j = p \<longrightarrow> lab x j = 1"
using assms(2-3) using as(1)[unfolded ksimplex_def] by auto
@@ -1060,7 +1060,7 @@
{ fix x assume "x\<in>f" hence "reduced lab (n + 1) x < n + 1" apply-apply(rule reduced_labelling_1)
defer using assms(3) using as(1)[unfolded ksimplex_def] by auto
hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc) using reduced_labelling(1) by auto }
- hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[THEN sym] apply- apply(rule set_ext) unfolding image_iff by auto
+ hence "reduced lab (n + 1) ` f = {0..n}" unfolding as(2)[THEN sym] apply- apply(rule set_eqI) unfolding image_iff by auto
moreover guess s using as(1)[unfolded simplex_top_face[OF assms(1) allp,THEN sym]] .. then guess a ..
ultimately show "\<exists>s a. ksimplex p (n + 1) s \<and>
a \<in> s \<and> f = s - {a} \<and> reduced lab (n + 1) ` f = {0..n} \<and> ((\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0) \<or> (\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = p))" (is ?ex)
@@ -1072,7 +1072,7 @@
hence "reduced lab (n + 1) x < n + 1" using sa(4) by auto
hence "reduced lab (n + 1) x = reduced lab n x" apply-apply(rule reduced_labelling_Suc)
using reduced_labelling(1) by auto }
- thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[THEN sym] apply-apply(rule set_ext) unfolding image_iff by auto
+ thus part1:"reduced lab n ` f = {0..n}" unfolding sa(4)[THEN sym] apply-apply(rule set_eqI) unfolding image_iff by auto
have *:"\<forall>x\<in>f. x (n + 1) = p" proof(cases "\<exists>j\<in>{1..n + 1}. \<forall>x\<in>f. x j = 0")
case True then guess j .. hence "\<And>x. x\<in>f \<Longrightarrow> reduced lab (n + 1) x \<noteq> j - 1" apply-apply(rule reduced_labelling_0) apply assumption
apply(rule assms(2)[rule_format]) using sa(1)[unfolded ksimplex_def] unfolding sa by auto moreover
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Sep 13 11:13:25 2010 +0200
@@ -880,7 +880,7 @@
by (simp add: row_def column_def transpose_def Cart_eq)
lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
-by (auto simp add: rows_def columns_def row_transpose intro: set_ext)
+by (auto simp add: rows_def columns_def row_transpose intro: set_eqI)
lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose)
@@ -986,7 +986,7 @@
subsection {* Standard bases are a spanning set, and obviously finite. *}
lemma span_stdbasis:"span {cart_basis i :: real^'n | i. i \<in> (UNIV :: 'n set)} = UNIV"
-apply (rule set_ext)
+apply (rule set_eqI)
apply auto
apply (subst basis_expansion'[symmetric])
apply (rule span_setsum)
@@ -1440,12 +1440,12 @@
lemma interval_cart: fixes a :: "'a::ord^'n" shows
"{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
"{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
- by (auto simp add: set_ext_iff vector_less_def vector_le_def)
+ by (auto simp add: set_eq_iff vector_less_def vector_le_def)
lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows
"x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
"x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
- using interval_cart[of a b] by(auto simp add: set_ext_iff vector_less_def vector_le_def)
+ using interval_cart[of a b] by(auto simp add: set_eq_iff vector_less_def vector_le_def)
lemma interval_eq_empty_cart: fixes a :: "real^'n" shows
"({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
@@ -1498,7 +1498,7 @@
lemma interval_sing: fixes a :: "'a::linorder^'n" shows
"{a .. a} = {a} \<and> {a<..<a} = {}"
-apply(auto simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
+apply(auto simp add: set_eq_iff vector_less_def vector_le_def Cart_eq)
apply (simp add: order_eq_iff)
apply (auto simp add: not_less less_imp_le)
done
@@ -1511,17 +1511,17 @@
{ fix i
have "a $ i \<le> x $ i"
using x order_less_imp_le[of "a$i" "x$i"]
- by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
+ by(simp add: set_eq_iff vector_less_def vector_le_def Cart_eq)
}
moreover
{ fix i
have "x $ i \<le> b $ i"
using x order_less_imp_le[of "x$i" "b$i"]
- by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
+ by(simp add: set_eq_iff vector_less_def vector_le_def Cart_eq)
}
ultimately
show "a \<le> x \<and> x \<le> b"
- by(simp add: set_ext_iff vector_less_def vector_le_def Cart_eq)
+ by(simp add: set_eq_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} \<inter> {c .. d} = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
- unfolding set_ext_iff and Int_iff and mem_interval_cart
+ unfolding set_eq_iff and Int_iff and mem_interval_cart
by auto
lemma closed_interval_left_cart: fixes b::"real^'n"
@@ -1656,7 +1656,7 @@
shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
"(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id"
using m0
-apply (auto simp add: ext_iff vector_add_ldistrib)
+apply (auto simp add: fun_eq_iff vector_add_ldistrib)
by (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1[symmetric])
lemma vector_affinity_eq:
@@ -1712,7 +1712,7 @@
lemma unit_interval_convex_hull_cart:
"{0::real^'n .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}" (is "?int = convex hull ?points")
unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"]
- apply(rule arg_cong[where f="\<lambda>x. convex hull x"]) apply(rule set_ext) unfolding mem_Collect_eq
+ apply(rule arg_cong[where f="\<lambda>x. convex hull x"]) apply(rule set_eqI) unfolding mem_Collect_eq
apply safe apply(erule_tac x="\<pi>' i" in allE) unfolding nth_conv_component defer
apply(erule_tac x="\<pi> i" in allE) by auto
@@ -1974,7 +1974,7 @@
apply (simp add: forall_3)
done
-lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
+lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_eqI,rule) unfolding image_iff defer
apply(rule_tac x="dest_vec1 x" in bexI) by auto
lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
@@ -2069,7 +2069,7 @@
lemma vec1_interval:fixes a::"real" shows
"vec1 ` {a .. b} = {vec1 a .. vec1 b}"
"vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
- apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval_cart
+ apply(rule_tac[!] set_eqI) unfolding image_iff vector_less_def unfolding mem_interval_cart
unfolding forall_1 unfolding vec1_dest_vec1_simps
apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
apply(rule_tac x="dest_vec1 x" in bexI) by auto
@@ -2119,10 +2119,10 @@
lemma open_closed_interval_1: fixes a :: "real^1" shows
"{a<..<b} = {a .. b} - {a, b}"
- 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)
+ unfolding set_eq_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 closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
- 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)
+ unfolding set_eq_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 \<Rightarrow> real^1" shows
"(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
@@ -2284,7 +2284,7 @@
lemma interval_split_cart:
"{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
"{a..b} \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
- apply(rule_tac[!] set_ext) unfolding Int_iff mem_interval_cart mem_Collect_eq
+ apply(rule_tac[!] set_eqI) unfolding Int_iff mem_interval_cart mem_Collect_eq
unfolding Cart_lambda_beta by auto
(*lemma content_split_cart:
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Sep 13 11:13:25 2010 +0200
@@ -191,7 +191,7 @@
lemma affine_hull_finite:
assumes "finite s"
shows "affine hull s = {y. \<exists>u. setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
- unfolding affine_hull_explicit and set_ext_iff and mem_Collect_eq apply (rule,rule)
+ unfolding affine_hull_explicit and set_eq_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" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"
thus "\<exists>sa u. finite sa \<and> \<not> (\<forall>x. (x \<in> sa) = (x \<in> {})) \<and> sa \<subseteq> s \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = x"
@@ -709,7 +709,7 @@
ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastsimp
hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto }
- ultimately show ?thesis unfolding set_ext_iff by blast
+ ultimately show ?thesis unfolding set_eq_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. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> DIM('a) + 1 \<and>
(\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
- unfolding convex_hull_explicit set_ext_iff mem_Collect_eq
+ unfolding convex_hull_explicit set_eq_iff mem_Collect_eq
proof(rule,rule)
fix y let ?P = "\<lambda>n. \<exists>s u. finite s \<and> card s = n \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
assume "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = y"
@@ -939,7 +939,7 @@
lemma caratheodory:
"convex hull p = {x::'a::euclidean_space. \<exists>s. finite s \<and> s \<subseteq> p \<and>
card s \<le> DIM('a) + 1 \<and> x \<in> convex hull s}"
- unfolding set_ext_iff apply(rule, rule) unfolding mem_Collect_eq proof-
+ unfolding set_eq_iff apply(rule, rule) unfolding mem_Collect_eq proof-
fix x assume "x \<in> convex hull p"
then obtain s u where "finite s" "s \<subseteq> p" "card s \<le> DIM('a) + 1"
"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>s. u v *\<^sub>R v) = x"unfolding convex_hull_caratheodory by auto
@@ -1000,7 +1000,7 @@
let ?X = "{0..1} \<times> s \<times> t"
let ?h = "(\<lambda>z. (1 - fst z) *\<^sub>R fst (snd z) + fst z *\<^sub>R snd (snd z))"
have *:"{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t} = ?h ` ?X"
- apply(rule set_ext) unfolding image_iff mem_Collect_eq
+ apply(rule set_eqI) unfolding image_iff mem_Collect_eq
apply rule apply auto
apply (rule_tac x=u in rev_bexI, simp)
apply (erule rev_bexI, erule rev_bexI, simp)
@@ -1029,7 +1029,7 @@
case (Suc n)
show ?case proof(cases "n=0")
case True have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} = s"
- unfolding set_ext_iff and mem_Collect_eq proof(rule, rule)
+ unfolding set_eq_iff and mem_Collect_eq proof(rule, rule)
fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
show "x\<in>s" proof(cases "card t = 0")
@@ -1048,7 +1048,7 @@
case False have "{x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t} =
{ (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u.
0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> {x. \<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> x \<in> convex hull t}}"
- unfolding set_ext_iff and mem_Collect_eq proof(rule,rule)
+ unfolding set_eq_iff and mem_Collect_eq proof(rule,rule)
fix x assume "\<exists>u v c. x = (1 - c) *\<^sub>R u + c *\<^sub>R v \<and>
0 \<le> c \<and> c \<le> 1 \<and> u \<in> s \<and> (\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> n \<and> v \<in> convex hull t)"
then obtain u v c t where obt:"x = (1 - c) *\<^sub>R u + c *\<^sub>R v"
@@ -1531,7 +1531,7 @@
fixes s :: "('a::euclidean_space) set"
assumes "closed s" "convex s"
shows "s = \<Inter> {h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
- apply(rule set_ext, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof-
+ apply(rule set_eqI, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof-
fix x assume "\<forall>xa. s \<subseteq> xa \<and> (\<exists>a b. xa = {x. inner a x \<le> b}) \<longrightarrow> x \<in> xa"
hence "\<forall>a b. s \<subseteq> {x. inner a x \<le> b} \<longrightarrow> x \<in> {x. inner a x \<le> b}" by blast
thus "x\<in>s" apply(rule_tac ccontr) apply(drule separating_hyperplane_closed_point[OF assms(2,1)])
@@ -1752,7 +1752,7 @@
have "\<exists>surf. homeomorphism (frontier s) sphere pi surf"
apply(rule homeomorphism_compact) apply(rule compact_frontier[OF assms(1)])
- apply(rule continuous_on_subset[OF contpi]) defer apply(rule set_ext,rule)
+ apply(rule continuous_on_subset[OF contpi]) defer apply(rule set_eqI,rule)
unfolding inj_on_def prefer 3 apply(rule,rule,rule)
proof- fix x assume "x\<in>pi ` frontier s" then obtain y where "y\<in>frontier s" "x = pi y" by auto
thus "x \<in> sphere" using pi(1)[of y] and `0 \<notin> frontier s` by auto
@@ -1813,7 +1813,7 @@
qed } note hom2 = this
show ?thesis apply(subst homeomorphic_sym) apply(rule homeomorphic_compact[where f="\<lambda>x. norm x *\<^sub>R surf (pi x)"])
- apply(rule compact_cball) defer apply(rule set_ext, rule, erule imageE, drule hom)
+ apply(rule compact_cball) defer apply(rule set_eqI, rule, erule imageE, drule hom)
prefer 4 apply(rule continuous_at_imp_continuous_on, rule) apply(rule_tac [3] hom2) proof-
fix x::"'a" assume as:"x \<in> cball 0 1"
thus "continuous (at x) (\<lambda>x. norm x *\<^sub>R surf (pi x))" proof(cases "x=0")
@@ -2119,7 +2119,7 @@
assumes "0 < d" obtains s::"('a::ordered_euclidean_space) set" where
"finite s" "{x - (\<chi>\<chi> i. d) .. x + (\<chi>\<chi> i. d)} = convex hull s" proof-
let ?d = "(\<chi>\<chi> i. d)::'a"
- have *:"{x - ?d .. x + ?d} = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. \<chi>\<chi> i. 1}" apply(rule set_ext, rule)
+ have *:"{x - ?d .. x + ?d} = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. \<chi>\<chi> i. 1}" apply(rule set_eqI, rule)
unfolding image_iff defer apply(erule bexE) proof-
fix y assume as:"y\<in>{x - ?d .. x + ?d}"
{ fix i assume i:"i<DIM('a)" have "x $$ i \<le> d + y $$ i" "y $$ i \<le> d + x $$ i"
@@ -2329,7 +2329,7 @@
"closed_segment a b = convex hull {a,b}" proof-
have *:"\<And>x. {x} \<noteq> {}" by auto
have **:"\<And>u v. u + v = 1 \<longleftrightarrow> u = 1 - (v::real)" by auto
- show ?thesis unfolding segment convex_hull_insert[OF *] convex_hull_singleton apply(rule set_ext)
+ show ?thesis unfolding segment convex_hull_insert[OF *] convex_hull_singleton apply(rule set_eqI)
unfolding mem_Collect_eq apply(rule,erule exE)
apply(rule_tac x="1 - u" in exI) apply rule defer apply(rule_tac x=u in exI) defer
apply(erule exE, (erule conjE)?)+ apply(rule_tac x="1 - u" in exI) unfolding ** by auto qed
@@ -2454,7 +2454,7 @@
lemma simplex:
assumes "finite s" "0 \<notin> s"
shows "convex hull (insert 0 s) = { y. (\<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s \<le> 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y)}"
- unfolding convex_hull_finite[OF finite.insertI[OF assms(1)]] apply(rule set_ext, rule) unfolding mem_Collect_eq
+ unfolding convex_hull_finite[OF finite.insertI[OF assms(1)]] apply(rule set_eqI, rule) unfolding mem_Collect_eq
apply(erule_tac[!] exE) apply(erule_tac[!] conjE)+ unfolding setsum_clauses(2)[OF assms(1)]
apply(rule_tac x=u in exI) defer apply(rule_tac x="\<lambda>x. if x = 0 then 1 - setsum u s else u x" in exI) using assms(2)
unfolding if_smult and setsum_delta_notmem[OF assms(2)] by auto
@@ -2467,7 +2467,7 @@
have *:"finite ?p" "0\<notin>?p" by auto
have "{(basis i)::'a |i. i<DIM('a)} = basis ` ?D" by auto
note sumbas = this setsum_reindex[OF basis_inj, unfolded o_def]
- show ?thesis unfolding simplex[OF *] apply(rule set_ext) unfolding mem_Collect_eq apply rule
+ show ?thesis unfolding simplex[OF *] apply(rule set_eqI) unfolding mem_Collect_eq apply rule
apply(erule exE, (erule conjE)+) apply(erule_tac[2] conjE)+ proof-
fix x::"'a" and u assume as: "\<forall>x\<in>{basis i |i. i<DIM('a)}. 0 \<le> u x"
"setsum u {basis i |i. i<DIM('a)} \<le> 1" "(\<Sum>x\<in>{basis i |i. i<DIM('a)}. u x *\<^sub>R x) = x"
@@ -2500,7 +2500,7 @@
lemma interior_std_simplex:
"interior (convex hull (insert 0 { basis i| i. i<DIM('a)})) =
{x::'a::euclidean_space. (\<forall>i<DIM('a). 0 < x$$i) \<and> setsum (\<lambda>i. x$$i) {..<DIM('a)} < 1 }"
- apply(rule set_ext) unfolding mem_interior std_simplex unfolding subset_eq mem_Collect_eq Ball_def mem_ball
+ apply(rule set_eqI) unfolding mem_interior std_simplex unfolding subset_eq mem_Collect_eq Ball_def mem_ball
unfolding Ball_def[symmetric] apply rule apply(erule exE, (erule conjE)+) defer apply(erule conjE) proof-
fix x::"'a" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x<DIM('a). 0 \<le> xa $$ x) \<and> setsum (op $$ xa) {..<DIM('a)} \<le> 1"
show "(\<forall>xa<DIM('a). 0 < x $$ xa) \<and> setsum (op $$ x) {..<DIM('a)} < 1" apply(safe) proof-
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Sep 13 11:13:25 2010 +0200
@@ -665,7 +665,7 @@
have "\<forall>i<DIM('a). f' (basis i) = 0"
by (simp add: euclidean_eq[of _ "0::'a"])
with derivative_is_linear[OF deriv, THEN linear_componentwise, of _ 0]
- show ?thesis by (simp add: ext_iff)
+ show ?thesis by (simp add: fun_eq_iff)
qed
lemma rolle: fixes f::"real\<Rightarrow>real"
@@ -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 ext_iff)
+ from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def fun_eq_iff)
by metis
from linear_surjective_isomorphism[OF lf fi]
obtain h:: "'a => 'a" where
h: "linear h" "\<forall>x. h (f x) = x" "\<forall>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 ext_iff)
+ apply (simp add: o_def id_def fun_eq_iff)
by metis
with h(1) show ?thesis by blast
qed
@@ -1268,7 +1268,7 @@
have "(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
using assms [unfolded has_vector_derivative_def]
by (rule frechet_derivative_unique_at)
- thus ?thesis unfolding ext_iff by auto
+ thus ?thesis unfolding fun_eq_iff by auto
qed
lemma vector_derivative_unique_within_closed_interval: fixes f::"real \<Rightarrow> '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' \<noteq> f''" moreover
- hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1" using * by (auto simp: ext_iff)
+ hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1" using * by (auto simp: fun_eq_iff)
ultimately show False unfolding o_def by auto qed qed
lemma vector_derivative_at:
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Mon Sep 13 11:13:25 2010 +0200
@@ -141,7 +141,7 @@
{fix i assume i: "i \<in> ?U"
from i permutes_inv_o[OF pU] permutes_in_image[OF pU]
have "((\<lambda>i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)"
- unfolding transpose_def by (simp add: ext_iff)}
+ unfolding transpose_def by (simp add: fun_eq_iff)}
then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
qed
finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth
@@ -207,7 +207,7 @@
have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
{fix p assume p: "p \<in> ?PU - {id}"
then have "p \<noteq> id" by simp
- then obtain i where i: "p i \<noteq> i" unfolding ext_iff by auto
+ then obtain i where i: "p i \<noteq> i" unfolding fun_eq_iff by auto
from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast
from setprod_zero [OF fU ex] have "?pp p = 0" by simp}
then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0" by blast
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Sep 13 11:13:25 2010 +0200
@@ -1112,7 +1112,7 @@
done}
moreover
{fix x assume x: "x \<in> span S"
- have th0:"(\<lambda>a. f a \<in> span (f ` S)) = {x. f x \<in> span (f ` S)}" apply (rule set_ext)
+ have th0:"(\<lambda>a. f a \<in> span (f ` S)) = {x. f x \<in> span (f ` S)}" apply (rule set_eqI)
unfolding mem_def Collect_def ..
have "f x \<in> span (f ` S)"
apply (rule span_induct[where S=S])
@@ -2363,7 +2363,7 @@
apply (rule span_mul)
by (rule span_superset)}
then have SC: "span ?C = span (insert a B)"
- unfolding set_ext_iff span_breakdown_eq C(3)[symmetric] by auto
+ unfolding set_eq_iff span_breakdown_eq C(3)[symmetric] by auto
thm pairwise_def
{fix x y assume xC: "x \<in> ?C" and yC: "y \<in> ?C" and xy: "x \<noteq> y"
{assume xa: "x = ?a" and ya: "y = ?a"
@@ -2826,7 +2826,7 @@
" \<forall>x \<in> f ` basis ` {..<DIM('a)}. h x = inv f x" by blast
from h(2)
have th: "\<forall>i<DIM('a). (h \<circ> f) (basis i) = id (basis i)"
- using inv_o_cancel[OF fi, unfolded ext_iff id_def o_def]
+ using inv_o_cancel[OF fi, unfolded fun_eq_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" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
from h(2)
have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
- using sf by(auto simp add: surj_iff o_def ext_iff)
+ using sf by(auto simp add: surj_iff o_def fun_eq_iff)
from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
have "f o h = id" .
then show ?thesis using h(1) by blast
@@ -2970,7 +2970,7 @@
lemma isomorphism_expand:
"f o g = id \<and> g o f = id \<longleftrightarrow> (\<forall>x. f(g x) = x) \<and> (\<forall>x. g(f x) = x)"
- by (simp add: ext_iff o_def id_def)
+ by (simp add: fun_eq_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 ext_iff id_def surj_def)
+ apply (auto simp add: o_def fun_eq_iff id_def surj_def)
by metis
from linear_surjective_isomorphism[OF lf(1) sf] lf f
- have "f' o f = id" unfolding ext_iff o_def id_def
+ have "f' o f = id" unfolding fun_eq_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 ext_iff)
+ from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def fun_eq_iff)
by metis
from linear_injective_isomorphism[OF lf fi]
obtain h:: "'a \<Rightarrow> 'a" where
h: "linear h" "\<forall>x. h (f x) = x" "\<forall>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 ext_iff)
+ apply (simp add: o_def id_def fun_eq_iff)
by metis
with h(1) show ?thesis by blast
qed
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Sep 13 11:13:25 2010 +0200
@@ -34,7 +34,7 @@
apply(subst infnorm_eq_0[THEN sym]) by auto
let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
- apply(rule set_ext) unfolding image_iff Bex_def mem_interval_cart apply rule defer
+ apply(rule set_eqI) unfolding image_iff Bex_def mem_interval_cart apply rule defer
apply(rule_tac x="vec x" in exI) by auto
{ fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
then guess w unfolding image_iff .. note w = this
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon Sep 13 11:13:25 2010 +0200
@@ -42,7 +42,7 @@
by (auto intro: ext)
lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
- by (simp add: Cart_nth_inject [symmetric] ext_iff)
+ by (simp add: Cart_nth_inject [symmetric] fun_eq_iff)
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i"
by (simp add: Cart_lambda_inverse)
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Sep 13 11:13:25 2010 +0200
@@ -102,7 +102,7 @@
abbreviation One where "One \<equiv> ((\<chi>\<chi> i. 1)::_::ordered_euclidean_space)"
lemma empty_as_interval: "{} = {One..0}"
- apply(rule set_ext,rule) defer unfolding mem_interval
+ apply(rule set_eqI,rule) defer unfolding mem_interval
using UNIV_witness[where 'a='n] apply(erule_tac exE,rule_tac x=x in allE) by auto
lemma interior_subset_union_intervals:
@@ -367,7 +367,7 @@
let ?A = "{s. s \<in> (\<lambda>(k1,k2). k1 \<inter> k2) ` (p1 \<times> p2) \<and> s \<noteq> {}}" have *:"?A' = ?A" by auto
show ?thesis unfolding * proof(rule division_ofI) have "?A \<subseteq> (\<lambda>(x, y). x \<inter> y) ` (p1 \<times> p2)" by auto
moreover have "finite (p1 \<times> p2)" using assms unfolding division_of_def by auto ultimately show "finite ?A" by auto
- have *:"\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s" by auto show "\<Union>?A = s1 \<inter> s2" apply(rule set_ext) unfolding * and Union_image_eq UN_iff
+ have *:"\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s" by auto show "\<Union>?A = s1 \<inter> s2" apply(rule set_eqI) unfolding * and Union_image_eq UN_iff
using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
{ fix k assume "k\<in>?A" then obtain k1 k2 where k:"k = k1 \<inter> k2" "k1\<in>p1" "k2\<in>p2" "k\<noteq>{}" by auto thus "k \<noteq> {}" by auto
show "k \<subseteq> s1 \<inter> s2" using division_ofD(2)[OF assms(1) k(2)] and division_ofD(2)[OF assms(2) k(3)] unfolding k by auto
@@ -1035,7 +1035,7 @@
next assume as:"c $$ i = (a $$ i + b $$ i) / 2" "d $$ i = b $$ i"
show False using e_f(2)[of i] and i x unfolding as by(fastsimp simp add:field_simps)
qed qed qed
- also have "\<Union> ?A = {a..b}" proof(rule set_ext,rule)
+ also have "\<Union> ?A = {a..b}" proof(rule set_eqI,rule)
fix x assume "x\<in>\<Union>?A" then guess Y unfolding Union_iff ..
from this(1) guess c unfolding mem_Collect_eq .. then guess d ..
note c_d = this[THEN conjunct2,rule_format] `x\<in>Y`[unfolded this[THEN conjunct1]]
@@ -1402,7 +1402,7 @@
apply(rule integral_unique) using has_integral_empty .
lemma has_integral_refl[intro]: shows "(f has_integral 0) {a..a}" "(f has_integral 0) {a::'a::ordered_euclidean_space}"
-proof- have *:"{a} = {a..a}" apply(rule set_ext) unfolding mem_interval singleton_iff euclidean_eq[where 'a='a]
+proof- have *:"{a} = {a..a}" apply(rule set_eqI) unfolding mem_interval singleton_iff euclidean_eq[where 'a='a]
apply safe prefer 3 apply(erule_tac x=i in allE) by(auto simp add: field_simps)
show "(f has_integral 0) {a..a}" "(f has_integral 0) {a}" unfolding *
apply(rule_tac[!] has_integral_null) unfolding content_eq_0_interior
@@ -1466,7 +1466,7 @@
lemma interval_split: fixes a::"'a::ordered_euclidean_space" assumes "k<DIM('a)" shows
"{a..b} \<inter> {x. x$$k \<le> c} = {a .. (\<chi>\<chi> i. if i = k then min (b$$k) c else b$$i)}"
"{a..b} \<inter> {x. x$$k \<ge> c} = {(\<chi>\<chi> i. if i = k then max (a$$k) c else a$$i) .. b}"
- apply(rule_tac[!] set_ext) unfolding Int_iff mem_interval mem_Collect_eq using assms by auto
+ apply(rule_tac[!] set_eqI) unfolding Int_iff mem_interval mem_Collect_eq using assms by auto
lemma content_split: fixes a::"'a::ordered_euclidean_space" assumes "k<DIM('a)" shows
"content {a..b} = content({a..b} \<inter> {x. x$$k \<le> c}) + content({a..b} \<inter> {x. x$$k >= c})"
@@ -2494,7 +2494,7 @@
note division_split(1)[OF assms, where c="c+e",unfolded interval_split[OF k]]
note division_split(2)[OF this, where c="c-e" and k=k,OF k]
thus ?thesis apply(rule **) using k apply- unfolding interval_doublesplit unfolding * unfolding interval_split interval_doublesplit
- apply(rule set_ext) unfolding mem_Collect_eq apply rule apply(erule conjE exE)+ apply(rule_tac x=la in exI) defer
+ apply(rule set_eqI) unfolding mem_Collect_eq apply rule apply(erule conjE exE)+ apply(rule_tac x=la in exI) defer
apply(erule conjE exE)+ apply(rule_tac x="l \<inter> {x. c + e \<ge> x $$ k}" in exI) apply rule defer apply rule
apply(rule_tac x=l in exI) by blast+ qed
@@ -2538,7 +2538,7 @@
apply(cases,rule disjI1,assumption,rule disjI2)
proof- fix x l assume as:"(x,l)\<in>p" "?i x \<noteq> 0" hence xk:"x$$k = c" unfolding indicator_def apply-by(rule ccontr,auto)
show "content l = content (l \<inter> {x. \<bar>x $$ k - c\<bar> \<le> d})" apply(rule arg_cong[where f=content])
- apply(rule set_ext,rule,rule) unfolding mem_Collect_eq
+ apply(rule set_eqI,rule,rule) unfolding mem_Collect_eq
proof- fix y assume y:"y\<in>l" note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(1),unfolded split_conv]
note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y] note le_less_trans[OF component_le_norm[of _ k] this]
thus "\<bar>y $$ k - c\<bar> \<le> d" unfolding euclidean_simps xk by auto
@@ -3280,7 +3280,7 @@
proof(cases "{a..b}={}") case True thus ?thesis unfolding True by auto
next have *:"\<And>P Q. (\<forall>i<DIM('a). P i) \<and> (\<forall>i<DIM('a). Q i) \<longleftrightarrow> (\<forall>i<DIM('a). P i \<and> Q i)" by auto
case False note ab = this[unfolded interval_ne_empty]
- show ?thesis apply-apply(rule set_ext)
+ show ?thesis apply-apply(rule set_eqI)
proof- fix x::"'a" have **:"\<And>P Q. (\<forall>i<DIM('a). P i = Q i) \<Longrightarrow> (\<forall>i<DIM('a). P i) = (\<forall>i<DIM('a). Q i)" by auto
show "x \<in> ?l \<longleftrightarrow> x \<in> ?r" unfolding if_not_P[OF False]
unfolding image_iff mem_interval Bex_def euclidean_simps euclidean_eq[where 'a='a] *
@@ -3334,7 +3334,7 @@
subsection {* even more special cases. *}
lemma uminus_interval_vector[simp]:"uminus ` {a..b} = {-b .. -a::'a::ordered_euclidean_space}"
- apply(rule set_ext,rule) defer unfolding image_iff
+ apply(rule set_eqI,rule) defer unfolding image_iff
apply(rule_tac x="-x" in bexI) by(auto simp add:minus_le_iff le_minus_iff eucl_le[where 'a='a])
lemma has_integral_reflect_lemma[intro]: assumes "(f has_integral i) {a..b}"
@@ -3694,7 +3694,7 @@
let ?thesis = "\<exists>d>0. \<forall>x'\<in>{a..b}. dist x' x < d \<longrightarrow> dist (integral {a..x'} f) (integral {a..x} f) < e"
{ presume *:"a<b \<Longrightarrow> ?thesis"
show ?thesis apply(cases,rule *,assumption)
- proof- case goal1 hence "{a..b} = {x}" using as(1) apply-apply(rule set_ext)
+ proof- case goal1 hence "{a..b} = {x}" using as(1) apply-apply(rule set_eqI)
unfolding atLeastAtMost_iff by(auto simp only:field_simps not_less DIM_real)
thus ?case using `e>0` by auto
qed } assume "a<b"
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Sep 13 11:13:25 2010 +0200
@@ -123,7 +123,7 @@
qed (auto simp add:le_less joinpaths_def) qed
next assume as:"continuous_on {0..1} g1" "continuous_on {0..1} g2"
have *:"{0 .. 1::real} = {0.. (1/2)*\<^sub>R 1} \<union> {(1/2) *\<^sub>R 1 .. 1}" by auto
- have **:"op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}" apply(rule set_ext, rule) unfolding image_iff
+ have **:"op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}" apply(rule set_eqI, rule) unfolding image_iff
defer apply(rule_tac x="(1/2)*\<^sub>R x" in bexI) by auto
have ***:"(\<lambda>x. 2 *\<^sub>R x - 1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real}"
apply (auto simp add: image_def)
@@ -322,7 +322,7 @@
unfolding path_def by(rule continuous_on_linepath)
lemma path_image_linepath[simp]: "path_image(linepath a b) = (closed_segment a b)"
- unfolding path_image_def segment linepath_def apply (rule set_ext, rule) defer
+ unfolding path_image_def segment linepath_def apply (rule set_eqI, rule) defer
unfolding mem_Collect_eq image_iff apply(erule exE) apply(rule_tac x="u *\<^sub>R 1" in bexI)
by auto
@@ -388,7 +388,7 @@
subsection {* Can also consider it as a set, as the name suggests. *}
lemma path_component_set: "path_component s x = { y. (\<exists>g. path g \<and> path_image g \<subseteq> s \<and> pathstart g = x \<and> pathfinish g = y )}"
- apply(rule set_ext) unfolding mem_Collect_eq unfolding mem_def path_component_def by auto
+ apply(rule set_eqI) unfolding mem_Collect_eq unfolding mem_def path_component_def by auto
lemma mem_path_component_set:"x \<in> path_component s y \<longleftrightarrow> path_component s y x" unfolding mem_def by auto
@@ -564,9 +564,9 @@
thus ?thesis using path_connected_singleton by simp
next
assume r: "0 < r"
- hence *:"{x::'a. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" apply -apply(rule set_ext,rule)
+ hence *:"{x::'a. norm(x - a) = r} = (\<lambda>x. a + r *\<^sub>R x) ` {x. norm x = 1}" apply -apply(rule set_eqI,rule)
unfolding image_iff apply(rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR by (auto simp add: scaleR_right_diff_distrib)
- have **:"{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule)
+ have **:"{x::'a. norm x = 1} = (\<lambda>x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_eqI,rule)
unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm)
have "continuous_on (UNIV - {0}) (\<lambda>x::'a. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within
apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Sep 13 11:13:25 2010 +0200
@@ -40,7 +40,7 @@
{assume "T1=T2" hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp}
moreover
{assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
- hence "openin T1 = openin T2" by (metis mem_def set_ext)
+ hence "openin T1 = openin T2" by (metis mem_def set_eqI)
hence "topology (openin T1) = topology (openin T2)" by simp
hence "T1 = T2" unfolding openin_inverse .}
ultimately show ?thesis by blast
@@ -141,7 +141,7 @@
moreover
{fix K assume K: "K \<subseteq> ?L"
have th0: "?L = (\<lambda>S. S \<inter> V) ` openin U "
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (simp add: Ball_def image_iff)
by (metis mem_def)
from K[unfolded th0 subset_image_iff]
@@ -213,7 +213,7 @@
lemma topspace_euclidean: "topspace euclidean = UNIV"
apply (simp add: topspace_def)
- apply (rule set_ext)
+ apply (rule set_eqI)
by (auto simp add: open_openin[symmetric])
lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
@@ -253,10 +253,10 @@
lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq)
lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
- by (simp add: set_ext_iff) arith
+ by (simp add: set_eq_iff) arith
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
- by (simp add: set_ext_iff)
+ by (simp add: set_eq_iff)
lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
"(a::real) - b < 0 \<longleftrightarrow> a < b"
@@ -289,7 +289,7 @@
by (metis open_contains_ball subset_eq centre_in_ball)
lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
- unfolding mem_ball set_ext_iff
+ unfolding mem_ball set_eq_iff
apply (simp add: not_less)
by (metis zero_le_dist order_trans dist_self)
@@ -447,7 +447,7 @@
let ?T = "\<Union>{S. open S \<and> a \<notin> S}"
have "open ?T" by (simp add: open_Union)
also have "?T = - {a}"
- by (simp add: set_ext_iff separation_t1, auto)
+ by (simp add: set_eq_iff separation_t1, auto)
finally show "closed {a}" unfolding closed_def .
qed
@@ -483,7 +483,7 @@
==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
have "open ?U \<and> open ?V \<and> x \<in> ?U \<and> y \<in> ?V \<and> ?U \<inter> ?V = {}"
using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute]
- by (auto simp add: set_ext_iff)
+ by (auto simp add: set_eq_iff)
then show "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {}"
by blast
qed
@@ -641,7 +641,7 @@
definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
- apply (simp add: set_ext_iff interior_def)
+ apply (simp add: set_eq_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 \<notin> interior S"
with `x \<in> R` `open R` obtain y where "y \<in> R - S"
- unfolding interior_def set_ext_iff by fast
+ unfolding interior_def set_eq_iff by fast
from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
@@ -1006,7 +1006,7 @@
unfolding trivial_limit_def
unfolding eventually_within eventually_at_topological
unfolding islimpt_def
- apply (clarsimp simp add: set_ext_iff)
+ apply (clarsimp simp add: set_eq_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: set_ext_iff)
+ apply (simp add: set_eq_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: set_ext_iff)
+ apply (simp add: set_eq_iff)
by arith
lemma cball_eq_empty: "(cball x e = {}) \<longleftrightarrow> e < 0"
- apply (simp add: set_ext_iff not_le)
+ apply (simp add: set_eq_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 \<noteq> x" "dist a x < e"
using perfect_choose_dist [OF e] by auto
hence "a \<noteq> x" "dist x a \<le> e" by (auto simp add: dist_commute)
- with e show ?thesis by (auto simp add: set_ext_iff)
+ with e show ?thesis by (auto simp add: set_eq_iff)
qed auto
lemma cball_sing:
fixes x :: "'a::metric_space"
shows "e = 0 ==> cball x e = {x}"
- by (auto simp add: set_ext_iff)
+ by (auto simp add: set_eq_iff)
text{* For points in the interior, localization of limits makes no difference. *}
@@ -3904,7 +3904,7 @@
lemma interior_translation:
fixes s :: "'a::real_normed_vector set"
shows "interior ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (interior s)"
-proof (rule set_ext, rule)
+proof (rule set_eqI, rule)
fix x assume "x \<in> interior (op + a ` s)"
then obtain e where "e>0" and e:"ball x e \<subseteq> op + a ` s" unfolding mem_interior by auto
hence "ball (x - a) e \<subseteq> s" unfolding subset_eq Ball_def mem_ball dist_norm apply auto apply(erule_tac x="a + xa" in allE) unfolding ab_group_add_class.diff_diff_eq[THEN sym] by auto
@@ -4615,12 +4615,12 @@
lemma interval: fixes a :: "'a::ordered_euclidean_space" shows
"{a <..< b} = {x::'a. \<forall>i<DIM('a). a$$i < x$$i \<and> x$$i < b$$i}" and
"{a .. b} = {x::'a. \<forall>i<DIM('a). a$$i \<le> x$$i \<and> x$$i \<le> b$$i}"
- by(auto simp add:set_ext_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
+ by(auto simp add:set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
lemma mem_interval: fixes a :: "'a::ordered_euclidean_space" shows
"x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < x$$i \<and> x$$i < b$$i)"
"x \<in> {a .. b} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i \<le> x$$i \<and> x$$i \<le> b$$i)"
- using interval[of a b] by(auto simp add: set_ext_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
+ using interval[of a b] by(auto simp add: set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
lemma interval_eq_empty: fixes a :: "'a::ordered_euclidean_space" shows
"({a <..< b} = {} \<longleftrightarrow> (\<exists>i<DIM('a). b$$i \<le> a$$i))" (is ?th1) and
@@ -4662,7 +4662,7 @@
lemma interval_sing: fixes a :: "'a::ordered_euclidean_space" shows
"{a .. a} = {a}" "{a<..<a} = {}"
- apply(auto simp add: set_ext_iff euclidean_eq[where 'a='a] eucl_less[where 'a='a] eucl_le[where 'a='a])
+ apply(auto simp add: set_eq_iff euclidean_eq[where 'a='a] eucl_less[where 'a='a] eucl_le[where 'a='a])
apply (simp add: order_eq_iff) apply(rule_tac x=0 in exI) by (auto simp add: not_less less_imp_le)
lemma subset_interval_imp: fixes a :: "'a::ordered_euclidean_space" shows
@@ -4681,17 +4681,17 @@
{ fix i assume "i<DIM('a)"
hence "a $$ i \<le> x $$ i"
using x order_less_imp_le[of "a$$i" "x$$i"]
- by(simp add: set_ext_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
+ by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
}
moreover
{ fix i assume "i<DIM('a)"
hence "x $$ i \<le> b $$ i"
using x order_less_imp_le[of "x$$i" "b$$i"]
- by(simp add: set_ext_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
+ by(simp add: set_eq_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
}
ultimately
show "a \<le> x \<and> x \<le> b"
- by(simp add: set_ext_iff eucl_less[where 'a='a] eucl_le[where 'a='a] euclidean_eq)
+ by(simp add: set_eq_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<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i<DIM('a). (b$$i \<le> a$$i \<or> d$$i \<le> c$$i \<or> b$$i \<le> c$$i \<or> d$$i \<le> a$$i))" (is ?th4)
proof-
let ?z = "(\<chi>\<chi> i. ((max (a$$i) (c$$i)) + (min (b$$i) (d$$i))) / 2)::'a"
- note * = set_ext_iff Int_iff empty_iff mem_interval all_conj_distrib[THEN sym] eq_False
+ note * = set_eq_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} \<inter> {c .. d} = {(\<chi>\<chi> i. max (a$$i) (c$$i)) .. (\<chi>\<chi> i. min (b$$i) (d$$i))}"
- unfolding set_ext_iff and Int_iff and mem_interval
+ unfolding set_eq_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 "\<forall>n. x n \<in> s \<and> g n = f (x n)"
using choice[of "\<lambda> n xa. xa \<in> s \<and> g n = f xa"] by auto
hence x:"\<forall>n. x n \<in> s" "\<forall>n. g n = f (x n)" by auto
- hence "f \<circ> x = g" unfolding ext_iff by auto
+ hence "f \<circ> x = g" unfolding fun_eq_iff by auto
then obtain l where "l\<in>s" and l:"(x ---> l) sequentially"
using cs[unfolded complete_def, THEN spec[where x="x"]]
using cauchy_isometric[OF `0<e` s f normf] and cfg and x(1) by auto
--- a/src/HOL/NSA/NatStar.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/NSA/NatStar.thy Mon Sep 13 11:13:25 2010 +0200
@@ -115,7 +115,7 @@
@{term real_of_nat} *}
lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
-by transfer (simp add: ext_iff real_of_nat_def)
+by transfer (simp add: fun_eq_iff real_of_nat_def)
lemma starfun_inverse_real_of_nat_eq:
"N \<in> HNatInfinite
--- a/src/HOL/NSA/Star.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/NSA/Star.thy Mon Sep 13 11:13:25 2010 +0200
@@ -87,7 +87,7 @@
sequence) as a special case of an internal set*}
lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
-apply (drule ext_iff [THEN iffD2])
+apply (drule fun_eq_iff [THEN iffD2])
apply (simp add: starset_n_def starset_def star_of_def)
done
@@ -102,7 +102,7 @@
(*----------------------------------------------------------------*)
lemma starfun_n_starfun: "\<forall>n. (F n = f) ==> *fn* F = *f* f"
-apply (drule ext_iff [THEN iffD2])
+apply (drule fun_eq_iff [THEN iffD2])
apply (simp add: starfun_n_def starfun_def star_of_def)
done
--- a/src/HOL/NSA/StarDef.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Sep 13 11:13:25 2010 +0200
@@ -145,7 +145,7 @@
"\<lbrakk>\<And>X. f (star_n X) = g (star_n X)
\<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk>
\<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>"
-by (simp only: ext_iff transfer_all)
+by (simp only: fun_eq_iff transfer_all)
lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)"
by (rule reflexive)
@@ -351,12 +351,12 @@
lemma transfer_Collect [transfer_intro]:
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
\<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))"
-by (simp add: atomize_eq set_ext_iff all_star_eq Iset_star_n)
+by (simp add: atomize_eq set_eq_iff all_star_eq Iset_star_n)
lemma transfer_set_eq [transfer_intro]:
"\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk>
\<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>"
-by (simp only: set_ext_iff transfer_all transfer_iff transfer_mem)
+by (simp only: set_eq_iff transfer_all transfer_iff transfer_mem)
lemma transfer_ball [transfer_intro]:
"\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk>
--- a/src/HOL/Nat.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Nat.thy Mon Sep 13 11:13:25 2010 +0200
@@ -1360,7 +1360,7 @@
by (induct n) simp_all
lemma of_nat_eq_id [simp]: "of_nat = id"
- by (auto simp add: ext_iff)
+ by (auto simp add: fun_eq_iff)
subsection {* The Set of Natural Numbers *}
--- a/src/HOL/Nat_Transfer.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Nat_Transfer.thy Mon Sep 13 11:13:25 2010 +0200
@@ -170,7 +170,7 @@
apply (rule iffI)
apply (erule finite_imageI)
apply (erule finite_imageD)
- apply (auto simp add: image_def set_ext_iff inj_on_def)
+ apply (auto simp add: image_def set_eq_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)
--- a/src/HOL/Nitpick.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Nitpick.thy Mon Sep 13 11:13:25 2010 +0200
@@ -58,7 +58,7 @@
lemma Ex1_def [nitpick_def, no_atp]:
"Ex1 P \<equiv> \<exists>x. P = {x}"
apply (rule eq_reflection)
-apply (simp add: Ex1_def set_ext_iff)
+apply (simp add: Ex1_def set_eq_iff)
apply (rule iffI)
apply (erule exE)
apply (erule conjE)
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Sep 13 11:13:25 2010 +0200
@@ -110,7 +110,7 @@
"my_int_rel (x, y) (u, v) = (x + v = u + y)"
quotient_type my_int = "nat \<times> nat" / my_int_rel
-by (auto simp add: equivp_def ext_iff)
+by (auto simp add: equivp_def fun_eq_iff)
definition add_raw where
"add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
--- a/src/HOL/Nominal/Examples/Class1.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy Mon Sep 13 11:13:25 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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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 <a>.M d = OrR1 <c>.([(c,a)]\<bullet>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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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 <a>.M d = OrR2 <c>.([(c,a)]\<bullet>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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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).<a>.M d = ImpR (ca).<c>.([(c,a)]\<bullet>[(ca,x)]\<bullet>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: ext_iff)
+apply(simp add: fun_eq_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: ext_iff)
+apply(simp add: fun_eq_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 <a>.M (x).N y = ImpL <ca>.([(ca,a)]\<bullet>M) (caa).([(caa,x)]\<bullet>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: ext_iff)
+apply(simp add: fun_eq_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)
--- a/src/HOL/Nominal/Nominal.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Nominal/Nominal.thy Mon Sep 13 11:13:25 2010 +0200
@@ -148,11 +148,11 @@
(* permutation on sets *)
lemma empty_eqvt:
shows "pi\<bullet>{} = {}"
- by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] ext_iff)
+ by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] fun_eq_iff)
lemma union_eqvt:
shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
- by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] ext_iff)
+ by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] fun_eq_iff)
(* permutations on products *)
lemma fst_eqvt:
@@ -2069,7 +2069,7 @@
show "?LHS"
proof (rule ccontr)
assume "(pi\<bullet>f) \<noteq> f"
- hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: ext_iff)
+ hence "\<exists>x. (pi\<bullet>f) x \<noteq> f x" by (simp add: fun_eq_iff)
then obtain x where b1: "(pi\<bullet>f) x \<noteq> f x" by force
from b have "pi\<bullet>(f ((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))" by force
hence "(pi\<bullet>f)(pi\<bullet>((rev pi)\<bullet>x)) = f (pi\<bullet>((rev pi)\<bullet>x))"
@@ -2763,7 +2763,7 @@
and at: "at TYPE ('x)"
shows "cp TYPE ('a\<Rightarrow>'b) TYPE('x) TYPE('y)"
using c1 c2
-apply(auto simp add: cp_def perm_fun_def ext_iff)
+apply(auto simp add: cp_def perm_fun_def fun_eq_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\<bullet>([a].x) = [(pi\<bullet>a)].(pi\<bullet>x)"
apply(simp add: abs_fun_def perm_fun_def abs_fun_if)
- apply(simp only: ext_iff)
+ apply(simp only: fun_eq_iff)
apply(rule allI)
apply(subgoal_tac "(((rev pi)\<bullet>(xa::'y)) = (a::'y)) = (xa = pi\<bullet>a)")(*A*)
apply(subgoal_tac "(((rev pi)\<bullet>xa)\<sharp>x) = (xa\<sharp>(pi\<bullet>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: ext_iff)
+apply(auto simp add: fun_eq_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)]\<bullet>y \<and> a\<sharp>y"
proof -
- from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: ext_iff)
+ from a2 have "\<forall>c::'x. ([a].x) c = ([b].y) c" by (force simp add: fun_eq_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)]\<bullet>y \<and> a\<sharp>y"
@@ -3076,7 +3076,7 @@
shows "[a].x =[b].y"
proof -
show ?thesis
- proof (simp only: abs_fun_def ext_iff, intro strip)
+ proof (simp only: abs_fun_def fun_eq_iff, intro strip)
fix c::"'x"
let ?LHS = "if c=a then nSome(x) else if c\<sharp>x then nSome([(a,c)]\<bullet>x) else nNone"
and ?RHS = "if c=b then nSome(y) else if c\<sharp>y then nSome([(b,c)]\<bullet>y) else nNone"
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Mon Sep 13 11:13:25 2010 +0200
@@ -213,7 +213,7 @@
ultimately have "count M a = count N a"
by auto
}
- thus ?thesis by (simp add:multiset_ext_iff)
+ thus ?thesis by (simp add:multiset_eq_iff)
qed
definition multiset_prime_factorization :: "nat => nat multiset" where
--- a/src/HOL/Predicate.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Predicate.thy Mon Sep 13 11:13:25 2010 +0200
@@ -72,7 +72,7 @@
by (simp add: mem_def)
lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
- by (simp add: ext_iff mem_def)
+ by (simp add: fun_eq_iff mem_def)
subsubsection {* Order relation *}
@@ -99,10 +99,10 @@
by (simp add: bot_fun_eq bot_bool_eq)
lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
- by (auto simp add: ext_iff)
+ by (auto simp add: fun_eq_iff)
lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
- by (auto simp add: ext_iff)
+ by (auto simp add: fun_eq_iff)
subsubsection {* Binary union *}
@@ -197,10 +197,10 @@
by (auto simp add: SUP2_iff)
lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
- by (simp add: SUP1_iff ext_iff)
+ by (simp add: SUP1_iff fun_eq_iff)
lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
- by (simp add: SUP2_iff ext_iff)
+ by (simp add: SUP2_iff fun_eq_iff)
subsubsection {* Intersections of families *}
@@ -230,10 +230,10 @@
by (auto simp add: INF2_iff)
lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
- by (simp add: INF1_iff ext_iff)
+ by (simp add: INF1_iff fun_eq_iff)
lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
- by (simp add: INF2_iff ext_iff)
+ by (simp add: INF2_iff fun_eq_iff)
subsection {* Predicates as relations *}
@@ -251,7 +251,7 @@
lemma pred_comp_rel_comp_eq [pred_set_conv]:
"((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
- by (auto simp add: ext_iff elim: pred_compE)
+ by (auto simp add: fun_eq_iff elim: pred_compE)
subsubsection {* Converse *}
@@ -276,7 +276,7 @@
lemma conversep_converse_eq [pred_set_conv]:
"(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
- by (auto simp add: ext_iff)
+ by (auto simp add: fun_eq_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: ext_iff)
+ by (auto simp add: fun_eq_iff)
lemma conversep_eq [simp]: "(op =)^--1 = op ="
- by (auto simp add: ext_iff)
+ by (auto simp add: fun_eq_iff)
subsubsection {* Domain *}
@@ -347,7 +347,7 @@
"Powp A == \<lambda>B. \<forall>x \<in> B. A x"
lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
- by (auto simp add: Powp_def ext_iff)
+ by (auto simp add: Powp_def fun_eq_iff)
lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]
@@ -430,7 +430,7 @@
lemma bind_bind:
"(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
- by (auto simp add: bind_def ext_iff)
+ by (auto simp add: bind_def fun_eq_iff)
lemma bind_single:
"P \<guillemotright>= single = P"
@@ -442,14 +442,14 @@
lemma bottom_bind:
"\<bottom> \<guillemotright>= P = \<bottom>"
- by (auto simp add: bot_pred_def bind_def ext_iff)
+ by (auto simp add: bot_pred_def bind_def fun_eq_iff)
lemma sup_bind:
"(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
- by (auto simp add: bind_def sup_pred_def ext_iff)
+ by (auto simp add: bind_def sup_pred_def fun_eq_iff)
lemma Sup_bind: "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
- by (auto simp add: bind_def Sup_pred_def SUP1_iff ext_iff)
+ by (auto simp add: bind_def Sup_pred_def SUP1_iff fun_eq_iff)
lemma pred_iffI:
assumes "\<And>x. eval A x \<Longrightarrow> eval B x"
@@ -457,7 +457,7 @@
shows "A = B"
proof -
from assms have "\<And>x. eval A x \<longleftrightarrow> eval B x" by blast
- then show ?thesis by (cases A, cases B) (simp add: ext_iff)
+ then show ?thesis by (cases A, cases B) (simp add: fun_eq_iff)
qed
lemma singleI: "eval (single x) x"
@@ -492,7 +492,7 @@
lemma single_not_bot [simp]:
"single x \<noteq> \<bottom>"
- by (auto simp add: single_def bot_pred_def ext_iff)
+ by (auto simp add: single_def bot_pred_def fun_eq_iff)
lemma not_bot:
assumes "A \<noteq> \<bottom>"
@@ -512,7 +512,7 @@
lemma not_is_empty_single:
"\<not> is_empty (single x)"
- by (auto simp add: is_empty_def single_def bot_pred_def ext_iff)
+ by (auto simp add: is_empty_def single_def bot_pred_def fun_eq_iff)
lemma is_empty_sup:
"is_empty (A \<squnion> B) \<longleftrightarrow> is_empty A \<and> is_empty B"
@@ -543,7 +543,7 @@
moreover from assm have "\<And>x. eval A x \<Longrightarrow> 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 ext_iff) blast
+ by (simp (no_asm_use) add: single_def fun_eq_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: ext_iff elim: botE)
+ by (auto simp add: fun_eq_iff elim: botE)
next
case Insert show ?case
- by (auto simp add: ext_iff elim: supE singleE intro: supI1 supI2 singleI)
+ by (auto simp add: fun_eq_iff elim: supE singleE intro: supI1 supI2 singleI)
next
case Join then show ?case
- by (auto simp add: ext_iff elim: supE intro: supI1 supI2)
+ by (auto simp add: fun_eq_iff elim: supE intro: supI1 supI2)
qed
lemma eval_code [code]: "eval (Seq f) = member (f ())"
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Mon Sep 13 11:13:25 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] ext_iff intro!: eq_reflection)
+by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
-by (auto simp add: Diff_iff[unfolded mem_def] ext_iff intro!: eq_reflection)
+by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Mon Sep 13 11:13:25 2010 +0200
@@ -31,7 +31,7 @@
lemma [code_pred_inline]:
"max = max_nat"
-by (simp add: ext_iff max_def max_nat_def)
+by (simp add: fun_eq_iff max_def max_nat_def)
definition
"max_of_my_Suc x = max x (Suc x)"
--- a/src/HOL/Probability/Borel.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Mon Sep 13 11:13:25 2010 +0200
@@ -1031,7 +1031,7 @@
have "f -` {\<omega>} \<inter> space M = {x\<in>space M. f x = \<omega>}" by auto
with * have **: "{x\<in>space M. f x = \<omega>} \<in> sets M" by simp
have f: "f = (\<lambda>x. if f x = \<omega> then \<omega> else Real (real (f x)))"
- by (simp add: ext_iff Real_real)
+ by (simp add: fun_eq_iff Real_real)
show "f \<in> borel_measurable M"
apply (subst f)
apply (rule measurable_If)
@@ -1264,7 +1264,7 @@
proof -
have *: "(\<lambda>x. f x + g x) =
(\<lambda>x. if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else Real (real (f x) + real (g x)))"
- by (auto simp: ext_iff pinfreal_noteq_omega_Ex)
+ by (auto simp: fun_eq_iff pinfreal_noteq_omega_Ex)
show ?thesis using assms unfolding *
by (auto intro!: measurable_If)
qed
@@ -1276,7 +1276,7 @@
have *: "(\<lambda>x. f x * g x) =
(\<lambda>x. if f x = 0 then 0 else if g x = 0 then 0 else if f x = \<omega> then \<omega> else if g x = \<omega> then \<omega> else
Real (real (f x) * real (g x)))"
- by (auto simp: ext_iff pinfreal_noteq_omega_Ex)
+ by (auto simp: fun_eq_iff pinfreal_noteq_omega_Ex)
show ?thesis using assms unfolding *
by (auto intro!: measurable_If)
qed
--- a/src/HOL/Probability/Euclidean_Lebesgue.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Probability/Euclidean_Lebesgue.thy Mon Sep 13 11:13:25 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 ext_iff SUPR_fun_expand mono_def by auto
+ unfolding fun_eq_iff SUPR_fun_expand mono_def by auto
moreover have "(SUP i. f i) \<in> borel_measurable M"
using i by (rule borel_measurable_SUP)
ultimately show "u \<in> borel_measurable M" by simp
--- a/src/HOL/Probability/Information.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Probability/Information.thy Mon Sep 13 11:13:25 2010 +0200
@@ -505,7 +505,7 @@
by auto
also have "\<dots> = log b (\<Sum>x\<in>X`space M. if ?d x \<noteq> 0 then 1 else 0)"
apply (rule arg_cong[where f="\<lambda>f. log b (\<Sum>x\<in>X`space M. f x)"])
- using distribution_finite[of X] by (auto simp: ext_iff real_of_pinfreal_eq_0)
+ using distribution_finite[of X] by (auto simp: fun_eq_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 \<times> Y ` space M \<times> Z ` space M"
- have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: ext_iff)
+ have split_beta: "\<And>f. split f = (\<lambda>x. f (fst x) (snd x))" by (simp add: fun_eq_iff)
have "- (\<Sum>(x, y, z) \<in> ?M. ?dXYZ {(x, y, z)} *
log b (?dXYZ {(x, y, z)} / (?dXZ {(x, z)} * ?dYZ {(y,z)} / ?dZ {z})))
--- a/src/HOL/Probability/Lebesgue_Integration.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Mon Sep 13 11:13:25 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 ext_iff SUPR_def Sup_fun_def)
+ simp: isoton_def le_fun_def psuminf_def fun_eq_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 *: "(\<lambda>x. g x * indicator A x) = g"
"\<And>x. g x * indicator A x = g x"
"\<And>x. g x \<le> f x"
- by (auto simp: le_fun_def ext_iff indicator_def split: split_if_asm)
+ by (auto simp: le_fun_def fun_eq_iff indicator_def split: split_if_asm)
from g show "\<exists>x. simple_function (\<lambda>xa. x xa * indicator A xa) \<and> x \<le> f \<and> (\<forall>xa\<in>A. \<omega> \<noteq> x xa) \<and>
simple_integral g = simple_integral (\<lambda>xa. x xa * indicator A xa)"
using `A \<in> sets M`[THEN sets_into_space]
--- a/src/HOL/Probability/Positive_Infinite_Real.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Probability/Positive_Infinite_Real.thy Mon Sep 13 11:13:25 2010 +0200
@@ -1036,7 +1036,7 @@
qed
from choice[OF this] obtain r where f: "f = (\<lambda>i. Real (r i))"
and pos: "\<forall>i. 0 \<le> r i"
- by (auto simp: ext_iff)
+ by (auto simp: fun_eq_iff)
hence [simp]: "\<And>i. real (f i) = r i" by auto
have "mono (\<lambda>n. setsum r {..<n})" (is "mono ?S")
@@ -1156,7 +1156,7 @@
lemma psuminf_0: "psuminf f = 0 \<longleftrightarrow> (\<forall>i. f i = 0)"
proof safe
assume "\<forall>i. f i = 0"
- hence "f = (\<lambda>i. 0)" by (simp add: ext_iff)
+ hence "f = (\<lambda>i. 0)" by (simp add: fun_eq_iff)
thus "psuminf f = 0" using psuminf_const by simp
next
fix i assume "psuminf f = 0"
--- a/src/HOL/Probability/Probability_Space.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Probability/Probability_Space.thy Mon Sep 13 11:13:25 2010 +0200
@@ -34,14 +34,14 @@
lemma (in prob_space) distribution_cong:
assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = Y x"
shows "distribution X = distribution Y"
- unfolding distribution_def ext_iff
+ unfolding distribution_def fun_eq_iff
using assms by (auto intro!: arg_cong[where f="\<mu>"])
lemma (in prob_space) joint_distribution_cong:
assumes "\<And>x. x \<in> space M \<Longrightarrow> X x = X' x"
assumes "\<And>x. x \<in> space M \<Longrightarrow> Y x = Y' x"
shows "joint_distribution X Y = joint_distribution X' Y'"
- unfolding distribution_def ext_iff
+ unfolding distribution_def fun_eq_iff
using assms by (auto intro!: arg_cong[where f="\<mu>"])
lemma prob_space: "prob (space M) = 1"
--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Sep 13 11:13:25 2010 +0200
@@ -716,7 +716,7 @@
lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
apply (simp add: binaryset_def)
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (auto simp add: image_iff)
done
--- a/src/HOL/Product_Type.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Product_Type.thy Mon Sep 13 11:13:25 2010 +0200
@@ -151,7 +151,7 @@
next
fix a c :: 'a and b d :: 'b
have "Pair_Rep a b = Pair_Rep c d \<longleftrightarrow> a = c \<and> b = d"
- by (auto simp add: Pair_Rep_def ext_iff)
+ by (auto simp add: Pair_Rep_def fun_eq_iff)
moreover have "Pair_Rep a b \<in> prod" and "Pair_Rep c d \<in> prod"
by (auto simp add: prod_def)
ultimately show "Pair a b = Pair c d \<longleftrightarrow> a = c \<and> 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: ext_iff split: prod.split)
+ by (simp add: fun_eq_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]: "(\<lambda>(x, y). (x, y)) = id"
- by (simp add: ext_iff split: prod.split)
+ by (simp add: fun_eq_iff split: prod.split)
lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
-- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
- by (simp add: ext_iff split: prod.split)
+ by (simp add: fun_eq_iff split: prod.split)
lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
by (cases x) simp
@@ -797,25 +797,25 @@
"f \<circ>\<rightarrow> g = (\<lambda>x. prod_case g (f x))"
lemma scomp_unfold: "scomp = (\<lambda>f g x. g (fst (f x)) (snd (f x)))"
- by (simp add: ext_iff scomp_def prod_case_unfold)
+ by (simp add: fun_eq_iff scomp_def prod_case_unfold)
lemma scomp_apply [simp]: "(f \<circ>\<rightarrow> g) x = prod_case g (f x)"
by (simp add: scomp_unfold prod_case_unfold)
lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
- by (simp add: ext_iff scomp_apply)
+ by (simp add: fun_eq_iff scomp_apply)
lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
- by (simp add: ext_iff scomp_apply)
+ by (simp add: fun_eq_iff scomp_apply)
lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
- by (simp add: ext_iff scomp_unfold)
+ by (simp add: fun_eq_iff scomp_unfold)
lemma scomp_fcomp: "(f \<circ>\<rightarrow> g) \<circ>> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>> h)"
- by (simp add: ext_iff scomp_unfold fcomp_def)
+ by (simp add: fun_eq_iff scomp_unfold fcomp_def)
lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
- by (simp add: ext_iff scomp_unfold fcomp_apply)
+ by (simp add: fun_eq_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: ext_iff)
+ by (simp add: fun_eq_iff)
lemma apsnd_id [simp] :
"apsnd id = id"
- by (simp add: ext_iff)
+ by (simp add: fun_eq_iff)
lemma apfst_eq_conv [simp]:
"apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)"
@@ -1130,7 +1130,7 @@
assumes "f ` A = A'" and "g ` B = B'"
shows "prod_fun f g ` (A \<times> B) = A' \<times> B'"
unfolding image_def
-proof(rule set_ext,rule iffI)
+proof(rule set_eqI,rule iffI)
fix x :: "'a \<times> 'c"
assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = prod_fun f g x}"
then obtain y where "y \<in> A \<times> B" and "x = prod_fun f g y" by blast
--- a/src/HOL/Quotient.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Quotient.thy Mon Sep 13 11:13:25 2010 +0200
@@ -34,7 +34,7 @@
lemma equivp_reflp_symp_transp:
shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
- unfolding equivp_def reflp_def symp_def transp_def ext_iff
+ unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
by blast
lemma equivp_reflp:
@@ -97,7 +97,7 @@
lemma eq_comp_r:
shows "((op =) OOO R) = R"
- by (auto simp add: ext_iff)
+ by (auto simp add: fun_eq_iff)
subsection {* Respects predicate *}
@@ -130,11 +130,11 @@
lemma fun_map_id:
shows "(id ---> id) = id"
- by (simp add: ext_iff id_def)
+ by (simp add: fun_eq_iff id_def)
lemma fun_rel_eq:
shows "((op =) ===> (op =)) = (op =)"
- by (simp add: ext_iff)
+ by (simp add: fun_eq_iff)
subsection {* Quotient Predicate *}
@@ -209,7 +209,7 @@
have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
using q1 q2
unfolding Quotient_def
- unfolding ext_iff
+ unfolding fun_eq_iff
by simp
moreover
have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
@@ -219,7 +219,7 @@
moreover
have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"
- unfolding ext_iff
+ unfolding fun_eq_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 ext_iff
+ unfolding fun_eq_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) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
- unfolding ext_iff
+ unfolding fun_eq_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) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
- unfolding ext_iff
+ unfolding fun_eq_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 \<Longrightarrow> Babs (Respects R) P = P"
- by (simp add: ext_iff Babs_def in_respects equivp_reflp)
+ by (simp add: fun_eq_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 \<circ> = op \<circ>"
and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
- unfolding o_def ext_iff by simp_all
+ unfolding o_def fun_eq_iff by simp_all
lemma o_rsp:
"((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
"(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
- unfolding fun_rel_def o_def ext_iff by auto
+ unfolding fun_rel_def o_def fun_eq_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: ext_iff)
+ by (auto simp add: fun_eq_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: ext_iff)
+ by (auto simp add: fun_eq_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 \<in> = op \<in>"
- by (simp add: ext_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
+ by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
locale quot_type =
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
--- a/src/HOL/Quotient_Examples/FSet.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Mon Sep 13 11:13:25 2010 +0200
@@ -563,12 +563,12 @@
lemma [quot_preserve]:
"(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
- by (simp add: ext_iff Quotient_abs_rep[OF Quotient_fset]
+ by (simp add: fun_eq_iff Quotient_abs_rep[OF Quotient_fset]
abs_o_rep[OF Quotient_fset] map_id finsert_def)
lemma [quot_preserve]:
"((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion"
- by (simp add: ext_iff Quotient_abs_rep[OF Quotient_fset]
+ by (simp add: fun_eq_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 \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
- by (simp add: set_ext_iff[symmetric] inj_image_eq_iff)
+ by (simp add: set_eq_iff[symmetric] inj_image_eq_iff)
text {* alternate formulation with a different decomposition principle
and a proof of equivalence *}
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Mon Sep 13 11:13:25 2010 +0200
@@ -14,7 +14,7 @@
"intrel (x, y) (u, v) = (x + v = u + y)"
quotient_type int = "nat \<times> nat" / intrel
- by (auto simp add: equivp_def ext_iff)
+ by (auto simp add: equivp_def fun_eq_iff)
instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
begin
--- a/src/HOL/Random.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Random.thy Mon Sep 13 11:13:25 2010 +0200
@@ -85,7 +85,7 @@
lemma pick_drop_zero:
"pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
- by (induct xs) (auto simp add: ext_iff)
+ by (induct xs) (auto simp add: fun_eq_iff)
lemma pick_same:
"l < length xs \<Longrightarrow> 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
- ext_iff pick_same [symmetric])
+ fun_eq_iff pick_same [symmetric])
qed
--- a/src/HOL/Recdef.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Recdef.thy Mon Sep 13 11:13:25 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: ext_iff cut_def)
+by (simp add: fun_eq_iff cut_def)
lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
by (simp add: cut_def)
--- a/src/HOL/Set.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Set.thy Mon Sep 13 11:13:25 2010 +0200
@@ -489,20 +489,18 @@
subsubsection {* Equality *}
-lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
+lemma set_eqI: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
apply (rule Collect_mem_eq)
apply (rule Collect_mem_eq)
done
-lemma set_ext_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
-by(auto intro:set_ext)
-
-lemmas expand_set_eq [no_atp] = set_ext_iff
+lemma set_eq_iff [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
+by(auto intro:set_eqI)
lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
-- {* Anti-symmetry of the subset relation. *}
- by (iprover intro: set_ext subsetD)
+ by (iprover intro: set_eqI subsetD)
text {*
\medskip Equality rules from ZF set theory -- are they appropriate
--- a/src/HOL/SetInterval.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/SetInterval.thy Mon Sep 13 11:13:25 2010 +0200
@@ -241,7 +241,7 @@
lemma atLeastatMost_psubset_iff:
"{a..b} < {c..d} \<longleftrightarrow>
((~ a <= b) | c <= a & b <= d & (c < a | b < d)) & c <= d"
-by(simp add: psubset_eq set_ext_iff less_le_not_le)(blast intro: order_trans)
+by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
lemma atLeastAtMost_singleton_iff[simp]:
"{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
--- a/src/HOL/String.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/String.thy Mon Sep 13 11:13:25 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: ext_iff split: char.split)
+ by (simp add: fun_eq_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: ext_iff split: char.split)
+ by (simp add: fun_eq_iff split: char.split)
syntax
"_Char" :: "xstr => char" ("CHR _")
--- a/src/HOL/Sum_Type.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Sum_Type.thy Mon Sep 13 11:13:25 2010 +0200
@@ -32,17 +32,17 @@
lemma Inl_Rep_inject: "inj_on Inl_Rep A"
proof (rule inj_onI)
show "\<And>a c. Inl_Rep a = Inl_Rep c \<Longrightarrow> a = c"
- by (auto simp add: Inl_Rep_def ext_iff)
+ by (auto simp add: Inl_Rep_def fun_eq_iff)
qed
lemma Inr_Rep_inject: "inj_on Inr_Rep A"
proof (rule inj_onI)
show "\<And>b d. Inr_Rep b = Inr_Rep d \<Longrightarrow> b = d"
- by (auto simp add: Inr_Rep_def ext_iff)
+ by (auto simp add: Inr_Rep_def fun_eq_iff)
qed
lemma Inl_Rep_not_Inr_Rep: "Inl_Rep a \<noteq> Inr_Rep b"
- by (auto simp add: Inl_Rep_def Inr_Rep_def ext_iff)
+ by (auto simp add: Inl_Rep_def Inr_Rep_def fun_eq_iff)
definition Inl :: "'a \<Rightarrow> 'a + 'b" where
"Inl = Abs_sum \<circ> Inl_Rep"
@@ -178,7 +178,7 @@
by auto
lemma UNIV_Plus_UNIV [simp]: "UNIV <+> UNIV = UNIV"
-proof (rule set_ext)
+proof (rule set_eqI)
fix u :: "'a + 'b"
show "u \<in> UNIV <+> UNIV \<longleftrightarrow> u \<in> UNIV" by (cases u) auto
qed
--- a/src/HOL/Tools/Datatype/datatype.ML Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Sep 13 11:13:25 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 ext_iff}) :: range_eqs),
+ Thm.symmetric (mk_meta_eq @{thm fun_eq_iff}) :: range_eqs),
rewrite_goals_tac (map Thm.symmetric range_eqs),
REPEAT (EVERY
[REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Sep 13 11:13:25 2010 +0200
@@ -78,7 +78,7 @@
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
-val fun_cong_all = @{thm ext_iff [THEN iffD1]}
+val fun_cong_all = @{thm fun_eq_iff [THEN iffD1]}
(* Removes the lambdas from an equation of the form "t = (%x. u)".
(Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
--- a/src/HOL/Transitive_Closure.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Transitive_Closure.thy Mon Sep 13 11:13:25 2010 +0200
@@ -82,7 +82,7 @@
subsection {* Reflexive-transitive closure *}
lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
- by (auto simp add: ext_iff)
+ by (auto simp add: fun_eq_iff)
lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
-- {* @{text rtrancl} of @{text r} contains @{text r} *}
@@ -186,7 +186,7 @@
lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set]
lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*"
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (simp only: split_tupled_all)
apply (blast intro: rtrancl_trans)
done
@@ -487,7 +487,7 @@
lemmas trancl_converseD = tranclp_converseD [to_set]
lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1"
- by (fastsimp simp add: ext_iff
+ by (fastsimp simp add: fun_eq_iff
intro!: tranclp_converseI dest!: tranclp_converseD)
lemmas trancl_converse = tranclp_converse [to_set]
--- a/src/HOL/UNITY/Comp/Alloc.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Sep 13 11:13:25 2010 +0200
@@ -358,7 +358,7 @@
done
lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
- apply (simp add: surj_iff ext_iff o_apply)
+ apply (simp add: surj_iff fun_eq_iff o_apply)
apply record_auto
done
@@ -386,7 +386,7 @@
done
lemma surj_sysOfClient [iff]: "surj sysOfClient"
- apply (simp add: surj_iff ext_iff o_apply)
+ apply (simp add: surj_iff fun_eq_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 ext_iff o_apply)
+ apply (simp add: surj_iff fun_eq_iff o_apply)
apply record_auto
done
--- a/src/HOL/UNITY/Lift_prog.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy Mon Sep 13 11:13:25 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: ext_iff o_def)
+by (simp add: fun_eq_iff o_def)
lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x"
-by (simp add: ext_iff o_def)
+by (simp add: fun_eq_iff o_def)
lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
apply (rule ext)
--- a/src/HOL/Wellfounded.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Wellfounded.thy Mon Sep 13 11:13:25 2010 +0200
@@ -781,7 +781,7 @@
let ?N1 = "{ n \<in> N. (n, a) \<in> r }"
let ?N2 = "{ n \<in> N. (n, a) \<notin> r }"
- have N: "?N1 \<union> ?N2 = N" by (rule set_ext) auto
+ have N: "?N1 \<union> ?N2 = N" by (rule set_eqI) auto
from Nless have "finite N" by (auto elim: max_ext.cases)
then have finites: "finite ?N1" "finite ?N2" by auto
--- a/src/HOL/Word/Misc_Typedef.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Word/Misc_Typedef.thy Mon Sep 13 11:13:25 2010 +0200
@@ -53,14 +53,14 @@
lemma set_Rep:
"A = range Rep"
-proof (rule set_ext)
+proof (rule set_eqI)
fix x
show "(x \<in> A) = (x \<in> range Rep)"
by (auto dest: Abs_inverse [of x, symmetric])
qed
lemma set_Rep_Abs: "A = range (Rep o Abs)"
-proof (rule set_ext)
+proof (rule set_eqI)
fix x
show "(x \<in> A) = (x \<in> range (Rep o Abs))"
by (auto dest: Abs_inverse [of x, symmetric])
--- a/src/HOL/Word/Word.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/Word/Word.thy Mon Sep 13 11:13:25 2010 +0200
@@ -4695,7 +4695,7 @@
apply simp
apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
in subst)
- apply (clarsimp simp add: ext_iff)
+ apply (clarsimp simp add: fun_eq_iff)
apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
apply simp
apply (rule refl)
--- a/src/HOL/ZF/Games.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/ZF/Games.thy Mon Sep 13 11:13:25 2010 +0200
@@ -323,7 +323,7 @@
lemma wf_option_of[recdef_wf, simp, intro]: "wf option_of"
proof -
have option_of: "option_of = inv_image is_option_of Rep_game"
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (case_tac "x")
by (simp add: option_to_is_option_of)
show ?thesis
--- a/src/HOL/ZF/HOLZF.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/ZF/HOLZF.thy Mon Sep 13 11:13:25 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) \<times> (explode b))"
- by (simp add: explode_def set_ext_iff CartProd image_def)
+ by (simp add: explode_def set_eq_iff CartProd image_def)
lemma explode_Repl_eq: "explode (Repl A f) = image f (explode A)"
by (simp add: explode_def Repl image_def)
@@ -830,7 +830,7 @@
apply (subst set_like_def)
apply (auto simp add: image_def)
apply (rule_tac x="Sep (Ext_ZF_hull R y) (\<lambda> z. z \<in> (Ext (R^+) y))" in exI)
- apply (auto simp add: explode_def Sep set_ext
+ apply (auto simp add: explode_def Sep set_eqI
in_Ext_RTrans_implies_Elem_Ext_ZF_hull)
done
--- a/src/HOL/ZF/Zet.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/ZF/Zet.thy Mon Sep 13 11:13:25 2010 +0200
@@ -22,7 +22,7 @@
"zimage f A == Abs_zet (image f (Rep_zet A))"
lemma zet_def': "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A = explode z}"
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (auto simp add: zet_def)
apply (rule_tac x=f in exI)
apply auto
@@ -118,7 +118,7 @@
"zsubset a b \<equiv> ! x. zin x a \<longrightarrow> zin x b"
lemma explode_union: "explode (union a b) = (explode a) \<union> (explode b)"
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (simp add: explode_def union)
done
@@ -163,7 +163,7 @@
by (simp add: zet_ext_eq zin_zexplode_eq Repl zimage_iff)
lemma range_explode_eq_zet: "range explode = zet"
- apply (rule set_ext)
+ apply (rule set_eqI)
apply (auto simp add: explode_mem_zet)
apply (drule image_zet_rep)
apply (simp add: image_def)
--- a/src/HOL/ex/Execute_Choice.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/ex/Execute_Choice.thy Mon Sep 13 11:13:25 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: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def ext_iff mem_def keys_def)
+ then have l: "\<exists>l. l \<in> dom (Mapping.lookup m)" by (auto simp add: is_empty_def fun_eq_iff mem_def keys_def)
then have "(let l = SOME l. l \<in> dom (Mapping.lookup m) in
the (Mapping.lookup m l) + (\<Sum>k \<in> dom (Mapping.lookup m) - {l}. the (Mapping.lookup m k))) =
(\<Sum>k \<in> dom (Mapping.lookup m). the (Mapping.lookup m k))"
--- a/src/HOL/ex/Landau.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/ex/Landau.thy Mon Sep 13 11:13:25 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: ext_iff equiv_def equiv_fun_less_eq_fun)
+ by (simp add: fun_eq_iff equiv_def equiv_fun_less_eq_fun)
qed
--- a/src/HOL/ex/Summation.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOL/ex/Summation.thy Mon Sep 13 11:13:25 2010 +0200
@@ -24,7 +24,7 @@
lemma \<Delta>_shift:
"\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
- by (simp add: \<Delta>_def ext_iff)
+ by (simp add: \<Delta>_def fun_eq_iff)
lemma \<Delta>_same_shift:
assumes "\<Delta> f = \<Delta> g"
@@ -100,7 +100,7 @@
proof -
from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
then obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
- then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: ext_iff)
+ then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: fun_eq_iff)
then show ?thesis by simp
qed
--- a/src/HOLCF/Algebraic.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/Algebraic.thy Mon Sep 13 11:13:25 2010 +0200
@@ -446,7 +446,7 @@
apply (clarify, simp add: fd_take_fixed_iff)
apply (simp add: finite_fixes_approx)
apply (rule inj_onI, clarify)
-apply (simp add: set_ext_iff fin_defl_eqI)
+apply (simp add: set_eq_iff fin_defl_eqI)
done
lemma fd_take_covers: "\<exists>n. fd_take n a = a"
--- a/src/HOLCF/Cfun.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/Cfun.thy Mon Sep 13 11:13:25 2010 +0200
@@ -178,7 +178,7 @@
text {* Extensionality for continuous functions *}
lemma expand_cfun_eq: "(f = g) = (\<forall>x. f\<cdot>x = g\<cdot>x)"
-by (simp add: Rep_CFun_inject [symmetric] ext_iff)
+by (simp add: Rep_CFun_inject [symmetric] fun_eq_iff)
lemma ext_cfun: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
by (simp add: expand_cfun_eq)
--- a/src/HOLCF/Ffun.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/Ffun.thy Mon Sep 13 11:13:25 2010 +0200
@@ -27,7 +27,7 @@
next
fix f g :: "'a \<Rightarrow> 'b"
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
- by (simp add: below_fun_def ext_iff below_antisym)
+ by (simp add: below_fun_def fun_eq_iff below_antisym)
next
fix f g h :: "'a \<Rightarrow> 'b"
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
@@ -103,7 +103,7 @@
proof
fix f g :: "'a \<Rightarrow> 'b"
show "f \<sqsubseteq> g \<longleftrightarrow> f = g"
- unfolding expand_fun_below ext_iff
+ unfolding expand_fun_below fun_eq_iff
by simp
qed
@@ -111,7 +111,7 @@
lemma maxinch2maxinch_lambda:
"(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
-unfolding max_in_chain_def ext_iff by simp
+unfolding max_in_chain_def fun_eq_iff by simp
lemma maxinch_mono:
"\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
--- a/src/HOLCF/IOA/ABP/Correctness.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.thy Mon Sep 13 11:13:25 2010 +0200
@@ -210,7 +210,7 @@
lemma compat_single_ch: "compatible srch_ioa rsch_ioa"
apply (simp add: compatible_def Int_def)
-apply (rule set_ext)
+apply (rule set_eqI)
apply (induct_tac x)
apply simp_all
done
@@ -218,7 +218,7 @@
text {* totally the same as before *}
lemma compat_single_fin_ch: "compatible srch_fin_ioa rsch_fin_ioa"
apply (simp add: compatible_def Int_def)
-apply (rule set_ext)
+apply (rule set_eqI)
apply (induct_tac x)
apply simp_all
done
@@ -232,7 +232,7 @@
apply (simp del: del_simps
add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
apply simp
-apply (rule set_ext)
+apply (rule set_eqI)
apply (induct_tac x)
apply simp_all
done
@@ -242,7 +242,7 @@
apply (simp del: del_simps
add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
apply simp
-apply (rule set_ext)
+apply (rule set_eqI)
apply (induct_tac x)
apply simp_all
done
@@ -252,7 +252,7 @@
apply (simp del: del_simps
add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
apply simp
-apply (rule set_ext)
+apply (rule set_eqI)
apply (induct_tac x)
apply simp_all
done
@@ -262,7 +262,7 @@
apply (simp del: del_simps
add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
apply simp
-apply (rule set_ext)
+apply (rule set_eqI)
apply (induct_tac x)
apply simp_all
done
@@ -272,7 +272,7 @@
apply (simp del: del_simps
add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
apply simp
-apply (rule set_ext)
+apply (rule set_eqI)
apply (induct_tac x)
apply simp_all
done
@@ -282,7 +282,7 @@
apply (simp del: del_simps
add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
apply simp
-apply (rule set_ext)
+apply (rule set_eqI)
apply (induct_tac x)
apply simp_all
done
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Mon Sep 13 11:13:25 2010 +0200
@@ -296,7 +296,7 @@
"Execs (A||B) = par_execs (Execs A) (Execs B)"
apply (unfold Execs_def par_execs_def)
apply (simp add: asig_of_par)
-apply (rule set_ext)
+apply (rule set_eqI)
apply (simp add: compositionality_ex actions_of_par)
done
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Mon Sep 13 11:13:25 2010 +0200
@@ -542,7 +542,7 @@
apply (unfold Scheds_def par_scheds_def)
apply (simp add: asig_of_par)
-apply (rule set_ext)
+apply (rule set_eqI)
apply (simp add: compositionality_sch actions_of_par)
done
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Mon Sep 13 11:13:25 2010 +0200
@@ -962,7 +962,7 @@
apply (unfold Traces_def par_traces_def)
apply (simp add: asig_of_par)
-apply (rule set_ext)
+apply (rule set_eqI)
apply (simp add: compositionality_tr externals_of_par)
done
--- a/src/HOLCF/Library/List_Cpo.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/Library/List_Cpo.thy Mon Sep 13 11:13:25 2010 +0200
@@ -115,7 +115,7 @@
apply (induct n arbitrary: S)
apply (subgoal_tac "S = (\<lambda>i. [])")
apply (fast intro: lub_const)
- apply (simp add: ext_iff)
+ apply (simp add: fun_eq_iff)
apply (drule_tac x="\<lambda>i. tl (S i)" in meta_spec, clarsimp)
apply (rule_tac x="(\<Squnion>i. hd (S i)) # x" in exI)
apply (subgoal_tac "range (\<lambda>i. hd (S i) # tl (S i)) = range S")
--- a/src/HOLCF/Pcpo.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/Pcpo.thy Mon Sep 13 11:13:25 2010 +0200
@@ -89,7 +89,7 @@
lemma lub_equal:
"\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
- by (simp only: ext_iff [symmetric])
+ by (simp only: fun_eq_iff [symmetric])
lemma lub_eq:
"(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
--- a/src/HOLCF/Up.thy Mon Sep 13 09:29:43 2010 +0200
+++ b/src/HOLCF/Up.thy Mon Sep 13 11:13:25 2010 +0200
@@ -135,7 +135,7 @@
(\<exists>A. chain A \<and> (\<Squnion>i. Y i) = Iup (\<Squnion>i. A i) \<and>
(\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
apply (rule disjCI)
-apply (simp add: ext_iff)
+apply (simp add: fun_eq_iff)
apply (erule exE, rename_tac j)
apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
apply (simp add: up_lemma4)