# HG changeset patch
# User blanchet
# Date 1289223234 -3600
# Node ID 29b610d53c48e9dadf5e89dc73ba6756a7b57198
# Parent  fb6ee11e776a284538ef3c55eea0e69f0085fd29# Parent  61176a1f9cd3a92ad0f8755fbf9c16968aa791f1
merge

diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/Adm.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -29,16 +29,6 @@
 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
 by (rule admI, erule spec)
 
-text {* improved admissibility introduction *}
-
-lemma admI2:
-  "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> 
-    \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
-apply (rule admI)
-apply (erule (1) increasing_chain_adm_lemma)
-apply fast
-done
-
 subsection {* Admissibility on chain-finite types *}
 
 text {* for chain-finite (easy) types every formula is admissible *}
@@ -122,25 +112,14 @@
 
 lemma adm_below [simp]:
   "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x \<sqsubseteq> v x)"
-apply (rule admI)
-apply (simp add: cont2contlubE)
-apply (rule lub_mono)
-apply (erule (1) ch2ch_cont)
-apply (erule (1) ch2ch_cont)
-apply (erule spec)
-done
+by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont)
 
 lemma adm_eq [simp]:
   "\<lbrakk>cont (\<lambda>x. u x); cont (\<lambda>x. v x)\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
 by (simp add: po_eq_conv)
 
 lemma adm_subst: "\<lbrakk>cont (\<lambda>x. t x); adm P\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P (t x))"
-apply (rule admI)
-apply (simp add: cont2contlubE)
-apply (erule admD)
-apply (erule (1) ch2ch_cont)
-apply (erule spec)
-done
+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)"
 by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/Cfun.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -355,16 +355,13 @@
   "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
 by (simp add: cont2cont_LAM)
 
-lemmas cont_lemmas1 =
-  cont_const cont_id cont_Rep_cfun2 cont2cont_APP cont2cont_LAM
-
 subsection {* Miscellaneous *}
 
 text {* Monotonicity of @{term Abs_cfun} *}
 
-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: below_cfun_def Abs_cfun_inverse2)
+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: cfun_below_iff)
 
 text {* some lemmata for functions with flat/chfin domain/range types *}
 
@@ -418,29 +415,6 @@
   "\<lbrakk>\<forall>x. f\<cdot>(g\<cdot>x) = x; z \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> g\<cdot>z \<noteq> \<bottom>"
 by (erule contrapos_nn, rule injection_defined_rev)
 
-text {* propagation of flatness and chain-finiteness by retractions *}
-
-lemma chfin2chfin:
-  "\<forall>y. (f::'a::chfin \<rightarrow> 'b)\<cdot>(g\<cdot>y) = y
-    \<Longrightarrow> \<forall>Y::nat \<Rightarrow> 'b. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
-apply clarify
-apply (drule_tac f=g in chain_monofun)
-apply (drule chfin)
-apply (unfold max_in_chain_def)
-apply (simp add: injection_eq)
-done
-
-lemma flat2flat:
-  "\<forall>y. (f::'a::flat \<rightarrow> 'b::pcpo)\<cdot>(g\<cdot>y) = y
-    \<Longrightarrow> \<forall>x y::'b. x \<sqsubseteq> y \<longrightarrow> x = \<bottom> \<or> x = y"
-apply clarify
-apply (drule_tac f=g in monofun_cfun_arg)
-apply (drule ax_flat)
-apply (erule disjE)
-apply (simp add: injection_defined_rev)
-apply (simp add: injection_eq)
-done
-
 text {* a result about functions with flat codomain *}
 
 lemma flat_eqI: "\<lbrakk>(x::'a::flat) \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> x = y"
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/ConvexPD.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -33,7 +33,7 @@
 unfolding convex_le_def by (fast intro: PDPlus_upper_mono PDPlus_lower_mono)
 
 lemma convex_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<natural> PDUnit b) = a \<sqsubseteq> b"
+  "(PDUnit a \<le>\<natural> PDUnit b) = (a \<sqsubseteq> b)"
 unfolding convex_le_def upper_le_def lower_le_def Rep_PDUnit by fast
 
 lemma convex_le_PDUnit_lemma1:
