# HG changeset patch
# User hoelzl
# Date 1486047316 18000
# Node ID 20a623d03d717d65b20644074e3008c7e5a5e470
# Parent  5b9ba120d222f4445e451a9757143a2de142c2a8
move mono_neutral_cong from AFP/Deep_Learning/PP_Auxiliary

diff -r 5b9ba120d222 -r 20a623d03d71 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Thu Feb 02 14:42:06 2017 +0100
+++ b/src/HOL/Groups_Big.thy	Thu Feb 02 09:55:16 2017 -0500
@@ -239,6 +239,20 @@
 lemma mono_neutral_right: "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<forall>i \<in> T - S. g i = \<^bold>1 \<Longrightarrow> F g T = F g S"
   by (blast intro!: mono_neutral_left [symmetric])
 
+lemma mono_neutral_cong:
+  assumes [simp]: "finite T" "finite S"
+    and *: "\<And>i. i \<in> T - S \<Longrightarrow> h i = \<^bold>1" "\<And>i. i \<in> S - T \<Longrightarrow> g i = \<^bold>1"
+    and gh: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x = h x"
+ shows "F g S = F h T"
+proof-
+  have "F g S = F g (S \<inter> T)"
+    by(rule mono_neutral_right)(auto intro: *)
+  also have "\<dots> = F h (S \<inter> T)" using refl gh by(rule cong)
+  also have "\<dots> = F h T"
+    by(rule mono_neutral_left)(auto intro: *)
+  finally show ?thesis .
+qed
+
 lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T"
   by (auto simp: bij_betw_def reindex)