--- 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)
--- 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"
--- 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)
--- 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
--- 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
--- 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)
--- 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)
--- 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
--- 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)
--- 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
--- 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"
--- 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:
--- 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
--- 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
--- 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:
--- 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
--- 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)
--- 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 ----- *)
--- 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