# HG changeset patch
# User nipkow
# Date 1283853858 -7200
# Node ID 720112792ba0361ad85ad4c0667cc1ca51c46f53
# Parent  f967a16dfcdda658afa03943d43bfd377f658012
renamed expand_*_eq in HOLCF as well

diff -r f967a16dfcdd -r 720112792ba0 NEWS
--- 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.
diff -r f967a16dfcdd -r 720112792ba0 src/HOLCF/Algebraic.thy
--- 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"
diff -r f967a16dfcdd -r 720112792ba0 src/HOLCF/Cfun.thy
--- 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)
diff -r f967a16dfcdd -r 720112792ba0 src/HOLCF/Ffun.thy
--- 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"
diff -r f967a16dfcdd -r 720112792ba0 src/HOLCF/Library/List_Cpo.thy
--- 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")
diff -r f967a16dfcdd -r 720112792ba0 src/HOLCF/Pcpo.thy
--- 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)"
diff -r f967a16dfcdd -r 720112792ba0 src/HOLCF/Up.thy
--- 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)