--- a/src/HOL/HOLCF/Algebraic.thy Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/Algebraic.thy Wed Dec 22 18:24:04 2010 -0800
@@ -152,12 +152,12 @@
definition
cast :: "'a defl \<rightarrow> 'a \<rightarrow> 'a"
where
- "cast = defl.basis_fun Rep_fin_defl"
+ "cast = defl.extension Rep_fin_defl"
lemma cast_defl_principal:
"cast\<cdot>(defl_principal a) = Rep_fin_defl a"
unfolding cast_def
-apply (rule defl.basis_fun_principal)
+apply (rule defl.extension_principal)
apply (simp only: below_fin_defl_def)
done
@@ -219,14 +219,14 @@
definition
"defl_fun1 e p f =
- defl.basis_fun (\<lambda>a.
+ defl.extension (\<lambda>a.
defl_principal (Abs_fin_defl
(e oo f\<cdot>(Rep_fin_defl a) oo p)))"
definition
"defl_fun2 e p f =
- defl.basis_fun (\<lambda>a.
- defl.basis_fun (\<lambda>b.
+ defl.extension (\<lambda>a.
+ defl.extension (\<lambda>b.
defl_principal (Abs_fin_defl
(e oo f\<cdot>(Rep_fin_defl a)\<cdot>(Rep_fin_defl b) oo p))))"
@@ -242,8 +242,8 @@
show ?thesis
by (induct A rule: defl.principal_induct, simp)
(simp only: defl_fun1_def
- defl.basis_fun_principal
- defl.basis_fun_mono
+ defl.extension_principal
+ defl.extension_mono
defl.principal_mono
Abs_fin_defl_mono [OF 1 1]
monofun_cfun below_refl
@@ -267,8 +267,8 @@
apply (induct A rule: defl.principal_induct, simp)
apply (induct B rule: defl.principal_induct, simp)
by (simp only: defl_fun2_def
- defl.basis_fun_principal
- defl.basis_fun_mono
+ defl.extension_principal
+ defl.extension_mono
defl.principal_mono
Abs_fin_defl_mono [OF 1 1]
monofun_cfun below_refl
--- a/src/HOL/HOLCF/Completion.thy Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/Completion.thy Wed Dec 22 18:24:04 2010 -0800
@@ -291,10 +291,10 @@
subsection {* Defining functions in terms of basis elements *}
definition
- basis_fun :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
- "basis_fun = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
+ extension :: "('a::type \<Rightarrow> 'c::cpo) \<Rightarrow> 'b \<rightarrow> 'c" where
+ "extension = (\<lambda>f. (\<Lambda> x. lub (f ` rep x)))"
-lemma basis_fun_lemma:
+lemma extension_lemma:
fixes f :: "'a::type \<Rightarrow> 'c::cpo"
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
shows "\<exists>u. f ` rep x <<| u"
@@ -320,14 +320,14 @@
thus ?thesis ..
qed
-lemma basis_fun_beta:
+lemma extension_beta:
fixes f :: "'a::type \<Rightarrow> 'c::cpo"
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
- shows "basis_fun f\<cdot>x = lub (f ` rep x)"
-unfolding basis_fun_def
+ shows "extension f\<cdot>x = lub (f ` rep x)"
+unfolding extension_def
proof (rule beta_cfun)
have lub: "\<And>x. \<exists>u. f ` rep x <<| u"
- using f_mono by (rule basis_fun_lemma)
+ using f_mono by (rule extension_lemma)
show cont: "cont (\<lambda>x. lub (f ` rep x))"
apply (rule contI2)
apply (rule monofunI)
@@ -341,11 +341,11 @@
done
qed
-lemma basis_fun_principal:
+lemma extension_principal:
fixes f :: "'a::type \<Rightarrow> 'c::cpo"
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
- shows "basis_fun f\<cdot>(principal a) = f a"
-apply (subst basis_fun_beta, erule f_mono)
+ shows "extension f\<cdot>(principal a) = f a"
+apply (subst extension_beta, erule f_mono)
apply (subst rep_principal)
apply (rule lub_eqI)
apply (rule is_lub_maximal)
@@ -355,34 +355,34 @@
apply (simp add: r_refl)
done
-lemma basis_fun_mono:
+lemma extension_mono:
assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
assumes below: "\<And>a. f a \<sqsubseteq> g a"
- shows "basis_fun f \<sqsubseteq> basis_fun g"
+ shows "extension f \<sqsubseteq> extension g"
apply (rule cfun_belowI)
- apply (simp only: basis_fun_beta f_mono g_mono)
+ apply (simp only: extension_beta f_mono g_mono)
apply (rule is_lub_thelub_ex)
- apply (rule basis_fun_lemma, erule f_mono)
+ apply (rule extension_lemma, erule f_mono)
apply (rule ub_imageI, rename_tac a)
apply (rule below_trans [OF below])
apply (rule is_ub_thelub_ex)
- apply (rule basis_fun_lemma, erule g_mono)
+ apply (rule extension_lemma, erule g_mono)
apply (erule imageI)
done
-lemma cont_basis_fun:
+lemma cont_extension:
assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b"
assumes f_cont: "\<And>a. cont (\<lambda>x. f x a)"
- shows "cont (\<lambda>x. basis_fun (\<lambda>a. f x a))"
+ shows "cont (\<lambda>x. extension (\<lambda>a. f x a))"
apply (rule contI2)
apply (rule monofunI)
- apply (rule basis_fun_mono, erule f_mono, erule f_mono)
+ apply (rule extension_mono, erule f_mono, erule f_mono)
apply (erule cont2monofunE [OF f_cont])
apply (rule cfun_belowI)
apply (rule principal_induct, simp)
apply (simp only: contlub_cfun_fun)
- apply (simp only: basis_fun_principal f_mono)
+ apply (simp only: extension_principal f_mono)
apply (simp add: cont2contlubE [OF f_cont])
done
--- a/src/HOL/HOLCF/ConvexPD.thy Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy Wed Dec 22 18:24:04 2010 -0800
@@ -168,11 +168,11 @@
definition
convex_unit :: "'a \<rightarrow> 'a convex_pd" where
- "convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
+ "convex_unit = compact_basis.extension (\<lambda>a. convex_principal (PDUnit a))"
definition
convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
- "convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
+ "convex_plus = convex_pd.extension (\<lambda>t. convex_pd.extension (\<lambda>u.
convex_principal (PDPlus t u)))"
abbreviation
@@ -190,13 +190,13 @@
lemma convex_unit_Rep_compact_basis [simp]:
"{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)"
unfolding convex_unit_def
-by (simp add: compact_basis.basis_fun_principal PDUnit_convex_mono)
+by (simp add: compact_basis.extension_principal PDUnit_convex_mono)
lemma convex_plus_principal [simp]:
"convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
unfolding convex_plus_def
-by (simp add: convex_pd.basis_fun_principal
- convex_pd.basis_fun_mono PDPlus_convex_mono)
+by (simp add: convex_pd.extension_principal
+ convex_pd.extension_mono PDPlus_convex_mono)
interpretation convex_add: semilattice convex_add proof
fix xs ys zs :: "'a convex_pd"
@@ -342,7 +342,7 @@
definition
convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
- "convex_bind = convex_pd.basis_fun convex_bind_basis"
+ "convex_bind = convex_pd.extension convex_bind_basis"
syntax
"_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
@@ -354,7 +354,7 @@
lemma convex_bind_principal [simp]:
"convex_bind\<cdot>(convex_principal t) = convex_bind_basis t"
unfolding convex_bind_def
-apply (rule convex_pd.basis_fun_principal)
+apply (rule convex_pd.extension_principal)
apply (erule convex_bind_basis_mono)
done
@@ -521,12 +521,12 @@
definition
convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where
- "convex_to_upper = convex_pd.basis_fun upper_principal"
+ "convex_to_upper = convex_pd.extension upper_principal"
lemma convex_to_upper_principal [simp]:
"convex_to_upper\<cdot>(convex_principal t) = upper_principal t"
unfolding convex_to_upper_def
-apply (rule convex_pd.basis_fun_principal)
+apply (rule convex_pd.extension_principal)
apply (rule upper_pd.principal_mono)
apply (erule convex_le_imp_upper_le)
done
@@ -560,12 +560,12 @@
definition
convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where
- "convex_to_lower = convex_pd.basis_fun lower_principal"
+ "convex_to_lower = convex_pd.extension lower_principal"
lemma convex_to_lower_principal [simp]:
"convex_to_lower\<cdot>(convex_principal t) = lower_principal t"
unfolding convex_to_lower_def
-apply (rule convex_pd.basis_fun_principal)
+apply (rule convex_pd.extension_principal)
apply (rule lower_pd.principal_mono)
apply (erule convex_le_imp_lower_le)
done
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Wed Dec 22 18:24:04 2010 -0800
@@ -569,18 +569,18 @@
definition
defl_approx :: "nat \<Rightarrow> 'a defl \<rightarrow> 'a defl"
where
- "defl_approx = (\<lambda>i. defl.basis_fun (\<lambda>d. defl_principal (fd_take i d)))"
+ "defl_approx = (\<lambda>i. defl.extension (\<lambda>d. defl_principal (fd_take i d)))"
lemma defl_approx_principal:
"defl_approx i\<cdot>(defl_principal d) = defl_principal (fd_take i d)"
unfolding defl_approx_def
-by (simp add: defl.basis_fun_principal fd_take_mono)
+by (simp add: defl.extension_principal fd_take_mono)
lemma defl_approx: "approx_chain defl_approx"
proof
show chain: "chain defl_approx"
unfolding defl_approx_def
- by (simp add: chainI defl.basis_fun_mono fd_take_mono fd_take_chain)
+ by (simp add: chainI defl.extension_mono fd_take_mono fd_take_chain)
show idem: "\<And>i x. defl_approx i\<cdot>(defl_approx i\<cdot>x) = defl_approx i\<cdot>x"
apply (induct_tac x rule: defl.principal_induct, simp)
apply (simp add: defl_approx_principal fd_take_idem)
@@ -594,7 +594,7 @@
apply (simp add: contlub_cfun_fun chain lub_below_iff chain below)
apply (induct_tac x rule: defl.principal_induct, simp)
apply (simp add: contlub_cfun_fun chain)
- apply (simp add: compact_below_lub_iff defl.compact_principal chain)
+ apply (simp add: compact_below_lub_iff chain)
apply (simp add: defl_approx_principal)
apply (subgoal_tac "\<exists>i. fd_take i a = a", metis below_refl)
apply (rule fd_take_covers)
--- a/src/HOL/HOLCF/LowerPD.thy Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy Wed Dec 22 18:24:04 2010 -0800
@@ -123,11 +123,11 @@
definition
lower_unit :: "'a \<rightarrow> 'a lower_pd" where
- "lower_unit = compact_basis.basis_fun (\<lambda>a. lower_principal (PDUnit a))"
+ "lower_unit = compact_basis.extension (\<lambda>a. lower_principal (PDUnit a))"
definition
lower_plus :: "'a lower_pd \<rightarrow> 'a lower_pd \<rightarrow> 'a lower_pd" where
- "lower_plus = lower_pd.basis_fun (\<lambda>t. lower_pd.basis_fun (\<lambda>u.
+ "lower_plus = lower_pd.extension (\<lambda>t. lower_pd.extension (\<lambda>u.
lower_principal (PDPlus t u)))"
abbreviation
@@ -145,13 +145,13 @@
lemma lower_unit_Rep_compact_basis [simp]:
"{Rep_compact_basis a}\<flat> = lower_principal (PDUnit a)"
unfolding lower_unit_def
-by (simp add: compact_basis.basis_fun_principal PDUnit_lower_mono)
+by (simp add: compact_basis.extension_principal PDUnit_lower_mono)
lemma lower_plus_principal [simp]:
"lower_principal t +\<flat> lower_principal u = lower_principal (PDPlus t u)"
unfolding lower_plus_def
-by (simp add: lower_pd.basis_fun_principal
- lower_pd.basis_fun_mono PDPlus_lower_mono)
+by (simp add: lower_pd.extension_principal
+ lower_pd.extension_mono PDPlus_lower_mono)
interpretation lower_add: semilattice lower_add proof
fix xs ys zs :: "'a lower_pd"
@@ -335,7 +335,7 @@
definition
lower_bind :: "'a lower_pd \<rightarrow> ('a \<rightarrow> 'b lower_pd) \<rightarrow> 'b lower_pd" where
- "lower_bind = lower_pd.basis_fun lower_bind_basis"
+ "lower_bind = lower_pd.extension lower_bind_basis"
syntax
"_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
@@ -347,7 +347,7 @@
lemma lower_bind_principal [simp]:
"lower_bind\<cdot>(lower_principal t) = lower_bind_basis t"
unfolding lower_bind_def
-apply (rule lower_pd.basis_fun_principal)
+apply (rule lower_pd.extension_principal)
apply (erule lower_bind_basis_mono)
done
--- a/src/HOL/HOLCF/Universal.thy Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/Universal.thy Wed Dec 22 18:24:04 2010 -0800
@@ -856,17 +856,17 @@
definition
udom_emb :: "'a \<rightarrow> udom"
where
- "udom_emb = compact_basis.basis_fun (\<lambda>x. udom_principal (basis_emb x))"
+ "udom_emb = compact_basis.extension (\<lambda>x. udom_principal (basis_emb x))"
definition
udom_prj :: "udom \<rightarrow> 'a"
where
- "udom_prj = udom.basis_fun (\<lambda>x. Rep_compact_basis (basis_prj x))"
+ "udom_prj = udom.extension (\<lambda>x. Rep_compact_basis (basis_prj x))"
lemma udom_emb_principal:
"udom_emb\<cdot>(Rep_compact_basis x) = udom_principal (basis_emb x)"
unfolding udom_emb_def
-apply (rule compact_basis.basis_fun_principal)
+apply (rule compact_basis.extension_principal)
apply (rule udom.principal_mono)
apply (erule basis_emb_mono)
done
@@ -874,7 +874,7 @@
lemma udom_prj_principal:
"udom_prj\<cdot>(udom_principal x) = Rep_compact_basis (basis_prj x)"
unfolding udom_prj_def
-apply (rule udom.basis_fun_principal)
+apply (rule udom.extension_principal)
apply (rule compact_basis.principal_mono)
apply (erule basis_prj_mono)
done
@@ -903,7 +903,7 @@
udom_approx :: "nat \<Rightarrow> udom \<rightarrow> udom"
where
"udom_approx i =
- udom.basis_fun (\<lambda>x. udom_principal (ubasis_until (\<lambda>y. y \<le> i) x))"
+ udom.extension (\<lambda>x. udom_principal (ubasis_until (\<lambda>y. y \<le> i) x))"
lemma udom_approx_mono:
"ubasis_le a b \<Longrightarrow>
@@ -923,7 +923,7 @@
"udom_approx i\<cdot>(udom_principal x) =
udom_principal (ubasis_until (\<lambda>y. y \<le> i) x)"
unfolding udom_approx_def
-apply (rule udom.basis_fun_principal)
+apply (rule udom.extension_principal)
apply (erule udom_approx_mono)
done
@@ -957,7 +957,7 @@
lemma chain_udom_approx [simp]: "chain (\<lambda>i. udom_approx i)"
unfolding udom_approx_def
apply (rule chainI)
-apply (rule udom.basis_fun_mono)
+apply (rule udom.extension_mono)
apply (erule udom_approx_mono)
apply (erule udom_approx_mono)
apply (rule udom.principal_mono)
--- a/src/HOL/HOLCF/UpperPD.thy Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy Wed Dec 22 18:24:04 2010 -0800
@@ -121,11 +121,11 @@
definition
upper_unit :: "'a \<rightarrow> 'a upper_pd" where
- "upper_unit = compact_basis.basis_fun (\<lambda>a. upper_principal (PDUnit a))"
+ "upper_unit = compact_basis.extension (\<lambda>a. upper_principal (PDUnit a))"
definition
upper_plus :: "'a upper_pd \<rightarrow> 'a upper_pd \<rightarrow> 'a upper_pd" where
- "upper_plus = upper_pd.basis_fun (\<lambda>t. upper_pd.basis_fun (\<lambda>u.
+ "upper_plus = upper_pd.extension (\<lambda>t. upper_pd.extension (\<lambda>u.
upper_principal (PDPlus t u)))"
abbreviation
@@ -143,13 +143,13 @@
lemma upper_unit_Rep_compact_basis [simp]:
"{Rep_compact_basis a}\<sharp> = upper_principal (PDUnit a)"
unfolding upper_unit_def
-by (simp add: compact_basis.basis_fun_principal PDUnit_upper_mono)
+by (simp add: compact_basis.extension_principal PDUnit_upper_mono)
lemma upper_plus_principal [simp]:
"upper_principal t +\<sharp> upper_principal u = upper_principal (PDPlus t u)"
unfolding upper_plus_def
-by (simp add: upper_pd.basis_fun_principal
- upper_pd.basis_fun_mono PDPlus_upper_mono)
+by (simp add: upper_pd.extension_principal
+ upper_pd.extension_mono PDPlus_upper_mono)
interpretation upper_add: semilattice upper_add proof
fix xs ys zs :: "'a upper_pd"
@@ -330,7 +330,7 @@
definition
upper_bind :: "'a upper_pd \<rightarrow> ('a \<rightarrow> 'b upper_pd) \<rightarrow> 'b upper_pd" where
- "upper_bind = upper_pd.basis_fun upper_bind_basis"
+ "upper_bind = upper_pd.extension upper_bind_basis"
syntax
"_upper_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
@@ -342,7 +342,7 @@
lemma upper_bind_principal [simp]:
"upper_bind\<cdot>(upper_principal t) = upper_bind_basis t"
unfolding upper_bind_def
-apply (rule upper_pd.basis_fun_principal)
+apply (rule upper_pd.extension_principal)
apply (erule upper_bind_basis_mono)
done