--- a/src/HOLCF/Adm.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/Adm.thy Thu Jan 17 21:44:19 2008 +0100
@@ -64,7 +64,7 @@
"\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk>
\<Longrightarrow> chain (\<lambda>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
apply (rule chainI)
-apply (erule chain_mono3)
+apply (erule chain_mono)
apply (rule Least_le)
apply (rule LeastI2_ex)
apply simp_all
@@ -78,7 +78,7 @@
apply (frule (1) adm_disj_lemma1)
apply (rule antisym_less)
apply (rule lub_mono [rule_format], assumption+)
- apply (erule chain_mono3)
+ apply (erule chain_mono)
apply (simp add: adm_disj_lemma2)
apply (rule lub_range_mono, fast, assumption+)
done
@@ -180,7 +180,7 @@
apply (erule exE, rule_tac x=i in exI)
apply (rule max_in_chainI)
apply (rule antisym_less)
-apply (erule (1) chain_mono3)
+apply (erule (1) chain_mono)
apply (erule (1) trans_less [OF is_ub_thelub])
done
--- a/src/HOLCF/Bifinite.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/Bifinite.thy Thu Jan 17 21:44:19 2008 +0100
@@ -56,7 +56,7 @@
apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
apply (rule monofun_cfun_arg)
apply (rule monofun_cfun_fun)
-apply (erule chain_mono3 [OF chain_approx])
+apply (erule chain_mono [OF chain_approx])
done
lemma approx_approx2:
@@ -65,7 +65,7 @@
apply (rule approx_less)
apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
apply (rule monofun_cfun_fun)
-apply (erule chain_mono3 [OF chain_approx])
+apply (erule chain_mono [OF chain_approx])
done
lemma approx_approx [simp]:
--- a/src/HOLCF/CompactBasis.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy Thu Jan 17 21:44:19 2008 +0100
@@ -429,7 +429,7 @@
apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
apply (simp add: approx_less compact_le_def)
apply (erule subst, erule subst)
- apply (simp add: monofun_cfun chain_mono3 [OF chain_approx])
+ apply (simp add: monofun_cfun chain_mono [OF chain_approx])
apply (simp add: compact_le_def)
apply (erule (1) trans_less)
done
@@ -493,7 +493,7 @@
"i \<le> j \<Longrightarrow> compact_le (compact_approx i a) (compact_approx j a)"
unfolding compact_le_def
apply (simp add: Rep_compact_approx)
-apply (rule chain_mono3, simp, assumption)
+apply (rule chain_mono, simp, assumption)
done
lemma compact_approx_mono:
--- a/src/HOLCF/FOCUS/Fstream.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/FOCUS/Fstream.thy Thu Jan 17 21:44:19 2008 +0100
@@ -239,7 +239,7 @@
apply (force)
apply (unfold max_in_chain_def)
apply auto
-apply (frule (1) chain_mono3)
+apply (frule (1) chain_mono)
apply (rule_tac x="Y j" in fstream_cases)
apply (force)
apply (drule_tac x="j" in is_ub_thelub)
@@ -254,7 +254,7 @@
apply (rule conjI)
apply (erule chain_shift [THEN chain_monofun])
apply safe
-apply (drule_tac x="j" and y="i+j" in chain_mono3)
+apply (drule_tac i="j" and j="i+j" in chain_mono)
apply (simp)
apply (simp)
apply (rule_tac x="i+j" in exI)
--- a/src/HOLCF/FOCUS/Fstreams.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy Thu Jan 17 21:44:19 2008 +0100
@@ -264,7 +264,7 @@
apply (subgoal_tac "Y ja << (LUB i. (Y i))", clarsimp)
apply (drule fstreams_mono, simp)
apply (rule is_ub_thelub, simp)
-apply (blast intro: chain_mono3)
+apply (blast intro: chain_mono)
by (rule stream_reach2)
@@ -285,7 +285,7 @@
apply (case_tac "Y j", auto)
apply (rule_tac x="j" in exI)
apply (case_tac "Y j",auto)
-by (drule chain_mono3, auto)
+by (drule chain_mono, auto)
lemma fstreams_lub_lemma2:
"[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
@@ -328,7 +328,7 @@
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)
-apply (simp add: chain_mono3)
+apply (simp add: chain_mono)
by (rule stream_reach2)
--- a/src/HOLCF/Pcpo.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/Pcpo.thy Thu Jan 17 21:44:19 2008 +0100
@@ -53,7 +53,7 @@
apply assumption
apply (rule ub_rangeI)
apply (rule_tac y="Y (i + j)" in trans_less)
-apply (erule chain_mono3)
+apply (erule chain_mono)
apply (rule le_add1)
apply (rule is_ub_thelub)
apply (erule chain_shift)
@@ -65,7 +65,7 @@
apply (fast intro!: thelubI lub_finch1)
apply (unfold max_in_chain_def)
apply (safe intro!: antisym_less)
-apply (fast elim!: chain_mono3)
+apply (fast elim!: chain_mono)
apply (drule sym)
apply (force elim!: is_ub_thelub)
done
@@ -147,8 +147,8 @@
apply (rule lub_mono3 [rule_format, OF 2 3])
apply (rule exI)
apply (rule trans_less)
- apply (rule chain_mono3 [OF 1 le_maxI1])
- apply (rule chain_mono3 [OF 2 le_maxI2])
+ apply (rule chain_mono [OF 1 le_maxI1])
+ apply (rule chain_mono [OF 2 le_maxI2])
done
show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
apply (rule lub_mono [rule_format, OF 3 4])
@@ -246,7 +246,7 @@
by (blast intro: UU_I)
lemma chain_mono2: "\<lbrakk>\<exists>j. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>"
-by (blast dest: notUU_I chain_mono)
+by (blast dest: notUU_I chain_mono_less)
subsection {* Chain-finite and flat cpos *}
@@ -298,7 +298,7 @@
apply (erule exE)
apply (rule_tac x="i" in exI)
apply clarify
-apply (blast dest: chain_mono3 ax_flat)
+apply (blast dest: chain_mono ax_flat)
done
text {* flat subclass of chfin; @{text adm_flat} not needed *}
@@ -338,7 +338,7 @@
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)
+apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
done
end
--- a/src/HOLCF/Porder.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/Porder.thy Thu Jan 17 21:44:19 2008 +0100
@@ -168,27 +168,29 @@
definition
-- {* Here we use countable chains and I prefer to code them as functions! *}
chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
- "chain F = (\<forall>i. F i \<sqsubseteq> F (Suc i))"
+ "chain Y = (\<forall>i. Y i \<sqsubseteq> Y (Suc i))"
+
+lemma chainI: "(\<And>i. Y i \<sqsubseteq> Y (Suc i)) \<Longrightarrow> chain Y"
+unfolding chain_def by fast
+
+lemma chainE: "chain Y \<Longrightarrow> Y i \<sqsubseteq> Y (Suc i)"
+unfolding chain_def by fast
text {* chains are monotone functions *}
-lemma chain_mono [rule_format]: "chain F \<Longrightarrow> x < y \<longrightarrow> F x \<sqsubseteq> F y"
-apply (unfold chain_def)
-apply (induct_tac y)
+lemma chain_mono:
+ assumes Y: "chain Y"
+ shows "i \<le> j \<Longrightarrow> Y i \<sqsubseteq> Y j"
+apply (induct j)
apply simp
-apply (blast elim: less_SucE intro: trans_less)
+apply (erule le_SucE)
+apply (rule trans_less [OF _ chainE [OF Y]])
+apply simp
+apply simp
done
-lemma chain_mono3: "\<lbrakk>chain F; x \<le> y\<rbrakk> \<Longrightarrow> F x \<sqsubseteq> F y"
-apply (drule le_imp_less_or_eq)
-apply (blast intro: chain_mono)
-done
-
-lemma chainE: "chain F \<Longrightarrow> F i \<sqsubseteq> F (Suc i)"
-by (unfold chain_def, simp)
-
-lemma chainI: "(\<And>i. F i \<sqsubseteq> F (Suc i)) \<Longrightarrow> chain F"
-by (unfold chain_def, simp)
+lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
+by (erule chain_mono, simp)
lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))"
apply (rule chainI)
@@ -206,7 +208,7 @@
apply (rule iffI)
apply (rule ub_rangeI)
apply (rule_tac y="S (i + j)" in trans_less)
-apply (erule chain_mono3)
+apply (erule chain_mono)
apply (rule le_add1)
apply (erule ub_rangeD)
apply (rule ub_rangeI)
@@ -237,24 +239,23 @@
text {* The range of a chain is a totally ordered *}
-lemma chain_tord: "chain F \<Longrightarrow> tord (range F)"
-apply (unfold tord_def, clarify)
-apply (rule nat_less_cases)
+lemma chain_tord: "chain Y \<Longrightarrow> tord (range Y)"
+unfolding tord_def
+apply (clarify, rename_tac i j)
+apply (rule_tac x=i and y=j in linorder_le_cases)
apply (fast intro: chain_mono)+
done
-lemma finite_tord_has_max [rule_format]:
- "finite S \<Longrightarrow> S \<noteq> {} \<longrightarrow> tord S \<longrightarrow> (\<exists>y\<in>S. \<forall>x\<in>S. x \<sqsubseteq> y)"
- apply (erule finite_induct, simp)
- apply (rename_tac a S, clarify)
- apply (case_tac "S = {}", simp)
- apply (drule (1) mp)
- apply (drule mp, simp add: tord_def)
+lemma finite_tord_has_max:
+ "\<lbrakk>finite S; S \<noteq> {}; tord S\<rbrakk> \<Longrightarrow> \<exists>y\<in>S. \<forall>x\<in>S. x \<sqsubseteq> y"
+ apply (induct S rule: finite_ne_induct)
+ apply simp
+ apply (drule meta_mp, simp add: tord_def)
apply (erule bexE, rename_tac z)
- apply (subgoal_tac "a \<sqsubseteq> z \<or> z \<sqsubseteq> a")
+ apply (subgoal_tac "x \<sqsubseteq> z \<or> z \<sqsubseteq> x")
apply (erule disjE)
apply (rule_tac x="z" in bexI, simp, simp)
- apply (rule_tac x="a" in bexI)
+ apply (rule_tac x="x" in bexI)
apply (clarsimp elim!: rev_trans_less)
apply simp
apply (simp add: tord_def)
@@ -284,7 +285,7 @@
apply (rule ub_rangeI, rename_tac j)
apply (rule_tac x=i and y=j in linorder_le_cases)
apply (drule (1) max_in_chainD, simp)
-apply (erule (1) chain_mono3)
+apply (erule (1) chain_mono)
apply (erule ub_rangeD)
done
@@ -315,7 +316,7 @@
apply (clarsimp, rename_tac i)
apply (subgoal_tac "max_in_chain i Y")
apply (simp add: finite_chain_def exI)
- apply (simp add: max_in_chain_def po_eq_conv chain_mono3)
+ apply (simp add: max_in_chain_def po_eq_conv chain_mono)
apply (erule finite_tord_has_max, simp)
apply (erule chain_tord)
done
@@ -418,7 +419,7 @@
apply (rule_tac x="S 0" in exI, simp)
apply (clarify, rename_tac m n)
apply (rule_tac x="S (max m n)" in bexI)
-apply (simp add: chain_mono3)
+apply (simp add: chain_mono)
apply simp
done
--- a/src/HOLCF/Up.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/Up.thy Thu Jan 17 21:44:19 2008 +0100
@@ -117,7 +117,7 @@
lemma up_lemma2:
"\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
apply (erule contrapos_nn)
-apply (drule_tac x="j" and y="i + j" in chain_mono3)
+apply (drule_tac i="j" and j="i + j" in chain_mono)
apply (rule le_add2)
apply (case_tac "Y j")
apply assumption
--- a/src/HOLCF/ex/Stream.thy Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/ex/Stream.thy Thu Jan 17 21:44:19 2008 +0100
@@ -220,7 +220,7 @@
lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1"
apply (insert chain_stream_take [of s1])
-by (drule chain_mono3,auto)
+by (drule chain_mono,auto)
lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2"
by (simp add: monofun_cfun_arg)