generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
--- a/NEWS Fri Mar 21 22:54:16 2014 +0100
+++ b/NEWS Sat Mar 22 08:37:43 2014 +0100
@@ -138,6 +138,10 @@
* Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
INCOMPATIBILITY.
+* Default congruence rules strong_INF_cong and strong_SUP_cong,
+with simplifier implication in premises. Generalized and replace
+former INT_cong, SUP_cong. INCOMPATIBILITY.
+
* Consolidated theorem names containing INFI and SUPR: have INF
and SUP instead uniformly. INCOMPATIBILITY.
--- a/src/HOL/Complete_Lattices.thy Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Complete_Lattices.thy Sat Mar 22 08:37:43 2014 +0100
@@ -40,6 +40,10 @@
"A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
by (simp add: INF_def image_def)
+lemma strong_INF_cong [cong]:
+ "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> INFIMUM A C = INFIMUM B D"
+ unfolding simp_implies_def by (fact INF_cong)
+
end
class Sup =
@@ -69,6 +73,10 @@
"A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
by (simp add: SUP_def image_def)
+lemma strong_SUP_cong [cong]:
+ "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> SUPREMUM A C = SUPREMUM B D"
+ unfolding simp_implies_def by (fact SUP_cong)
+
end
text {*
@@ -447,21 +455,23 @@
lemma INF_le_SUP: "A \<noteq> {} \<Longrightarrow> INFIMUM A f \<le> SUPREMUM A f"
using Inf_le_Sup [of "f ` A"] by simp
-lemma SUP_eq_const:
- "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
- by (auto intro: SUP_eqI)
-
lemma INF_eq_const:
"I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> INFIMUM I f = x"
by (auto intro: INF_eqI)
-lemma SUP_eq_iff:
- "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
- using SUP_eq_const[of I f c] SUP_upper[of _ I f] by (auto intro: antisym)
+lemma SUP_eq_const:
+ "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i = x) \<Longrightarrow> SUPREMUM I f = x"
+ by (auto intro: SUP_eqI)
lemma INF_eq_iff:
"I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> (INFIMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
- using INF_eq_const[of I f c] INF_lower[of _ I f] by (auto intro: antisym)
+ using INF_eq_const [of I f c] INF_lower [of _ I f]
+ by (auto intro: antisym cong del: strong_INF_cong)
+
+lemma SUP_eq_iff:
+ "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> (SUPREMUM I f = c) \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
+ using SUP_eq_const [of I f c] SUP_upper [of _ I f]
+ by (auto intro: antisym cong del: strong_SUP_cong)
end
@@ -937,10 +947,6 @@
-- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
by (auto simp add: INF_def image_def)
-lemma INT_cong [cong]:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Inter>x\<in>A. C x) = (\<Inter>x\<in>B. D x)"
- by (fact INF_cong)
-
lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
by blast
@@ -1132,14 +1138,6 @@
lemma UN_E [elim!]: "b \<in> (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x\<in>A \<Longrightarrow> b \<in> B x \<Longrightarrow> R) \<Longrightarrow> R"
by (auto simp add: SUP_def image_def)
-lemma UN_cong [cong]:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
- by (fact SUP_cong)
-
-lemma strong_UN_cong:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
- by (unfold simp_implies_def) (fact UN_cong)
-
lemma image_eq_UN: "f ` A = (\<Union>x\<in>A. {f x})"
by blast
--- a/src/HOL/Fun_Def.thy Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Fun_Def.thy Sat Mar 22 08:37:43 2014 +0100
@@ -144,7 +144,7 @@
unfolding Let_def by blast
lemmas [fundef_cong] =
- if_cong image_cong INT_cong UN_cong
+ if_cong image_cong INF_cong SUP_cong
bex_cong ball_cong imp_cong map_option_cong Option.bind_cong
lemma split_cong [fundef_cong]:
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Sat Mar 22 08:37:43 2014 +0100
@@ -117,11 +117,11 @@
apply simp
apply clarify
apply simp
- apply(subgoal_tac "j=0")
- apply (simp)
+ apply(subgoal_tac "xa=0")
+ apply simp
apply arith
apply clarify
- apply(case_tac i,simp,simp)
+ apply(case_tac xaa, simp, simp)
apply clarify
apply simp
apply(erule_tac x=0 in all_dupE)
@@ -319,11 +319,10 @@
\<lbrace>True\<rbrace>,
\<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and>
(\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
-apply(rule Parallel)
---{* 5 subgoals left *}
-apply auto
-apply force+
-apply(rule While)
+apply (rule Parallel)
+apply (auto cong del: strong_INF_cong strong_SUP_cong)
+apply force
+apply (rule While)
apply force
apply force
apply force
--- a/src/HOL/Library/Extended_Real.thy Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Library/Extended_Real.thy Sat Mar 22 08:37:43 2014 +0100
@@ -1613,7 +1613,8 @@
using `0 \<le> c` by (rule ereal_mult_left_mono)
next
fix y
- assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
+ assume "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
+ then have *: "\<And>i. c * f i \<le> y" by simp
show "c * SUPREMUM UNIV f \<le> y"
proof (cases "0 < c \<and> c \<noteq> \<infinity>")
case True
@@ -1631,7 +1632,7 @@
then have "range f = {0}"
by auto
with True show "c * SUPREMUM UNIV f \<le> y"
- using * by (auto simp: SUP_def max.absorb1)
+ using * by auto
next
case False
then obtain i where "f i \<noteq> 0"
--- a/src/HOL/Library/Old_Recdef.thy Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Library/Old_Recdef.thy Sat Mar 22 08:37:43 2014 +0100
@@ -77,7 +77,7 @@
less_Suc_eq [THEN iffD2]
lemmas [recdef_cong] =
- if_cong let_cong image_cong INT_cong UN_cong bex_cong ball_cong imp_cong
+ if_cong let_cong image_cong INF_cong SUP_cong bex_cong ball_cong imp_cong
map_cong filter_cong takeWhile_cong dropWhile_cong foldl_cong foldr_cong
lemmas [recdef_wf] =
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sat Mar 22 08:37:43 2014 +0100
@@ -204,9 +204,9 @@
rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
(fn (i, (set_map0, coalg_set)) =>
- EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
+ EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm SUP_cong})),
etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map0,
- rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
+ rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm SUP_cong}),
ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
REPEAT_DETERM o etac allE, atac, atac])
(rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
@@ -866,14 +866,14 @@
(rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
rtac Un_cong, rtac refl,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
- (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
+ (fn i => EVERY' [rtac @{thm SUP_cong[OF refl]},
REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
(rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1
end;
fun mk_set_map0_tac col_natural =
EVERY' (map rtac [@{thm ext}, o_apply RS trans, sym, o_apply RS trans, @{thm image_UN} RS trans,
- refl RS @{thm UN_cong}, col_natural]) 1;
+ refl RS @{thm SUP_cong}, col_natural]) 1;
fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
let
@@ -964,7 +964,7 @@
rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
(fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
- rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
+ rtac @{thm SUP_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
rtac active_set_map0, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
dtac @{thm ssubst_mem[OF pair_collapse]},
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sat Mar 22 08:37:43 2014 +0100
@@ -196,7 +196,7 @@
fun mk_min_algs_tac worel in_congs =
let
- val minG_tac = EVERY' [rtac @{thm UN_cong}, rtac refl, dtac bspec, atac, etac arg_cong];
+ val minG_tac = EVERY' [rtac @{thm SUP_cong}, rtac refl, dtac bspec, atac, etac arg_cong];
fun minH_tac thm =
EVERY' [rtac Un_cong, minG_tac, rtac @{thm image_cong}, rtac thm,
REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl];
@@ -530,8 +530,8 @@
let
val n = length ctor_maps;
- fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm UN_cong},
- rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong},
+ fun useIH set_nat = EVERY' [rtac trans, rtac @{thm image_UN}, rtac trans, rtac @{thm SUP_cong},
+ rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm SUP_cong},
rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
fun mk_set_nat cset ctor_map ctor_set set_nats =
@@ -672,7 +672,7 @@
rtac passive_set_map0, rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
(fn (active_set_map0, in_Irel) => EVERY' [rtac ord_eq_le_trans,
- rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map0, rtac @{thm UN_least},
+ rtac @{thm SUP_cong[OF _ refl]}, rtac active_set_map0, rtac @{thm UN_least},
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
dtac @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
--- a/src/HOL/UNITY/Follows.thy Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/UNITY/Follows.thy Sat Mar 22 08:37:43 2014 +0100
@@ -94,7 +94,7 @@
apply (simp add: Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
-apply (erule_tac A = "{s. z \<le> f s}" and A' = "{s. z \<le> f s}"
+apply (erule_tac A = "{s. x \<le> f s}" and A' = "{s. x \<le> f s}"
in Always_Constrains_weaken, auto)
apply (drule Always_Int_I, assumption)
apply (force intro: Always_weaken)
@@ -104,7 +104,7 @@
"[| F \<in> Always {s. g s = g' s}; F \<in> f Fols g |] ==> F \<in> f Fols g'"
apply (simp add: Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
-apply (erule_tac A = "{s. z \<le> g s}" and A' = "{s. z \<le> g s}"
+apply (erule_tac A = "{s. x \<le> g s}" and A' = "{s. x \<le> g s}"
in Always_Constrains_weaken, auto)
apply (drule Always_Int_I, assumption)
apply (force intro: Always_weaken)
@@ -114,12 +114,13 @@
subsection{*Union properties (with the subset ordering)*}
(*Can replace "Un" by any sup. But existing max only works for linorders.*)
+
lemma increasing_Un:
"[| F \<in> increasing f; F \<in> increasing g |]
==> F \<in> increasing (%s. (f s) \<union> (g s))"
apply (simp add: increasing_def stable_def constrains_def, auto)
-apply (drule_tac x = "f xa" in spec)
-apply (drule_tac x = "g xa" in spec)
+apply (drule_tac x = "f xb" in spec)
+apply (drule_tac x = "g xb" in spec)
apply (blast dest!: bspec)
done
@@ -128,8 +129,8 @@
==> F \<in> Increasing (%s. (f s) \<union> (g s))"
apply (auto simp add: Increasing_def Stable_def Constrains_def
stable_def constrains_def)
-apply (drule_tac x = "f xa" in spec)
-apply (drule_tac x = "g xa" in spec)
+apply (drule_tac x = "f xb" in spec)
+apply (drule_tac x = "g xb" in spec)
apply (blast dest!: bspec)
done
@@ -172,8 +173,8 @@
"[| F \<in> increasing f; F \<in> increasing g |]
==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))"
apply (simp add: increasing_def stable_def constrains_def, auto)
-apply (drule_tac x = "f xa" in spec)
-apply (drule_tac x = "g xa" in spec)
+apply (drule_tac x = "f xb" in spec)
+apply (drule_tac x = "g xb" in spec)
apply (drule bspec, assumption)
apply (blast intro: add_mono order_trans)
done
@@ -183,8 +184,8 @@
==> F \<in> Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
apply (auto simp add: Increasing_def Stable_def Constrains_def
stable_def constrains_def)
-apply (drule_tac x = "f xa" in spec)
-apply (drule_tac x = "g xa" in spec)
+apply (drule_tac x = "f xb" in spec)
+apply (drule_tac x = "g xb" in spec)
apply (drule bspec, assumption)
apply (blast intro: add_mono order_trans)
done
--- a/src/HOL/UNITY/Transformers.thy Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/UNITY/Transformers.thy Sat Mar 22 08:37:43 2014 +0100
@@ -346,7 +346,7 @@
apply (rule equalityI)
apply (simp_all add: Un_upper1)
apply (simp add: wens_single_def wp_UN_eq, clarify)
-apply (rule_tac a="Suc(i)" in UN_I, auto)
+apply (rule_tac a="Suc xa" in UN_I, auto)
done
lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}"
--- a/src/HOL/UNITY/Union.thy Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/UNITY/Union.thy Sat Mar 22 08:37:43 2014 +0100
@@ -404,16 +404,16 @@
by (simp add: stable_def)
lemma safety_prop_Int [simp]:
- "[| safety_prop X; safety_prop Y |] ==> safety_prop (X \<inter> Y)"
-by (simp add: safety_prop_def, blast)
+ "safety_prop X \<Longrightarrow> safety_prop Y \<Longrightarrow> safety_prop (X \<inter> Y)"
+ by (simp add: safety_prop_def) blast
+
+lemma safety_prop_INTER [simp]:
+ "(\<And>i. i \<in> I \<Longrightarrow> safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i\<in>I. X i)"
+ by (simp add: safety_prop_def) blast
lemma safety_prop_INTER1 [simp]:
- "(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)"
-by (auto simp add: safety_prop_def, blast)
-
-lemma safety_prop_INTER [simp]:
- "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
-by (auto simp add: safety_prop_def, blast)
+ "(\<And>i. safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i. X i)"
+ by (rule safety_prop_INTER) simp
lemma def_prg_Allowed:
"[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]