# HG changeset patch
# User huffman
# Date 1292469306 28800
# Node ID 717404c7d59aa9618f7f4ccbe076b9bcfae5e3b0
# Parent  9240be8c8c69e16d044a3cd9a585a02cff8d99c6
add notsqsubseteq syntax

diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/Adm.thy
--- 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]:
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/Completion.thy
--- 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:
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/Cpodef.thy
--- 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 *}
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/Deflation.thy
--- 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
 
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/Domain_Aux.thy
--- 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"
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/One.thy
--- 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"
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/Porder.thy
--- 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
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/Tr.thy
--- 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
 
 
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/Universal.thy
--- 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")
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/Up.thy
--- 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"
diff -r 9240be8c8c69 -r 717404c7d59a src/HOL/HOLCF/document/root.tex
--- 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}