--- a/src/HOLCF/Cfun.thy Tue Jan 15 16:19:23 2008 +0100
+++ b/src/HOLCF/Cfun.thy Wed Jan 16 22:41:49 2008 +0100
@@ -414,7 +414,7 @@
\<Longrightarrow> \<forall>x y::'b. x \<sqsubseteq> y \<longrightarrow> x = \<bottom> \<or> x = y"
apply clarify
apply (drule_tac f=g in monofun_cfun_arg)
-apply (drule ax_flat [rule_format])
+apply (drule ax_flat)
apply (erule disjE)
apply (simp add: injection_defined_rev)
apply (simp add: injection_eq)
@@ -423,7 +423,7 @@
text {* a result about functions with flat codomain *}
lemma flat_eqI: "\<lbrakk>(x::'a::flat) \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> x = y"
-by (drule ax_flat [rule_format], simp)
+by (drule ax_flat, simp)
lemma flat_codom:
"f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
--- a/src/HOLCF/Cont.thy Tue Jan 15 16:19:23 2008 +0100
+++ b/src/HOLCF/Cont.thy Wed Jan 16 22:41:49 2008 +0100
@@ -222,7 +222,7 @@
lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
apply (rule monofunI)
-apply (drule ax_flat [rule_format])
+apply (drule ax_flat)
apply auto
done
--- a/src/HOLCF/FOCUS/Fstreams.thy Tue Jan 15 16:19:23 2008 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy Wed Jan 16 22:41:49 2008 +0100
@@ -180,7 +180,7 @@
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (simp add: fsingleton_def2, auto)
apply (auto simp add: stream.inverts)
-apply (drule ax_flat [rule_format], simp)
+apply (drule ax_flat, simp)
by (erule sconc_mono)
lemma ft_fstreams[simp]: "ft$(<a> ooo s) = Def a"
@@ -280,7 +280,7 @@
apply (simp add: max_in_chain_def, auto)
apply (subgoal_tac "Y i << Y j",auto)
apply (simp add: less_cprod_def, clarsimp)
-apply (drule ax_flat [rule_format], auto)
+apply (drule ax_flat, auto)
apply (case_tac "snd (Y j) = UU",auto)
apply (case_tac "Y j", auto)
apply (rule_tac x="j" in exI)
@@ -292,7 +292,7 @@
apply (frule lub_Pair_not_UU_lemma, auto)
apply (drule_tac x="j" in is_ub_thelub, auto)
apply (simp add: less_cprod_def, clarsimp)
-apply (drule ax_flat [rule_format], clarsimp)
+apply (drule ax_flat, clarsimp)
by (drule fstreams_prefix' [THEN iffD1], auto)
lemma fstreams_lub2:
@@ -326,7 +326,7 @@
apply (rule is_ub_thelub chainI)
apply (simp add: chain_def less_cprod_def)
apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp)
-apply (drule ax_flat[rule_format], simp)+
+apply (drule ax_flat, simp)+
apply (drule prod_eqI, auto)
apply (simp add: chain_mono3)
by (rule stream_reach2)
--- a/src/HOLCF/Lift.thy Tue Jan 15 16:19:23 2008 +0100
+++ b/src/HOLCF/Lift.thy Wed Jan 16 22:41:49 2008 +0100
@@ -98,7 +98,7 @@
by (induct x, simp_all)
instance lift :: (type) flat
-by (intro_classes, simp add: less_lift)
+by (intro_classes, auto simp add: less_lift)
text {*
\medskip Two specific lemmas for the combination of LCF and HOL
--- a/src/HOLCF/Pcpo.thy Tue Jan 15 16:19:23 2008 +0100
+++ b/src/HOLCF/Pcpo.thy Wed Jan 16 22:41:49 2008 +0100
@@ -258,7 +258,7 @@
chfin: "\<forall>Y. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
axclass flat < pcpo
- ax_flat: "\<forall>x y. x \<sqsubseteq> y \<longrightarrow> (x = \<bottom>) \<or> (x = y)"
+ ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
text {* finite partial orders are chain-finite and directed-complete *}
@@ -292,8 +292,8 @@
text {* flat types are chfin *}
-lemma flat_imp_chfin:
- "\<forall>Y::nat \<Rightarrow> 'a::flat. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
+instance flat < chfin
+apply intro_classes
apply (unfold max_in_chain_def)
apply clarify
apply (case_tac "\<forall>i. Y i = \<bottom>")
@@ -302,21 +302,18 @@
apply (erule exE)
apply (rule_tac x="i" in exI)
apply clarify
-apply (blast dest: chain_mono3 ax_flat [rule_format])
+apply (blast dest: chain_mono3 ax_flat)
done
-instance flat < chfin
-by intro_classes (rule flat_imp_chfin)
-
text {* flat subclass of chfin; @{text adm_flat} not needed *}
lemma flat_less_iff:
fixes x y :: "'a::flat"
shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
-by (safe dest!: ax_flat [rule_format])
+by (safe dest!: ax_flat)
lemma flat_eq: "(a::'a::flat) \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
-by (safe dest!: ax_flat [rule_format])
+by (safe dest!: ax_flat)
lemma chfin2finch: "chain (Y::nat \<Rightarrow> 'a::chfin) \<Longrightarrow> finite_chain Y"
by (simp add: chfin finite_chain_def)
--- a/src/HOLCF/ex/Stream.thy Tue Jan 15 16:19:23 2008 +0100
+++ b/src/HOLCF/ex/Stream.thy Wed Jan 16 22:41:49 2008 +0100
@@ -102,7 +102,7 @@
"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
apply (case_tac "y=UU",auto)
apply (auto simp add: stream.inverts)
-by (drule ax_flat [rule_format],simp)
+by (drule ax_flat,simp)
@@ -490,7 +490,7 @@
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
apply (erule_tac x="ya" in allE, simp)
apply (auto simp add: stream.inverts)
-by (drule ax_flat [rule_format], simp)
+by (drule ax_flat, simp)
lemma slen_strict_mono_lemma:
"stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t"
@@ -498,7 +498,7 @@
apply (case_tac "sa=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
apply (simp add: stream.inverts, clarsimp)
-by (drule ax_flat [rule_format], simp)
+by (drule ax_flat, simp)
lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
apply (intro ilessI1, auto)