change class axiom ax_flat to rule_format
authorhuffman
Wed Jan 16 22:41:49 2008 +0100 (2008-01-16)
changeset 259208df5eabda5f6
parent 25919 8b1c0d434824
child 25921 0ca392ab7f37
change class axiom ax_flat to rule_format
src/HOLCF/Cfun.thy
src/HOLCF/Cont.thy
src/HOLCF/FOCUS/Fstreams.thy
src/HOLCF/Lift.thy
src/HOLCF/Pcpo.thy
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOLCF/Cfun.thy	Tue Jan 15 16:19:23 2008 +0100
     1.2 +++ b/src/HOLCF/Cfun.thy	Wed Jan 16 22:41:49 2008 +0100
     1.3 @@ -414,7 +414,7 @@
     1.4      \<Longrightarrow> \<forall>x y::'b. x \<sqsubseteq> y \<longrightarrow> x = \<bottom> \<or> x = y"
     1.5  apply clarify
     1.6  apply (drule_tac f=g in monofun_cfun_arg)
     1.7 -apply (drule ax_flat [rule_format])
     1.8 +apply (drule ax_flat)
     1.9  apply (erule disjE)
    1.10  apply (simp add: injection_defined_rev)
    1.11  apply (simp add: injection_eq)
    1.12 @@ -423,7 +423,7 @@
    1.13  text {* a result about functions with flat codomain *}
    1.14  
    1.15  lemma flat_eqI: "\<lbrakk>(x::'a::flat) \<sqsubseteq> y; x \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> x = y"
    1.16 -by (drule ax_flat [rule_format], simp)
    1.17 +by (drule ax_flat, simp)
    1.18  
    1.19  lemma flat_codom:
    1.20    "f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
     2.1 --- a/src/HOLCF/Cont.thy	Tue Jan 15 16:19:23 2008 +0100
     2.2 +++ b/src/HOLCF/Cont.thy	Wed Jan 16 22:41:49 2008 +0100
     2.3 @@ -222,7 +222,7 @@
     2.4  
     2.5  lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
     2.6  apply (rule monofunI)
     2.7 -apply (drule ax_flat [rule_format])
     2.8 +apply (drule ax_flat)
     2.9  apply auto
    2.10  done
    2.11  
     3.1 --- a/src/HOLCF/FOCUS/Fstreams.thy	Tue Jan 15 16:19:23 2008 +0100
     3.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Wed Jan 16 22:41:49 2008 +0100
     3.3 @@ -180,7 +180,7 @@
     3.4  apply (drule stream_exhaust_eq [THEN iffD1], auto)
     3.5  apply (simp add: fsingleton_def2, auto)
     3.6  apply (auto simp add: stream.inverts)
     3.7 -apply (drule ax_flat [rule_format], simp)
     3.8 +apply (drule ax_flat, simp)
     3.9  by (erule sconc_mono)
    3.10  
    3.11  lemma ft_fstreams[simp]: "ft$(<a> ooo s) = Def a"
    3.12 @@ -280,7 +280,7 @@
    3.13  apply (simp add: max_in_chain_def, auto)
    3.14  apply (subgoal_tac "Y i << Y j",auto)
    3.15  apply (simp add: less_cprod_def, clarsimp)
    3.16 -apply (drule ax_flat [rule_format], auto)
    3.17 +apply (drule ax_flat, auto)
    3.18  apply (case_tac "snd (Y j) = UU",auto)
    3.19  apply (case_tac "Y j", auto)
    3.20  apply (rule_tac x="j" in exI)
    3.21 @@ -292,7 +292,7 @@
    3.22  apply (frule lub_Pair_not_UU_lemma, auto)
    3.23  apply (drule_tac x="j" in is_ub_thelub, auto)
    3.24  apply (simp add: less_cprod_def, clarsimp)
    3.25 -apply (drule ax_flat [rule_format], clarsimp)
    3.26 +apply (drule ax_flat, clarsimp)
    3.27  by (drule fstreams_prefix' [THEN iffD1], auto)
    3.28  
    3.29  lemma fstreams_lub2:
    3.30 @@ -326,7 +326,7 @@
    3.31  apply (rule is_ub_thelub chainI)
    3.32  apply (simp add: chain_def less_cprod_def)
    3.33  apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp)
    3.34 -apply (drule ax_flat[rule_format], simp)+
    3.35 +apply (drule ax_flat, simp)+
    3.36  apply (drule prod_eqI, auto)
    3.37  apply (simp add: chain_mono3)
    3.38  by (rule stream_reach2)
     4.1 --- a/src/HOLCF/Lift.thy	Tue Jan 15 16:19:23 2008 +0100
     4.2 +++ b/src/HOLCF/Lift.thy	Wed Jan 16 22:41:49 2008 +0100
     4.3 @@ -98,7 +98,7 @@
     4.4  by (induct x, simp_all)
     4.5  
     4.6  instance lift :: (type) flat
     4.7 -by (intro_classes, simp add: less_lift)
     4.8 +by (intro_classes, auto simp add: less_lift)
     4.9  
    4.10  text {*
    4.11    \medskip Two specific lemmas for the combination of LCF and HOL
     5.1 --- a/src/HOLCF/Pcpo.thy	Tue Jan 15 16:19:23 2008 +0100
     5.2 +++ b/src/HOLCF/Pcpo.thy	Wed Jan 16 22:41:49 2008 +0100
     5.3 @@ -258,7 +258,7 @@
     5.4    chfin: "\<forall>Y. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
     5.5  
     5.6  axclass flat < pcpo
     5.7 -  ax_flat: "\<forall>x y. x \<sqsubseteq> y \<longrightarrow> (x = \<bottom>) \<or> (x = y)"
     5.8 +  ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
     5.9  
    5.10  text {* finite partial orders are chain-finite and directed-complete *}
    5.11  
    5.12 @@ -292,8 +292,8 @@
    5.13  
    5.14  text {* flat types are chfin *}
    5.15  
    5.16 -lemma flat_imp_chfin: 
    5.17 -     "\<forall>Y::nat \<Rightarrow> 'a::flat. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
    5.18 +instance flat < chfin
    5.19 +apply intro_classes
    5.20  apply (unfold max_in_chain_def)
    5.21  apply clarify
    5.22  apply (case_tac "\<forall>i. Y i = \<bottom>")
    5.23 @@ -302,21 +302,18 @@
    5.24  apply (erule exE)
    5.25  apply (rule_tac x="i" in exI)
    5.26  apply clarify
    5.27 -apply (blast dest: chain_mono3 ax_flat [rule_format])
    5.28 +apply (blast dest: chain_mono3 ax_flat)
    5.29  done
    5.30  
    5.31 -instance flat < chfin
    5.32 -by intro_classes (rule flat_imp_chfin)
    5.33 -
    5.34  text {* flat subclass of chfin; @{text adm_flat} not needed *}
    5.35  
    5.36  lemma flat_less_iff:
    5.37    fixes x y :: "'a::flat"
    5.38    shows "(x \<sqsubseteq> y) = (x = \<bottom> \<or> x = y)"
    5.39 -by (safe dest!: ax_flat [rule_format])
    5.40 +by (safe dest!: ax_flat)
    5.41  
    5.42  lemma flat_eq: "(a::'a::flat) \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
    5.43 -by (safe dest!: ax_flat [rule_format])
    5.44 +by (safe dest!: ax_flat)
    5.45  
    5.46  lemma chfin2finch: "chain (Y::nat \<Rightarrow> 'a::chfin) \<Longrightarrow> finite_chain Y"
    5.47  by (simp add: chfin finite_chain_def)
     6.1 --- a/src/HOLCF/ex/Stream.thy	Tue Jan 15 16:19:23 2008 +0100
     6.2 +++ b/src/HOLCF/ex/Stream.thy	Wed Jan 16 22:41:49 2008 +0100
     6.3 @@ -102,7 +102,7 @@
     6.4    "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
     6.5  apply (case_tac "y=UU",auto)
     6.6  apply (auto simp add: stream.inverts)
     6.7 -by (drule ax_flat [rule_format],simp)
     6.8 +by (drule ax_flat,simp)
     6.9  
    6.10  
    6.11  
    6.12 @@ -490,7 +490,7 @@
    6.13  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
    6.14  apply (erule_tac x="ya" in allE, simp)
    6.15  apply (auto simp add: stream.inverts)
    6.16 -by (drule ax_flat [rule_format], simp)
    6.17 +by (drule ax_flat, simp)
    6.18  
    6.19  lemma slen_strict_mono_lemma:
    6.20    "stream_finite t ==> !s. #(s::'a::flat stream) = #t &  s << t --> s = t"
    6.21 @@ -498,7 +498,7 @@
    6.22  apply (case_tac "sa=UU", auto)
    6.23  apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
    6.24  apply (simp add: stream.inverts, clarsimp)
    6.25 -by (drule ax_flat [rule_format], simp)
    6.26 +by (drule ax_flat, simp)
    6.27  
    6.28  lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
    6.29  apply (intro ilessI1, auto)