convert lemma lub_mono to rule_format
authorhuffman
Thu Jan 17 21:56:33 2008 +0100 (2008-01-17)
changeset 259235fe4b543512e
parent 25922 cb04d05e95fb
child 25924 f974a1c64348
convert lemma lub_mono to rule_format
src/HOLCF/Adm.thy
src/HOLCF/Bifinite.thy
src/HOLCF/Ffun.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/Pcpo.thy
     1.1 --- a/src/HOLCF/Adm.thy	Thu Jan 17 21:44:19 2008 +0100
     1.2 +++ b/src/HOLCF/Adm.thy	Thu Jan 17 21:56:33 2008 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4      (\<Squnion>i. Y i) = (\<Squnion>i. Y (LEAST j. i \<le> j \<and> P (Y j)))"
     1.5   apply (frule (1) adm_disj_lemma1)
     1.6   apply (rule antisym_less)
     1.7 -  apply (rule lub_mono [rule_format], assumption+)
     1.8 +  apply (rule lub_mono, assumption+)
     1.9    apply (erule chain_mono)
    1.10    apply (simp add: adm_disj_lemma2)
    1.11   apply (rule lub_range_mono, fast, assumption+)
    1.12 @@ -128,7 +128,7 @@
    1.13  apply (rule lub_mono)
    1.14  apply (erule (1) ch2ch_cont)
    1.15  apply (erule (1) ch2ch_cont)
    1.16 -apply assumption
    1.17 +apply (erule spec)
    1.18  done
    1.19  
    1.20  lemma adm_eq: "\<lbrakk>cont u; cont v\<rbrakk> \<Longrightarrow> adm (\<lambda>x. u x = v x)"
     2.1 --- a/src/HOLCF/Bifinite.thy	Thu Jan 17 21:44:19 2008 +0100
     2.2 +++ b/src/HOLCF/Bifinite.thy	Thu Jan 17 21:56:33 2008 +0100
     2.3 @@ -153,7 +153,7 @@
     2.4    fixes x y :: "'a::bifinite_cpo"
     2.5    shows "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
     2.6  apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
     2.7 -apply (rule lub_mono [rule_format], simp, simp, simp)
     2.8 +apply (rule lub_mono, simp, simp, simp)
     2.9  done
    2.10  
    2.11  subsection {* Instance for continuous function space *}
     3.1 --- a/src/HOLCF/Ffun.thy	Thu Jan 17 21:44:19 2008 +0100
     3.2 +++ b/src/HOLCF/Ffun.thy	Thu Jan 17 21:56:33 2008 +0100
     3.3 @@ -179,7 +179,7 @@
     3.4      \<Longrightarrow> monofun (\<Squnion>i. F i)"
     3.5  apply (rule monofunI)
     3.6  apply (simp add: thelub_fun)
     3.7 -apply (rule lub_mono [rule_format])
     3.8 +apply (rule lub_mono)
     3.9  apply (erule ch2ch_fun)
    3.10  apply (erule ch2ch_fun)
    3.11  apply (simp add: monofunE)
     4.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Jan 17 21:44:19 2008 +0100
     4.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Jan 17 21:56:33 2008 +0100
     4.3 @@ -916,7 +916,6 @@
     4.4  apply (rule lub_mono)
     4.5  apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
     4.6  apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
     4.7 -apply (rule allI)
     4.8  apply (rule prems [unfolded seq.take_def])
     4.9  done
    4.10  
     5.1 --- a/src/HOLCF/Pcpo.thy	Thu Jan 17 21:44:19 2008 +0100
     5.2 +++ b/src/HOLCF/Pcpo.thy	Thu Jan 17 21:56:33 2008 +0100
     5.3 @@ -73,12 +73,12 @@
     5.4  text {* the @{text "\<sqsubseteq>"} relation between two chains is preserved by their lubs *}
     5.5  
     5.6  lemma lub_mono:
     5.7 -  "\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<forall>k. X k \<sqsubseteq> Y k\<rbrakk> 
     5.8 +  "\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk> 
     5.9      \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
    5.10  apply (erule is_lub_thelub)
    5.11  apply (rule ub_rangeI)
    5.12  apply (rule trans_less)
    5.13 -apply (erule spec)
    5.14 +apply (erule meta_spec)
    5.15  apply (erule is_ub_thelub)
    5.16  done
    5.17  
    5.18 @@ -123,7 +123,7 @@
    5.19    assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
    5.20    shows "chain (\<lambda>i. \<Squnion>j. Y i j)"
    5.21  apply (rule chainI)
    5.22 -apply (rule lub_mono [rule_format, OF 2 2])
    5.23 +apply (rule lub_mono [OF 2 2])
    5.24  apply (rule chainE [OF 1])
    5.25  done
    5.26  
    5.27 @@ -151,7 +151,7 @@
    5.28      apply (rule chain_mono [OF 2 le_maxI2])
    5.29      done
    5.30    show "(\<Squnion>i. Y i i) \<sqsubseteq> (\<Squnion>i. \<Squnion>j. Y i j)"
    5.31 -    apply (rule lub_mono [rule_format, OF 3 4])
    5.32 +    apply (rule lub_mono [OF 3 4])
    5.33      apply (rule is_ub_thelub [OF 2])
    5.34      done
    5.35  qed