@@ -329,10 +329,6 @@
 apply (rule fold_pd_PDPlus [OF ACI_convex_bind])
 done
 
-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: cfun_below_iff)
-
 lemma convex_bind_basis_mono:
   "t \<le>\<natural> u \<Longrightarrow> convex_bind_basis t \<sqsubseteq> convex_bind_basis u"
 apply (erule convex_le_induct)
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/Discrete.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -10,39 +10,18 @@
 
 datatype 'a discr = Discr "'a :: type"
 
-subsection {* Discrete ordering *}
+subsection {* Discrete cpo class instance *}
 
-instantiation discr :: (type) below
+instantiation discr :: (type) discrete_cpo
 begin
 
 definition
-  below_discr_def:
-    "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
-
-instance ..
-end
-
-subsection {* Discrete cpo class instance *}
-
-instance discr :: (type) discrete_cpo
-by intro_classes (simp add: below_discr_def)
-
-lemma discr_below_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
-by simp (* FIXME: same discrete_cpo - remove? is [iff] important? *)
+  "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
 
-lemma discr_chain0: 
- "!!S::nat=>('a::type)discr. chain S ==> S i = S 0"
-apply (unfold chain_def)
-apply (induct_tac "i")
-apply (rule refl)
-apply (erule subst)
-apply (rule sym)
-apply fast
-done
+instance
+by default (simp add: below_discr_def)
 
-lemma discr_chain_range0 [simp]: 
- "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
-by (fast elim: discr_chain0)
+end
 
 subsection {* \emph{undiscr} *}
 
@@ -56,11 +35,4 @@
 lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
 by (induct y) simp
 
-lemma discr_chain_f_range0:
- "!!S::nat=>('a::type)discr. chain(S) ==> range(%i. f(S i)) = {f(S 0)}"
-by (fast dest: discr_chain0 elim: arg_cong)
-
-lemma cont_discr [iff]: "cont (%x::('a::type)discr. f x)"
-by (rule cont_discrete_cpo)
-
 end
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/FOCUS/Fstream.thy
--- a/src/HOLCF/FOCUS/Fstream.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -94,7 +94,7 @@
 apply (rule lift.exhaust)
 apply (erule (1) notE)
 apply (safe)
-apply (drule Def_inject_less_eq [THEN iffD1])
+apply (drule Def_below_Def [THEN iffD1])
 apply fast
 done
 
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/FOCUS/Fstreams.thy
--- a/src/HOLCF/FOCUS/Fstreams.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -217,7 +217,7 @@
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (case_tac "y=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (simp add: flat_less_iff)
+apply (simp add: flat_below_iff)
 apply (case_tac "s=UU", auto)
 apply (drule stream_exhaust_eq [THEN iffD1], auto)
 apply (erule_tac x="ya" in allE)
@@ -225,11 +225,11 @@
 apply (case_tac "y=UU",auto)
 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
 apply auto
-apply (simp add: flat_less_iff)
+apply (simp add: flat_below_iff)
 apply (erule_tac x="tt" in allE)
 apply (erule_tac x="yb" in allE, auto)
-apply (simp add: flat_less_iff)
-by (simp add: flat_less_iff)
+apply (simp add: flat_below_iff)
+by (simp add: flat_below_iff)
 
 lemma fstreams_lub_lemma1: "[| chain Y; (LUB i. Y i) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
 apply (subgoal_tac "(LUB i. Y i) ~= UU")
@@ -249,7 +249,7 @@
 apply (frule lub_finch1 [THEN thelubI], auto)
 apply (rule_tac x="j" in exI)
 apply (erule subst) back back
-apply (simp add: less_cprod_def sconc_mono)
+apply (simp add: below_prod_def sconc_mono)
 apply (simp add: max_in_chain_def, auto)
 apply (rule_tac x="ja" in exI)
 apply (subgoal_tac "Y j << Y ja")
@@ -274,7 +274,7 @@
 apply (rule_tac x="i" in exI, auto)
 apply (simp add: max_in_chain_def, auto)
 apply (subgoal_tac "Y i << Y j",auto)
-apply (simp add: less_cprod_def, clarsimp)
+apply (simp add: below_prod_def, clarsimp)
 apply (drule ax_flat, auto)
 apply (case_tac "snd (Y j) = UU",auto)
 apply (case_tac "Y j", auto)
@@ -305,8 +305,8 @@
 apply (simp add: max_in_chain_def, auto)
 apply (rule_tac x="ja" in exI)
 apply (subgoal_tac "Y j << Y ja")
-apply (simp add: less_cprod_def, auto)
-apply (drule trans_less)
+apply (simp add: below_prod_def, auto)
+apply (drule below_trans)
 apply (simp add: ax_flat, auto)
 apply (drule fstreams_prefix, auto)+
 apply (rule sconc_mono)
@@ -316,7 +316,7 @@
 apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
 apply (drule fstreams_mono, simp)
 apply (rule is_ub_thelub chainI)
-apply (simp add: chain_def less_cprod_def)
+apply (simp add: chain_def below_prod_def)
 apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp)
 apply (drule ax_flat, simp)+
 apply (drule prod_eqI, auto)
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -29,6 +29,31 @@
 
 section "admissibility"
 
