add notsqsubseteq syntax
authorhuffman
Wed Dec 15 19:15:06 2010 -0800 (2010-12-15)
changeset 41182717404c7d59a
parent 41181 9240be8c8c69
child 41183 e20f0d0e2af3
add notsqsubseteq syntax
src/HOL/HOLCF/Adm.thy
src/HOL/HOLCF/Completion.thy
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/Deflation.thy
src/HOL/HOLCF/Domain_Aux.thy
src/HOL/HOLCF/One.thy
src/HOL/HOLCF/Porder.thy
src/HOL/HOLCF/Tr.thy
src/HOL/HOLCF/Universal.thy
src/HOL/HOLCF/Up.thy
src/HOL/HOLCF/document/root.tex
     1.1 --- a/src/HOL/HOLCF/Adm.thy	Wed Dec 15 20:52:20 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/Adm.thy	Wed Dec 15 19:15:06 2010 -0800
     1.3 @@ -121,19 +121,19 @@
     1.4  lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
     1.5  by (simp add: adm_def cont2contlubE ch2ch_cont)
     1.6  
     1.7 -lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
     1.8 +lemma adm_not_below [simp]: "cont (\<lambda>x. t x) \<Longrightarrow> adm (\<lambda>x. t x \<notsqsubseteq> u)"
     1.9  by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
    1.10  
    1.11  subsection {* Compactness *}
    1.12  
    1.13  definition
    1.14    compact :: "'a::cpo \<Rightarrow> bool" where
    1.15 -  "compact k = adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
    1.16 +  "compact k = adm (\<lambda>x. k \<notsqsubseteq> x)"
    1.17  
    1.18 -lemma compactI: "adm (\<lambda>x. \<not> k \<sqsubseteq> x) \<Longrightarrow> compact k"
    1.19 +lemma compactI: "adm (\<lambda>x. k \<notsqsubseteq> x) \<Longrightarrow> compact k"
    1.20  unfolding compact_def .
    1.21  
    1.22 -lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> x)"
    1.23 +lemma compactD: "compact k \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> x)"
    1.24  unfolding compact_def .
    1.25  
    1.26  lemma compactI2:
    1.27 @@ -164,7 +164,7 @@
    1.28  text {* admissibility and compactness *}
    1.29  
    1.30  lemma adm_compact_not_below [simp]:
    1.31 -  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<not> k \<sqsubseteq> t x)"
    1.32 +  "\<lbrakk>compact k; cont (\<lambda>x. t x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. k \<notsqsubseteq> t x)"
    1.33  unfolding compact_def by (rule adm_subst)
    1.34  
    1.35  lemma adm_neq_compact [simp]:
     2.1 --- a/src/HOL/HOLCF/Completion.thy	Wed Dec 15 20:52:20 2010 +0100
     2.2 +++ b/src/HOL/HOLCF/Completion.thy	Wed Dec 15 19:15:06 2010 -0800
     2.3 @@ -371,6 +371,21 @@
     2.4   apply (erule imageI)
     2.5  done
     2.6  
     2.7 +lemma cont_basis_fun:
     2.8 +  assumes f_mono: "\<And>a b x. a \<preceq> b \<Longrightarrow> f x a \<sqsubseteq> f x b"
     2.9 +  assumes f_cont: "\<And>a. cont (\<lambda>x. f x a)"
    2.10 +  shows "cont (\<lambda>x. basis_fun (\<lambda>a. f x a))"
    2.11 + apply (rule contI2)
    2.12 +  apply (rule monofunI)
    2.13 +  apply (rule basis_fun_mono, erule f_mono, erule f_mono)
    2.14 +  apply (erule cont2monofunE [OF f_cont])
    2.15 + apply (rule cfun_belowI)
    2.16 + apply (rule principal_induct, simp)
    2.17 + apply (simp only: contlub_cfun_fun)
    2.18 + apply (simp only: basis_fun_principal f_mono)
    2.19 + apply (simp add: cont2contlubE [OF f_cont])
    2.20 +done
    2.21 +
    2.22  end
    2.23  
    2.24  lemma (in preorder) typedef_ideal_completion:
     3.1 --- a/src/HOL/HOLCF/Cpodef.thy	Wed Dec 15 20:52:20 2010 +0100
     3.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Wed Dec 15 19:15:06 2010 -0800
     3.3 @@ -168,9 +168,9 @@
     3.4  proof (unfold compact_def)
     3.5    have cont_Rep: "cont Rep"
     3.6      by (rule typedef_cont_Rep [OF type below adm cont_id])
     3.7 -  assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
     3.8 -  with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
     3.9 -  thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
    3.10 +  assume "adm (\<lambda>x. Rep k \<notsqsubseteq> x)"
    3.11 +  with cont_Rep have "adm (\<lambda>x. Rep k \<notsqsubseteq> Rep x)" by (rule adm_subst)
    3.12 +  thus "adm (\<lambda>x. k \<notsqsubseteq> x)" by (unfold below)
    3.13  qed
    3.14  
    3.15  subsection {* Proving a subtype is pointed *}
     4.1 --- a/src/HOL/HOLCF/Deflation.thy	Wed Dec 15 20:52:20 2010 +0100
     4.2 +++ b/src/HOL/HOLCF/Deflation.thy	Wed Dec 15 19:15:06 2010 -0800
     4.3 @@ -206,18 +206,18 @@
     4.4  lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
     4.5  proof -
     4.6    assume "compact (e\<cdot>x)"
     4.7 -  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
     4.8 -  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
     4.9 -  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
    4.10 +  hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (rule compactD)
    4.11 +  hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
    4.12 +  hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by simp
    4.13    thus "compact x" by (rule compactI)
    4.14  qed
    4.15  
    4.16  lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
    4.17  proof -
    4.18    assume "compact x"
    4.19 -  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
    4.20 -  hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
    4.21 -  hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
    4.22 +  hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by (rule compactD)
    4.23 +  hence "adm (\<lambda>y. x \<notsqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
    4.24 +  hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p)
    4.25    thus "compact (e\<cdot>x)" by (rule compactI)
    4.26  qed
    4.27  
     5.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Wed Dec 15 20:52:20 2010 +0100
     5.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Wed Dec 15 19:15:06 2010 -0800
     5.3 @@ -86,10 +86,10 @@
     5.4  
     5.5  lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
     5.6  proof (unfold compact_def)
     5.7 -  assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
     5.8 +  assume "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> y)"
     5.9    with cont_Rep_cfun2
    5.10 -  have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
    5.11 -  then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
    5.12 +  have "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> abs\<cdot>y)" by (rule adm_subst)
    5.13 +  then show "adm (\<lambda>y. x \<notsqsubseteq> y)" using abs_below by simp
    5.14  qed
    5.15  
    5.16  lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
     6.1 --- a/src/HOL/HOLCF/One.thy	Wed Dec 15 20:52:20 2010 +0100
     6.2 +++ b/src/HOL/HOLCF/One.thy	Wed Dec 15 19:15:06 2010 -0800
     6.3 @@ -28,7 +28,7 @@
     6.4  lemma one_induct [case_names bottom ONE]: "\<lbrakk>P \<bottom>; P ONE\<rbrakk> \<Longrightarrow> P x"
     6.5  by (cases x rule: oneE) simp_all
     6.6  
     6.7 -lemma dist_below_one [simp]: "\<not> ONE \<sqsubseteq> \<bottom>"
     6.8 +lemma dist_below_one [simp]: "ONE \<notsqsubseteq> \<bottom>"
     6.9  unfolding ONE_def by simp
    6.10  
    6.11  lemma below_ONE [simp]: "x \<sqsubseteq> ONE"
     7.1 --- a/src/HOL/HOLCF/Porder.thy	Wed Dec 15 20:52:20 2010 +0100
     7.2 +++ b/src/HOL/HOLCF/Porder.thy	Wed Dec 15 19:15:06 2010 -0800
     7.3 @@ -20,6 +20,13 @@
     7.4  notation (xsymbols)
     7.5    below (infix "\<sqsubseteq>" 50)
     7.6  
     7.7 +abbreviation
     7.8 +  not_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "~<<" 50)
     7.9 +  where "not_below x y \<equiv> \<not> below x y"
    7.10 +
    7.11 +notation (xsymbols)
    7.12 +  not_below (infix "\<notsqsubseteq>" 50)
    7.13 +
    7.14  lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
    7.15    by (rule subst)
    7.16  
    7.17 @@ -46,7 +53,7 @@
    7.18  lemma rev_below_trans: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
    7.19    by (rule below_trans)
    7.20  
    7.21 -lemma not_below2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
    7.22 +lemma not_below2not_eq: "x \<notsqsubseteq> y \<Longrightarrow> x \<noteq> y"
    7.23    by auto
    7.24  
    7.25  end
     8.1 --- a/src/HOL/HOLCF/Tr.thy	Wed Dec 15 20:52:20 2010 +0100
     8.2 +++ b/src/HOL/HOLCF/Tr.thy	Wed Dec 15 19:15:06 2010 -0800
     8.3 @@ -40,7 +40,7 @@
     8.4  text {* distinctness for type @{typ tr} *}
     8.5  
     8.6  lemma dist_below_tr [simp]:
     8.7 -  "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
     8.8 +  "TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT"
     8.9  unfolding TT_def FF_def by simp_all
    8.10  
    8.11  lemma dist_eq_tr [simp]:
    8.12 @@ -53,10 +53,10 @@
    8.13  lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
    8.14  by (induct x rule: tr_induct) simp_all
    8.15  
    8.16 -lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
    8.17 +lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF"
    8.18  by (induct x rule: tr_induct) simp_all
    8.19  
    8.20 -lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
    8.21 +lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT"
    8.22  by (induct x rule: tr_induct) simp_all
    8.23  
    8.24  
     9.1 --- a/src/HOL/HOLCF/Universal.thy	Wed Dec 15 20:52:20 2010 +0100
     9.2 +++ b/src/HOL/HOLCF/Universal.thy	Wed Dec 15 19:15:06 2010 -0800
     9.3 @@ -392,7 +392,7 @@
     9.4  done
     9.5  
     9.6  lemma choose_pos_lessD:
     9.7 -  "\<lbrakk>choose_pos A x < choose_pos A y; finite A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<not> x \<sqsubseteq> y"
     9.8 +  "\<lbrakk>choose_pos A x < choose_pos A y; finite A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x \<notsqsubseteq> y"
     9.9   apply (induct A x arbitrary: y rule: choose_pos.induct)
    9.10   apply simp
    9.11   apply (case_tac "x = choose A")
    10.1 --- a/src/HOL/HOLCF/Up.thy	Wed Dec 15 20:52:20 2010 +0100
    10.2 +++ b/src/HOL/HOLCF/Up.thy	Wed Dec 15 19:15:06 2010 -0800
    10.3 @@ -38,7 +38,7 @@
    10.4  lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
    10.5  by (simp add: below_up_def)
    10.6  
    10.7 -lemma not_Iup_below [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
    10.8 +lemma not_Iup_below [iff]: "Iup x \<notsqsubseteq> Ibottom"
    10.9  by (simp add: below_up_def)
   10.10  
   10.11  lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
   10.12 @@ -200,7 +200,7 @@
   10.13  lemma up_defined [simp]: "up\<cdot>x \<noteq> \<bottom>"
   10.14  by (simp add: up_def cont_Iup inst_up_pcpo)
   10.15  
   10.16 -lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
   10.17 +lemma not_up_less_UU: "up\<cdot>x \<notsqsubseteq> \<bottom>"
   10.18  by simp (* FIXME: remove? *)
   10.19  
   10.20  lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
    11.1 --- a/src/HOL/HOLCF/document/root.tex	Wed Dec 15 20:52:20 2010 +0100
    11.2 +++ b/src/HOL/HOLCF/document/root.tex	Wed Dec 15 19:15:06 2010 -0800
    11.3 @@ -12,6 +12,7 @@
    11.4  \pagestyle{myheadings}
    11.5  \newcommand{\isasymas}{\textsf{as}}
    11.6  \newcommand{\isasymlazy}{\isamath{\sim}}
    11.7 +\newcommand{\isasymnotsqsubseteq}{\isamath{\not\sqsubseteq}}
    11.8  
    11.9  \begin{document}
   11.10