--- a/src/HOL/HOLCF/Adm.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Adm.thy Wed Dec 15 19:15:06 2010 -0800
@@ -121,19 +121,19 @@
lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
by (simp add: adm_def cont2contlubE ch2ch_cont)
-lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
+lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
subsection {* Compactness *}
definition
compact :: "'a::cpo \<Rightarrow> bool" where
- "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
+ "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
-lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k"
+lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k"
unfolding compact_def .
-lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
+lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> x)"
unfolding compact_def .
lemma compactI2:
@@ -164,7 +164,7 @@
text {* admissibility and compactness *}
lemma adm_compact_not_below [simp]:
- "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
+ "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
unfolding compact_def by (rule adm_subst)
lemma adm_neq_compact [simp]:
--- a/src/HOL/HOLCF/Completion.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Completion.thy Wed Dec 15 19:15:06 2010 -0800
@@ -371,6 +371,21 @@
apply (erule imageI)
done
+lemma cont_basis_fun:
+ assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b"
+ assumes f_cont: "\<And>a. cont (\<lambda>x. f x a)"
+ shows "cont (\<lambda>x. basis_fun (\<lambda>a. f x a))"
+ apply (rule contI2)
+ apply (rule monofunI)
+ apply (rule basis_fun_mono, erule f_mono, erule f_mono)
+ apply (erule cont2monofunE [OF f_cont])
+ apply (rule cfun_belowI)
+ apply (rule principal_induct, simp)
+ apply (simp only: contlub_cfun_fun)
+ apply (simp only: basis_fun_principal f_mono)
+ apply (simp add: cont2contlubE [OF f_cont])
+done
+
end
lemma (in preorder) typedef_ideal_completion:
--- a/src/HOL/HOLCF/Cpodef.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy Wed Dec 15 19:15:06 2010 -0800
@@ -168,9 +168,9 @@
proof (unfold compact_def)
have cont_Rep: "cont Rep"
by (rule typedef_cont_Rep [OF type below adm cont_id])
- 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 below)
+ assume "adm (\<lambda>x. Rep k \<notsqsubseteq> x)"
+ with cont_Rep have "adm (\<lambda>x. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst)
+ thus "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below)
qed
subsection {* Proving a subtype is pointed *}
--- a/src/HOL/HOLCF/Deflation.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Deflation.thy Wed Dec 15 19:15:06 2010 -0800
@@ -206,18 +206,18 @@
lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
proof -
assume "compact (e\<cdot>x)"
- hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
- hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
- hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
+ hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (rule compactD)
+ hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
+ hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by simp
thus "compact x" by (rule compactI)
qed
lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
proof -
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_below_iff_below_p)
+ hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by (rule compactD)
+ hence "adm (\<lambda>y. x \<notsqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
+ hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p)
thus "compact (e\<cdot>x)" by (rule compactI)
qed
--- a/src/HOL/HOLCF/Domain_Aux.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Domain_Aux.thy Wed Dec 15 19:15:06 2010 -0800
@@ -86,10 +86,10 @@
lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
proof (unfold compact_def)
- assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
+ assume "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> 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_below by simp
+ have "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> abs\<cdot>y)" by (rule adm_subst)
+ then show "adm (\<lambda>y. x \<notsqsubseteq> y)" using abs_below by simp
qed
lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
--- a/src/HOL/HOLCF/One.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/One.thy Wed Dec 15 19:15:06 2010 -0800
@@ -28,7 +28,7 @@
lemma one_induct [case_names bottom ONE]: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
by (cases x rule: oneE) simp_all
-lemma dist_below_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
+lemma dist_below_one [simp]: "ONE \<notsqsubseteq> \<bottom>"
unfolding ONE_def by simp
lemma below_ONE [simp]: "x \<sqsubseteq> ONE"
--- a/src/HOL/HOLCF/Porder.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Porder.thy Wed Dec 15 19:15:06 2010 -0800
@@ -20,6 +20,13 @@
notation (xsymbols)
below (infix "\<sqsubseteq>" 50)
+abbreviation
+ not_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "~<<" 50)
+ where "not_below x y \<equiv> \<not> below x y"
+
+notation (xsymbols)
+ not_below (infix "\<notsqsubseteq>" 50)
+
lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
by (rule subst)
@@ -46,7 +53,7 @@
lemma rev_below_trans: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
by (rule below_trans)
-lemma not_below2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
+lemma not_below2not_eq: "x \<notsqsubseteq> y \<Longrightarrow> x \<noteq> y"
by auto
end
--- a/src/HOL/HOLCF/Tr.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Tr.thy Wed Dec 15 19:15:06 2010 -0800
@@ -40,7 +40,7 @@
text {* distinctness for type @{typ tr} *}
lemma dist_below_tr [simp]:
- "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
+ "TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT"
unfolding TT_def FF_def by simp_all
lemma dist_eq_tr [simp]:
@@ -53,10 +53,10 @@
lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all
-lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
+lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all
-lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
+lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT"
by (induct x rule: tr_induct) simp_all
--- a/src/HOL/HOLCF/Universal.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Universal.thy Wed Dec 15 19:15:06 2010 -0800
@@ -392,7 +392,7 @@
done
lemma choose_pos_lessD:
- "\<lbrakk>choose_pos A x < choose_pos A y; finite A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<not> x \<sqsubseteq> y"
+ "\<lbrakk>choose_pos A x < choose_pos A y; finite A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<notsqsubseteq> y"
apply (induct A x arbitrary: y rule: choose_pos.induct)
apply simp
apply (case_tac "x = choose A")
--- a/src/HOL/HOLCF/Up.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Up.thy Wed Dec 15 19:15:06 2010 -0800
@@ -38,7 +38,7 @@
lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
by (simp add: below_up_def)
-lemma not_Iup_below [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
+lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom"
by (simp add: below_up_def)
lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
@@ -200,7 +200,7 @@
lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
by (simp add: up_def cont_Iup inst_up_pcpo)
-lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
+lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>"
by simp (* FIXME: remove? *)
lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
--- a/src/HOL/HOLCF/document/root.tex Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/document/root.tex Wed Dec 15 19:15:06 2010 -0800
@@ -12,6 +12,7 @@
\pagestyle{myheadings}
\newcommand{\isasymas}{\textsf{as}}
\newcommand{\isasymlazy}{\isamath{\sim}}
+\newcommand{\isasymnotsqsubseteq}{\isamath{\not\sqsubseteq}}
\begin{document}