63 by (auto intro: finite_subset) |
63 by (auto intro: finite_subset) |
64 show ?thesis using assms(4) |
64 show ?thesis using assms(4) |
65 by (simp add: union_disjoint[OF f d, unfolded eq[symmetric]] F_neutral'[OF assms(3)]) |
65 by (simp add: union_disjoint[OF f d, unfolded eq[symmetric]] F_neutral'[OF assms(3)]) |
66 qed |
66 qed |
67 |
67 |
68 lemmas F_mono_neutral_cong_right = F_mono_neutral_cong_left[symmetric] |
68 lemma F_mono_neutral_cong_right: |
|
69 "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1; \<And>x. x \<in> S \<Longrightarrow> g x = h x \<rbrakk> |
|
70 \<Longrightarrow> F g T = F h S" |
|
71 by(auto intro!: F_mono_neutral_cong_left[symmetric]) |
69 |
72 |
70 lemma F_mono_neutral_left: |
73 lemma F_mono_neutral_left: |
71 "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T" |
74 "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g S = F g T" |
72 by(blast intro: F_mono_neutral_cong_left) |
75 by(blast intro: F_mono_neutral_cong_left) |
73 |
76 |
74 lemmas F_mono_neutral_right = F_mono_neutral_left[symmetric] |
77 lemma F_mono_neutral_right: |
|
78 "\<lbrakk> finite T; S \<subseteq> T; \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S" |
|
79 by(blast intro!: F_mono_neutral_left[symmetric]) |
75 |
80 |
76 lemma F_delta: |
81 lemma F_delta: |
77 assumes fS: "finite S" |
82 assumes fS: "finite S" |
78 shows "F (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)" |
83 shows "F (\<lambda>k. if k=a then b k else 1) S = (if a \<in> S then b a else 1)" |
79 proof- |
84 proof- |