--- a/NEWS Tue Sep 07 10:05:19 2010 +0200
+++ b/NEWS Tue Sep 07 12:04:18 2010 +0200
@@ -68,6 +68,8 @@
*** HOL ***
+* Renamed lemmas: expand_fun_eq -> ext_iff, expand_set_eq -> set_ext_iff
+
* Renamed class eq and constant eq (for code generation) to class equal
and constant equal, plus renaming of related facts and various tuning.
INCOMPATIBILITY.
--- a/src/HOLCF/Algebraic.thy Tue Sep 07 10:05:19 2010 +0200
+++ b/src/HOLCF/Algebraic.thy Tue Sep 07 12:04:18 2010 +0200
@@ -446,7 +446,7 @@
apply (clarify, simp add: fd_take_fixed_iff)
apply (simp add: finite_fixes_approx)
apply (rule inj_onI, clarify)
-apply (simp add: expand_set_eq fin_defl_eqI)
+apply (simp add: set_ext_iff fin_defl_eqI)
done
lemma fd_take_covers: "\<exists>n. fd_take n a = a"
--- a/src/HOLCF/Cfun.thy Tue Sep 07 10:05:19 2010 +0200
+++ b/src/HOLCF/Cfun.thy Tue Sep 07 12:04:18 2010 +0200
@@ -178,7 +178,7 @@
text {* Extensionality for continuous functions *}
lemma expand_cfun_eq: "(f = g) = (\<forall>x. f\<cdot>x = g\<cdot>x)"
-by (simp add: Rep_CFun_inject [symmetric] expand_fun_eq)
+by (simp add: Rep_CFun_inject [symmetric] ext_iff)
lemma ext_cfun: "(\<And>x. f\<cdot>x = g\<cdot>x) \<Longrightarrow> f = g"
by (simp add: expand_cfun_eq)
--- a/src/HOLCF/Ffun.thy Tue Sep 07 10:05:19 2010 +0200
+++ b/src/HOLCF/Ffun.thy Tue Sep 07 12:04:18 2010 +0200
@@ -27,7 +27,7 @@
next
fix f g :: "'a \<Rightarrow> 'b"
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
- by (simp add: below_fun_def expand_fun_eq below_antisym)
+ by (simp add: below_fun_def ext_iff below_antisym)
next
fix f g h :: "'a \<Rightarrow> 'b"
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
@@ -103,7 +103,7 @@
proof
fix f g :: "'a \<Rightarrow> 'b"
show "f \<sqsubseteq> g \<longleftrightarrow> f = g"
- unfolding expand_fun_below expand_fun_eq
+ unfolding expand_fun_below ext_iff
by simp
qed
@@ -111,7 +111,7 @@
lemma maxinch2maxinch_lambda:
"(\<And>x. max_in_chain n (\<lambda>i. S i x)) \<Longrightarrow> max_in_chain n S"
-unfolding max_in_chain_def expand_fun_eq by simp
+unfolding max_in_chain_def ext_iff by simp
lemma maxinch_mono:
"\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> max_in_chain j Y"
--- a/src/HOLCF/Library/List_Cpo.thy Tue Sep 07 10:05:19 2010 +0200
+++ b/src/HOLCF/Library/List_Cpo.thy Tue Sep 07 12:04:18 2010 +0200
@@ -115,7 +115,7 @@
apply (induct n arbitrary: S)
apply (subgoal_tac "S = (\<lambda>i. [])")
apply (fast intro: lub_const)
- apply (simp add: expand_fun_eq)
+ apply (simp add: ext_iff)
apply (drule_tac x="\<lambda>i. tl (S i)" in meta_spec, clarsimp)
apply (rule_tac x="(\<Squnion>i. hd (S i)) # x" in exI)
apply (subgoal_tac "range (\<lambda>i. hd (S i) # tl (S i)) = range S")
--- a/src/HOLCF/Pcpo.thy Tue Sep 07 10:05:19 2010 +0200
+++ b/src/HOLCF/Pcpo.thy Tue Sep 07 12:04:18 2010 +0200
@@ -89,7 +89,7 @@
lemma lub_equal:
"\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
- by (simp only: expand_fun_eq [symmetric])
+ by (simp only: ext_iff [symmetric])
lemma lub_eq:
"(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
--- a/src/HOLCF/Up.thy Tue Sep 07 10:05:19 2010 +0200
+++ b/src/HOLCF/Up.thy Tue Sep 07 12:04:18 2010 +0200
@@ -135,7 +135,7 @@
(\<exists>A. chain A \<and> (\<Squnion>i. Y i) = Iup (\<Squnion>i. A i) \<and>
(\<exists>j. \<forall>i. Y (i + j) = Iup (A i))) \<or> (Y = (\<lambda>i. Ibottom))"
apply (rule disjCI)
-apply (simp add: expand_fun_eq)
+apply (simp add: ext_iff)
apply (erule exE, rename_tac j)
apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
apply (simp add: up_lemma4)