# HG changeset patch
# User huffman
# Date 1200684127 -3600
# Node ID 3dc4acca43887a61fb2ed99150df4b01ab04fcd6
# Parent  f974a1c64348aedb51a53e8dc03d0a18e97504e7
change lemma admD to rule_format

diff -r f974a1c64348 -r 3dc4acca4388 src/HOLCF/Adm.thy
--- a/src/HOLCF/Adm.thy	Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/Adm.thy	Fri Jan 18 20:22:07 2008 +0100
@@ -21,7 +21,7 @@
    "(\<And>Y. \<lbrakk>chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)) \<Longrightarrow> adm P"
 unfolding adm_def by fast
 
-lemma admD: "\<lbrakk>adm P; chain Y; \<forall>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
+lemma admD: "\<lbrakk>adm P; chain Y; \<And>i. P (Y i)\<rbrakk> \<Longrightarrow> P (\<Squnion>i. Y i)"
 unfolding adm_def by fast
 
 lemma triv_admI: "\<forall>x. P x \<Longrightarrow> adm P"
@@ -50,7 +50,7 @@
 by (rule admI, simp)
 
 lemma adm_conj: "\<lbrakk>adm P; adm Q\<rbrakk> \<Longrightarrow> adm (\<lambda>x. P x \<and> Q x)"
-by (fast elim: admD intro: admI)
+by (fast intro: admI elim: admD)
 
 lemma adm_all: "(\<And>y. adm (P y)) \<Longrightarrow> adm (\<lambda>x. \<forall>y. P y x)"
 by (fast intro: admI elim: admD)
@@ -139,7 +139,7 @@
 apply (simp add: cont2contlubE)
 apply (erule admD)
 apply (erule (1) ch2ch_cont)
-apply assumption
+apply (erule spec)
 done
 
 lemma adm_not_less: "cont t \<Longrightarrow> adm (\<lambda>x. \<not> t x \<sqsubseteq> u)"
diff -r f974a1c64348 -r 3dc4acca4388 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/CompactBasis.thy	Fri Jan 18 20:22:07 2008 +0100
@@ -340,7 +340,7 @@
   shows "P x"
  apply (subgoal_tac "P (\<Squnion>i. basis_fun (\<lambda>a. principal (take i a))\<cdot>x)")
  apply (simp add: lub_basis_fun_take)
- apply (rule admD [rule_format, OF adm])
+ apply (rule admD [OF adm])
   apply (simp add: chain_basis_fun_take)
  apply (cut_tac x=x and i=i in basis_fun_take_eq_principal)
  apply (clarify, simp add: P)
@@ -452,7 +452,7 @@
 
 lemma compacts_lessD: "compacts x \<subseteq> compacts y \<Longrightarrow> x \<sqsubseteq> y"
 apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
-apply (rule admD [rule_format], simp, simp)
+apply (rule admD, simp, simp)
 apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
 apply (simp add: compacts_def Abs_compact_basis_inverse approx_less)
 apply (simp add: compacts_def Abs_compact_basis_inverse)
diff -r f974a1c64348 -r 3dc4acca4388 src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/ConvexPD.thy	Fri Jan 18 20:22:07 2008 +0100
@@ -372,7 +372,7 @@
  apply (rule iffI)
   apply (subgoal_tac
     "adm (\<lambda>f. f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>(convex_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
-   apply (drule admD [rule_format], rule chain_approx)
+   apply (drule admD, rule chain_approx)
     apply (drule_tac f="approx i" in monofun_cfun_arg)
     apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
     apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
@@ -391,7 +391,7 @@
  apply (rule iffI)
   apply (subgoal_tac
     "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z) \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>(convex_unit\<cdot>z))")
-   apply (drule admD [rule_format], rule chain_approx)
+   apply (drule admD, rule chain_approx)
     apply (drule_tac f="approx i" in monofun_cfun_arg)
     apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_convex_principal, simp)
     apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_convex_principal, simp)
diff -r f974a1c64348 -r 3dc4acca4388 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/Fix.thy	Fri Jan 18 20:22:07 2008 +0100
@@ -153,7 +153,7 @@
 
 lemma fix_ind: "\<lbrakk>adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F\<cdot>x)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
 apply (subst fix_def2)
-apply (erule admD [rule_format])
+apply (erule admD)
 apply (rule chain_iterate)
 apply (induct_tac "i", simp_all)
 done
@@ -233,7 +233,7 @@
 apply (intro strip)
 apply (erule admD)
 apply (rule chain_iterate)
-apply assumption
+apply (erule spec)
 done
 
 text {* computational induction for weak admissible formulae *}
diff -r f974a1c64348 -r 3dc4acca4388 src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/LowerPD.thy	Fri Jan 18 20:22:07 2008 +0100
@@ -376,7 +376,7 @@
  apply (rule iffI)
   apply (subgoal_tac
     "adm (\<lambda>f. f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>(lower_unit\<cdot>x) \<sqsubseteq> f\<cdot>zs)")
-   apply (drule admD [rule_format], rule chain_approx)
+   apply (drule admD, rule chain_approx)
     apply (drule_tac f="approx i" in monofun_cfun_arg)
     apply (cut_tac x="approx i\<cdot>x" in compact_imp_Rep_compact_basis, simp)
     apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_lower_principal, simp)
diff -r f974a1c64348 -r 3dc4acca4388 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/Pcpodef.thy	Fri Jan 18 20:22:07 2008 +0100
@@ -104,7 +104,7 @@
     and adm:  "adm (\<lambda>x. x \<in> A)"
   shows "chain S \<Longrightarrow> Rep (Abs (\<Squnion>i. Rep (S i))) = (\<Squnion>i. Rep (S i))"
  apply (rule type_definition.Abs_inverse [OF type])
- apply (erule admD [OF adm ch2ch_Rep [OF less], rule_format])
+ apply (erule admD [OF adm ch2ch_Rep [OF less]])
  apply (rule type_definition.Rep [OF type])
 done
 
diff -r f974a1c64348 -r 3dc4acca4388 src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Fri Jan 18 08:30:12 2008 +0100
+++ b/src/HOLCF/UpperPD.thy	Fri Jan 18 20:22:07 2008 +0100
@@ -346,7 +346,7 @@
  apply (rule iffI)
   apply (subgoal_tac
     "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z) \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>(upper_unit\<cdot>z))")
-   apply (drule admD [rule_format], rule chain_approx)
+   apply (drule admD, rule chain_approx)
     apply (drule_tac f="approx i" in monofun_cfun_arg)
     apply (cut_tac xs="approx i\<cdot>xs" in compact_imp_upper_principal, simp)
     apply (cut_tac xs="approx i\<cdot>ys" in compact_imp_upper_principal, simp)