rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
--- a/src/HOLCF/Adm.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Adm.thy Fri May 08 16:19:51 2009 -0700
@@ -78,7 +78,7 @@
"\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk> \<Longrightarrow>
(\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
apply (frule (1) adm_disj_lemma1)
- apply (rule antisym_less)
+ apply (rule below_antisym)
apply (rule lub_mono, assumption+)
apply (erule chain_mono)
apply (simp add: adm_disj_lemma2)
@@ -122,7 +122,7 @@
text {* admissibility and continuity *}
-lemma adm_less: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
+lemma adm_below: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
apply (rule admI)
apply (simp add: cont2contlubE)
apply (rule lub_mono)
@@ -132,7 +132,7 @@
done
lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
-by (simp add: po_eq_conv adm_conj adm_less)
+by (simp add: po_eq_conv adm_conj adm_below)
lemma adm_subst: "\<lbrakk>cont t; adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
apply (rule admI)
@@ -142,11 +142,11 @@
apply (erule spec)
done
-lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
+lemma adm_not_below: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
apply (rule admI)
apply (drule_tac x=0 in spec)
apply (erule contrapos_nn)
-apply (erule rev_trans_less)
+apply (erule rev_below_trans)
apply (erule cont2mono [THEN monofunE])
apply (erule is_ub_thelub)
done
@@ -179,21 +179,21 @@
apply (drule (1) compactD2, simp)
apply (erule exE, rule_tac x=i in exI)
apply (rule max_in_chainI)
-apply (rule antisym_less)
+apply (rule below_antisym)
apply (erule (1) chain_mono)
-apply (erule (1) trans_less [OF is_ub_thelub])
+apply (erule (1) below_trans [OF is_ub_thelub])
done
text {* admissibility and compactness *}
-lemma adm_compact_not_less: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
+lemma adm_compact_not_below: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
unfolding compact_def by (rule adm_subst)
lemma adm_neq_compact: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. t x \<noteq> k)"
-by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less)
+by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
lemma adm_compact_neq: "\<lbrakk>compact k; cont t\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<noteq> t x)"
-by (simp add: po_eq_conv adm_imp adm_not_less adm_compact_not_less)
+by (simp add: po_eq_conv adm_imp adm_not_below adm_compact_not_below)
lemma compact_UU [simp, intro]: "compact \<bottom>"
by (rule compactI, simp add: adm_not_free)
@@ -210,7 +210,7 @@
lemmas adm_lemmas [simp] =
adm_not_free adm_conj adm_all adm_ball adm_disj adm_imp adm_iff
- adm_less adm_eq adm_not_less
- adm_compact_not_less adm_compact_neq adm_neq_compact adm_not_UU
+ adm_below adm_eq adm_not_below
+ adm_compact_not_below adm_compact_neq adm_neq_compact adm_not_UU
end
--- a/src/HOLCF/Algebraic.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Algebraic.thy Fri May 08 16:19:51 2009 -0700
@@ -33,21 +33,21 @@
locale pre_deflation =
fixes f :: "'a \<rightarrow> 'a::cpo"
- assumes less: "\<And>x. f\<cdot>x \<sqsubseteq> x"
+ assumes below: "\<And>x. f\<cdot>x \<sqsubseteq> x"
assumes finite_range: "finite (range (\<lambda>x. f\<cdot>x))"
begin
-lemma iterate_less: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
-by (induct i, simp_all add: trans_less [OF less])
+lemma iterate_below: "iterate i\<cdot>f\<cdot>x \<sqsubseteq> x"
+by (induct i, simp_all add: below_trans [OF below])
lemma iterate_fixed: "f\<cdot>x = x \<Longrightarrow> iterate i\<cdot>f\<cdot>x = x"
by (induct i, simp_all)
lemma antichain_iterate_app: "i \<le> j \<Longrightarrow> iterate j\<cdot>f\<cdot>x \<sqsubseteq> iterate i\<cdot>f\<cdot>x"
apply (erule le_Suc_induct)
-apply (simp add: less)
-apply (rule refl_less)
-apply (erule (1) trans_less)
+apply (simp add: below)
+apply (rule below_refl)
+apply (erule (1) below_trans)
done
lemma finite_range_iterate_app: "finite (range (\<lambda>i. iterate i\<cdot>f\<cdot>x))"
@@ -144,7 +144,7 @@
next
fix x :: 'a
show "d\<cdot>x \<sqsubseteq> x"
- by (rule MOST_d, simp add: iterate_less)
+ by (rule MOST_d, simp add: iterate_below)
next
from finite_range
have "finite {x. f\<cdot>x = x}"
@@ -163,7 +163,7 @@
interpret d: finite_deflation d by fact
fix x
show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
- by (simp, rule trans_less [OF d.less f])
+ by (simp, rule below_trans [OF d.below f])
show "finite (range (\<lambda>x. (d oo f)\<cdot>x))"
by (rule finite_subset [OF _ d.finite_range], auto)
qed
@@ -185,9 +185,9 @@
apply safe
apply (erule subst)
apply (rule d.idem)
- apply (rule antisym_less)
+ apply (rule below_antisym)
apply (rule f)
- apply (erule subst, rule d.less)
+ apply (erule subst, rule d.below)
apply simp
done
qed
@@ -199,18 +199,17 @@
typedef (open) 'a fin_defl = "{d::'a \<rightarrow> 'a. finite_deflation d}"
by (fast intro: finite_deflation_approx)
-instantiation fin_defl :: (profinite) sq_ord
+instantiation fin_defl :: (profinite) below
begin
-definition
- sq_le_fin_defl_def:
+definition below_fin_defl_def:
"op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_fin_defl x \<sqsubseteq> Rep_fin_defl y"
instance ..
end
instance fin_defl :: (profinite) po
-by (rule typedef_po [OF type_definition_fin_defl sq_le_fin_defl_def])
+by (rule typedef_po [OF type_definition_fin_defl below_fin_defl_def])
lemma finite_deflation_Rep_fin_defl: "finite_deflation (Rep_fin_defl d)"
using Rep_fin_defl by simp
@@ -218,27 +217,27 @@
interpretation Rep_fin_defl: finite_deflation "Rep_fin_defl d"
by (rule finite_deflation_Rep_fin_defl)
-lemma fin_defl_lessI:
+lemma fin_defl_belowI:
"(\<And>x. Rep_fin_defl a\<cdot>x = x \<Longrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a \<sqsubseteq> b"
-unfolding sq_le_fin_defl_def
-by (rule Rep_fin_defl.lessI)
+unfolding below_fin_defl_def
+by (rule Rep_fin_defl.belowI)
-lemma fin_defl_lessD:
+lemma fin_defl_belowD:
"\<lbrakk>a \<sqsubseteq> b; Rep_fin_defl a\<cdot>x = x\<rbrakk> \<Longrightarrow> Rep_fin_defl b\<cdot>x = x"
-unfolding sq_le_fin_defl_def
-by (rule Rep_fin_defl.lessD)
+unfolding below_fin_defl_def
+by (rule Rep_fin_defl.belowD)
lemma fin_defl_eqI:
"(\<And>x. Rep_fin_defl a\<cdot>x = x \<longleftrightarrow> Rep_fin_defl b\<cdot>x = x) \<Longrightarrow> a = b"
-apply (rule antisym_less)
-apply (rule fin_defl_lessI, simp)
-apply (rule fin_defl_lessI, simp)
+apply (rule below_antisym)
+apply (rule fin_defl_belowI, simp)
+apply (rule fin_defl_belowI, simp)
done
lemma Abs_fin_defl_mono:
"\<lbrakk>finite_deflation a; finite_deflation b; a \<sqsubseteq> b\<rbrakk>
\<Longrightarrow> Abs_fin_defl a \<sqsubseteq> Abs_fin_defl b"
-unfolding sq_le_fin_defl_def
+unfolding below_fin_defl_def
by (simp add: Abs_fin_defl_inverse)
@@ -257,7 +256,7 @@
apply (rule pre_deflation.finite_deflation_d)
apply (rule pre_deflation_d_f)
apply (rule finite_deflation_approx)
-apply (rule Rep_fin_defl.less)
+apply (rule Rep_fin_defl.below)
done
lemma fd_take_fixed_iff:
@@ -265,10 +264,10 @@
approx i\<cdot>x = x \<and> Rep_fin_defl d\<cdot>x = x"
unfolding Rep_fin_defl_fd_take
by (rule eventual_iterate_oo_fixed_iff
- [OF finite_deflation_approx Rep_fin_defl.less])
+ [OF finite_deflation_approx Rep_fin_defl.below])
-lemma fd_take_less: "fd_take n d \<sqsubseteq> d"
-apply (rule fin_defl_lessI)
+lemma fd_take_below: "fd_take n d \<sqsubseteq> d"
+apply (rule fin_defl_belowI)
apply (simp add: fd_take_fixed_iff)
done
@@ -278,16 +277,16 @@
done
lemma fd_take_mono: "a \<sqsubseteq> b \<Longrightarrow> fd_take n a \<sqsubseteq> fd_take n b"
-apply (rule fin_defl_lessI)
+apply (rule fin_defl_belowI)
apply (simp add: fd_take_fixed_iff)
-apply (simp add: fin_defl_lessD)
+apply (simp add: fin_defl_belowD)
done
lemma approx_fixed_le_lemma: "\<lbrakk>i \<le> j; approx i\<cdot>x = x\<rbrakk> \<Longrightarrow> approx j\<cdot>x = x"
by (erule subst, simp add: min_def)
lemma fd_take_chain: "m \<le> n \<Longrightarrow> fd_take m a \<sqsubseteq> fd_take n a"
-apply (rule fin_defl_lessI)
+apply (rule fin_defl_belowI)
apply (simp add: fd_take_fixed_iff)
apply (simp add: approx_fixed_le_lemma)
done
@@ -304,9 +303,9 @@
lemma fd_take_covers: "\<exists>n. fd_take n a = a"
apply (rule_tac x=
"Max ((\<lambda>x. LEAST n. approx n\<cdot>x = x) ` {x. Rep_fin_defl a\<cdot>x = x})" in exI)
-apply (rule antisym_less)
-apply (rule fd_take_less)
-apply (rule fin_defl_lessI)
+apply (rule below_antisym)
+apply (rule fd_take_below)
+apply (rule fin_defl_belowI)
apply (simp add: fd_take_fixed_iff)
apply (rule approx_fixed_le_lemma)
apply (rule Max_ge)
@@ -320,9 +319,9 @@
apply (rule Rep_fin_defl.compact)
done
-interpretation fin_defl: basis_take sq_le fd_take
+interpretation fin_defl: basis_take below fd_take
apply default
-apply (rule fd_take_less)
+apply (rule fd_take_below)
apply (rule fd_take_idem)
apply (erule fd_take_mono)
apply (rule fd_take_chain, simp)
@@ -333,10 +332,10 @@
subsection {* Defining algebraic deflations by ideal completion *}
typedef (open) 'a alg_defl =
- "{S::'a fin_defl set. sq_le.ideal S}"
-by (fast intro: sq_le.ideal_principal)
+ "{S::'a fin_defl set. below.ideal S}"
+by (fast intro: below.ideal_principal)
-instantiation alg_defl :: (profinite) sq_ord
+instantiation alg_defl :: (profinite) below
begin
definition
@@ -346,19 +345,19 @@
end
instance alg_defl :: (profinite) po
-by (rule sq_le.typedef_ideal_po
- [OF type_definition_alg_defl sq_le_alg_defl_def])
+by (rule below.typedef_ideal_po
+ [OF type_definition_alg_defl below_alg_defl_def])
instance alg_defl :: (profinite) cpo
-by (rule sq_le.typedef_ideal_cpo
- [OF type_definition_alg_defl sq_le_alg_defl_def])
+by (rule below.typedef_ideal_cpo
+ [OF type_definition_alg_defl below_alg_defl_def])
lemma Rep_alg_defl_lub:
"chain Y \<Longrightarrow> Rep_alg_defl (\<Squnion>i. Y i) = (\<Union>i. Rep_alg_defl (Y i))"
-by (rule sq_le.typedef_ideal_rep_contlub
- [OF type_definition_alg_defl sq_le_alg_defl_def])
+by (rule below.typedef_ideal_rep_contlub
+ [OF type_definition_alg_defl below_alg_defl_def])
-lemma ideal_Rep_alg_defl: "sq_le.ideal (Rep_alg_defl xs)"
+lemma ideal_Rep_alg_defl: "below.ideal (Rep_alg_defl xs)"
by (rule Rep_alg_defl [unfolded mem_Collect_eq])
definition
@@ -368,15 +367,15 @@
lemma Rep_alg_defl_principal:
"Rep_alg_defl (alg_defl_principal t) = {u. u \<sqsubseteq> t}"
unfolding alg_defl_principal_def
-by (simp add: Abs_alg_defl_inverse sq_le.ideal_principal)
+by (simp add: Abs_alg_defl_inverse below.ideal_principal)
interpretation alg_defl:
- ideal_completion sq_le fd_take alg_defl_principal Rep_alg_defl
+ ideal_completion below fd_take alg_defl_principal Rep_alg_defl
apply default
apply (rule ideal_Rep_alg_defl)
apply (erule Rep_alg_defl_lub)
apply (rule Rep_alg_defl_principal)
-apply (simp only: sq_le_alg_defl_def)
+apply (simp only: below_alg_defl_def)
done
text {* Algebraic deflations are pointed *}
@@ -443,7 +442,7 @@
"cast\<cdot>(alg_defl_principal a) = Rep_fin_defl a"
unfolding cast_def
apply (rule alg_defl.basis_fun_principal)
-apply (simp only: sq_le_fin_defl_def)
+apply (simp only: below_fin_defl_def)
done
lemma deflation_cast: "deflation (cast\<cdot>d)"
@@ -522,10 +521,10 @@
apply (rule finite_deflation_p_d_e)
apply (rule finite_deflation_cast)
apply (rule compact_approx)
- apply (rule sq_ord_less_eq_trans [OF _ d])
+ apply (rule below_eq_trans [OF _ d])
apply (rule monofun_cfun_fun)
apply (rule monofun_cfun_arg)
- apply (rule approx_less)
+ apply (rule approx_below)
done
show "(\<Squnion>i. ?a i) = ID"
apply (rule ext_cfun, simp)
--- a/src/HOLCF/Bifinite.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Bifinite.thy Fri May 08 16:19:51 2009 -0700
@@ -19,7 +19,7 @@
class bifinite = profinite + pcpo
-lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x"
+lemma approx_below: "approx i\<cdot>x \<sqsubseteq> x"
proof -
have "chain (\<lambda>i. approx i\<cdot>x)" by simp
hence "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by (rule is_ub_thelub)
@@ -32,7 +32,7 @@
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
by (rule approx_idem)
show "approx i\<cdot>x \<sqsubseteq> x"
- by (rule approx_less)
+ by (rule approx_below)
show "finite {x. approx i\<cdot>x = x}"
by (rule finite_fixes_approx)
qed
@@ -49,17 +49,17 @@
by (rule ext_cfun, simp add: contlub_cfun_fun)
lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
-by (rule UU_I, rule approx_less)
+by (rule UU_I, rule approx_below)
lemma approx_approx1:
"i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x"
-apply (rule deflation_less_comp1 [OF deflation_approx deflation_approx])
+apply (rule deflation_below_comp1 [OF deflation_approx deflation_approx])
apply (erule chain_mono [OF chain_approx])
done
lemma approx_approx2:
"j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>x"
-apply (rule deflation_less_comp2 [OF deflation_approx deflation_approx])
+apply (rule deflation_below_comp2 [OF deflation_approx deflation_approx])
apply (erule chain_mono [OF chain_approx])
done
@@ -99,7 +99,7 @@
thus "P x" by simp
qed
-lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
+lemma profinite_below_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
apply (rule lub_mono, simp, simp, simp)
done
--- a/src/HOLCF/Cfun.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Cfun.thy Fri May 08 16:19:51 2009 -0700
@@ -105,19 +105,19 @@
by (rule typedef_finite_po [OF type_definition_CFun])
instance "->" :: (finite_po, chfin) chfin
-by (rule typedef_chfin [OF type_definition_CFun less_CFun_def])
+by (rule typedef_chfin [OF type_definition_CFun below_CFun_def])
instance "->" :: (cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: less_CFun_def Rep_CFun_inject)
+by intro_classes (simp add: below_CFun_def Rep_CFun_inject)
instance "->" :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo [OF type_definition_CFun less_CFun_def UU_CFun])
+by (rule typedef_pcpo [OF type_definition_CFun below_CFun_def UU_CFun])
lemmas Rep_CFun_strict =
- typedef_Rep_strict [OF type_definition_CFun less_CFun_def UU_CFun]
+ typedef_Rep_strict [OF type_definition_CFun below_CFun_def UU_CFun]
lemmas Abs_CFun_strict =
- typedef_Abs_strict [OF type_definition_CFun less_CFun_def UU_CFun]
+ typedef_Abs_strict [OF type_definition_CFun below_CFun_def UU_CFun]
text {* function application is strict in its first argument *}
@@ -153,11 +153,11 @@
text {* Extensionality wrt. ordering for continuous functions *}
-lemma expand_cfun_less: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)"
-by (simp add: less_CFun_def expand_fun_less)
+lemma expand_cfun_below: "f \<sqsubseteq> g = (\<forall>x. f\<cdot>x \<sqsubseteq> g\<cdot>x)"
+by (simp add: below_CFun_def expand_fun_below)
-lemma less_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: expand_cfun_less)
+lemma below_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: expand_cfun_below)
text {* Congruence for continuous function application *}
@@ -205,13 +205,13 @@
text {* monotonicity of application *}
lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
-by (simp add: expand_cfun_less)
+by (simp add: expand_cfun_below)
lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
by (rule monofun_Rep_CFun2 [THEN monofunE])
lemma monofun_cfun: "\<lbrakk>f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>y"
-by (rule trans_less [OF monofun_cfun_fun monofun_cfun_arg])
+by (rule below_trans [OF monofun_cfun_fun monofun_cfun_arg])
text {* ch2ch - rules for the type @{typ "'a -> 'b"} *}
@@ -230,7 +230,7 @@
lemma ch2ch_LAM [simp]:
"\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)"
-by (simp add: chain_def expand_cfun_less)
+by (simp add: chain_def expand_cfun_below)
text {* contlub, cont properties of @{term Rep_CFun} in both arguments *}
@@ -316,7 +316,7 @@
lemma cont2mono_LAM:
"\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
\<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
- unfolding monofun_def expand_cfun_less by simp
+ unfolding monofun_def expand_cfun_below by simp
text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
@@ -365,7 +365,7 @@
lemma semi_monofun_Abs_CFun:
"\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_CFun f \<sqsubseteq> Abs_CFun g"
-by (simp add: less_CFun_def Abs_CFun_inverse2)
+by (simp add: below_CFun_def Abs_CFun_inverse2)
text {* some lemmata for functions with flat/chfin domain/range types *}
@@ -401,7 +401,7 @@
apply simp
done
-lemma injection_less:
+lemma injection_below:
"\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> (g\<cdot>x \<sqsubseteq> g\<cdot>y) = (x \<sqsubseteq> y)"
apply (rule iffI)
apply (drule_tac f=f in monofun_cfun_arg)
--- a/src/HOLCF/CompactBasis.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/CompactBasis.thy Fri May 08 16:19:51 2009 -0700
@@ -18,7 +18,7 @@
lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
by (rule Rep_compact_basis [unfolded mem_Collect_eq])
-instantiation compact_basis :: (profinite) sq_ord
+instantiation compact_basis :: (profinite) below
begin
definition
@@ -47,12 +47,12 @@
lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
interpretation compact_basis:
- basis_take sq_le compact_take
+ basis_take below compact_take
proof
fix n :: nat and a :: "'a compact_basis"
show "compact_take n a \<sqsubseteq> a"
unfolding compact_le_def
- by (simp add: Rep_compact_take approx_less)
+ by (simp add: Rep_compact_take approx_below)
next
fix n :: nat and a :: "'a compact_basis"
show "compact_take n (compact_take n a) = compact_take n a"
@@ -93,15 +93,15 @@
"approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
interpretation compact_basis:
- ideal_completion sq_le compact_take Rep_compact_basis approximants
+ ideal_completion below compact_take Rep_compact_basis approximants
proof
fix w :: 'a
- show "preorder.ideal sq_le (approximants w)"
- proof (rule sq_le.idealI)
+ show "preorder.ideal below (approximants w)"
+ proof (rule below.idealI)
show "\<exists>x. x \<in> approximants w"
unfolding approximants_def
apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
- apply (simp add: Abs_compact_basis_inverse approx_less)
+ apply (simp add: Abs_compact_basis_inverse approx_below)
done
next
fix x y :: "'a compact_basis"
@@ -116,7 +116,7 @@
apply (clarify, rename_tac i j)
apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
apply (simp add: compact_le_def)
- apply (simp add: Abs_compact_basis_inverse approx_less)
+ apply (simp add: Abs_compact_basis_inverse approx_below)
apply (erule subst, erule subst)
apply (simp add: monofun_cfun chain_mono [OF chain_approx])
done
@@ -126,7 +126,7 @@
unfolding approximants_def
apply simp
apply (simp add: compact_le_def)
- apply (erule (1) trans_less)
+ apply (erule (1) below_trans)
done
qed
next
@@ -136,7 +136,7 @@
unfolding approximants_def
apply safe
apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
- apply (erule trans_less, rule is_ub_thelub [OF Y])
+ apply (erule below_trans, rule is_ub_thelub [OF Y])
done
next
fix a :: "'a compact_basis"
@@ -148,7 +148,7 @@
apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
apply (rule admD, simp, simp)
apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
- apply (simp add: approximants_def Abs_compact_basis_inverse approx_less)
+ apply (simp add: approximants_def Abs_compact_basis_inverse approx_below)
apply (simp add: approximants_def Abs_compact_basis_inverse)
done
qed
@@ -288,7 +288,7 @@
apply (cut_tac a=a in compact_basis.take_covers)
apply (clarify, rule_tac x=n in exI)
apply (clarify, simp)
-apply (rule antisym_less)
+apply (rule below_antisym)
apply (rule compact_basis.take_less)
apply (drule_tac a=a in compact_basis.take_chain_le)
apply simp
--- a/src/HOLCF/Completion.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Completion.thy Fri May 08 16:19:51 2009 -0700
@@ -108,11 +108,11 @@
done
lemma typedef_ideal_po:
- fixes Abs :: "'a set \<Rightarrow> 'b::sq_ord"
+ fixes Abs :: "'a set \<Rightarrow> 'b::below"
assumes type: "type_definition Rep Abs {S. ideal S}"
- assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
+ assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
shows "OFCLASS('b, po_class)"
- apply (intro_classes, unfold less)
+ apply (intro_classes, unfold below)
apply (rule subset_refl)
apply (erule (1) subset_trans)
apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
@@ -122,7 +122,7 @@
lemma
fixes Abs :: "'a set \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs {S. ideal S}"
- assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
+ assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
assumes S: "chain S"
shows typedef_ideal_lub: "range S <<| Abs (\<Union>i. Rep (S i))"
and typedef_ideal_rep_contlub: "Rep (\<Squnion>i. S i) = (\<Union>i. Rep (S i))"
@@ -130,7 +130,7 @@
have 1: "ideal (\<Union>i. Rep (S i))"
apply (rule ideal_UN)
apply (rule type_definition.Rep [OF type, unfolded mem_Collect_eq])
- apply (subst less [symmetric])
+ apply (subst below [symmetric])
apply (erule chain_mono [OF S])
done
hence 2: "Rep (Abs (\<Union>i. Rep (S i))) = (\<Union>i. Rep (S i))"
@@ -138,8 +138,8 @@
show 3: "range S <<| Abs (\<Union>i. Rep (S i))"
apply (rule is_lubI)
apply (rule is_ubI)
- apply (simp add: less 2, fast)
- apply (simp add: less 2 is_ub_def, fast)
+ apply (simp add: below 2, fast)
+ apply (simp add: below 2 is_ub_def, fast)
done
hence 4: "(\<Squnion>i. S i) = Abs (\<Union>i. Rep (S i))"
by (rule thelubI)
@@ -150,16 +150,16 @@
lemma typedef_ideal_cpo:
fixes Abs :: "'a set \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs {S. ideal S}"
- assumes less: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
+ assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
shows "OFCLASS('b, cpo_class)"
-by (default, rule exI, erule typedef_ideal_lub [OF type less])
+by (default, rule exI, erule typedef_ideal_lub [OF type below])
end
-interpretation sq_le: preorder "sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
+interpretation below: preorder "below :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"
apply unfold_locales
-apply (rule refl_less)
-apply (erule (1) trans_less)
+apply (rule below_refl)
+apply (erule (1) below_trans)
done
subsection {* Lemmas about least upper bounds *}
@@ -229,43 +229,43 @@
apply (rule subsetI, rule UN_I [where a=0], simp_all)
done
-lemma less_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
+lemma below_def: "x \<sqsubseteq> y \<longleftrightarrow> rep x \<subseteq> rep y"
by (rule iffI [OF rep_mono subset_repD])
lemma rep_eq: "rep x = {a. principal a \<sqsubseteq> x}"
-unfolding less_def rep_principal
+unfolding below_def rep_principal
apply safe
apply (erule (1) idealD3 [OF ideal_rep])
apply (erule subsetD, simp add: r_refl)
done
-lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
+lemma mem_rep_iff_principal_below: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
by (simp add: rep_eq)
-lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
+lemma principal_below_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
by (simp add: rep_eq)
-lemma principal_less_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
-by (simp add: principal_less_iff_mem_rep rep_principal)
+lemma principal_below_iff [simp]: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
+by (simp add: principal_below_iff_mem_rep rep_principal)
lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a"
-unfolding po_eq_conv [where 'a='b] principal_less_iff ..
+unfolding po_eq_conv [where 'a='b] principal_below_iff ..
lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
by (simp add: rep_eq)
lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
-by (simp only: principal_less_iff)
+by (simp only: principal_below_iff)
-lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
-unfolding principal_less_iff_mem_rep
-by (simp add: less_def subset_eq)
+lemma belowI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
+unfolding principal_below_iff_mem_rep
+by (simp add: below_def subset_eq)
lemma lub_principal_rep: "principal ` rep x <<| x"
apply (rule is_lubI)
apply (rule ub_imageI)
apply (erule repD)
-apply (subst less_def)
+apply (subst below_def)
apply (rule subsetI)
apply (drule (1) ub_imageD)
apply (simp add: rep_eq)
@@ -299,7 +299,7 @@
apply (rule is_lub_thelub0)
apply (rule basis_fun_lemma0, erule f_mono)
apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule trans_less [OF f_mono [OF take_chain]])
+ apply (rule below_trans [OF f_mono [OF take_chain]])
apply (rule is_ub_thelub0)
apply (rule basis_fun_lemma0, erule f_mono)
apply simp
@@ -313,7 +313,7 @@
apply (rule ub_imageI, rename_tac a)
apply (cut_tac a=a in take_covers, erule exE, rename_tac i)
apply (erule subst)
- apply (rule rev_trans_less)
+ apply (rule rev_below_trans)
apply (rule_tac x=i in is_ub_thelub)
apply (rule basis_fun_lemma1, erule f_mono)
apply (rule is_ub_thelub0)
@@ -324,7 +324,7 @@
apply (rule is_lub_thelub0)
apply (rule basis_fun_lemma0, erule f_mono)
apply (rule is_ubI, clarsimp, rename_tac a)
- apply (rule trans_less [OF f_mono [OF take_less]])
+ apply (rule below_trans [OF f_mono [OF take_less]])
apply (erule (1) ub_imageD)
done
@@ -350,7 +350,7 @@
apply (erule (1) subsetD [OF rep_mono])
apply (rule is_lub_thelub0 [OF lub ub_imageI])
apply (simp add: rep_contlub, clarify)
- apply (erule rev_trans_less [OF is_ub_thelub])
+ apply (erule rev_below_trans [OF is_ub_thelub])
apply (erule is_ub_thelub0 [OF lub imageI])
done
qed
@@ -367,21 +367,21 @@
lemma basis_fun_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 less: "\<And>a. f a \<sqsubseteq> g a"
+ assumes below: "\<And>a. f a \<sqsubseteq> g a"
shows "basis_fun f \<sqsubseteq> basis_fun g"
- apply (rule less_cfun_ext)
+ apply (rule below_cfun_ext)
apply (simp only: basis_fun_beta f_mono g_mono)
apply (rule is_lub_thelub0)
apply (rule basis_fun_lemma, erule f_mono)
apply (rule ub_imageI, rename_tac a)
- apply (rule trans_less [OF less])
+ apply (rule below_trans [OF below])
apply (rule is_ub_thelub0)
apply (rule basis_fun_lemma, erule g_mono)
apply (erule imageI)
done
lemma compact_principal [simp]: "compact (principal a)"
-by (rule compactI2, simp add: principal_less_iff_mem_rep rep_contlub)
+by (rule compactI2, simp add: principal_below_iff_mem_rep rep_contlub)
subsection {* Bifiniteness of ideal completions *}
--- a/src/HOLCF/Cont.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Cont.thy Fri May 08 16:19:51 2009 -0700
@@ -121,14 +121,14 @@
lemma contI2:
assumes mono: "monofun f"
- assumes less: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
+ assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
\<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))"
shows "cont f"
apply (rule monocontlub2cont)
apply (rule mono)
apply (rule contlubI)
-apply (rule antisym_less)
-apply (rule less, assumption)
+apply (rule below_antisym)
+apply (rule below, assumption)
apply (erule ch2ch_monofun [OF mono])
apply (rule is_lub_thelub)
apply (erule ch2ch_monofun [OF mono])
@@ -192,7 +192,7 @@
by (auto intro: cont2monofunE [OF 1]
cont2monofunE [OF 2]
cont2monofunE [OF 3]
- trans_less)
+ below_trans)
next
fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) = (\<Squnion>i. f (Y i) (t (Y i)))"
--- a/src/HOLCF/ConvexPD.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/ConvexPD.thy Fri May 08 16:19:51 2009 -0700
@@ -144,7 +144,7 @@
"{S::'a pd_basis set. convex_le.ideal S}"
by (fast intro: convex_le.ideal_principal)
-instantiation convex_pd :: (profinite) sq_ord
+instantiation convex_pd :: (profinite) below
begin
definition
@@ -155,16 +155,16 @@
instance convex_pd :: (profinite) po
by (rule convex_le.typedef_ideal_po
- [OF type_definition_convex_pd sq_le_convex_pd_def])
+ [OF type_definition_convex_pd below_convex_pd_def])
instance convex_pd :: (profinite) cpo
by (rule convex_le.typedef_ideal_cpo
- [OF type_definition_convex_pd sq_le_convex_pd_def])
+ [OF type_definition_convex_pd below_convex_pd_def])
lemma Rep_convex_pd_lub:
"chain Y \<Longrightarrow> Rep_convex_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_convex_pd (Y i))"
by (rule convex_le.typedef_ideal_rep_contlub
- [OF type_definition_convex_pd sq_le_convex_pd_def])
+ [OF type_definition_convex_pd below_convex_pd_def])
lemma ideal_Rep_convex_pd: "convex_le.ideal (Rep_convex_pd xs)"
by (rule Rep_convex_pd [unfolded mem_Collect_eq])
@@ -190,7 +190,7 @@
apply (rule ideal_Rep_convex_pd)
apply (erule Rep_convex_pd_lub)
apply (rule Rep_convex_principal)
-apply (simp only: sq_le_convex_pd_def)
+apply (simp only: below_convex_pd_def)
done
text {* Convex powerdomain is pointed *}
@@ -311,7 +311,7 @@
lemmas convex_plus_aci =
convex_plus_ac convex_plus_absorb convex_plus_left_absorb
-lemma convex_unit_less_plus_iff [simp]:
+lemma convex_unit_below_plus_iff [simp]:
"{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
apply (rule iffI)
apply (subgoal_tac
@@ -329,7 +329,7 @@
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
-lemma convex_plus_less_unit_iff [simp]:
+lemma convex_plus_below_unit_iff [simp]:
"xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
apply (rule iffI)
apply (subgoal_tac
@@ -347,9 +347,9 @@
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
-lemma convex_unit_less_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
+lemma convex_unit_below_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
apply (rule iffI)
- apply (rule profinite_less_ext)
+ apply (rule profinite_below_ext)
apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -433,12 +433,12 @@
lemma monofun_LAM:
"\<lbrakk>cont f; cont g; \<And>x. f x \<sqsubseteq> g x\<rbrakk> \<Longrightarrow> (\<Lambda> x. f x) \<sqsubseteq> (\<Lambda> x. g x)"
-by (simp add: expand_cfun_less)
+by (simp add: expand_cfun_below)
lemma convex_bind_basis_mono:
"t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
apply (erule convex_le_induct)
-apply (erule (1) trans_less)
+apply (erule (1) below_trans)
apply (simp add: monofun_LAM monofun_cfun)
apply (simp add: monofun_LAM monofun_cfun)
done
@@ -606,12 +606,12 @@
text {* Ordering property *}
-lemma convex_pd_less_iff:
+lemma convex_pd_below_iff:
"(xs \<sqsubseteq> ys) =
(convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
apply (safe elim!: monofun_cfun_arg)
- apply (rule profinite_less_ext)
+ apply (rule profinite_below_ext)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (drule_tac f="approx i" in monofun_cfun_arg)
apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
@@ -620,19 +620,19 @@
apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
done
-lemmas convex_plus_less_plus_iff =
- convex_pd_less_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
+lemmas convex_plus_below_plus_iff =
+ convex_pd_below_iff [where xs="xs +\<natural> ys" and ys="zs +\<natural> ws", standard]
-lemmas convex_pd_less_simps =
- convex_unit_less_plus_iff
- convex_plus_less_unit_iff
- convex_plus_less_plus_iff
- convex_unit_less_iff
+lemmas convex_pd_below_simps =
+ convex_unit_below_plus_iff
+ convex_plus_below_unit_iff
+ convex_plus_below_plus_iff
+ convex_unit_below_iff
convex_to_upper_unit
convex_to_upper_plus
convex_to_lower_unit
convex_to_lower_plus
- upper_pd_less_simps
- lower_pd_less_simps
+ upper_pd_below_simps
+ lower_pd_below_simps
end
--- a/src/HOLCF/Cprod.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Cprod.thy Fri May 08 16:19:51 2009 -0700
@@ -68,7 +68,7 @@
lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' \<and> b = b')"
by (simp add: cpair_eq_pair)
-lemma cpair_less [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
+lemma cpair_below [iff]: "(<a, b> \<sqsubseteq> <a', b'>) = (a \<sqsubseteq> a' \<and> b \<sqsubseteq> b')"
by (simp add: cpair_eq_pair)
lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
@@ -107,23 +107,23 @@
lemmas surjective_pairing_Cprod2 = cpair_cfst_csnd
-lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
-by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
+lemma below_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
+by (simp add: below_prod_def cfst_def csnd_def cont_fst cont_snd)
lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
-by (auto simp add: po_eq_conv less_cprod)
+by (auto simp add: po_eq_conv below_cprod)
-lemma cfst_less_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
-by (simp add: less_cprod)
+lemma cfst_below_iff: "cfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <y, csnd\<cdot>x>"
+by (simp add: below_cprod)
-lemma csnd_less_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
-by (simp add: less_cprod)
+lemma csnd_below_iff: "csnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> <cfst\<cdot>x, y>"
+by (simp add: below_cprod)
lemma compact_cfst: "compact x \<Longrightarrow> compact (cfst\<cdot>x)"
-by (rule compactI, simp add: cfst_less_iff)
+by (rule compactI, simp add: cfst_below_iff)
lemma compact_csnd: "compact x \<Longrightarrow> compact (csnd\<cdot>x)"
-by (rule compactI, simp add: csnd_less_iff)
+by (rule compactI, simp add: csnd_below_iff)
lemma compact_cpair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact <x, y>"
by (simp add: cpair_eq_pair)
--- a/src/HOLCF/Deflation.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Deflation.thy Fri May 08 16:19:51 2009 -0700
@@ -15,11 +15,11 @@
locale deflation =
fixes d :: "'a \<rightarrow> 'a"
assumes idem: "\<And>x. d\<cdot>(d\<cdot>x) = d\<cdot>x"
- assumes less: "\<And>x. d\<cdot>x \<sqsubseteq> x"
+ assumes below: "\<And>x. d\<cdot>x \<sqsubseteq> x"
begin
-lemma less_ID: "d \<sqsubseteq> ID"
-by (rule less_cfun_ext, simp add: less)
+lemma below_ID: "d \<sqsubseteq> ID"
+by (rule below_cfun_ext, simp add: below)
text {* The set of fixed points is the same as the range. *}
@@ -34,18 +34,18 @@
the subset ordering of their sets of fixed-points.
*}
-lemma lessI:
+lemma belowI:
assumes f: "\<And>x. d\<cdot>x = x \<Longrightarrow> f\<cdot>x = x" shows "d \<sqsubseteq> f"
-proof (rule less_cfun_ext)
+proof (rule below_cfun_ext)
fix x
- from less have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
+ from below have "f\<cdot>(d\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
also from idem have "f\<cdot>(d\<cdot>x) = d\<cdot>x" by (rule f)
finally show "d\<cdot>x \<sqsubseteq> f\<cdot>x" .
qed
-lemma lessD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
-proof (rule antisym_less)
- from less show "d\<cdot>x \<sqsubseteq> x" .
+lemma belowD: "\<lbrakk>f \<sqsubseteq> d; f\<cdot>x = x\<rbrakk> \<Longrightarrow> d\<cdot>x = x"
+proof (rule below_antisym)
+ from below show "d\<cdot>x \<sqsubseteq> x" .
next
assume "f \<sqsubseteq> d"
hence "f\<cdot>x \<sqsubseteq> d\<cdot>x" by (rule monofun_cfun_fun)
@@ -64,11 +64,11 @@
lemma deflation_UU: "deflation \<bottom>"
by (simp add: deflation.intro)
-lemma deflation_less_iff:
+lemma deflation_below_iff:
"\<lbrakk>deflation p; deflation q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q \<longleftrightarrow> (\<forall>x. p\<cdot>x = x \<longrightarrow> q\<cdot>x = x)"
apply safe
- apply (simp add: deflation.lessD)
- apply (simp add: deflation.lessI)
+ apply (simp add: deflation.belowD)
+ apply (simp add: deflation.belowI)
done
text {*
@@ -76,13 +76,13 @@
the lesser of the two (if they are comparable).
*}
-lemma deflation_less_comp1:
+lemma deflation_below_comp1:
assumes "deflation f"
assumes "deflation g"
shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
-proof (rule antisym_less)
+proof (rule below_antisym)
interpret g: deflation g by fact
- from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
+ from g.below show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
next
interpret f: deflation f by fact
assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
@@ -91,9 +91,9 @@
finally show "f\<cdot>x \<sqsubseteq> f\<cdot>(g\<cdot>x)" .
qed
-lemma deflation_less_comp2:
+lemma deflation_below_comp2:
"\<lbrakk>deflation f; deflation g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> g\<cdot>(f\<cdot>x) = f\<cdot>x"
-by (simp only: deflation.lessD deflation.idem)
+by (simp only: deflation.belowD deflation.idem)
subsection {* Deflations with finite range *}
@@ -143,7 +143,7 @@
hence "d\<cdot>x \<sqsubseteq> d\<cdot>(Y j)"
using j by simp
hence "d\<cdot>x \<sqsubseteq> Y j"
- using less by (rule trans_less)
+ using below by (rule below_trans)
thus "\<exists>j. d\<cdot>x \<sqsubseteq> Y j" ..
qed
@@ -155,10 +155,10 @@
locale ep_pair =
fixes e :: "'a \<rightarrow> 'b" and p :: "'b \<rightarrow> 'a"
assumes e_inverse [simp]: "\<And>x. p\<cdot>(e\<cdot>x) = x"
- and e_p_less: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
+ and e_p_below: "\<And>y. e\<cdot>(p\<cdot>y) \<sqsubseteq> y"
begin
-lemma e_less_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
+lemma e_below_iff [simp]: "e\<cdot>x \<sqsubseteq> e\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
proof
assume "e\<cdot>x \<sqsubseteq> e\<cdot>y"
hence "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>(e\<cdot>y)" by (rule monofun_cfun_arg)
@@ -169,7 +169,7 @@
qed
lemma e_eq_iff [simp]: "e\<cdot>x = e\<cdot>y \<longleftrightarrow> x = y"
-unfolding po_eq_conv e_less_iff ..
+unfolding po_eq_conv e_below_iff ..
lemma p_eq_iff:
"\<lbrakk>e\<cdot>(p\<cdot>x) = x; e\<cdot>(p\<cdot>y) = y\<rbrakk> \<Longrightarrow> p\<cdot>x = p\<cdot>y \<longleftrightarrow> x = y"
@@ -178,7 +178,7 @@
lemma p_inverse: "(\<exists>x. y = e\<cdot>x) = (e\<cdot>(p\<cdot>y) = y)"
by (auto, rule exI, erule sym)
-lemma e_less_iff_less_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
+lemma e_below_iff_below_p: "e\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> p\<cdot>y"
proof
assume "e\<cdot>x \<sqsubseteq> y"
then have "p\<cdot>(e\<cdot>x) \<sqsubseteq> p\<cdot>y" by (rule monofun_cfun_arg)
@@ -186,7 +186,7 @@
next
assume "x \<sqsubseteq> p\<cdot>y"
then have "e\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>y)" by (rule monofun_cfun_arg)
- then show "e\<cdot>x \<sqsubseteq> y" using e_p_less by (rule trans_less)
+ then show "e\<cdot>x \<sqsubseteq> y" using e_p_below by (rule below_trans)
qed
lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
@@ -203,7 +203,7 @@
assume "compact x"
hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_CFun2])
- hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_less_iff_less_p)
+ hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
thus "compact (e\<cdot>x)" by (rule compactI)
qed
@@ -213,7 +213,7 @@
text {* Deflations from ep-pairs *}
lemma deflation_e_p: "deflation (e oo p)"
-by (simp add: deflation.intro e_p_less)
+by (simp add: deflation.intro e_p_below)
lemma deflation_e_d_p:
assumes "deflation d"
@@ -224,7 +224,7 @@
show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
by (simp add: idem)
show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
- by (simp add: e_less_iff_less_p less)
+ by (simp add: e_below_iff_below_p below)
qed
lemma finite_deflation_e_d_p:
@@ -236,7 +236,7 @@
show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
by (simp add: idem)
show "(e oo d oo p)\<cdot>x \<sqsubseteq> x"
- by (simp add: e_less_iff_less_p less)
+ by (simp add: e_below_iff_below_p below)
have "finite ((\<lambda>x. e\<cdot>x) ` (\<lambda>x. d\<cdot>x) ` range (\<lambda>x. p\<cdot>x))"
by (simp add: finite_image)
hence "finite (range (\<lambda>x. (e oo d oo p)\<cdot>x))"
@@ -254,24 +254,24 @@
{
fix x
have "d\<cdot>(e\<cdot>x) \<sqsubseteq> e\<cdot>x"
- by (rule d.less)
+ by (rule d.below)
hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(e\<cdot>x)"
by (rule monofun_cfun_arg)
hence "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
by simp
}
- note p_d_e_less = this
+ note p_d_e_below = this
show ?thesis
proof
fix x
show "(p oo d oo e)\<cdot>x \<sqsubseteq> x"
- by (rule p_d_e_less)
+ by (rule p_d_e_below)
next
fix x
show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) = (p oo d oo e)\<cdot>x"
- proof (rule antisym_less)
+ proof (rule below_antisym)
show "(p oo d oo e)\<cdot>((p oo d oo e)\<cdot>x) \<sqsubseteq> (p oo d oo e)\<cdot>x"
- by (rule p_d_e_less)
+ by (rule p_d_e_below)
have "p\<cdot>(d\<cdot>(d\<cdot>(d\<cdot>(e\<cdot>x)))) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
by (intro monofun_cfun_arg d)
hence "p\<cdot>(d\<cdot>(e\<cdot>x)) \<sqsubseteq> p\<cdot>(d\<cdot>(e\<cdot>(p\<cdot>(d\<cdot>(e\<cdot>x)))))"
@@ -315,29 +315,29 @@
lemma ep_pair_unique_e_lemma:
assumes "ep_pair e1 p" and "ep_pair e2 p"
shows "e1 \<sqsubseteq> e2"
-proof (rule less_cfun_ext)
+proof (rule below_cfun_ext)
interpret e1: ep_pair e1 p by fact
interpret e2: ep_pair e2 p by fact
fix x
have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
- by (rule e1.e_p_less)
+ by (rule e1.e_p_below)
thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
by (simp only: e2.e_inverse)
qed
lemma ep_pair_unique_e:
"\<lbrakk>ep_pair e1 p; ep_pair e2 p\<rbrakk> \<Longrightarrow> e1 = e2"
-by (fast intro: antisym_less elim: ep_pair_unique_e_lemma)
+by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
lemma ep_pair_unique_p_lemma:
assumes "ep_pair e p1" and "ep_pair e p2"
shows "p1 \<sqsubseteq> p2"
-proof (rule less_cfun_ext)
+proof (rule below_cfun_ext)
interpret p1: ep_pair e p1 by fact
interpret p2: ep_pair e p2 by fact
fix x
have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
- by (rule p1.e_p_less)
+ by (rule p1.e_p_below)
hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
by (rule monofun_cfun_arg)
thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
@@ -346,7 +346,7 @@
lemma ep_pair_unique_p:
"\<lbrakk>ep_pair e p1; ep_pair e p2\<rbrakk> \<Longrightarrow> p1 = p2"
-by (fast intro: antisym_less elim: ep_pair_unique_p_lemma)
+by (fast intro: below_antisym elim: ep_pair_unique_p_lemma)
subsection {* Composing ep-pairs *}
@@ -363,11 +363,11 @@
show "(p1 oo p2)\<cdot>((e2 oo e1)\<cdot>x) = x"
by simp
have "e1\<cdot>(p1\<cdot>(p2\<cdot>y)) \<sqsubseteq> p2\<cdot>y"
- by (rule ep1.e_p_less)
+ by (rule ep1.e_p_below)
hence "e2\<cdot>(e1\<cdot>(p1\<cdot>(p2\<cdot>y))) \<sqsubseteq> e2\<cdot>(p2\<cdot>y)"
by (rule monofun_cfun_arg)
also have "e2\<cdot>(p2\<cdot>y) \<sqsubseteq> y"
- by (rule ep2.e_p_less)
+ by (rule ep2.e_p_below)
finally show "(e2 oo e1)\<cdot>((p1 oo p2)\<cdot>y) \<sqsubseteq> y"
by simp
qed
@@ -381,7 +381,7 @@
proof -
have "\<bottom> \<sqsubseteq> p\<cdot>\<bottom>" by (rule minimal)
hence "e\<cdot>\<bottom> \<sqsubseteq> e\<cdot>(p\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
- also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_less)
+ also have "e\<cdot>(p\<cdot>\<bottom>) \<sqsubseteq> \<bottom>" by (rule e_p_below)
finally show "e\<cdot>\<bottom> = \<bottom>" by simp
qed
--- a/src/HOLCF/Discrete.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Discrete.thy Fri May 08 16:19:51 2009 -0700
@@ -12,21 +12,21 @@
subsection {* Type @{typ "'a discr"} is a discrete cpo *}
-instantiation discr :: (type) sq_ord
+instantiation discr :: (type) below
begin
definition
- less_discr_def:
+ below_discr_def:
"(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
instance ..
end
instance discr :: (type) discrete_cpo
-by intro_classes (simp add: less_discr_def)
+by intro_classes (simp add: below_discr_def)
-lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
-by simp
+lemma discr_below_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
+by simp (* FIXME: same discrete_cpo - remove? is [iff] important? *)
subsection {* Type @{typ "'a discr"} is a cpo *}
--- a/src/HOLCF/Domain.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Domain.thy Fri May 08 16:19:51 2009 -0700
@@ -33,7 +33,7 @@
lemma swap: "iso rep abs"
by (rule iso.intro [OF rep_iso abs_iso])
-lemma abs_less: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
+lemma abs_below: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
proof
assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
@@ -43,11 +43,11 @@
then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
qed
-lemma rep_less: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
- by (rule iso.abs_less [OF swap])
+lemma rep_below: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
+ by (rule iso.abs_below [OF swap])
lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
- by (simp add: po_eq_conv abs_less)
+ by (simp add: po_eq_conv abs_below)
lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
by (rule iso.abs_eq [OF swap])
@@ -91,7 +91,7 @@
assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
with cont_Rep_CFun2
have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
- then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_less by simp
+ then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
qed
lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
--- a/src/HOLCF/Ffun.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Ffun.thy Fri May 08 16:19:51 2009 -0700
@@ -10,11 +10,11 @@
subsection {* Full function space is a partial order *}
-instantiation "fun" :: (type, sq_ord) sq_ord
+instantiation "fun" :: (type, below) below
begin
definition
- less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
+ below_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"
instance ..
end
@@ -23,45 +23,45 @@
proof
fix f :: "'a \<Rightarrow> 'b"
show "f \<sqsubseteq> f"
- by (simp add: less_fun_def)
+ by (simp add: below_fun_def)
next
fix f g :: "'a \<Rightarrow> 'b"
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> f" thus "f = g"
- by (simp add: less_fun_def expand_fun_eq antisym_less)
+ by (simp add: below_fun_def expand_fun_eq below_antisym)
next
fix f g h :: "'a \<Rightarrow> 'b"
assume "f \<sqsubseteq> g" and "g \<sqsubseteq> h" thus "f \<sqsubseteq> h"
- unfolding less_fun_def by (fast elim: trans_less)
+ unfolding below_fun_def by (fast elim: below_trans)
qed
text {* make the symbol @{text "<<"} accessible for type fun *}
-lemma expand_fun_less: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
-by (simp add: less_fun_def)
+lemma expand_fun_below: "(f \<sqsubseteq> g) = (\<forall>x. f x \<sqsubseteq> g x)"
+by (simp add: below_fun_def)
-lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: less_fun_def)
+lemma below_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
+by (simp add: below_fun_def)
subsection {* Full function space is chain complete *}
text {* function application is monotone *}
lemma monofun_app: "monofun (\<lambda>f. f x)"
-by (rule monofunI, simp add: less_fun_def)
+by (rule monofunI, simp add: below_fun_def)
text {* chains of functions yield chains in the po range *}
lemma ch2ch_fun: "chain S \<Longrightarrow> chain (\<lambda>i. S i x)"
-by (simp add: chain_def less_fun_def)
+by (simp add: chain_def below_fun_def)
lemma ch2ch_lambda: "(\<And>x. chain (\<lambda>i. S i x)) \<Longrightarrow> chain S"
-by (simp add: chain_def less_fun_def)
+by (simp add: chain_def below_fun_def)
text {* upper bounds of function chains yield upper bound in the po range *}
lemma ub2ub_fun:
"range S <| u \<Longrightarrow> range (\<lambda>i. S i x) <| u x"
-by (auto simp add: is_ub_def less_fun_def)
+by (auto simp add: is_ub_def below_fun_def)
text {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
@@ -70,9 +70,9 @@
shows "range Y <<| f"
apply (rule is_lubI)
apply (rule ub_rangeI)
-apply (rule less_fun_ext)
+apply (rule below_fun_ext)
apply (rule is_ub_lub [OF f])
-apply (rule less_fun_ext)
+apply (rule below_fun_ext)
apply (rule is_lub_lub [OF f])
apply (erule ub2ub_fun)
done
@@ -103,7 +103,7 @@
proof
fix f g :: "'a \<Rightarrow> 'b"
show "f \<sqsubseteq> g \<longleftrightarrow> f = g"
- unfolding expand_fun_less expand_fun_eq
+ unfolding expand_fun_below expand_fun_eq
by simp
qed
@@ -148,7 +148,7 @@
subsection {* Full function space is pointed *}
lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
-by (simp add: less_fun_def)
+by (simp add: below_fun_def)
lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y"
apply (rule_tac x = "\<lambda>x. \<bottom>" in exI)
@@ -171,13 +171,13 @@
*}
lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
-by (simp add: less_fun_def)
+by (simp add: below_fun_def)
lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
by (rule monofunE)
lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y"
-by (rule trans_less [OF monofun_fun_arg monofun_fun_fun])
+by (rule below_trans [OF monofun_fun_arg monofun_fun_fun])
subsection {* Propagation of monotonicity and continuity *}
@@ -236,7 +236,7 @@
lemma mono2mono_lambda:
assumes f: "\<And>y. monofun (\<lambda>x. f x y)" shows "monofun f"
apply (rule monofunI)
-apply (rule less_fun_ext)
+apply (rule below_fun_ext)
apply (erule monofunE [OF f])
done
@@ -296,4 +296,3 @@
by (rule cont2cont_app2 [OF cont_const])
end
-
--- a/src/HOLCF/Fix.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Fix.thy Fri May 08 16:19:51 2009 -0700
@@ -90,7 +90,7 @@
apply simp
done
-lemma fix_least_less: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
+lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
apply (simp add: fix_def2)
apply (rule is_lub_thelub)
apply (rule chain_iterate)
@@ -98,17 +98,17 @@
apply (induct_tac i)
apply simp
apply simp
-apply (erule rev_trans_less)
+apply (erule rev_below_trans)
apply (erule monofun_cfun_arg)
done
lemma fix_least: "F\<cdot>x = x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
-by (rule fix_least_less, simp)
+by (rule fix_least_below, simp)
lemma fix_eqI:
assumes fixed: "F\<cdot>x = x" and least: "\<And>z. F\<cdot>z = z \<Longrightarrow> x \<sqsubseteq> z"
shows "fix\<cdot>F = x"
-apply (rule antisym_less)
+apply (rule below_antisym)
apply (rule fix_least [OF fixed])
apply (rule least [OF fix_eq [symmetric]])
done
@@ -230,10 +230,10 @@
have "?y1 \<sqsubseteq> y" by (rule fix_least, simp add: F_y)
hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> cfst\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
hence "cfst\<cdot>(F\<cdot>\<langle>x, ?y1\<rangle>) \<sqsubseteq> x" using F_x by simp
- hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_less)
+ hence 1: "?x \<sqsubseteq> x" by (simp add: fix_least_below)
hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> csnd\<cdot>(F\<cdot>\<langle>x, y\<rangle>)" by (simp add: monofun_cfun)
hence "csnd\<cdot>(F\<cdot>\<langle>?x, y\<rangle>) \<sqsubseteq> y" using F_y by simp
- hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_less)
+ hence 2: "?y \<sqsubseteq> y" by (simp add: fix_least_below)
show "\<langle>?x, ?y\<rangle> \<sqsubseteq> z" using z 1 2 by simp
qed
--- a/src/HOLCF/HOLCF.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/HOLCF.thy Fri May 08 16:19:51 2009 -0700
@@ -21,4 +21,58 @@
(cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
*}
+text {* Legacy theorem names *}
+
+lemmas sq_ord_less_eq_trans = below_eq_trans
+lemmas sq_ord_eq_less_trans = eq_below_trans
+lemmas refl_less = below_refl
+lemmas trans_less = below_trans
+lemmas antisym_less = below_antisym
+lemmas antisym_less_inverse = below_antisym_inverse
+lemmas box_less = box_below
+lemmas rev_trans_less = rev_below_trans
+lemmas not_less2not_eq = not_below2not_eq
+lemmas less_UU_iff = below_UU_iff
+lemmas flat_less_iff = flat_below_iff
+lemmas adm_less = adm_below
+lemmas adm_not_less = adm_not_below
+lemmas adm_compact_not_less = adm_compact_not_below
+lemmas less_fun_def = below_fun_def
+lemmas expand_fun_less = expand_fun_below
+lemmas less_fun_ext = below_fun_ext
+lemmas less_discr_def = below_discr_def
+lemmas discr_less_eq = discr_below_eq
+lemmas less_unit_def = below_unit_def
+lemmas less_cprod_def = below_prod_def
+lemmas prod_lessI = prod_belowI
+lemmas Pair_less_iff = Pair_below_iff
+lemmas fst_less_iff = fst_below_iff
+lemmas snd_less_iff = snd_below_iff
+lemmas expand_cfun_less = expand_cfun_below
+lemmas less_cfun_ext = below_cfun_ext
+lemmas injection_less = injection_below
+lemmas approx_less = approx_below
+lemmas profinite_less_ext = profinite_below_ext
+lemmas less_up_def = below_up_def
+lemmas not_Iup_less = not_Iup_below
+lemmas Iup_less = Iup_below
+lemmas up_less = up_below
+lemmas cpair_less = cpair_below
+lemmas less_cprod = below_cprod
+lemmas cfst_less_iff = cfst_below_iff
+lemmas csnd_less_iff = csnd_below_iff
+lemmas Def_inject_less_eq = Def_below_Def
+lemmas Def_less_is_eq = Def_below_iff
+lemmas spair_less_iff = spair_below_iff
+lemmas less_sprod = below_sprod
+lemmas spair_less = spair_below
+lemmas sfst_less_iff = sfst_below_iff
+lemmas ssnd_less_iff = ssnd_below_iff
+lemmas fix_least_less = fix_least_below
+lemmas dist_less_one = dist_below_one
+lemmas less_ONE = below_ONE
+lemmas ONE_less_iff = ONE_below_iff
+lemmas less_sinlD = below_sinlD
+lemmas less_sinrD = below_sinrD
+
end
--- a/src/HOLCF/Lift.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Lift.thy Fri May 08 16:19:51 2009 -0700
@@ -70,11 +70,11 @@
lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
by simp
-lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
-by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def)
+lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
+by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def)
-lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
-by (induct y, simp, simp add: Def_inject_less_eq)
+lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
+by (induct y, simp, simp add: Def_below_Def)
subsection {* Lift is flat *}
@@ -134,7 +134,7 @@
"(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
apply (rule monofunE [where f=flift1])
apply (rule cont2mono [OF cont_flift1])
-apply (simp add: less_fun_ext)
+apply (simp add: below_fun_ext)
done
lemma cont2cont_flift1 [simp]:
@@ -216,7 +216,7 @@
apply (rule is_lubI)
apply (rule ub_rangeI, simp)
apply (drule ub_rangeD)
- apply (erule rev_trans_less)
+ apply (erule rev_below_trans)
apply simp
apply (rule lessI)
done
--- a/src/HOLCF/LowerPD.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/LowerPD.thy Fri May 08 16:19:51 2009 -0700
@@ -23,7 +23,7 @@
apply (drule (1) bspec, erule bexE)
apply (drule (1) bspec, erule bexE)
apply (erule rev_bexI)
-apply (erule (1) trans_less)
+apply (erule (1) below_trans)
done
interpretation lower_le: preorder lower_le
@@ -39,7 +39,7 @@
lemma PDPlus_lower_mono: "\<lbrakk>s \<le>\<flat> t; u \<le>\<flat> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<flat> PDPlus t v"
unfolding lower_le_def Rep_PDPlus by fast
-lemma PDPlus_lower_less: "t \<le>\<flat> PDPlus t u"
+lemma PDPlus_lower_le: "t \<le>\<flat> PDPlus t u"
unfolding lower_le_def Rep_PDPlus by fast
lemma lower_le_PDUnit_PDUnit_iff [simp]:
@@ -99,7 +99,7 @@
"{S::'a pd_basis set. lower_le.ideal S}"
by (fast intro: lower_le.ideal_principal)
-instantiation lower_pd :: (profinite) sq_ord
+instantiation lower_pd :: (profinite) below
begin
definition
@@ -110,16 +110,16 @@
instance lower_pd :: (profinite) po
by (rule lower_le.typedef_ideal_po
- [OF type_definition_lower_pd sq_le_lower_pd_def])
+ [OF type_definition_lower_pd below_lower_pd_def])
instance lower_pd :: (profinite) cpo
by (rule lower_le.typedef_ideal_cpo
- [OF type_definition_lower_pd sq_le_lower_pd_def])
+ [OF type_definition_lower_pd below_lower_pd_def])
lemma Rep_lower_pd_lub:
"chain Y \<Longrightarrow> Rep_lower_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_lower_pd (Y i))"
by (rule lower_le.typedef_ideal_rep_contlub
- [OF type_definition_lower_pd sq_le_lower_pd_def])
+ [OF type_definition_lower_pd below_lower_pd_def])
lemma ideal_Rep_lower_pd: "lower_le.ideal (Rep_lower_pd xs)"
by (rule Rep_lower_pd [unfolded mem_Collect_eq])
@@ -145,7 +145,7 @@
apply (rule ideal_Rep_lower_pd)
apply (erule Rep_lower_pd_lub)
apply (rule Rep_lower_principal)
-apply (simp only: sq_le_lower_pd_def)
+apply (simp only: below_lower_pd_def)
done
text {* Lower powerdomain is pointed *}
@@ -264,28 +264,28 @@
lemmas lower_plus_aci =
lower_plus_ac lower_plus_absorb lower_plus_left_absorb
-lemma lower_plus_less1: "xs \<sqsubseteq> xs +\<flat> ys"
+lemma lower_plus_below1: "xs \<sqsubseteq> xs +\<flat> ys"
apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_lower_less)
+apply (simp add: PDPlus_lower_le)
done
-lemma lower_plus_less2: "ys \<sqsubseteq> xs +\<flat> ys"
-by (subst lower_plus_commute, rule lower_plus_less1)
+lemma lower_plus_below2: "ys \<sqsubseteq> xs +\<flat> ys"
+by (subst lower_plus_commute, rule lower_plus_below1)
lemma lower_plus_least: "\<lbrakk>xs \<sqsubseteq> zs; ys \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs +\<flat> ys \<sqsubseteq> zs"
apply (subst lower_plus_absorb [of zs, symmetric])
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
-lemma lower_plus_less_iff:
+lemma lower_plus_below_iff:
"xs +\<flat> ys \<sqsubseteq> zs \<longleftrightarrow> xs \<sqsubseteq> zs \<and> ys \<sqsubseteq> zs"
apply safe
-apply (erule trans_less [OF lower_plus_less1])
-apply (erule trans_less [OF lower_plus_less2])
+apply (erule below_trans [OF lower_plus_below1])
+apply (erule below_trans [OF lower_plus_below2])
apply (erule (1) lower_plus_least)
done
-lemma lower_unit_less_plus_iff:
+lemma lower_unit_below_plus_iff:
"{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
apply (rule iffI)
apply (subgoal_tac
@@ -299,13 +299,13 @@
apply simp
apply simp
apply (erule disjE)
- apply (erule trans_less [OF _ lower_plus_less1])
- apply (erule trans_less [OF _ lower_plus_less2])
+ apply (erule below_trans [OF _ lower_plus_below1])
+ apply (erule below_trans [OF _ lower_plus_below2])
done
-lemma lower_unit_less_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
+lemma lower_unit_below_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
apply (rule iffI)
- apply (rule profinite_less_ext)
+ apply (rule profinite_below_ext)
apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -313,10 +313,10 @@
apply (erule monofun_cfun_arg)
done
-lemmas lower_pd_less_simps =
- lower_unit_less_iff
- lower_plus_less_iff
- lower_unit_less_plus_iff
+lemmas lower_pd_below_simps =
+ lower_unit_below_iff
+ lower_plus_below_iff
+ lower_unit_below_plus_iff
lemma lower_unit_eq_iff [simp]: "{x}\<flat> = {y}\<flat> \<longleftrightarrow> x = y"
by (simp add: po_eq_conv)
@@ -330,18 +330,18 @@
lemma lower_plus_strict_iff [simp]:
"xs +\<flat> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<and> ys = \<bottom>"
apply safe
-apply (rule UU_I, erule subst, rule lower_plus_less1)
-apply (rule UU_I, erule subst, rule lower_plus_less2)
+apply (rule UU_I, erule subst, rule lower_plus_below1)
+apply (rule UU_I, erule subst, rule lower_plus_below2)
apply (rule lower_plus_absorb)
done
lemma lower_plus_strict1 [simp]: "\<bottom> +\<flat> ys = ys"
-apply (rule antisym_less [OF _ lower_plus_less2])
+apply (rule below_antisym [OF _ lower_plus_below2])
apply (simp add: lower_plus_least)
done
lemma lower_plus_strict2 [simp]: "xs +\<flat> \<bottom> = xs"
-apply (rule antisym_less [OF _ lower_plus_less1])
+apply (rule below_antisym [OF _ lower_plus_below1])
apply (simp add: lower_plus_least)
done
@@ -412,11 +412,11 @@
lemma lower_bind_basis_mono:
"t \<le>\<flat> u \<Longrightarrow> lower_bind_basis t \<sqsubseteq> lower_bind_basis u"
-unfolding expand_cfun_less
+unfolding expand_cfun_below
apply (erule lower_le_induct, safe)
apply (simp add: monofun_cfun)
-apply (simp add: rev_trans_less [OF lower_plus_less1])
-apply (simp add: lower_plus_less_iff)
+apply (simp add: rev_below_trans [OF lower_plus_below1])
+apply (simp add: lower_plus_below_iff)
done
definition
--- a/src/HOLCF/One.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/One.thy Fri May 08 16:19:51 2009 -0700
@@ -28,13 +28,13 @@
lemma one_induct: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
by (cases x rule: oneE) simp_all
-lemma dist_less_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
+lemma dist_below_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
unfolding ONE_def by simp
-lemma less_ONE [simp]: "x \<sqsubseteq> ONE"
+lemma below_ONE [simp]: "x \<sqsubseteq> ONE"
by (induct x rule: one_induct) simp_all
-lemma ONE_less_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
+lemma ONE_below_iff [simp]: "ONE \<sqsubseteq> x \<longleftrightarrow> x = ONE"
by (induct x rule: one_induct) simp_all
lemma ONE_defined [simp]: "ONE \<noteq> \<bottom>"
--- a/src/HOLCF/Pcpo.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Pcpo.thy Fri May 08 16:19:51 2009 -0700
@@ -46,7 +46,7 @@
lemma lub_range_shift:
"chain Y \<Longrightarrow> (\<Squnion>i. Y (i + j)) = (\<Squnion>i. Y i)"
-apply (rule antisym_less)
+apply (rule below_antisym)
apply (rule lub_range_mono)
apply fast
apply assumption
@@ -54,7 +54,7 @@
apply (rule is_lub_thelub)
apply assumption
apply (rule ub_rangeI)
-apply (rule_tac y="Y (i + j)" in trans_less)
+apply (rule_tac y="Y (i + j)" in below_trans)
apply (erule chain_mono)
apply (rule le_add1)
apply (rule is_ub_thelub)
@@ -66,7 +66,7 @@
apply (rule iffI)
apply (fast intro!: thelubI lub_finch1)
apply (unfold max_in_chain_def)
-apply (safe intro!: antisym_less)
+apply (safe intro!: below_antisym)
apply (fast elim!: chain_mono)
apply (drule sym)
apply (force elim!: is_ub_thelub)
@@ -79,7 +79,7 @@
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
apply (erule is_lub_thelub)
apply (rule ub_rangeI)
-apply (rule trans_less)
+apply (rule below_trans)
apply (erule meta_spec)
apply (erule is_ub_thelub)
done
@@ -106,7 +106,7 @@
lemma lub_equal2:
"\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
- by (blast intro: antisym_less lub_mono2 sym)
+ by (blast intro: below_antisym lub_mono2 sym)
lemma lub_mono3:
"\<lbrakk>chain Y; chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
@@ -115,7 +115,7 @@
apply (rule ub_rangeI)
apply (erule allE)
apply (erule exE)
-apply (erule trans_less)
+apply (erule below_trans)
apply (erule is_ub_thelub)
done
@@ -132,10 +132,10 @@
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
shows "(\<Squnion>i. \<Squnion>j. Y i j) = (\<Squnion>i. Y i i)"
-proof (rule antisym_less)
+proof (rule below_antisym)
have 3: "chain (\<lambda>i. Y i i)"
apply (rule chainI)
- apply (rule trans_less)
+ apply (rule below_trans)
apply (rule chainE [OF 1])
apply (rule chainE [OF 2])
done
@@ -146,7 +146,7 @@
apply (rule ub_rangeI)
apply (rule lub_mono3 [rule_format, OF 2 3])
apply (rule exI)
- apply (rule trans_less)
+ apply (rule below_trans)
apply (rule chain_mono [OF 1 le_maxI1])
apply (rule chain_mono [OF 2 le_maxI2])
done
@@ -185,7 +185,7 @@
apply (rule theI')
apply (rule ex_ex1I)
apply (rule least)
-apply (blast intro: antisym_less)
+apply (blast intro: below_antisym)
done
lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
@@ -207,7 +207,7 @@
text {* useful lemmas about @{term \<bottom>} *}
-lemma less_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
+lemma below_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
by (simp add: po_eq_conv)
lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
@@ -287,7 +287,7 @@
apply (blast dest: chain_mono ax_flat)
done
-lemma flat_less_iff:
+lemma flat_below_iff:
shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
by (safe dest!: ax_flat)
@@ -298,7 +298,7 @@
text {* Discrete cpos *}
-class discrete_cpo = sq_ord +
+class discrete_cpo = below +
assumes discrete_cpo [simp]: "x \<sqsubseteq> y \<longleftrightarrow> x = y"
begin
--- a/src/HOLCF/Pcpodef.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Pcpodef.thy Fri May 08 16:19:51 2009 -0700
@@ -16,22 +16,22 @@
if the ordering is defined in the standard way.
*}
-setup {* Sign.add_const_constraint (@{const_name Porder.sq_le}, NONE) *}
+setup {* Sign.add_const_constraint (@{const_name Porder.below}, NONE) *}
theorem typedef_po:
fixes Abs :: "'a::po \<Rightarrow> 'b::type"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "OFCLASS('b, po_class)"
- apply (intro_classes, unfold less)
- apply (rule refl_less)
- apply (erule (1) trans_less)
+ apply (intro_classes, unfold below)
+ apply (rule below_refl)
+ apply (erule (1) below_trans)
apply (rule type_definition.Rep_inject [OF type, THEN iffD1])
- apply (erule (1) antisym_less)
+ apply (erule (1) below_antisym)
done
-setup {* Sign.add_const_constraint (@{const_name Porder.sq_le},
- SOME @{typ "'a::sq_ord \<Rightarrow> 'a::sq_ord \<Rightarrow> bool"}) *}
+setup {* Sign.add_const_constraint (@{const_name Porder.below},
+ SOME @{typ "'a::below \<Rightarrow> 'a::below \<Rightarrow> bool"}) *}
subsection {* Proving a subtype is finite *}
@@ -58,9 +58,9 @@
subsection {* Proving a subtype is chain-finite *}
lemma monofun_Rep:
- assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "monofun Rep"
-by (rule monofunI, unfold less)
+by (rule monofunI, unfold below)
lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep]
lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep]
@@ -68,10 +68,10 @@
theorem typedef_chfin:
fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "OFCLASS('b, chfin_class)"
apply intro_classes
- apply (drule ch2ch_Rep [OF less])
+ apply (drule ch2ch_Rep [OF below])
apply (drule chfin)
apply (unfold max_in_chain_def)
apply (simp add: type_definition.Rep_inject [OF type])
@@ -90,28 +90,28 @@
lemma Abs_inverse_lub_Rep:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
apply (rule type_definition.Abs_inverse [OF type])
- apply (erule admD [OF adm ch2ch_Rep [OF less]])
+ apply (erule admD [OF adm ch2ch_Rep [OF below]])
apply (rule type_definition.Rep [OF type])
done
theorem typedef_lub:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
- apply (frule ch2ch_Rep [OF less])
+ apply (frule ch2ch_Rep [OF below])
apply (rule is_lubI)
apply (rule ub_rangeI)
- apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
+ apply (simp only: below Abs_inverse_lub_Rep [OF type below adm])
apply (erule is_ub_thelub)
- apply (simp only: less Abs_inverse_lub_Rep [OF type less adm])
+ apply (simp only: below Abs_inverse_lub_Rep [OF type below adm])
apply (erule is_lub_thelub)
- apply (erule ub2ub_Rep [OF less])
+ apply (erule ub2ub_Rep [OF below])
done
lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
@@ -119,13 +119,13 @@
theorem typedef_cpo:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "OFCLASS('b, cpo_class)"
proof
fix S::"nat \<Rightarrow> 'b" assume "chain S"
hence "range S <<| Abs (\<Squnion>i. Rep (S i))"
- by (rule typedef_lub [OF type less adm])
+ by (rule typedef_lub [OF type below adm])
thus "\<exists>x. range S <<| x" ..
qed
@@ -136,14 +136,14 @@
theorem typedef_cont_Rep:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "cont Rep"
apply (rule contI)
- apply (simp only: typedef_thelub [OF type less adm])
- apply (simp only: Abs_inverse_lub_Rep [OF type less adm])
+ apply (simp only: typedef_thelub [OF type below adm])
+ apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
apply (rule cpo_lubI)
- apply (erule ch2ch_Rep [OF less])
+ apply (erule ch2ch_Rep [OF below])
done
text {*
@@ -153,28 +153,28 @@
*}
theorem typedef_is_lubI:
- assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
apply (rule is_lubI)
apply (rule ub_rangeI)
- apply (subst less)
+ apply (subst below)
apply (erule is_ub_lub)
- apply (subst less)
+ apply (subst below)
apply (erule is_lub_lub)
- apply (erule ub2ub_Rep [OF less])
+ apply (erule ub2ub_Rep [OF below])
done
theorem typedef_cont_Abs:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
and f_in_A: "\<And>x. f x \<in> A"
and cont_f: "cont f"
shows "cont (\<lambda>x. Abs (f x))"
apply (rule contI)
- apply (rule typedef_is_lubI [OF less])
+ apply (rule typedef_is_lubI [OF below])
apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
apply (erule cont_f [THEN contE])
done
@@ -184,15 +184,15 @@
theorem typedef_compact:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and adm: "adm (\<lambda>x. x \<in> A)"
shows "compact (Rep k) \<Longrightarrow> compact k"
proof (unfold compact_def)
have cont_Rep: "cont Rep"
- by (rule typedef_cont_Rep [OF type less adm])
+ by (rule typedef_cont_Rep [OF type below adm])
assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
- thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold less)
+ thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
qed
subsection {* Proving a subtype is pointed *}
@@ -205,13 +205,13 @@
theorem typedef_pcpo_generic:
fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and z_in_A: "z \<in> A"
and z_least: "\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x"
shows "OFCLASS('b, pcpo_class)"
apply (intro_classes)
apply (rule_tac x="Abs z" in exI, rule allI)
- apply (unfold less)
+ apply (unfold below)
apply (subst type_definition.Abs_inverse [OF type z_in_A])
apply (rule z_least [OF type_definition.Rep [OF type]])
done
@@ -224,10 +224,10 @@
theorem typedef_pcpo:
fixes Abs :: "'a::pcpo \<Rightarrow> 'b::cpo"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "OFCLASS('b, pcpo_class)"
-by (rule typedef_pcpo_generic [OF type less UU_in_A], rule minimal)
+by (rule typedef_pcpo_generic [OF type below UU_in_A], rule minimal)
subsubsection {* Strictness of @{term Rep} and @{term Abs} *}
@@ -238,66 +238,66 @@
theorem typedef_Abs_strict:
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "Abs \<bottom> = \<bottom>"
- apply (rule UU_I, unfold less)
+ apply (rule UU_I, unfold below)
apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
done
theorem typedef_Rep_strict:
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "Rep \<bottom> = \<bottom>"
- apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
+ apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
apply (rule type_definition.Abs_inverse [OF type UU_in_A])
done
theorem typedef_Abs_strict_iff:
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "x \<in> A \<Longrightarrow> (Abs x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
+ apply (rule typedef_Abs_strict [OF type below UU_in_A, THEN subst])
apply (simp add: type_definition.Abs_inject [OF type] UU_in_A)
done
theorem typedef_Rep_strict_iff:
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "(Rep x = \<bottom>) = (x = \<bottom>)"
- apply (rule typedef_Rep_strict [OF type less UU_in_A, THEN subst])
+ apply (rule typedef_Rep_strict [OF type below UU_in_A, THEN subst])
apply (simp add: type_definition.Rep_inject [OF type])
done
theorem typedef_Abs_defined:
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
-by (simp add: typedef_Abs_strict_iff [OF type less UU_in_A])
+by (simp add: typedef_Abs_strict_iff [OF type below UU_in_A])
theorem typedef_Rep_defined:
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
-by (simp add: typedef_Rep_strict_iff [OF type less UU_in_A])
+by (simp add: typedef_Rep_strict_iff [OF type below UU_in_A])
subsection {* Proving a subtype is flat *}
theorem typedef_flat:
fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
assumes type: "type_definition Rep Abs A"
- and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+ and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
and UU_in_A: "\<bottom> \<in> A"
shows "OFCLASS('b, flat_class)"
apply (intro_classes)
- apply (unfold less)
+ apply (unfold below)
apply (simp add: type_definition.Rep_inject [OF type, symmetric])
- apply (simp add: typedef_Rep_strict [OF type less UU_in_A])
+ apply (simp add: typedef_Rep_strict [OF type below UU_in_A])
apply (simp add: ax_flat)
done
--- a/src/HOLCF/Porder.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Porder.thy Fri May 08 16:19:51 2009 -0700
@@ -10,59 +10,59 @@
subsection {* Type class for partial orders *}
-class sq_ord =
- fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+class below =
+ fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
begin
notation
- sq_le (infixl "<<" 55)
+ below (infixl "<<" 55)
notation (xsymbols)
- sq_le (infixl "\<sqsubseteq>" 55)
+ below (infixl "\<sqsubseteq>" 55)
-lemma sq_ord_less_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
by (rule subst)
-lemma sq_ord_eq_less_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
+lemma eq_below_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
by (rule ssubst)
end
-class po = sq_ord +
- assumes refl_less [iff]: "x \<sqsubseteq> x"
- assumes trans_less: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
- assumes antisym_less: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
+class po = below +
+ assumes below_refl [iff]: "x \<sqsubseteq> x"
+ assumes below_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+ assumes below_antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
begin
text {* minimal fixes least element *}
lemma minimal2UU[OF allI] : "\<forall>x. uu \<sqsubseteq> x \<Longrightarrow> uu = (THE u. \<forall>y. u \<sqsubseteq> y)"
- by (blast intro: theI2 antisym_less)
+ by (blast intro: theI2 below_antisym)
text {* the reverse law of anti-symmetry of @{term "op <<"} *}
-
-lemma antisym_less_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
+(* Is this rule ever useful? *)
+lemma below_antisym_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
by simp
-lemma box_less: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
- by (rule trans_less [OF trans_less])
+lemma box_below: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
+ by (rule below_trans [OF below_trans])
lemma po_eq_conv: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
- by (fast elim!: antisym_less_inverse intro!: antisym_less)
+ by (fast intro!: below_antisym)
-lemma rev_trans_less: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
- by (rule trans_less)
+lemma rev_below_trans: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
+ by (rule below_trans)
-lemma not_less2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
+lemma not_below2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
by auto
end
lemmas HOLCF_trans_rules [trans] =
- trans_less
- antisym_less
- sq_ord_less_eq_trans
- sq_ord_eq_less_trans
+ below_trans
+ below_antisym
+ below_eq_trans
+ eq_below_trans
context po
begin
@@ -97,7 +97,7 @@
unfolding is_ub_def by fast
lemma is_ub_upward: "\<lbrakk>S <| x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S <| y"
- unfolding is_ub_def by (fast intro: trans_less)
+ unfolding is_ub_def by (fast intro: below_trans)
subsection {* Least upper bounds *}
@@ -143,7 +143,7 @@
lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
apply (unfold is_lub_def is_ub_def)
-apply (blast intro: antisym_less)
+apply (blast intro: below_antisym)
done
text {* technical lemmas about @{term lub} and @{term is_lub} *}
@@ -191,7 +191,7 @@
text {* chains are monotone functions *}
lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
- by (erule less_Suc_induct, erule chainE, erule trans_less)
+ by (erule less_Suc_induct, erule chainE, erule below_trans)
lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
by (cases "i = j", simp, simp add: chain_mono_less)
@@ -208,7 +208,7 @@
"chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x"
apply (rule iffI)
apply (rule ub_rangeI)
-apply (rule_tac y="S (i + j)" in trans_less)
+apply (rule_tac y="S (i + j)" in below_trans)
apply (erule chain_mono)
apply (rule le_add1)
apply (erule ub_rangeD)
@@ -313,7 +313,7 @@
apply (erule exE)
apply (rule finite_chainI, assumption)
apply (rule max_in_chainI)
- apply (rule antisym_less)
+ apply (rule below_antisym)
apply (erule (1) chain_mono)
apply (erule spec)
apply (rule finite_range_has_max)
@@ -451,4 +451,4 @@
end
-end
\ No newline at end of file
+end
--- a/src/HOLCF/Product_Cpo.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Product_Cpo.thy Fri May 08 16:19:51 2009 -0700
@@ -12,11 +12,11 @@
subsection {* Type @{typ unit} is a pcpo *}
-instantiation unit :: sq_ord
+instantiation unit :: below
begin
definition
- less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
+ below_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<longleftrightarrow> True"
instance ..
end
@@ -32,11 +32,11 @@
subsection {* Product type is a partial order *}
-instantiation "*" :: (sq_ord, sq_ord) sq_ord
+instantiation "*" :: (below, below) below
begin
definition
- less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
+ below_prod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
instance ..
end
@@ -45,26 +45,26 @@
proof
fix x :: "'a \<times> 'b"
show "x \<sqsubseteq> x"
- unfolding less_cprod_def by simp
+ unfolding below_prod_def by simp
next
fix x y :: "'a \<times> 'b"
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
- unfolding less_cprod_def Pair_fst_snd_eq
- by (fast intro: antisym_less)
+ unfolding below_prod_def Pair_fst_snd_eq
+ by (fast intro: below_antisym)
next
fix x y z :: "'a \<times> 'b"
assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
- unfolding less_cprod_def
- by (fast intro: trans_less)
+ unfolding below_prod_def
+ by (fast intro: below_trans)
qed
subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
-lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
-unfolding less_cprod_def by simp
+lemma prod_belowI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
+unfolding below_prod_def by simp
-lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
-unfolding less_cprod_def by simp
+lemma Pair_below_iff [simp]: "(a, b) \<sqsubseteq> (c, d) \<longleftrightarrow> a \<sqsubseteq> c \<and> b \<sqsubseteq> d"
+unfolding below_prod_def by simp
text {* Pair @{text "(_,_)"} is monotone in both arguments *}
@@ -81,20 +81,20 @@
text {* @{term fst} and @{term snd} are monotone *}
lemma monofun_fst: "monofun fst"
-by (simp add: monofun_def less_cprod_def)
+by (simp add: monofun_def below_prod_def)
lemma monofun_snd: "monofun snd"
-by (simp add: monofun_def less_cprod_def)
+by (simp add: monofun_def below_prod_def)
subsection {* Product type is a cpo *}
lemma is_lub_Pair:
"\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: less_cprod_def is_ub_lub)
+apply (simp add: below_prod_def is_ub_lub)
apply (frule ub2ub_monofun [OF monofun_fst])
apply (drule ub2ub_monofun [OF monofun_snd])
-apply (simp add: less_cprod_def is_lub_lub)
+apply (simp add: below_prod_def is_lub_lub)
done
lemma lub_cprod:
@@ -134,14 +134,14 @@
proof
fix x y :: "'a \<times> 'b"
show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
- unfolding less_cprod_def Pair_fst_snd_eq
+ unfolding below_prod_def Pair_fst_snd_eq
by simp
qed
subsection {* Product type is pointed *}
lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
-by (simp add: less_cprod_def)
+by (simp add: below_prod_def)
instance "*" :: (pcpo, pcpo) pcpo
by intro_classes (fast intro: minimal_cprod)
@@ -257,20 +257,20 @@
subsection {* Compactness and chain-finiteness *}
-lemma fst_less_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
-unfolding less_cprod_def by simp
+lemma fst_below_iff: "fst (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (y, snd x)"
+unfolding below_prod_def by simp
-lemma snd_less_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y = x \<sqsubseteq> (fst x, y)"
-unfolding less_cprod_def by simp
+lemma snd_below_iff: "snd (x::'a \<times> 'b) \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (fst x, y)"
+unfolding below_prod_def by simp
lemma compact_fst: "compact x \<Longrightarrow> compact (fst x)"
-by (rule compactI, simp add: fst_less_iff)
+by (rule compactI, simp add: fst_below_iff)
lemma compact_snd: "compact x \<Longrightarrow> compact (snd x)"
-by (rule compactI, simp add: snd_less_iff)
+by (rule compactI, simp add: snd_below_iff)
lemma compact_Pair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (x, y)"
-by (rule compactI, simp add: less_cprod_def)
+by (rule compactI, simp add: below_prod_def)
lemma compact_Pair_iff [simp]: "compact (x, y) \<longleftrightarrow> compact x \<and> compact y"
apply (safe intro!: compact_Pair)
--- a/src/HOLCF/Sprod.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Sprod.thy Fri May 08 16:19:51 2009 -0700
@@ -20,7 +20,7 @@
by (rule typedef_finite_po [OF type_definition_Sprod])
instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_Sprod less_Sprod_def])
+by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
syntax (xsymbols)
"**" :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
@@ -67,7 +67,7 @@
by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
lemmas Rep_Sprod_simps =
- Rep_Sprod_inject [symmetric] less_Sprod_def
+ Rep_Sprod_inject [symmetric] below_Sprod_def
Rep_Sprod_strict Rep_Sprod_spair
lemma Exh_Sprod:
@@ -99,7 +99,7 @@
lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
by (simp add: Rep_Sprod_simps strictify_conv_if)
-lemma spair_less_iff:
+lemma spair_below_iff:
"((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
by (simp add: Rep_Sprod_simps strictify_conv_if)
@@ -160,38 +160,38 @@
lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
by (cases p, simp_all)
-lemma less_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
-apply (simp add: less_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
-apply (rule less_cprod)
+lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
+apply (simp add: below_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
+apply (rule below_cprod)
done
lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
-by (auto simp add: po_eq_conv less_sprod)
+by (auto simp add: po_eq_conv below_sprod)
-lemma spair_less:
+lemma spair_below:
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
apply (cases "a = \<bottom>", simp)
apply (cases "b = \<bottom>", simp)
-apply (simp add: less_sprod)
+apply (simp add: below_sprod)
done
-lemma sfst_less_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
+lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
-apply (simp add: less_sprod)
+apply (simp add: below_sprod)
done
-lemma ssnd_less_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
+lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
-apply (simp add: less_sprod)
+apply (simp add: below_sprod)
done
subsection {* Compactness *}
lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)"
-by (rule compactI, simp add: sfst_less_iff)
+by (rule compactI, simp add: sfst_below_iff)
lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)"
-by (rule compactI, simp add: ssnd_less_iff)
+by (rule compactI, simp add: ssnd_below_iff)
lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if)
@@ -224,7 +224,7 @@
assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
apply (induct x, simp)
apply (induct y, simp)
- apply (simp add: spair_less_iff flat_less_iff)
+ apply (simp add: spair_below_iff flat_below_iff)
done
qed
--- a/src/HOLCF/Ssum.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Ssum.thy Fri May 08 16:19:51 2009 -0700
@@ -22,7 +22,7 @@
by (rule typedef_finite_po [OF type_definition_Ssum])
instance "++" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
-by (rule typedef_chfin [OF type_definition_Ssum less_Ssum_def])
+by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
syntax (xsymbols)
"++" :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
@@ -61,17 +61,17 @@
text {* Ordering *}
-lemma sinl_less [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl strictify_conv_if)
+lemma sinl_below [simp]: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
+by (simp add: below_Ssum_def Rep_Ssum_sinl strictify_conv_if)
-lemma sinr_less [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_Ssum_def Rep_Ssum_sinr strictify_conv_if)
+lemma sinr_below [simp]: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
+by (simp add: below_Ssum_def Rep_Ssum_sinr strictify_conv_if)
-lemma sinl_less_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
+lemma sinl_below_sinr [simp]: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
+by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
-lemma sinr_less_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
+lemma sinr_below_sinl [simp]: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
+by (simp add: below_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr strictify_conv_if)
text {* Equality *}
@@ -167,10 +167,10 @@
"\<lbrakk>\<And>x. p = sinl\<cdot>x \<Longrightarrow> Q; \<And>y. p = sinr\<cdot>y \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
by (cases p, simp only: sinl_strict [symmetric], simp, simp)
-lemma less_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
+lemma below_sinlD: "p \<sqsubseteq> sinl\<cdot>x \<Longrightarrow> \<exists>y. p = sinl\<cdot>y \<and> y \<sqsubseteq> x"
by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
-lemma less_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
+lemma below_sinrD: "p \<sqsubseteq> sinr\<cdot>x \<Longrightarrow> \<exists>y. p = sinr\<cdot>y \<and> y \<sqsubseteq> x"
by (cases p, rule_tac x="\<bottom>" in exI, simp_all)
subsection {* Case analysis combinator *}
@@ -207,8 +207,8 @@
instance "++" :: (flat, flat) flat
apply (intro_classes, clarify)
apply (rule_tac p=x in ssumE, simp)
-apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
-apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
+apply (rule_tac p=y in ssumE, simp_all add: flat_below_iff)
+apply (rule_tac p=y in ssumE, simp_all add: flat_below_iff)
done
subsection {* Strict sum is a bifinite domain *}
--- a/src/HOLCF/Sum_Cpo.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Sum_Cpo.thy Fri May 08 16:19:51 2009 -0700
@@ -10,28 +10,28 @@
subsection {* Ordering on type @{typ "'a + 'b"} *}
-instantiation "+" :: (sq_ord, sq_ord) sq_ord
+instantiation "+" :: (below, below) below
begin
-definition
- less_sum_def: "x \<sqsubseteq> y \<equiv> case x of
+definition below_sum_def:
+ "x \<sqsubseteq> y \<equiv> case x of
Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
instance ..
end
-lemma Inl_less_iff [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
-unfolding less_sum_def by simp
+lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
+unfolding below_sum_def by simp
-lemma Inr_less_iff [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
-unfolding less_sum_def by simp
+lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
+unfolding below_sum_def by simp
-lemma Inl_less_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
-unfolding less_sum_def by simp
+lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
+unfolding below_sum_def by simp
-lemma Inr_less_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
-unfolding less_sum_def by simp
+lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
+unfolding below_sum_def by simp
lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
by simp
@@ -39,20 +39,20 @@
lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
by simp
-lemma Inl_lessE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by (cases x, simp_all)
-lemma Inr_lessE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
by (cases x, simp_all)
-lemmas sum_less_elims = Inl_lessE Inr_lessE
+lemmas sum_below_elims = Inl_belowE Inr_belowE
-lemma sum_less_cases:
+lemma sum_below_cases:
"\<lbrakk>x \<sqsubseteq> y;
\<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
\<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
\<Longrightarrow> R"
-by (cases x, safe elim!: sum_less_elims, auto)
+by (cases x, safe elim!: sum_below_elims, auto)
subsection {* Sum type is a complete partial order *}
@@ -64,18 +64,18 @@
next
fix x y :: "'a + 'b"
assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
- by (induct x, auto elim!: sum_less_elims intro: antisym_less)
+ by (induct x, auto elim!: sum_below_elims intro: below_antisym)
next
fix x y z :: "'a + 'b"
assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
- by (induct x, auto elim!: sum_less_elims intro: trans_less)
+ by (induct x, auto elim!: sum_below_elims intro: below_trans)
qed
lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
-by (rule monofunI, erule sum_less_cases, simp_all)
+by (rule monofunI, erule sum_below_cases, simp_all)
lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
-by (rule monofunI, erule sum_less_cases, simp_all)
+by (rule monofunI, erule sum_below_cases, simp_all)
lemma sum_chain_cases:
assumes Y: "chain Y"
@@ -87,12 +87,12 @@
apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
apply (rule ext)
apply (cut_tac j=i in chain_mono [OF Y le0], simp)
- apply (erule Inl_lessE, simp)
+ apply (erule Inl_belowE, simp)
apply (rule B)
apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
apply (rule ext)
apply (cut_tac j=i in chain_mono [OF Y le0], simp)
- apply (erule Inr_lessE, simp)
+ apply (erule Inr_belowE, simp)
done
lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
@@ -100,7 +100,7 @@
apply (rule ub_rangeI)
apply (simp add: is_ub_lub)
apply (frule ub_rangeD [where i=arbitrary])
- apply (erule Inl_lessE, simp)
+ apply (erule Inl_belowE, simp)
apply (erule is_lub_lub)
apply (rule ub_rangeI)
apply (drule ub_rangeD, simp)
@@ -111,7 +111,7 @@
apply (rule ub_rangeI)
apply (simp add: is_ub_lub)
apply (frule ub_rangeD [where i=arbitrary])
- apply (erule Inr_lessE, simp)
+ apply (erule Inr_belowE, simp)
apply (erule is_lub_lub)
apply (rule ub_rangeI)
apply (drule ub_rangeD, simp)
@@ -226,7 +226,7 @@
instance "+" :: (finite_po, finite_po) finite_po ..
instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: less_sum_def split: sum.split)
+by intro_classes (simp add: below_sum_def split: sum.split)
subsection {* Sum type is a bifinite domain *}
--- a/src/HOLCF/Tools/domain/domain_library.ML Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_library.ML Fri May 08 16:19:51 2009 -0700
@@ -257,7 +257,7 @@
infix 0 ==; fun S == T = %%:"==" $ S $ T;
infix 1 ===; fun S === T = %%:"op =" $ S $ T;
infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
-infix 1 <<; fun S << T = %%: @{const_name Porder.sq_le} $ S $ T;
+infix 1 <<; fun S << T = %%: @{const_name Porder.below} $ S $ T;
infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T);
infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Fri May 08 16:19:51 2009 -0700
@@ -29,7 +29,7 @@
val adm_all = @{thm adm_all};
val adm_conj = @{thm adm_conj};
val adm_subst = @{thm adm_subst};
-val antisym_less_inverse = @{thm antisym_less_inverse};
+val antisym_less_inverse = @{thm below_antisym_inverse};
val beta_cfun = @{thm beta_cfun};
val cfun_arg_cong = @{thm cfun_arg_cong};
val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL};
@@ -44,12 +44,12 @@
val contlub_cfun_fun = @{thm contlub_cfun_fun};
val fix_def2 = @{thm fix_def2};
val injection_eq = @{thm injection_eq};
-val injection_less = @{thm injection_less};
+val injection_less = @{thm injection_below};
val lub_equal = @{thm lub_equal};
val monofun_cfun_arg = @{thm monofun_cfun_arg};
val retraction_strict = @{thm retraction_strict};
val spair_eq = @{thm spair_eq};
-val spair_less = @{thm spair_less};
+val spair_less = @{thm spair_below};
val sscase1 = @{thm sscase1};
val ssplit1 = @{thm ssplit1};
val strictify1 = @{thm strictify1};
@@ -121,7 +121,7 @@
val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
-val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: antisym_less_inverse)}
+val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)}
in
--- a/src/HOLCF/Tools/pcpodef_package.ML Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML Fri May 08 16:19:51 2009 -0700
@@ -66,9 +66,9 @@
NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
| SOME morphs => morphs);
val RepC = Const (full Rep_name, newT --> oldT);
- fun lessC T = Const (@{const_name sq_le}, T --> T --> HOLogic.boolT);
- val less_def = Logic.mk_equals (lessC newT,
- Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
+ fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
+ val below_def = Logic.mk_equals (belowC newT,
+ Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
fun make_po tac thy1 =
let
@@ -76,22 +76,22 @@
|> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
val lthy3 = thy2
|> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
- val less_def' = Syntax.check_term lthy3 less_def;
- val ((_, (_, less_definition')), lthy4) = lthy3
+ val below_def' = Syntax.check_term lthy3 below_def;
+ val ((_, (_, below_definition')), lthy4) = lthy3
|> Specification.definition (NONE,
- ((Binding.prefix_name "less_" (Binding.suffix_name "_def" name), []), less_def'));
+ ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
- val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
+ val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
val thy5 = lthy4
|> Class.prove_instantiation_instance
- (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, less_definition]) 1))
+ (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
|> LocalTheory.exit_global;
- in ((type_definition, less_definition, set_def), thy5) end;
+ in ((type_definition, below_definition, set_def), thy5) end;
- fun make_cpo admissible (type_def, less_def, set_def) theory =
+ fun make_cpo admissible (type_def, below_def, set_def) theory =
let
val admissible' = fold_rule (the_list set_def) admissible;
- val cpo_thms = map (Thm.transfer theory) [type_def, less_def, admissible'];
+ val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
val theory' = theory
|> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
(Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
@@ -110,10 +110,10 @@
|> Sign.parent_path
end;
- fun make_pcpo UU_mem (type_def, less_def, set_def) theory =
+ fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
let
val UU_mem' = fold_rule (the_list set_def) UU_mem;
- val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UU_mem'];
+ val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
val theory' = theory
|> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
(Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
--- a/src/HOLCF/Tr.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Tr.thy Fri May 08 16:19:51 2009 -0700
@@ -37,7 +37,7 @@
text {* distinctness for type @{typ tr} *}
-lemma dist_less_tr [simp]:
+lemma dist_below_tr [simp]:
"\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
unfolding TT_def FF_def by simp_all
@@ -45,16 +45,16 @@
"TT \<noteq> \<bottom>" "FF \<noteq> \<bottom>" "TT \<noteq> FF" "\<bottom> \<noteq> TT" "\<bottom> \<noteq> FF" "FF \<noteq> TT"
unfolding TT_def FF_def by simp_all
-lemma TT_less_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
+lemma TT_below_iff [simp]: "TT \<sqsubseteq> x \<longleftrightarrow> x = TT"
by (induct x rule: tr_induct) simp_all
-lemma FF_less_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
+lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all
-lemma not_less_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
+lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all
-lemma not_less_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
+lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
by (induct x rule: tr_induct) simp_all
--- a/src/HOLCF/Universal.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Universal.thy Fri May 08 16:19:51 2009 -0700
@@ -251,7 +251,7 @@
typedef (open) udom = "{S. udom.ideal S}"
by (fast intro: udom.ideal_principal)
-instantiation udom :: sq_ord
+instantiation udom :: below
begin
definition
@@ -262,16 +262,16 @@
instance udom :: po
by (rule udom.typedef_ideal_po
- [OF type_definition_udom sq_le_udom_def])
+ [OF type_definition_udom below_udom_def])
instance udom :: cpo
by (rule udom.typedef_ideal_cpo
- [OF type_definition_udom sq_le_udom_def])
+ [OF type_definition_udom below_udom_def])
lemma Rep_udom_lub:
"chain Y \<Longrightarrow> Rep_udom (\<Squnion>i. Y i) = (\<Union>i. Rep_udom (Y i))"
by (rule udom.typedef_ideal_rep_contlub
- [OF type_definition_udom sq_le_udom_def])
+ [OF type_definition_udom below_udom_def])
lemma ideal_Rep_udom: "udom.ideal (Rep_udom xs)"
by (rule Rep_udom [unfolded mem_Collect_eq])
@@ -291,7 +291,7 @@
apply (rule ideal_Rep_udom)
apply (erule Rep_udom_lub)
apply (rule Rep_udom_principal)
-apply (simp only: sq_le_udom_def)
+apply (simp only: below_udom_def)
done
text {* Universal domain is pointed *}
@@ -359,9 +359,9 @@
assume "y \<in> insert a A" and "(if x \<sqsubseteq> a then a else x) \<sqsubseteq> y"
thus "(if x \<sqsubseteq> a then a else x) = y"
apply auto
- apply (frule (1) trans_less)
+ apply (frule (1) below_trans)
apply (frule (1) x_eq)
- apply (rule antisym_less, assumption)
+ apply (rule below_antisym, assumption)
apply simp
apply (erule (1) x_eq)
done
@@ -503,7 +503,7 @@
done
lemma rank_leD: "rank x \<le> n \<Longrightarrow> cb_take n x = x"
-apply (rule antisym_less [OF cb_take_less])
+apply (rule below_antisym [OF cb_take_less])
apply (subst compact_approx_rank [symmetric])
apply (erule cb_take_chain_le)
done
@@ -727,7 +727,7 @@
apply (rule IH)
apply (simp add: less_max_iff_disj)
apply (erule place_sub_less)
- apply (erule rev_trans_less)
+ apply (erule rev_below_trans)
apply (rule sub_below)
done
qed
@@ -779,9 +779,9 @@
lemma basis_prj_mono: "ubasis_le a b \<Longrightarrow> basis_prj a \<sqsubseteq> basis_prj b"
proof (induct a b rule: ubasis_le.induct)
- case (ubasis_le_refl a) show ?case by (rule refl_less)
+ case (ubasis_le_refl a) show ?case by (rule below_refl)
next
- case (ubasis_le_trans a b c) thus ?case by - (rule trans_less)
+ case (ubasis_le_trans a b c) thus ?case by - (rule below_trans)
next
case (ubasis_le_lower S a i) thus ?case
apply (cases "node i a S \<in> range (basis_emb :: 'a compact_basis \<Rightarrow> nat)")
--- a/src/HOLCF/Up.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Up.thy Fri May 08 16:19:51 2009 -0700
@@ -26,11 +26,11 @@
subsection {* Ordering on lifted cpo *}
-instantiation u :: (cpo) sq_ord
+instantiation u :: (cpo) below
begin
definition
- less_up_def:
+ below_up_def:
"(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
(case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
@@ -38,13 +38,13 @@
end
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
-by (simp add: less_up_def)
+by (simp add: below_up_def)
-lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
-by (simp add: less_up_def)
+lemma not_Iup_below [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
+by (simp add: below_up_def)
-lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
-by (simp add: less_up_def)
+lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
+by (simp add: below_up_def)
subsection {* Lifted cpo is a partial order *}
@@ -52,17 +52,17 @@
proof
fix x :: "'a u"
show "x \<sqsubseteq> x"
- unfolding less_up_def by (simp split: u.split)
+ unfolding below_up_def by (simp split: u.split)
next
fix x y :: "'a u"
assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
- unfolding less_up_def
- by (auto split: u.split_asm intro: antisym_less)
+ unfolding below_up_def
+ by (auto split: u.split_asm intro: below_antisym)
next
fix x y z :: "'a u"
assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
- unfolding less_up_def
- by (auto split: u.split_asm intro: trans_less)
+ unfolding below_up_def
+ by (auto split: u.split_asm intro: below_trans)
qed
lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
@@ -78,7 +78,7 @@
"range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
apply (rule is_lubI)
apply (rule ub_rangeI)
-apply (subst Iup_less)
+apply (subst Iup_below)
apply (erule is_ub_lub)
apply (case_tac u)
apply (drule ub_rangeD)
@@ -112,7 +112,7 @@
lemma up_lemma4:
"\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
apply (rule chainI)
-apply (rule Iup_less [THEN iffD1])
+apply (rule Iup_below [THEN iffD1])
apply (subst up_lemma3, assumption+)+
apply (simp add: chainE)
done
@@ -235,9 +235,9 @@
by (simp add: up_def cont_Iup inst_up_pcpo)
lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
-by simp
+by simp (* FIXME: remove? *)
-lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
+lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
by (simp add: up_def cont_Iup)
lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
--- a/src/HOLCF/UpperPD.thy Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/UpperPD.thy Fri May 08 16:19:51 2009 -0700
@@ -23,7 +23,7 @@
apply (drule (1) bspec, erule bexE)
apply (drule (1) bspec, erule bexE)
apply (erule rev_bexI)
-apply (erule (1) trans_less)
+apply (erule (1) below_trans)
done
interpretation upper_le: preorder upper_le
@@ -38,7 +38,7 @@
lemma PDPlus_upper_mono: "\<lbrakk>s \<le>\<sharp> t; u \<le>\<sharp> v\<rbrakk> \<Longrightarrow> PDPlus s u \<le>\<sharp> PDPlus t v"
unfolding upper_le_def Rep_PDPlus by fast
-lemma PDPlus_upper_less: "PDPlus t u \<le>\<sharp> t"
+lemma PDPlus_upper_le: "PDPlus t u \<le>\<sharp> t"
unfolding upper_le_def Rep_PDPlus by fast
lemma upper_le_PDUnit_PDUnit_iff [simp]:
@@ -97,7 +97,7 @@
"{S::'a pd_basis set. upper_le.ideal S}"
by (fast intro: upper_le.ideal_principal)
-instantiation upper_pd :: (profinite) sq_ord
+instantiation upper_pd :: (profinite) below
begin
definition
@@ -108,16 +108,16 @@
instance upper_pd :: (profinite) po
by (rule upper_le.typedef_ideal_po
- [OF type_definition_upper_pd sq_le_upper_pd_def])
+ [OF type_definition_upper_pd below_upper_pd_def])
instance upper_pd :: (profinite) cpo
by (rule upper_le.typedef_ideal_cpo
- [OF type_definition_upper_pd sq_le_upper_pd_def])
+ [OF type_definition_upper_pd below_upper_pd_def])
lemma Rep_upper_pd_lub:
"chain Y \<Longrightarrow> Rep_upper_pd (\<Squnion>i. Y i) = (\<Union>i. Rep_upper_pd (Y i))"
by (rule upper_le.typedef_ideal_rep_contlub
- [OF type_definition_upper_pd sq_le_upper_pd_def])
+ [OF type_definition_upper_pd below_upper_pd_def])
lemma ideal_Rep_upper_pd: "upper_le.ideal (Rep_upper_pd xs)"
by (rule Rep_upper_pd [unfolded mem_Collect_eq])
@@ -143,7 +143,7 @@
apply (rule ideal_Rep_upper_pd)
apply (erule Rep_upper_pd_lub)
apply (rule Rep_upper_principal)
-apply (simp only: sq_le_upper_pd_def)
+apply (simp only: below_upper_pd_def)
done
text {* Upper powerdomain is pointed *}
@@ -262,28 +262,28 @@
lemmas upper_plus_aci =
upper_plus_ac upper_plus_absorb upper_plus_left_absorb
-lemma upper_plus_less1: "xs +\<sharp> ys \<sqsubseteq> xs"
+lemma upper_plus_below1: "xs +\<sharp> ys \<sqsubseteq> xs"
apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
-apply (simp add: PDPlus_upper_less)
+apply (simp add: PDPlus_upper_le)
done
-lemma upper_plus_less2: "xs +\<sharp> ys \<sqsubseteq> ys"
-by (subst upper_plus_commute, rule upper_plus_less1)
+lemma upper_plus_below2: "xs +\<sharp> ys \<sqsubseteq> ys"
+by (subst upper_plus_commute, rule upper_plus_below1)
lemma upper_plus_greatest: "\<lbrakk>xs \<sqsubseteq> ys; xs \<sqsubseteq> zs\<rbrakk> \<Longrightarrow> xs \<sqsubseteq> ys +\<sharp> zs"
apply (subst upper_plus_absorb [of xs, symmetric])
apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
done
-lemma upper_less_plus_iff:
+lemma upper_below_plus_iff:
"xs \<sqsubseteq> ys +\<sharp> zs \<longleftrightarrow> xs \<sqsubseteq> ys \<and> xs \<sqsubseteq> zs"
apply safe
-apply (erule trans_less [OF _ upper_plus_less1])
-apply (erule trans_less [OF _ upper_plus_less2])
+apply (erule below_trans [OF _ upper_plus_below1])
+apply (erule below_trans [OF _ upper_plus_below2])
apply (erule (1) upper_plus_greatest)
done
-lemma upper_plus_less_unit_iff:
+lemma upper_plus_below_unit_iff:
"xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
apply (rule iffI)
apply (subgoal_tac
@@ -297,13 +297,13 @@
apply simp
apply simp
apply (erule disjE)
- apply (erule trans_less [OF upper_plus_less1])
- apply (erule trans_less [OF upper_plus_less2])
+ apply (erule below_trans [OF upper_plus_below1])
+ apply (erule below_trans [OF upper_plus_below2])
done
-lemma upper_unit_less_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
+lemma upper_unit_below_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
apply (rule iffI)
- apply (rule profinite_less_ext)
+ apply (rule profinite_below_ext)
apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
@@ -311,10 +311,10 @@
apply (erule monofun_cfun_arg)
done
-lemmas upper_pd_less_simps =
- upper_unit_less_iff
- upper_less_plus_iff
- upper_plus_less_unit_iff
+lemmas upper_pd_below_simps =
+ upper_unit_below_iff
+ upper_below_plus_iff
+ upper_plus_below_unit_iff
lemma upper_unit_eq_iff [simp]: "{x}\<sharp> = {y}\<sharp> \<longleftrightarrow> x = y"
unfolding po_eq_conv by simp
@@ -323,10 +323,10 @@
unfolding inst_upper_pd_pcpo Rep_compact_bot [symmetric] by simp
lemma upper_plus_strict1 [simp]: "\<bottom> +\<sharp> ys = \<bottom>"
-by (rule UU_I, rule upper_plus_less1)
+by (rule UU_I, rule upper_plus_below1)
lemma upper_plus_strict2 [simp]: "xs +\<sharp> \<bottom> = \<bottom>"
-by (rule UU_I, rule upper_plus_less2)
+by (rule UU_I, rule upper_plus_below2)
lemma upper_unit_strict_iff [simp]: "{x}\<sharp> = \<bottom> \<longleftrightarrow> x = \<bottom>"
unfolding upper_unit_strict [symmetric] by (rule upper_unit_eq_iff)
@@ -407,11 +407,11 @@
lemma upper_bind_basis_mono:
"t \<le>\<sharp> u \<Longrightarrow> upper_bind_basis t \<sqsubseteq> upper_bind_basis u"
-unfolding expand_cfun_less
+unfolding expand_cfun_below
apply (erule upper_le_induct, safe)
apply (simp add: monofun_cfun)
-apply (simp add: trans_less [OF upper_plus_less1])
-apply (simp add: upper_less_plus_iff)
+apply (simp add: below_trans [OF upper_plus_below1])
+apply (simp add: upper_below_plus_iff)
done
definition