8 imports |
8 imports |
9 Derivative |
9 Derivative |
10 Uniform_Limit |
10 Uniform_Limit |
11 "~~/src/HOL/Library/Indicator_Function" |
11 "~~/src/HOL/Library/Indicator_Function" |
12 begin |
12 begin |
|
13 |
|
14 (*FIXME: move elsewhere and use the existing locales*) |
|
15 |
|
16 subsection \<open>Using additivity of lifted function to encode definedness.\<close> |
|
17 |
|
18 definition "neutral opp = (SOME x. \<forall>y. opp x y = y \<and> opp y x = y)" |
|
19 |
|
20 fun lifted where |
|
21 "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)" |
|
22 | "lifted opp None _ = (None::'b option)" |
|
23 | "lifted opp _ None = None" |
|
24 |
|
25 lemma lifted_simp_1[simp]: "lifted opp v None = None" |
|
26 by (induct v) auto |
|
27 |
|
28 definition "monoidal opp \<longleftrightarrow> |
|
29 (\<forall>x y. opp x y = opp y x) \<and> |
|
30 (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and> |
|
31 (\<forall>x. opp (neutral opp) x = x)" |
|
32 |
|
33 lemma monoidalI: |
|
34 assumes "\<And>x y. opp x y = opp y x" |
|
35 and "\<And>x y z. opp x (opp y z) = opp (opp x y) z" |
|
36 and "\<And>x. opp (neutral opp) x = x" |
|
37 shows "monoidal opp" |
|
38 unfolding monoidal_def using assms by fastforce |
|
39 |
|
40 lemma monoidal_ac: |
|
41 assumes "monoidal opp" |
|
42 shows [simp]: "opp (neutral opp) a = a" |
|
43 and [simp]: "opp a (neutral opp) = a" |
|
44 and "opp a b = opp b a" |
|
45 and "opp (opp a b) c = opp a (opp b c)" |
|
46 and "opp a (opp b c) = opp b (opp a c)" |
|
47 using assms unfolding monoidal_def by metis+ |
|
48 |
|
49 lemma neutral_lifted [cong]: |
|
50 assumes "monoidal opp" |
|
51 shows "neutral (lifted opp) = Some (neutral opp)" |
|
52 proof - |
|
53 { fix x |
|
54 assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y" |
|
55 then have "Some (neutral opp) = x" |
|
56 apply (induct x) |
|
57 apply force |
|
58 by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) } |
|
59 note [simp] = this |
|
60 show ?thesis |
|
61 apply (subst neutral_def) |
|
62 apply (intro some_equality allI) |
|
63 apply (induct_tac y) |
|
64 apply (auto simp add:monoidal_ac[OF assms]) |
|
65 done |
|
66 qed |
|
67 |
|
68 lemma monoidal_lifted[intro]: |
|
69 assumes "monoidal opp" |
|
70 shows "monoidal (lifted opp)" |
|
71 unfolding monoidal_def split_option_all neutral_lifted[OF assms] |
|
72 using monoidal_ac[OF assms] |
|
73 by auto |
|
74 |
|
75 definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}" |
|
76 definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)" |
|
77 definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)" |
|
78 |
|
79 lemma support_subset[intro]: "support opp f s \<subseteq> s" |
|
80 unfolding support_def by auto |
|
81 |
|
82 lemma support_empty[simp]: "support opp f {} = {}" |
|
83 using support_subset[of opp f "{}"] by auto |
|
84 |
|
85 lemma comp_fun_commute_monoidal[intro]: |
|
86 assumes "monoidal opp" |
|
87 shows "comp_fun_commute opp" |
|
88 unfolding comp_fun_commute_def |
|
89 using monoidal_ac[OF assms] |
|
90 by auto |
|
91 |
|
92 lemma support_clauses: |
|
93 "\<And>f g s. support opp f {} = {}" |
|
94 "\<And>f g s. support opp f (insert x s) = |
|
95 (if f(x) = neutral opp then support opp f s else insert x (support opp f s))" |
|
96 "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}" |
|
97 "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)" |
|
98 "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)" |
|
99 "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)" |
|
100 "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)" |
|
101 unfolding support_def by auto |
|
102 |
|
103 lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)" |
|
104 unfolding support_def by auto |
|
105 |
|
106 lemma iterate_empty[simp]: "iterate opp {} f = neutral opp" |
|
107 unfolding iterate_def fold'_def by auto |
|
108 |
|
109 lemma iterate_insert[simp]: |
|
110 assumes "monoidal opp" |
|
111 and "finite s" |
|
112 shows "iterate opp (insert x s) f = |
|
113 (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))" |
|
114 proof (cases "x \<in> s") |
|
115 case True |
|
116 then show ?thesis by (auto simp: insert_absorb iterate_def) |
|
117 next |
|
118 case False |
|
119 note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]] |
|
120 show ?thesis |
|
121 proof (cases "f x = neutral opp") |
|
122 case True |
|
123 then show ?thesis |
|
124 using assms \<open>x \<notin> s\<close> |
|
125 by (auto simp: iterate_def support_clauses) |
|
126 next |
|
127 case False |
|
128 with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis |
|
129 apply (simp add: iterate_def fold'_def support_clauses) |
|
130 apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def]) |
|
131 apply (force simp add: )+ |
|
132 done |
|
133 qed |
|
134 qed |
|
135 |
|
136 lemma iterate_some: |
|
137 "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)" |
|
138 by (erule finite_induct) (auto simp: monoidal_lifted) |
|
139 |
|
140 lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)" |
|
141 unfolding neutral_def |
|
142 by (force elim: allE [where x=0]) |
|
143 |
|
144 lemma support_if: "a \<noteq> neutral opp \<Longrightarrow> support opp (\<lambda>x. if P x then a else neutral opp) A = {x \<in> A. P x}" |
|
145 unfolding support_def |
|
146 by (force intro: Collect_cong) |
|
147 |
|
148 lemma support_if_subset: "support opp (\<lambda>x. if P x then a else neutral opp) A \<subseteq> {x \<in> A. P x}" |
|
149 by (simp add: subset_iff support_def) |
|
150 |
|
151 definition supp_setsum where "supp_setsum f A \<equiv> setsum f (support op+ f A)" |
|
152 |
|
153 lemma supp_setsum_divide_distrib: |
|
154 "supp_setsum f A / (r::'a::field) = supp_setsum (\<lambda>n. f n / r) A" |
|
155 apply (cases "r = 0") |
|
156 apply (simp add: supp_setsum_def) |
|
157 apply (simp add: supp_setsum_def setsum_divide_distrib support_def) |
|
158 done |
|
159 |
|
160 (*FIXME move up e.g. to Library/Convex.thy*) |
|
161 lemma convex_supp_setsum: |
|
162 assumes "convex S" and 1: "supp_setsum u I = 1" |
|
163 and "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> u i \<and> (u i = 0 \<or> f i \<in> S)" |
|
164 shows "supp_setsum (\<lambda>i. u i *\<^sub>R f i) I \<in> S" |
|
165 proof - |
|
166 have fin: "finite {i \<in> I. u i \<noteq> 0}" |
|
167 using 1 setsum.infinite by (force simp: supp_setsum_def support_def) |
|
168 then have eq: "supp_setsum(\<lambda>i. u i *\<^sub>R f i) I = |
|
169 setsum (\<lambda>i. u i *\<^sub>R f i) {i \<in> I. u i \<noteq> 0}" |
|
170 by (force intro: setsum.mono_neutral_left simp: supp_setsum_def support_def) |
|
171 show ?thesis |
|
172 apply (simp add: eq) |
|
173 apply (rule convex_setsum [OF fin \<open>convex S\<close>]) |
|
174 using 1 assms apply (auto simp: supp_setsum_def support_def) |
|
175 done |
|
176 qed |
|
177 |
|
178 (*END OF SUPPORT, ETC.*) |
|
179 |
13 |
180 |
14 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib |
181 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib |
15 scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff |
182 scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff |
16 scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one |
183 scaleR_cancel_left scaleR_cancel_right scaleR_add_right scaleR_add_left real_vector_class.scaleR_one |
17 |
184 |
3585 |
3750 |
3586 lemma operative_empty: "operative opp f \<Longrightarrow> f {} = neutral opp" |
3751 lemma operative_empty: "operative opp f \<Longrightarrow> f {} = neutral opp" |
3587 unfolding operative_def by (rule property_empty_interval) auto |
3752 unfolding operative_def by (rule property_empty_interval) auto |
3588 |
3753 |
3589 |
3754 |
3590 subsection \<open>Using additivity of lifted function to encode definedness.\<close> |
|
3591 |
|
3592 fun lifted where |
|
3593 "lifted (opp :: 'a \<Rightarrow> 'a \<Rightarrow> 'b) (Some x) (Some y) = Some (opp x y)" |
|
3594 | "lifted opp None _ = (None::'b option)" |
|
3595 | "lifted opp _ None = None" |
|
3596 |
|
3597 lemma lifted_simp_1[simp]: "lifted opp v None = None" |
|
3598 by (induct v) auto |
|
3599 |
|
3600 definition "monoidal opp \<longleftrightarrow> |
|
3601 (\<forall>x y. opp x y = opp y x) \<and> |
|
3602 (\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and> |
|
3603 (\<forall>x. opp (neutral opp) x = x)" |
|
3604 |
|
3605 lemma monoidalI: |
|
3606 assumes "\<And>x y. opp x y = opp y x" |
|
3607 and "\<And>x y z. opp x (opp y z) = opp (opp x y) z" |
|
3608 and "\<And>x. opp (neutral opp) x = x" |
|
3609 shows "monoidal opp" |
|
3610 unfolding monoidal_def using assms by fastforce |
|
3611 |
|
3612 lemma monoidal_ac: |
|
3613 assumes "monoidal opp" |
|
3614 shows [simp]: "opp (neutral opp) a = a" |
|
3615 and [simp]: "opp a (neutral opp) = a" |
|
3616 and "opp a b = opp b a" |
|
3617 and "opp (opp a b) c = opp a (opp b c)" |
|
3618 and "opp a (opp b c) = opp b (opp a c)" |
|
3619 using assms unfolding monoidal_def by metis+ |
|
3620 |
|
3621 lemma neutral_lifted [cong]: |
|
3622 assumes "monoidal opp" |
|
3623 shows "neutral (lifted opp) = Some (neutral opp)" |
|
3624 proof - |
|
3625 { fix x |
|
3626 assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y" |
|
3627 then have "Some (neutral opp) = x" |
|
3628 apply (induct x) |
|
3629 apply force |
|
3630 by (metis assms lifted.simps(1) monoidal_ac(2) option.inject) } |
|
3631 note [simp] = this |
|
3632 show ?thesis |
|
3633 apply (subst neutral_def) |
|
3634 apply (intro some_equality allI) |
|
3635 apply (induct_tac y) |
|
3636 apply (auto simp add:monoidal_ac[OF assms]) |
|
3637 done |
|
3638 qed |
|
3639 |
|
3640 lemma monoidal_lifted[intro]: |
|
3641 assumes "monoidal opp" |
|
3642 shows "monoidal (lifted opp)" |
|
3643 unfolding monoidal_def split_option_all neutral_lifted[OF assms] |
|
3644 using monoidal_ac[OF assms] |
|
3645 by auto |
|
3646 |
|
3647 definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}" |
|
3648 definition "fold' opp e s = (if finite s then Finite_Set.fold opp e s else e)" |
|
3649 definition "iterate opp s f = fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)" |
|
3650 |
|
3651 lemma support_subset[intro]: "support opp f s \<subseteq> s" |
|
3652 unfolding support_def by auto |
|
3653 |
|
3654 lemma support_empty[simp]: "support opp f {} = {}" |
|
3655 using support_subset[of opp f "{}"] by auto |
|
3656 |
|
3657 lemma comp_fun_commute_monoidal[intro]: |
|
3658 assumes "monoidal opp" |
|
3659 shows "comp_fun_commute opp" |
|
3660 unfolding comp_fun_commute_def |
|
3661 using monoidal_ac[OF assms] |
|
3662 by auto |
|
3663 |
|
3664 lemma support_clauses: |
|
3665 "\<And>f g s. support opp f {} = {}" |
|
3666 "\<And>f g s. support opp f (insert x s) = |
|
3667 (if f(x) = neutral opp then support opp f s else insert x (support opp f s))" |
|
3668 "\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}" |
|
3669 "\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)" |
|
3670 "\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)" |
|
3671 "\<And>f g s. support opp f (s - t) = (support opp f s) - (support opp f t)" |
|
3672 "\<And>f g s. support opp g (f ` s) = f ` (support opp (g \<circ> f) s)" |
|
3673 unfolding support_def by auto |
|
3674 |
|
3675 lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support opp f s)" |
|
3676 unfolding support_def by auto |
|
3677 |
|
3678 lemma iterate_empty[simp]: "iterate opp {} f = neutral opp" |
|
3679 unfolding iterate_def fold'_def by auto |
|
3680 |
|
3681 lemma iterate_insert[simp]: |
|
3682 assumes "monoidal opp" |
|
3683 and "finite s" |
|
3684 shows "iterate opp (insert x s) f = |
|
3685 (if x \<in> s then iterate opp s f else opp (f x) (iterate opp s f))" |
|
3686 proof (cases "x \<in> s") |
|
3687 case True |
|
3688 then show ?thesis by (auto simp: insert_absorb iterate_def) |
|
3689 next |
|
3690 case False |
|
3691 note * = comp_fun_commute.comp_comp_fun_commute [OF comp_fun_commute_monoidal[OF assms(1)]] |
|
3692 show ?thesis |
|
3693 proof (cases "f x = neutral opp") |
|
3694 case True |
|
3695 then show ?thesis |
|
3696 using assms \<open>x \<notin> s\<close> |
|
3697 by (auto simp: iterate_def support_clauses) |
|
3698 next |
|
3699 case False |
|
3700 with \<open>x \<notin> s\<close> \<open>finite s\<close> support_subset show ?thesis |
|
3701 apply (simp add: iterate_def fold'_def support_clauses) |
|
3702 apply (subst comp_fun_commute.fold_insert[OF * finite_support, simplified comp_def]) |
|
3703 apply (force simp add: )+ |
|
3704 done |
|
3705 qed |
|
3706 qed |
|
3707 |
|
3708 lemma iterate_some: |
|
3709 "\<lbrakk>monoidal opp; finite s\<rbrakk> \<Longrightarrow> iterate (lifted opp) s (\<lambda>x. Some(f x)) = Some (iterate opp s f)" |
|
3710 by (erule finite_induct) (auto simp: monoidal_lifted) |
|
3711 |
|
3712 |
|
3713 subsection \<open>Two key instances of additivity.\<close> |
3755 subsection \<open>Two key instances of additivity.\<close> |
3714 |
|
3715 lemma neutral_add[simp]: "neutral op + = (0::'a::comm_monoid_add)" |
|
3716 unfolding neutral_def |
|
3717 by (force elim: allE [where x=0]) |
|
3718 |
3756 |
3719 lemma operative_content[intro]: "operative (op +) content" |
3757 lemma operative_content[intro]: "operative (op +) content" |
3720 by (force simp add: operative_def content_split[symmetric]) |
3758 by (force simp add: operative_def content_split[symmetric]) |
3721 |
3759 |
3722 lemma monoidal_monoid[intro]: "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)" |
3760 lemma monoidal_monoid[intro]: "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)" |