# HG changeset patch
# User huffman
# Date 1200602659 -3600
# Node ID cb04d05e95fb454d92e61315890fdea0395e3a96
# Parent  0ca392ab7f37ee02b71f9e99d711662eb023d9cb
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less

diff -r 0ca392ab7f37 -r cb04d05e95fb src/HOLCF/Adm.thy
--- 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
 
diff -r 0ca392ab7f37 -r cb04d05e95fb src/HOLCF/Bifinite.thy
--- 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]:
diff -r 0ca392ab7f37 -r cb04d05e95fb src/HOLCF/CompactBasis.thy
--- 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:
diff -r 0ca392ab7f37 -r cb04d05e95fb src/HOLCF/FOCUS/Fstream.thy
--- 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)
diff -r 0ca392ab7f37 -r cb04d05e95fb src/HOLCF/FOCUS/Fstreams.thy
--- 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)
 
 
diff -r 0ca392ab7f37 -r cb04d05e95fb src/HOLCF/Pcpo.thy
--- 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
diff -r 0ca392ab7f37 -r cb04d05e95fb src/HOLCF/Porder.thy
--- 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
 
diff -r 0ca392ab7f37 -r cb04d05e95fb src/HOLCF/Up.thy
--- 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
diff -r 0ca392ab7f37 -r cb04d05e95fb src/HOLCF/ex/Stream.thy
--- 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)