rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
authorhuffman
Thu Jan 17 21:44:19 2008 +0100 (2008-01-17)
changeset 25922cb04d05e95fb
parent 25921 0ca392ab7f37
child 25923 5fe4b543512e
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
src/HOLCF/Adm.thy
src/HOLCF/Bifinite.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/FOCUS/Fstreams.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.thy
src/HOLCF/Up.thy
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOLCF/Adm.thy	Thu Jan 17 00:51:20 2008 +0100
     1.2 +++ b/src/HOLCF/Adm.thy	Thu Jan 17 21:44:19 2008 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4    "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j)\<rbrakk>
     1.5      \<Longrightarrow> chain (\<lambda>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
     1.6  apply (rule chainI)
     1.7 -apply (erule chain_mono3)
     1.8 +apply (erule chain_mono)
     1.9  apply (rule Least_le)
    1.10  apply (rule LeastI2_ex)
    1.11  apply simp_all
    1.12 @@ -78,7 +78,7 @@
    1.13   apply (frule (1) adm_disj_lemma1)
    1.14   apply (rule antisym_less)
    1.15    apply (rule lub_mono [rule_format], assumption+)
    1.16 -  apply (erule chain_mono3)
    1.17 +  apply (erule chain_mono)
    1.18    apply (simp add: adm_disj_lemma2)
    1.19   apply (rule lub_range_mono, fast, assumption+)
    1.20  done
    1.21 @@ -180,7 +180,7 @@
    1.22  apply (erule exE, rule_tac x=i in exI)
    1.23  apply (rule max_in_chainI)
    1.24  apply (rule antisym_less)
    1.25 -apply (erule (1) chain_mono3)
    1.26 +apply (erule (1) chain_mono)
    1.27  apply (erule (1) trans_less [OF is_ub_thelub])
    1.28  done
    1.29  
     2.1 --- a/src/HOLCF/Bifinite.thy	Thu Jan 17 00:51:20 2008 +0100
     2.2 +++ b/src/HOLCF/Bifinite.thy	Thu Jan 17 21:44:19 2008 +0100
     2.3 @@ -56,7 +56,7 @@
     2.4  apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
     2.5  apply (rule monofun_cfun_arg)
     2.6  apply (rule monofun_cfun_fun)
     2.7 -apply (erule chain_mono3 [OF chain_approx])
     2.8 +apply (erule chain_mono [OF chain_approx])
     2.9  done
    2.10  
    2.11  lemma approx_approx2:
    2.12 @@ -65,7 +65,7 @@
    2.13  apply (rule approx_less)
    2.14  apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
    2.15  apply (rule monofun_cfun_fun)
    2.16 -apply (erule chain_mono3 [OF chain_approx])
    2.17 +apply (erule chain_mono [OF chain_approx])
    2.18  done
    2.19  
    2.20  lemma approx_approx [simp]:
     3.1 --- a/src/HOLCF/CompactBasis.thy	Thu Jan 17 00:51:20 2008 +0100
     3.2 +++ b/src/HOLCF/CompactBasis.thy	Thu Jan 17 21:44:19 2008 +0100
     3.3 @@ -429,7 +429,7 @@
     3.4    apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
     3.5    apply (simp add: approx_less compact_le_def)
     3.6    apply (erule subst, erule subst)
     3.7 -  apply (simp add: monofun_cfun chain_mono3 [OF chain_approx])
     3.8 +  apply (simp add: monofun_cfun chain_mono [OF chain_approx])
     3.9   apply (simp add: compact_le_def)
    3.10   apply (erule (1) trans_less)
    3.11  done
    3.12 @@ -493,7 +493,7 @@
    3.13    "i \<le> j \<Longrightarrow> compact_le (compact_approx i a) (compact_approx j a)"
    3.14  unfolding compact_le_def
    3.15  apply (simp add: Rep_compact_approx)
    3.16 -apply (rule chain_mono3, simp, assumption)
    3.17 +apply (rule chain_mono, simp, assumption)
    3.18  done
    3.19  
    3.20  lemma compact_approx_mono:
     4.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Thu Jan 17 00:51:20 2008 +0100
     4.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Thu Jan 17 21:44:19 2008 +0100
     4.3 @@ -239,7 +239,7 @@
     4.4  apply  (force)
     4.5  apply (unfold max_in_chain_def)
     4.6  apply auto
     4.7 -apply (frule (1) chain_mono3)
     4.8 +apply (frule (1) chain_mono)
     4.9  apply (rule_tac x="Y j" in fstream_cases)
    4.10  apply  (force)
    4.11  apply (drule_tac x="j" in is_ub_thelub)
    4.12 @@ -254,7 +254,7 @@
    4.13  apply (rule conjI)
    4.14  apply  (erule chain_shift [THEN chain_monofun])
    4.15  apply safe
    4.16 -apply  (drule_tac x="j" and y="i+j" in chain_mono3)
    4.17 +apply  (drule_tac i="j" and j="i+j" in chain_mono)
    4.18  apply   (simp)
    4.19  apply  (simp)
    4.20  apply  (rule_tac x="i+j" in exI)
     5.1 --- a/src/HOLCF/FOCUS/Fstreams.thy	Thu Jan 17 00:51:20 2008 +0100
     5.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Thu Jan 17 21:44:19 2008 +0100
     5.3 @@ -264,7 +264,7 @@
     5.4  apply (subgoal_tac "Y ja << (LUB i. (Y i))", clarsimp)
     5.5  apply (drule fstreams_mono, simp)
     5.6  apply (rule is_ub_thelub, simp)
     5.7 -apply (blast intro: chain_mono3)
     5.8 +apply (blast intro: chain_mono)
     5.9  by (rule stream_reach2)
    5.10  
    5.11  
    5.12 @@ -285,7 +285,7 @@
    5.13  apply (case_tac "Y j", auto)
    5.14  apply (rule_tac x="j" in exI)
    5.15  apply (case_tac "Y j",auto)
    5.16 -by (drule chain_mono3, auto)
    5.17 +by (drule chain_mono, auto)
    5.18  
    5.19  lemma fstreams_lub_lemma2: 
    5.20    "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
    5.21 @@ -328,7 +328,7 @@
    5.22  apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp)
    5.23  apply (drule ax_flat, simp)+
    5.24  apply (drule prod_eqI, auto)
    5.25 -apply (simp add: chain_mono3)
    5.26 +apply (simp add: chain_mono)
    5.27  by (rule stream_reach2)
    5.28  
    5.29  
     6.1 --- a/src/HOLCF/Pcpo.thy	Thu Jan 17 00:51:20 2008 +0100
     6.2 +++ b/src/HOLCF/Pcpo.thy	Thu Jan 17 21:44:19 2008 +0100
     6.3 @@ -53,7 +53,7 @@
     6.4  apply assumption
     6.5  apply (rule ub_rangeI)
     6.6  apply (rule_tac y="Y (i + j)" in trans_less)
     6.7 -apply (erule chain_mono3)
     6.8 +apply (erule chain_mono)
     6.9  apply (rule le_add1)
    6.10  apply (rule is_ub_thelub)
    6.11  apply (erule chain_shift)
    6.12 @@ -65,7 +65,7 @@
    6.13  apply (fast intro!: thelubI lub_finch1)
    6.14  apply (unfold max_in_chain_def)
    6.15  apply (safe intro!: antisym_less)
    6.16 -apply (fast elim!: chain_mono3)
    6.17 +apply (fast elim!: chain_mono)
    6.18  apply (drule sym)
    6.19  apply (force elim!: is_ub_thelub)
    6.20  done
    6.21 @@ -147,8 +147,8 @@
    6.22      apply (rule lub_mono3 [rule_format, OF 2 3])
    6.23      apply (rule exI)
    6.24      apply (rule trans_less)
    6.25 -    apply (rule chain_mono3 [OF 1 le_maxI1])
    6.26 -    apply (rule chain_mono3 [OF 2 le_maxI2])
    6.27 +    apply (rule chain_mono [OF 1 le_maxI1])
    6.28 +    apply (rule chain_mono [OF 2 le_maxI2])
    6.29      done
    6.30    show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
    6.31      apply (rule lub_mono [rule_format, OF 3 4])
    6.32 @@ -246,7 +246,7 @@
    6.33  by (blast intro: UU_I)
    6.34  
    6.35  lemma chain_mono2: "\<lbrakk>\<exists>j. Y j \<noteq> \<bottom>; chain Y\<rbrakk> \<Longrightarrow> \<exists>j. \<forall>i>j. Y i \<noteq> \<bottom>"
    6.36 -by (blast dest: notUU_I chain_mono)
    6.37 +by (blast dest: notUU_I chain_mono_less)
    6.38  
    6.39  subsection {* Chain-finite and flat cpos *}
    6.40  
    6.41 @@ -298,7 +298,7 @@
    6.42  apply (erule exE)
    6.43  apply (rule_tac x="i" in exI)
    6.44  apply clarify
    6.45 -apply (blast dest: chain_mono3 ax_flat)
    6.46 +apply (blast dest: chain_mono ax_flat)
    6.47  done
    6.48  
    6.49  text {* flat subclass of chfin; @{text adm_flat} not needed *}
    6.50 @@ -338,7 +338,7 @@
    6.51  apply (erule thin_rl)
    6.52  apply (unfold finite_chain_def)
    6.53  apply (unfold max_in_chain_def)
    6.54 -apply (fast dest: le_imp_less_or_eq elim: chain_mono)
    6.55 +apply (fast dest: le_imp_less_or_eq elim: chain_mono_less)
    6.56  done
    6.57  
    6.58  end
     7.1 --- a/src/HOLCF/Porder.thy	Thu Jan 17 00:51:20 2008 +0100
     7.2 +++ b/src/HOLCF/Porder.thy	Thu Jan 17 21:44:19 2008 +0100
     7.3 @@ -168,27 +168,29 @@
     7.4  definition
     7.5    -- {* Here we use countable chains and I prefer to code them as functions! *}
     7.6    chain :: "(nat \<Rightarrow> 'a::po) \<Rightarrow> bool" where
     7.7 -  "chain F = (\<forall>i. F i \<sqsubseteq> F (Suc i))"
     7.8 +  "chain Y = (\<forall>i. Y i \<sqsubseteq> Y (Suc i))"
     7.9 +
    7.10 +lemma chainI: "(\<And>i. Y i \<sqsubseteq> Y (Suc i)) \<Longrightarrow> chain Y"
    7.11 +unfolding chain_def by fast
    7.12 +
    7.13 +lemma chainE: "chain Y \<Longrightarrow> Y i \<sqsubseteq> Y (Suc i)"
    7.14 +unfolding chain_def by fast
    7.15  
    7.16  text {* chains are monotone functions *}
    7.17  
    7.18 -lemma chain_mono [rule_format]: "chain F \<Longrightarrow> x < y \<longrightarrow> F x \<sqsubseteq> F y"
    7.19 -apply (unfold chain_def)
    7.20 -apply (induct_tac y)
    7.21 +lemma chain_mono:
    7.22 +  assumes Y: "chain Y"
    7.23 +  shows "i \<le> j \<Longrightarrow> Y i \<sqsubseteq> Y j"
    7.24 +apply (induct j)
    7.25  apply simp
    7.26 -apply (blast elim: less_SucE intro: trans_less)
    7.27 +apply (erule le_SucE)
    7.28 +apply (rule trans_less [OF _ chainE [OF Y]])
    7.29 +apply simp
    7.30 +apply simp
    7.31  done
    7.32  
    7.33 -lemma chain_mono3: "\<lbrakk>chain F; x \<le> y\<rbrakk> \<Longrightarrow> F x \<sqsubseteq> F y"
    7.34 -apply (drule le_imp_less_or_eq)
    7.35 -apply (blast intro: chain_mono)
    7.36 -done
    7.37 -
    7.38 -lemma chainE: "chain F \<Longrightarrow> F i \<sqsubseteq> F (Suc i)"
    7.39 -by (unfold chain_def, simp)
    7.40 -
    7.41 -lemma chainI: "(\<And>i. F i \<sqsubseteq> F (Suc i)) \<Longrightarrow> chain F"
    7.42 -by (unfold chain_def, simp)
    7.43 +lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
    7.44 +by (erule chain_mono, simp)
    7.45  
    7.46  lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))"
    7.47  apply (rule chainI)
    7.48 @@ -206,7 +208,7 @@
    7.49  apply (rule iffI)
    7.50  apply (rule ub_rangeI)
    7.51  apply (rule_tac y="S (i + j)" in trans_less)
    7.52 -apply (erule chain_mono3)
    7.53 +apply (erule chain_mono)
    7.54  apply (rule le_add1)
    7.55  apply (erule ub_rangeD)
    7.56  apply (rule ub_rangeI)
    7.57 @@ -237,24 +239,23 @@
    7.58  
    7.59  text {* The range of a chain is a totally ordered *}
    7.60  
    7.61 -lemma chain_tord: "chain F \<Longrightarrow> tord (range F)"
    7.62 -apply (unfold tord_def, clarify)
    7.63 -apply (rule nat_less_cases)
    7.64 +lemma chain_tord: "chain Y \<Longrightarrow> tord (range Y)"
    7.65 +unfolding tord_def
    7.66 +apply (clarify, rename_tac i j)
    7.67 +apply (rule_tac x=i and y=j in linorder_le_cases)
    7.68  apply (fast intro: chain_mono)+
    7.69  done
    7.70  
    7.71 -lemma finite_tord_has_max [rule_format]:
    7.72 -  "finite S \<Longrightarrow> S \<noteq> {} \<longrightarrow> tord S \<longrightarrow> (\<exists>y\<in>S. \<forall>x\<in>S. x \<sqsubseteq> y)"
    7.73 - apply (erule finite_induct, simp)
    7.74 - apply (rename_tac a S, clarify)
    7.75 - apply (case_tac "S = {}", simp)
    7.76 - apply (drule (1) mp)
    7.77 - apply (drule mp, simp add: tord_def)
    7.78 +lemma finite_tord_has_max:
    7.79 +  "\<lbrakk>finite S; S \<noteq> {}; tord S\<rbrakk> \<Longrightarrow> \<exists>y\<in>S. \<forall>x\<in>S. x \<sqsubseteq> y"
    7.80 + apply (induct S rule: finite_ne_induct)
    7.81 +  apply simp
    7.82 + apply (drule meta_mp, simp add: tord_def)
    7.83   apply (erule bexE, rename_tac z)
    7.84 - apply (subgoal_tac "a \<sqsubseteq> z \<or> z \<sqsubseteq> a")
    7.85 + apply (subgoal_tac "x \<sqsubseteq> z \<or> z \<sqsubseteq> x")
    7.86    apply (erule disjE)
    7.87     apply (rule_tac x="z" in bexI, simp, simp)
    7.88 -  apply (rule_tac x="a" in bexI)
    7.89 +  apply (rule_tac x="x" in bexI)
    7.90     apply (clarsimp elim!: rev_trans_less)
    7.91    apply simp
    7.92   apply (simp add: tord_def)
    7.93 @@ -284,7 +285,7 @@
    7.94  apply (rule ub_rangeI, rename_tac j)
    7.95  apply (rule_tac x=i and y=j in linorder_le_cases)
    7.96  apply (drule (1) max_in_chainD, simp)
    7.97 -apply (erule (1) chain_mono3)
    7.98 +apply (erule (1) chain_mono)
    7.99  apply (erule ub_rangeD)
   7.100  done
   7.101  
   7.102 @@ -315,7 +316,7 @@
   7.103    apply (clarsimp, rename_tac i)
   7.104    apply (subgoal_tac "max_in_chain i Y")
   7.105     apply (simp add: finite_chain_def exI)
   7.106 -  apply (simp add: max_in_chain_def po_eq_conv chain_mono3)
   7.107 +  apply (simp add: max_in_chain_def po_eq_conv chain_mono)
   7.108   apply (erule finite_tord_has_max, simp)
   7.109   apply (erule chain_tord)
   7.110  done
   7.111 @@ -418,7 +419,7 @@
   7.112  apply (rule_tac x="S 0" in exI, simp)
   7.113  apply (clarify, rename_tac m n)
   7.114  apply (rule_tac x="S (max m n)" in bexI)
   7.115 -apply (simp add: chain_mono3)
   7.116 +apply (simp add: chain_mono)
   7.117  apply simp
   7.118  done
   7.119  
     8.1 --- a/src/HOLCF/Up.thy	Thu Jan 17 00:51:20 2008 +0100
     8.2 +++ b/src/HOLCF/Up.thy	Thu Jan 17 21:44:19 2008 +0100
     8.3 @@ -117,7 +117,7 @@
     8.4  lemma up_lemma2:
     8.5    "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
     8.6  apply (erule contrapos_nn)
     8.7 -apply (drule_tac x="j" and y="i + j" in chain_mono3)
     8.8 +apply (drule_tac i="j" and j="i + j" in chain_mono)
     8.9  apply (rule le_add2)
    8.10  apply (case_tac "Y j")
    8.11  apply assumption
     9.1 --- a/src/HOLCF/ex/Stream.thy	Thu Jan 17 00:51:20 2008 +0100
     9.2 +++ b/src/HOLCF/ex/Stream.thy	Thu Jan 17 21:44:19 2008 +0100
     9.3 @@ -220,7 +220,7 @@
     9.4  
     9.5  lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1"
     9.6  apply (insert chain_stream_take [of s1])
     9.7 -by (drule chain_mono3,auto)
     9.8 +by (drule chain_mono,auto)
     9.9  
    9.10  lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2"
    9.11  by (simp add: monofun_cfun_arg)