+lemma infinite_chain_adm_lemma:
+  "\<lbrakk>Porder.chain Y; \<forall>i. P (Y i);  
+    \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
+      \<Longrightarrow> P (\<Squnion>i. Y i)"
+apply (case_tac "finite_chain Y")
+prefer 2 apply fast
+apply (unfold finite_chain_def)
+apply safe
+apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
+apply assumption
+apply (erule spec)
+done
+
+lemma increasing_chain_adm_lemma:
+  "\<lbrakk>Porder.chain Y;  \<forall>i. P (Y i); \<And>Y. \<lbrakk>Porder.chain Y; \<forall>i. P (Y i);
+    \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
+      \<Longrightarrow> P (\<Squnion>i. Y i)"
+apply (erule infinite_chain_adm_lemma)
+apply assumption
+apply (erule thin_rl)
+apply (unfold finite_chain_def)
+apply (unfold max_in_chain_def)
+apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
+done
+
 lemma flatstream_adm_lemma:
   assumes 1: "Porder.chain Y"
   assumes 2: "!i. P (Y i)"
@@ -132,7 +157,7 @@
 apply ( fast)
 apply (unfold linorder_not_less)
 apply (drule (1) mp)
-apply (erule all_dupE, drule mp, rule refl_less)
+apply (erule all_dupE, drule mp, rule below_refl)
 apply (erule ssubst)
 apply (erule allE, drule (1) mp)
 apply (drule_tac P="%x. x" in subst, assumption)
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/HOLCF.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -31,52 +31,4 @@
 lemmas cont_Rep_CFun_app = cont_APP_app
 lemmas cont_Rep_CFun_app_app = cont_APP_app_app
 
