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