# HG changeset patch
# User huffman
# Date 1200519709 -3600
# Node ID 8df5eabda5f6044f2b2c53db8e8bb852d36e5f6e
# Parent  8b1c0d434824453cfd64a90265cfa7b891f7a514
change class axiom ax_flat to rule_format

diff -r 8b1c0d434824 -r 8df5eabda5f6 src/HOLCF/Cfun.thy
--- 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)"
diff -r 8b1c0d434824 -r 8df5eabda5f6 src/HOLCF/Cont.thy
--- 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
 
diff -r 8b1c0d434824 -r 8df5eabda5f6 src/HOLCF/FOCUS/Fstreams.thy
--- 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)
diff -r 8b1c0d434824 -r 8df5eabda5f6 src/HOLCF/Lift.thy
--- 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
diff -r 8b1c0d434824 -r 8df5eabda5f6 src/HOLCF/Pcpo.thy
--- 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)
diff -r 8b1c0d434824 -r 8df5eabda5f6 src/HOLCF/ex/Stream.thy
--- 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)