author hoelzl Thu, 02 Feb 2017 09:55:16 -0500 changeset 64979 20a623d03d71 parent 64978 5b9ba120d222 child 64980 7dc25cf5793e
move mono_neutral_cong from AFP/Deep_Learning/PP_Auxiliary
 src/HOL/Groups_Big.thy file | annotate | diff | comparison | revisions
--- 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)