equal
deleted
inserted
replaced
145 assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x" |
145 assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x" |
146 shows "F g A = F h B" |
146 shows "F g A = F h B" |
147 using g_h unfolding \<open>A = B\<close> |
147 using g_h unfolding \<open>A = B\<close> |
148 by (induct B rule: infinite_finite_induct) auto |
148 by (induct B rule: infinite_finite_induct) auto |
149 |
149 |
150 lemma cong_strong [cong]: |
150 lemma cong_simp [cong]: |
151 "\<lbrakk> A = B; \<And>x. x \<in> B =simp=> g x = h x \<rbrakk> \<Longrightarrow> F (\<lambda>x. g x) A = F (\<lambda>x. h x) B" |
151 "\<lbrakk> A = B; \<And>x. x \<in> B =simp=> g x = h x \<rbrakk> \<Longrightarrow> F (\<lambda>x. g x) A = F (\<lambda>x. h x) B" |
152 by (rule cong) (simp_all add: simp_implies_def) |
152 by (rule cong) (simp_all add: simp_implies_def) |
153 |
153 |
154 lemma reindex_cong: |
154 lemma reindex_cong: |
155 assumes "inj_on l B" |
155 assumes "inj_on l B" |