-text {* Older 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 less_up_def = below_up_def
-lemmas not_Iup_less = not_Iup_below
-lemmas Iup_less = Iup_below
-lemmas up_less = up_below
-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
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -260,8 +260,8 @@
 apply auto
 
 (* a: act A; a: act B *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 back
 apply (erule conjE)+
 (* Finite (tw iA x) and Finite (tw iB y) *)
@@ -275,7 +275,7 @@
 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
 
 (* a: act B; a~: act A *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 
 apply (erule conjE)+
 (* Finite (tw iB y) *)
@@ -287,7 +287,7 @@
 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
 
 (* a~: act B; a: act A *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 
 apply (erule conjE)+
 (* Finite (tw iA x) *)
@@ -327,7 +327,7 @@
 apply (erule conjE)+
 apply simp
 (* divide_Seq on s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 (* transform assumption f eB y = f B (s@z) *)
 apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $ (s@@z) " in subst_lemma2)
@@ -373,7 +373,7 @@
 apply (erule conjE)+
 apply simp
 (* divide_Seq on s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 (* transform assumption f eA x = f A (s@z) *)
 apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $ (s@@z) " in subst_lemma2)
@@ -557,7 +557,7 @@
 prefer 2 apply fast
 
 (* bring in divide Seq for s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
 (* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -610,7 +610,7 @@
 prefer 2 apply (fast)
 
 (* bring in divide Seq for s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
 (* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -628,7 +628,7 @@
 apply (simp add: ext_and_act)
 
 (* divide_Seq for schB2 *)
-apply (frule_tac y = "y2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule_tac y = "y2" in sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 (* assumption schA *)
 apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
@@ -776,7 +776,7 @@
 prefer 2 apply (fast)
 
 (* bring in divide Seq for s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
 (* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -827,7 +827,7 @@
 prefer 2 apply (fast)
 
 (* bring in divide Seq for s *)
-apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 
 (* subst divide_Seq in conclusion, but only at the righest occurence *)
@@ -845,7 +845,7 @@
 apply (simp add: ext_and_act)
 
 (* divide_Seq for schB2 *)
-apply (frule_tac y = "x2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
+apply (frule_tac y = "x2" in sym [THEN eq_imp_below, THEN divide_Seq])
 apply (erule conjE)+
 (* assumption schA *)
 apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -293,7 +293,7 @@
 
 lemma Cons_not_less_UU: "~(a>>x) << UU"
 apply (rule notI)
-apply (drule antisym_less)
+apply (drule below_antisym)
 apply simp
 apply (simp add: Cons_not_UU)
 done
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/Library/Sum_Cpo.thy
--- a/src/HOLCF/Library/Sum_Cpo.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/Library/Sum_Cpo.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -21,10 +21,10 @@
 instance ..
 end
 
-lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
+lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y \<longleftrightarrow> x \<sqsubseteq> y"
 unfolding below_sum_def by simp
 
-lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
+lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y \<longleftrightarrow> x \<sqsubseteq> y"
 unfolding below_sum_def by simp
 
 lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/LowerPD.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -43,7 +43,7 @@
 unfolding lower_le_def Rep_PDPlus by fast
 
 lemma lower_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<flat> PDUnit b) = a \<sqsubseteq> b"
+  "(PDUnit a \<le>\<flat> PDUnit b) = (a \<sqsubseteq> b)"
 unfolding lower_le_def Rep_PDUnit by fast
 
 lemma lower_le_PDUnit_PDPlus_iff:
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/Porder.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -15,10 +15,10 @@
 begin
 
 notation
-  below (infixl "<<" 55)
+  below (infix "<<" 50)
 
 notation (xsymbols)
-  below (infixl "\<sqsubseteq>" 55)
+  below (infix "\<sqsubseteq>" 50)
 
 lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
   by (rule subst)
@@ -34,14 +34,7 @@
   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 below_antisym)
-
-text {* the reverse law of anti-symmetry of @{term "op <<"} *}
-(* Is this rule ever useful? *)
-lemma below_antisym_inverse: "x = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
+lemma eq_imp_below: "x = y \<Longrightarrow> x \<sqsubseteq> y"
   by simp
 
 lemma box_below: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
@@ -69,7 +62,7 @@
 
 subsection {* Upper bounds *}
 
-definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<|" 55) where
+definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<|" 55) where
   "S <| x \<longleftrightarrow> (\<forall>y\<in>S. y \<sqsubseteq> x)"
 
 lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S <| u"
@@ -101,7 +94,7 @@
 
 subsection {* Least upper bounds *}
 
-definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<|" 55) where
+definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<<|" 55) where
   "S <<| x \<longleftrightarrow> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
 
 definition lub :: "'a set \<Rightarrow> 'a" where
@@ -344,33 +337,6 @@
 lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
   by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI)
 
-text {* lemmata for improved admissibility introdution rule *}
-
-lemma infinite_chain_adm_lemma:
-  "\<lbrakk>chain Y; \<forall>i. P (Y i);  
-    \<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i); \<not> finite_chain Y\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
-      \<Longrightarrow> P (\<Squnion>i. Y i)"
-apply (case_tac "finite_chain Y")
-prefer 2 apply fast
-apply (unfold finite_chain_def)
-apply safe
-apply (erule lub_finch1 [THEN thelubI, THEN ssubst])
-apply assumption
-apply (erule spec)
-done
-
-lemma increasing_chain_adm_lemma:
-  "\<lbrakk>chain Y;  \<forall>i. P (Y i); \<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i);
-    \<forall>i. \<exists>j>i. Y i \<noteq> Y j \<and> Y i \<sqsubseteq> Y j\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)\<rbrakk>
-      \<Longrightarrow> P (\<Squnion>i. Y i)"
-apply (erule infinite_chain_adm_lemma)
-apply assumption
-apply (erule thin_rl)
-apply (unfold finite_chain_def)
-apply (unfold max_in_chain_def)
-apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
-done
-
 end
 
 end
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/Sprod.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -151,18 +151,18 @@
 lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
 by (cases p, simp_all)
 
-lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
+lemma below_sprod: "(x \<sqsubseteq> y) = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
 by (simp add: Rep_sprod_simps sfst_def ssnd_def cont_Rep_sprod)
 
 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 below_sprod)
 
-lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
+lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
 apply (simp add: below_sprod)
 done
 
-lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
+lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y \<longleftrightarrow> x \<sqsubseteq> (:sfst\<cdot>x, y:)"
 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
 apply (simp add: below_sprod)
 done
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/UpperPD.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -42,7 +42,7 @@
 unfolding upper_le_def Rep_PDPlus by fast
 
 lemma upper_le_PDUnit_PDUnit_iff [simp]:
-  "(PDUnit a \<le>\<sharp> PDUnit b) = a \<sqsubseteq> b"
+  "(PDUnit a \<le>\<sharp> PDUnit b) = (a \<sqsubseteq> b)"
 unfolding upper_le_def Rep_PDUnit by fast
 
 lemma upper_le_PDPlus_PDUnit_iff:
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/ex/Dagstuhl.thy
--- a/src/HOLCF/ex/Dagstuhl.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/ex/Dagstuhl.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -46,7 +46,7 @@
   done
 
 lemma lemma5: "y && YYS = YYS"
-  apply (rule antisym_less)
+  apply (rule below_antisym)
   apply (rule lemma4)
   apply (rule lemma3)
   done
@@ -84,7 +84,7 @@
   done
 
 lemma wir_moel': "YS = YYS"
-  apply (rule antisym_less)
+  apply (rule below_antisym)
   apply (rule lemma7)
   apply (rule lemma6)
   done
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/ex/Fix2.thy
--- a/src/HOLCF/ex/Fix2.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/ex/Fix2.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -17,7 +17,7 @@
 
 lemma lemma1: "fix = gix"
 apply (rule cfun_eqI)
-apply (rule antisym_less)
+apply (rule below_antisym)
 apply (rule fix_least)
 apply (rule gix1_def)
 apply (rule gix2_def)
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/ex/Hoare.thy
--- a/src/HOLCF/ex/Hoare.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/ex/Hoare.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -95,9 +95,7 @@
 
 
 lemma hoare_lemma28: "f$(y::'a)=(UU::tr) ==> f$UU = UU"
-apply (erule flat_codom [THEN disjE])
-apply auto
-done
+by (rule strictI)
 
 
 (* ----- access to definitions ----- *)
diff -r fb6ee11e776a -r 29b610d53c48 src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Mon Nov 08 14:33:30 2010 +0100
+++ b/src/HOLCF/ex/Loop.thy	Mon Nov 08 14:33:54 2010 +0100
@@ -47,8 +47,7 @@
 apply simp
 apply (rule allI)
 apply (rule trans)
-apply (subst while_unfold)
-apply (rule_tac [2] refl)
+apply (rule while_unfold)
 apply (subst iterate_Suc2)
 apply (rule trans)
 apply (erule_tac [2] spec)
@@ -57,9 +56,7 @@
 apply simp
 apply (subst while_unfold)
 apply (rule_tac s = "UU" and t = "b$UU" in ssubst)
-apply (erule flat_codom [THEN disjE])
-apply assumption
-apply (erule spec)
+apply (erule strictI)
 apply simp
 apply simp
 apply simp