# HG changeset patch
# User haftmann
# Date 1395473863 -3600
# Node ID 67dc9549fa157355cd5a7a43d0e2cbff4d899b73
# Parent  1ad01f98dc3eac8ab28d159b3f9d0a71867c5c7c
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198

diff -r 1ad01f98dc3e -r 67dc9549fa15 NEWS
--- 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.
 
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/Complete_Lattices.thy
--- 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
 
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/Fun_Def.thy
--- 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]:
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/Hoare_Parallel/RG_Examples.thy
--- 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
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/Library/Extended_Real.thy
--- 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"
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/Library/Old_Recdef.thy
--- 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] =
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- 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]},
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- 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 ::
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/UNITY/Follows.thy
--- 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
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/UNITY/Transformers.thy
--- 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> {}"
diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/UNITY/Union.thy
--- 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 |]