change lemma admD to rule_format
authorhuffman
Fri Jan 18 20:22:07 2008 +0100 (2008-01-18)
changeset 259253dc4acca4388
parent 25924 f974a1c64348
child 25926 aa0eca1ccb19
change lemma admD to rule_format
src/HOLCF/Adm.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/Fix.thy
src/HOLCF/LowerPD.thy
src/HOLCF/Pcpodef.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/src/HOLCF/Adm.thy	Fri Jan 18 08:30:12 2008 +0100
     1.2 +++ b/src/HOLCF/Adm.thy	Fri Jan 18 20:22:07 2008 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4     "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
     1.5  unfolding adm_def by fast
     1.6  
     1.7 -lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
     1.8 +lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
     1.9  unfolding adm_def by fast
    1.10  
    1.11  lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
    1.12 @@ -50,7 +50,7 @@
    1.13  by (rule admI, simp)
    1.14  
    1.15  lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
    1.16 -by (fast elim: admD intro: admI)
    1.17 +by (fast intro: admI elim: admD)
    1.18  
    1.19  lemma adm_all: "(\<And>y. adm (P y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)"
    1.20  by (fast intro: admI elim: admD)
    1.21 @@ -139,7 +139,7 @@
    1.22  apply (simp add: cont2contlubE)
    1.23  apply (erule admD)
    1.24  apply (erule (1) ch2ch_cont)
    1.25 -apply assumption
    1.26 +apply (erule spec)
    1.27  done
    1.28  
    1.29  lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
     2.1 --- a/src/HOLCF/CompactBasis.thy	Fri Jan 18 08:30:12 2008 +0100
     2.2 +++ b/src/HOLCF/CompactBasis.thy	Fri Jan 18 20:22:07 2008 +0100
     2.3 @@ -340,7 +340,7 @@
     2.4    shows "P x"
     2.5   apply (subgoal_tac "P (\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x)")
     2.6   apply (simp add: lub_basis_fun_take)
     2.7 - apply (rule admD [rule_format, OF adm])
     2.8 + apply (rule admD [OF adm])
     2.9    apply (simp add: chain_basis_fun_take)
    2.10   apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
    2.11   apply (clarify, simp add: P)
    2.12 @@ -452,7 +452,7 @@
    2.13  
    2.14  lemma compacts_lessD: "compacts x \<subseteq> compacts y \<Longrightarrow> x \<sqsubseteq> y"
    2.15  apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
    2.16 -apply (rule admD [rule_format], simp, simp)
    2.17 +apply (rule admD, simp, simp)
    2.18  apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
    2.19  apply (simp add: compacts_def Abs_compact_basis_inverse approx_less)
    2.20  apply (simp add: compacts_def Abs_compact_basis_inverse)
     3.1 --- a/src/HOLCF/ConvexPD.thy	Fri Jan 18 08:30:12 2008 +0100
     3.2 +++ b/src/HOLCF/ConvexPD.thy	Fri Jan 18 20:22:07 2008 +0100
     3.3 @@ -372,7 +372,7 @@
     3.4   apply (rule iffI)
     3.5    apply (subgoal_tac
     3.6      "adm (\<lambda>f. f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
     3.7 -   apply (drule admD [rule_format], rule chain_approx)
     3.8 +   apply (drule admD, rule chain_approx)
     3.9      apply (drule_tac f="approx i" in monofun_cfun_arg)
    3.10      apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
    3.11      apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
    3.12 @@ -391,7 +391,7 @@
    3.13   apply (rule iffI)
    3.14    apply (subgoal_tac
    3.15      "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z) \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z))")
    3.16 -   apply (drule admD [rule_format], rule chain_approx)
    3.17 +   apply (drule admD, rule chain_approx)
    3.18      apply (drule_tac f="approx i" in monofun_cfun_arg)
    3.19      apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
    3.20      apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
     4.1 --- a/src/HOLCF/Fix.thy	Fri Jan 18 08:30:12 2008 +0100
     4.2 +++ b/src/HOLCF/Fix.thy	Fri Jan 18 20:22:07 2008 +0100
     4.3 @@ -153,7 +153,7 @@
     4.4  
     4.5  lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
     4.6  apply (subst fix_def2)
     4.7 -apply (erule admD [rule_format])
     4.8 +apply (erule admD)
     4.9  apply (rule chain_iterate)
    4.10  apply (induct_tac "i", simp_all)
    4.11  done
    4.12 @@ -233,7 +233,7 @@
    4.13  apply (intro strip)
    4.14  apply (erule admD)
    4.15  apply (rule chain_iterate)
    4.16 -apply assumption
    4.17 +apply (erule spec)
    4.18  done
    4.19  
    4.20  text {* computational induction for weak admissible formulae *}
     5.1 --- a/src/HOLCF/LowerPD.thy	Fri Jan 18 08:30:12 2008 +0100
     5.2 +++ b/src/HOLCF/LowerPD.thy	Fri Jan 18 20:22:07 2008 +0100
     5.3 @@ -376,7 +376,7 @@
     5.4   apply (rule iffI)
     5.5    apply (subgoal_tac
     5.6      "adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
     5.7 -   apply (drule admD [rule_format], rule chain_approx)
     5.8 +   apply (drule admD, rule chain_approx)
     5.9      apply (drule_tac f="approx i" in monofun_cfun_arg)
    5.10      apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
    5.11      apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_lower_principal, simp)
     6.1 --- a/src/HOLCF/Pcpodef.thy	Fri Jan 18 08:30:12 2008 +0100
     6.2 +++ b/src/HOLCF/Pcpodef.thy	Fri Jan 18 20:22:07 2008 +0100
     6.3 @@ -104,7 +104,7 @@
     6.4      and adm:  "adm (\<lambda>x. x \<in> A)"
     6.5    shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
     6.6   apply (rule type_definition.Abs_inverse [OF type])
     6.7 - apply (erule admD [OF adm ch2ch_Rep [OF less], rule_format])
     6.8 + apply (erule admD [OF adm ch2ch_Rep [OF less]])
     6.9   apply (rule type_definition.Rep [OF type])
    6.10  done
    6.11  
     7.1 --- a/src/HOLCF/UpperPD.thy	Fri Jan 18 08:30:12 2008 +0100
     7.2 +++ b/src/HOLCF/UpperPD.thy	Fri Jan 18 20:22:07 2008 +0100
     7.3 @@ -346,7 +346,7 @@
     7.4   apply (rule iffI)
     7.5    apply (subgoal_tac
     7.6      "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z) \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z))")
     7.7 -   apply (drule admD [rule_format], rule chain_approx)
     7.8 +   apply (drule admD, rule chain_approx)
     7.9      apply (drule_tac f="approx i" in monofun_cfun_arg)
    7.10      apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
    7.11      apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_upper_principal, simp)