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)