2 Author: Fabian Immler, TU München |
2 Author: Fabian Immler, TU München |
3 *) |
3 *) |
4 theory Group_On_With |
4 theory Group_On_With |
5 imports |
5 imports |
6 Prerequisites |
6 Prerequisites |
|
7 Types_To_Sets |
7 begin |
8 begin |
8 |
9 |
9 subsection \<open>\<^emph>\<open>on\<close> carrier set \<^emph>\<open>with\<close> explicit group operations\<close> |
10 subsection \<open>\<^emph>\<open>on\<close> carrier set \<^emph>\<open>with\<close> explicit group operations\<close> |
10 |
11 |
11 locale semigroup_add_on_with = |
12 locale semigroup_add_on_with = |
12 fixes S::"'a set" and pls::"'a\<Rightarrow>'a\<Rightarrow>'a" |
13 fixes S::"'a set" and pls::"'a\<Rightarrow>'a\<Rightarrow>'a" |
13 assumes add_assoc: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> c \<in> S \<Longrightarrow> pls (pls a b) c = pls a (pls b c)" |
14 assumes add_assoc: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> c \<in> S \<Longrightarrow> pls (pls a b) c = pls a (pls b c)" |
14 assumes add_mem: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> pls a b \<in> S" |
15 assumes add_mem: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> pls a b \<in> S" |
15 |
16 |
16 lemma semigroup_add_on_with_Ball_def: "semigroup_add_on_with S pls \<longleftrightarrow> |
|
17 (\<forall>a\<in>S. \<forall>b\<in>S. \<forall>c\<in>S. pls (pls a b) c = pls a (pls b c)) \<and> (\<forall>a\<in>S. \<forall>b\<in>S. pls a b \<in> S)" |
|
18 by (auto simp: semigroup_add_on_with_def) |
|
19 |
|
20 lemma semigroup_add_on_with_transfer[transfer_rule]: |
|
21 includes lifting_syntax |
|
22 assumes [transfer_rule]: "bi_unique A" |
|
23 shows "(rel_set A ===> (A ===> A ===> A) ===> (=)) semigroup_add_on_with semigroup_add_on_with" |
|
24 unfolding semigroup_add_on_with_Ball_def |
|
25 by transfer_prover |
|
26 |
|
27 lemma semigroup_add_on_with[simp]: "semigroup_add_on_with (UNIV::'a::semigroup_add set) (+)" |
|
28 by (auto simp: semigroup_add_on_with_def ac_simps) |
|
29 |
|
30 lemma Domainp_applyI: |
|
31 includes lifting_syntax |
|
32 shows "(A ===> B) f g \<Longrightarrow> A x y \<Longrightarrow> Domainp B (f x)" |
|
33 by (auto simp: rel_fun_def) |
|
34 |
|
35 lemma Domainp_apply2I: |
|
36 includes lifting_syntax |
|
37 shows "(A ===> B ===> C) f g \<Longrightarrow> A x y \<Longrightarrow> B x' y' \<Longrightarrow> Domainp C (f x x')" |
|
38 by (force simp: rel_fun_def) |
|
39 |
|
40 lemma right_total_semigroup_add_transfer[transfer_rule]: |
|
41 includes lifting_syntax |
|
42 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
43 shows "((A ===> A ===> A) ===> (=)) (semigroup_add_on_with (Collect (Domainp A))) class.semigroup_add" |
|
44 proof (intro rel_funI) |
|
45 fix x y assume xy[transfer_rule]: "(A ===> A ===> A) x y" |
|
46 show "semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y" |
|
47 unfolding semigroup_add_on_with_def class.semigroup_add_def |
|
48 by transfer (auto intro!: Domainp_apply2I[OF xy]) |
|
49 qed |
|
50 |
|
51 locale ab_semigroup_add_on_with = semigroup_add_on_with + |
17 locale ab_semigroup_add_on_with = semigroup_add_on_with + |
52 assumes add_commute: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> pls a b = pls b a" |
18 assumes add_commute: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> pls a b = pls b a" |
53 |
|
54 lemma ab_semigroup_add_on_with_Ball_def: |
|
55 "ab_semigroup_add_on_with S pls \<longleftrightarrow> semigroup_add_on_with S pls \<and> (\<forall>a\<in>S. \<forall>b\<in>S. pls a b = pls b a)" |
|
56 by (auto simp: ab_semigroup_add_on_with_def ab_semigroup_add_on_with_axioms_def) |
|
57 |
|
58 lemma ab_semigroup_add_on_with_transfer[transfer_rule]: |
|
59 includes lifting_syntax |
|
60 assumes [transfer_rule]: "bi_unique A" |
|
61 shows |
|
62 "(rel_set A ===> (A ===> A ===> A) ===> (=)) ab_semigroup_add_on_with ab_semigroup_add_on_with" |
|
63 unfolding ab_semigroup_add_on_with_Ball_def by transfer_prover |
|
64 |
|
65 lemma right_total_ab_semigroup_add_transfer[transfer_rule]: |
|
66 includes lifting_syntax |
|
67 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
68 shows |
|
69 "((A ===> A ===> A) ===> (=)) (ab_semigroup_add_on_with (Collect (Domainp A))) class.ab_semigroup_add" |
|
70 unfolding class.ab_semigroup_add_def class.ab_semigroup_add_axioms_def ab_semigroup_add_on_with_Ball_def |
|
71 by transfer_prover |
|
72 |
|
73 lemma ab_semigroup_add_on_with[simp]: "ab_semigroup_add_on_with (UNIV::'a::ab_semigroup_add set) (+)" |
|
74 by (auto simp: ab_semigroup_add_on_with_Ball_def ac_simps) |
|
75 |
19 |
76 locale comm_monoid_add_on_with = ab_semigroup_add_on_with + |
20 locale comm_monoid_add_on_with = ab_semigroup_add_on_with + |
77 fixes z |
21 fixes z |
78 assumes add_zero: "a \<in> S \<Longrightarrow> pls z a = a" |
22 assumes add_zero: "a \<in> S \<Longrightarrow> pls z a = a" |
79 assumes zero_mem: "z \<in> S" |
23 assumes zero_mem: "z \<in> S" |
80 |
24 begin |
81 lemma comm_monoid_add_on_with_Ball_def: |
25 |
82 "comm_monoid_add_on_with S pls z \<longleftrightarrow> ab_semigroup_add_on_with S pls \<and> (\<forall>a\<in>S. pls z a = a) \<and> z \<in> S" |
26 lemma carrier_ne: "S \<noteq> {}" using zero_mem by auto |
83 by (auto simp: comm_monoid_add_on_with_def comm_monoid_add_on_with_axioms_def) |
27 |
84 |
28 end |
85 lemma comm_monoid_add_on_with_transfer[transfer_rule]: |
|
86 includes lifting_syntax |
|
87 assumes [transfer_rule]: "bi_unique A" |
|
88 shows |
|
89 "(rel_set A ===> (A ===> A ===> A) ===> A ===> (=)) comm_monoid_add_on_with comm_monoid_add_on_with" |
|
90 unfolding comm_monoid_add_on_with_Ball_def |
|
91 by transfer_prover |
|
92 |
|
93 lemma right_total_comm_monoid_add_transfer[transfer_rule]: |
|
94 includes lifting_syntax |
|
95 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
96 shows |
|
97 "((A ===> A ===> A) ===> A ===> (=)) |
|
98 (comm_monoid_add_on_with (Collect (Domainp A))) class.comm_monoid_add" |
|
99 proof (intro rel_funI) |
|
100 fix p p' z z' |
|
101 assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" |
|
102 show "comm_monoid_add_on_with (Collect (Domainp A)) p z = class.comm_monoid_add p' z'" |
|
103 unfolding class.comm_monoid_add_def class.comm_monoid_add_axioms_def comm_monoid_add_on_with_Ball_def |
|
104 apply transfer |
|
105 using \<open>A z z'\<close> |
|
106 by auto |
|
107 qed |
|
108 |
|
109 lemma comm_monoid_add_on_with[simp]: "comm_monoid_add_on_with UNIV (+) (0::'a::comm_monoid_add)" |
|
110 by (auto simp: comm_monoid_add_on_with_Ball_def ab_semigroup_add_on_with_Ball_def |
|
111 semigroup_add_on_with_Ball_def ac_simps) |
|
112 |
|
113 locale ab_group_add_on_with = comm_monoid_add_on_with + |
|
114 fixes mns um |
|
115 assumes ab_left_minus: "a \<in> S \<Longrightarrow> pls (um a) a = z" |
|
116 assumes ab_diff_conv_add_uminus: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> mns a b = pls a (um b)" |
|
117 assumes uminus_mem: "a \<in> S \<Longrightarrow> um a \<in> S" |
|
118 |
|
119 lemma ab_group_add_on_with_Ball_def: |
|
120 "ab_group_add_on_with S pls z mns um \<longleftrightarrow> comm_monoid_add_on_with S pls z \<and> |
|
121 (\<forall>a\<in>S. pls (um a) a = z) \<and> (\<forall>a\<in>S. \<forall>b\<in>S. mns a b = pls a (um b)) \<and> (\<forall>a\<in>S. um a \<in> S)" |
|
122 by (auto simp: ab_group_add_on_with_def ab_group_add_on_with_axioms_def) |
|
123 |
|
124 lemma ab_group_add_transfer[transfer_rule]: |
|
125 includes lifting_syntax |
|
126 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
127 shows "((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A)===> (=)) |
|
128 (ab_group_add_on_with (Collect (Domainp A))) class.ab_group_add" |
|
129 proof (intro rel_funI) |
|
130 fix p p' z z' m m' um um' |
|
131 assume [transfer_rule]: |
|
132 "(A ===> A ===> A) p p'" "A z z'" "(A ===> A ===> A) m m'" |
|
133 and um[transfer_rule]: "(A ===> A) um um'" |
|
134 show "ab_group_add_on_with (Collect (Domainp A)) p z m um = class.ab_group_add p' z' m' um'" |
|
135 unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_Ball_def |
|
136 by transfer (use um in \<open>auto simp: rel_fun_def\<close>) |
|
137 qed |
|
138 |
|
139 lemma ab_group_add_on_with_transfer[transfer_rule]: |
|
140 includes lifting_syntax |
|
141 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
142 shows |
|
143 "(rel_set A ===> (A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A)===> (=)) |
|
144 ab_group_add_on_with ab_group_add_on_with" |
|
145 unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_Ball_def |
|
146 by transfer_prover |
|
147 |
|
148 lemma ab_group_add_on_with[simp]: "ab_group_add_on_with (UNIV::'a::ab_group_add set) (+) 0 (-) uminus" |
|
149 by (auto simp: ab_group_add_on_with_Ball_def) |
|
150 |
29 |
151 definition "sum_with pls z f S = |
30 definition "sum_with pls z f S = |
152 (if \<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls z then |
31 (if \<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls z then |
153 Finite_Set.fold (pls o f) z S else z)" |
32 Finite_Set.fold (pls o f) z S else z)" |
154 |
33 |
160 if "\<And>C. f ` S \<subseteq> C \<Longrightarrow> comm_monoid_add_on_with C pls z \<Longrightarrow> P (Finite_Set.fold (pls o f) z S)" |
39 if "\<And>C. f ` S \<subseteq> C \<Longrightarrow> comm_monoid_add_on_with C pls z \<Longrightarrow> P (Finite_Set.fold (pls o f) z S)" |
161 "(\<And>C. comm_monoid_add_on_with C pls z \<Longrightarrow> (\<exists>s\<in>S. f s \<notin> C)) \<Longrightarrow> P z" |
40 "(\<And>C. comm_monoid_add_on_with C pls z \<Longrightarrow> (\<exists>s\<in>S. f s \<notin> C)) \<Longrightarrow> P z" |
162 using that |
41 using that |
163 by (auto simp: sum_with_def) |
42 by (auto simp: sum_with_def) |
164 |
43 |
165 lemma sum_with: "sum f S = sum_with (+) 0 f S" |
|
166 proof (induction rule: sum_with_cases) |
|
167 case (comm C) |
|
168 then show ?case |
|
169 unfolding sum.eq_fold |
|
170 by simp |
|
171 next |
|
172 case zero |
|
173 from zero[OF comm_monoid_add_on_with] |
|
174 show ?case by simp |
|
175 qed |
|
176 |
|
177 context comm_monoid_add_on_with begin |
44 context comm_monoid_add_on_with begin |
178 |
45 |
179 lemma sum_with_infinite: "infinite A \<Longrightarrow> sum_with pls z g A = z" |
46 lemma sum_with_infinite: "infinite A \<Longrightarrow> sum_with pls z g A = z" |
180 by (induction rule: sum_with_cases) auto |
47 by (induction rule: sum_with_cases) auto |
181 |
|
182 lemmas comm_monoid_add_unfolded = |
|
183 comm_monoid_add_on_with_axioms[unfolded |
|
184 comm_monoid_add_on_with_Ball_def ab_semigroup_add_on_with_Ball_def semigroup_add_on_with_Ball_def] |
|
185 |
48 |
186 context begin |
49 context begin |
187 |
50 |
188 private abbreviation "pls' \<equiv> \<lambda>x y. pls (if x \<in> S then x else z) (if y \<in> S then y else z)" |
51 private abbreviation "pls' \<equiv> \<lambda>x y. pls (if x \<in> S then x else z) (if y \<in> S then y else z)" |
189 |
52 |
190 lemma fold_pls'_mem: "Finite_Set.fold (pls' \<circ> g) z A \<in> S" |
53 lemma fold_pls'_mem: "Finite_Set.fold (pls' \<circ> g) z A \<in> S" |
191 if "g ` A \<subseteq> S" |
54 if "g ` A \<subseteq> S" |
192 proof cases |
55 proof cases |
193 assume A: "finite A" |
56 assume A: "finite A" |
194 interpret comp_fun_commute "pls' o g" |
57 interpret comp_fun_commute "pls' o g" |
195 using comm_monoid_add_unfolded that |
58 using that |
|
59 using add_assoc add_commute add_mem zero_mem |
196 by unfold_locales auto |
60 by unfold_locales auto |
197 from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" . |
61 from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" . |
198 from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"] comm_monoid_add_unfolded |
62 from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"] |
|
63 add_assoc add_commute add_mem zero_mem |
199 show ?thesis |
64 show ?thesis |
200 by auto |
65 by auto |
201 qed (use comm_monoid_add_unfolded in simp) |
66 qed (use add_assoc add_commute add_mem zero_mem in simp) |
202 |
67 |
203 lemma fold_pls'_eq: "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A" |
68 lemma fold_pls'_eq: "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A" |
204 if "g ` A \<subseteq> S" |
69 if "g ` A \<subseteq> S" |
205 using comm_monoid_add_unfolded that |
70 using add_assoc add_commute add_mem zero_mem that |
206 by (intro fold_closed_eq[where B=S]) auto |
71 by (intro fold_closed_eq[where B=S]) auto |
207 |
72 |
208 lemma sum_with_mem: "sum_with pls z g A \<in> S" if "g ` A \<subseteq> S" |
73 lemma sum_with_mem: "sum_with pls z g A \<in> S" if "g ` A \<subseteq> S" |
209 proof - |
74 proof - |
210 interpret comp_fun_commute "pls' o g" |
75 interpret comp_fun_commute "pls' o g" |
211 using comm_monoid_add_unfolded that |
76 using add_assoc add_commute add_mem zero_mem that |
212 by unfold_locales auto |
77 by unfold_locales auto |
213 have "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z" |
78 have "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z" |
214 using that comm_monoid_add_on_with_axioms by auto |
79 using that comm_monoid_add_on_with_axioms by auto |
215 then show ?thesis |
80 then show ?thesis |
216 using fold_pls'_mem[OF that] |
81 using fold_pls'_mem[OF that] |
221 "sum_with pls z g (insert x A) = pls (g x) (sum_with pls z g A)" |
86 "sum_with pls z g (insert x A) = pls (g x) (sum_with pls z g A)" |
222 if g_into: "g x \<in> S" "g ` A \<subseteq> S" |
87 if g_into: "g x \<in> S" "g ` A \<subseteq> S" |
223 and A: "finite A" and x: "x \<notin> A" |
88 and A: "finite A" and x: "x \<notin> A" |
224 proof - |
89 proof - |
225 interpret comp_fun_commute "pls' o g" |
90 interpret comp_fun_commute "pls' o g" |
226 using comm_monoid_add_unfolded g_into |
91 using add_assoc add_commute add_mem zero_mem g_into |
227 by unfold_locales auto |
92 by unfold_locales auto |
228 have "Finite_Set.fold (pls \<circ> g) z (insert x A) = Finite_Set.fold (pls' \<circ> g) z (insert x A)" |
93 have "Finite_Set.fold (pls \<circ> g) z (insert x A) = Finite_Set.fold (pls' \<circ> g) z (insert x A)" |
229 using g_into |
94 using g_into |
230 by (subst fold_pls'_eq) auto |
95 by (subst fold_pls'_eq) auto |
231 also have "\<dots> = pls' (g x) (Finite_Set.fold (pls' \<circ> g) z A)" |
96 also have "\<dots> = pls' (g x) (Finite_Set.fold (pls' \<circ> g) z A)" |
232 unfolding fold_insert[OF A x] |
97 unfolding fold_insert[OF A x] |
233 by (auto simp: o_def) |
98 by (auto simp: o_def) |
234 also have "\<dots> = pls (g x) (Finite_Set.fold (pls' \<circ> g) z A)" |
99 also have "\<dots> = pls (g x) (Finite_Set.fold (pls' \<circ> g) z A)" |
235 proof - |
100 proof - |
236 from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" . |
101 from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" . |
237 from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"] comm_monoid_add_unfolded |
102 from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"] add_assoc add_commute add_mem zero_mem |
238 have "Finite_Set.fold (pls' \<circ> g) z A \<in> S" |
103 have "Finite_Set.fold (pls' \<circ> g) z A \<in> S" |
239 by auto |
104 by auto |
240 then show ?thesis |
105 then show ?thesis |
241 using g_into by auto |
106 using g_into by auto |
242 qed |
107 qed |
254 qed |
119 qed |
255 |
120 |
256 end |
121 end |
257 |
122 |
258 end |
123 end |
|
124 |
|
125 locale ab_group_add_on_with = comm_monoid_add_on_with + |
|
126 fixes mns um |
|
127 assumes ab_left_minus: "a \<in> S \<Longrightarrow> pls (um a) a = z" |
|
128 assumes ab_diff_conv_add_uminus: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> mns a b = pls a (um b)" |
|
129 assumes uminus_mem: "a \<in> S \<Longrightarrow> um a \<in> S" |
|
130 |
|
131 |
|
132 subsection \<open>obvious instances (by type class constraints)\<close> |
|
133 |
|
134 lemma semigroup_add_on_with[simp]: "semigroup_add_on_with (UNIV::'a::semigroup_add set) (+)" |
|
135 by (auto simp: semigroup_add_on_with_def ac_simps) |
|
136 |
|
137 lemma semigroup_add_on_with_Ball_def: "semigroup_add_on_with S pls \<longleftrightarrow> |
|
138 (\<forall>a\<in>S. \<forall>b\<in>S. \<forall>c\<in>S. pls (pls a b) c = pls a (pls b c)) \<and> (\<forall>a\<in>S. \<forall>b\<in>S. pls a b \<in> S)" |
|
139 by (auto simp: semigroup_add_on_with_def) |
|
140 |
|
141 lemma ab_semigroup_add_on_with_Ball_def: |
|
142 "ab_semigroup_add_on_with S pls \<longleftrightarrow> semigroup_add_on_with S pls \<and> (\<forall>a\<in>S. \<forall>b\<in>S. pls a b = pls b a)" |
|
143 by (auto simp: ab_semigroup_add_on_with_def ab_semigroup_add_on_with_axioms_def) |
|
144 |
|
145 lemma ab_semigroup_add_on_with[simp]: "ab_semigroup_add_on_with (UNIV::'a::ab_semigroup_add set) (+)" |
|
146 by (auto simp: ab_semigroup_add_on_with_Ball_def ac_simps) |
|
147 |
|
148 lemma comm_monoid_add_on_with_Ball_def: |
|
149 "comm_monoid_add_on_with S pls z \<longleftrightarrow> ab_semigroup_add_on_with S pls \<and> (\<forall>a\<in>S. pls z a = a) \<and> z \<in> S" |
|
150 by (auto simp: comm_monoid_add_on_with_def comm_monoid_add_on_with_axioms_def) |
|
151 |
|
152 lemma comm_monoid_add_on_with[simp]: "comm_monoid_add_on_with UNIV (+) (0::'a::comm_monoid_add)" |
|
153 by (auto simp: comm_monoid_add_on_with_Ball_def ab_semigroup_add_on_with_Ball_def |
|
154 semigroup_add_on_with_Ball_def ac_simps) |
|
155 |
|
156 lemma ab_group_add_on_with_Ball_def: |
|
157 "ab_group_add_on_with S pls z mns um \<longleftrightarrow> comm_monoid_add_on_with S pls z \<and> |
|
158 (\<forall>a\<in>S. pls (um a) a = z) \<and> (\<forall>a\<in>S. \<forall>b\<in>S. mns a b = pls a (um b)) \<and> (\<forall>a\<in>S. um a \<in> S)" |
|
159 by (auto simp: ab_group_add_on_with_def ab_group_add_on_with_axioms_def) |
|
160 |
|
161 lemma ab_group_add_on_with[simp]: "ab_group_add_on_with (UNIV::'a::ab_group_add set) (+) 0 (-) uminus" |
|
162 by (auto simp: ab_group_add_on_with_Ball_def) |
|
163 |
|
164 lemma sum_with: "sum f S = sum_with (+) 0 f S" |
|
165 proof (induction rule: sum_with_cases) |
|
166 case (comm C) |
|
167 then show ?case |
|
168 unfolding sum.eq_fold |
|
169 by simp |
|
170 next |
|
171 case zero |
|
172 from zero[OF comm_monoid_add_on_with] |
|
173 show ?case by simp |
|
174 qed |
|
175 |
|
176 |
|
177 subsection \<open>transfer rules\<close> |
|
178 |
|
179 lemma semigroup_add_on_with_transfer[transfer_rule]: |
|
180 includes lifting_syntax |
|
181 assumes [transfer_rule]: "bi_unique A" |
|
182 shows "(rel_set A ===> (A ===> A ===> A) ===> (=)) semigroup_add_on_with semigroup_add_on_with" |
|
183 unfolding semigroup_add_on_with_Ball_def |
|
184 by transfer_prover |
|
185 |
|
186 lemma Domainp_applyI: |
|
187 includes lifting_syntax |
|
188 shows "(A ===> B) f g \<Longrightarrow> A x y \<Longrightarrow> Domainp B (f x)" |
|
189 by (auto simp: rel_fun_def) |
|
190 |
|
191 lemma Domainp_apply2I: |
|
192 includes lifting_syntax |
|
193 shows "(A ===> B ===> C) f g \<Longrightarrow> A x y \<Longrightarrow> B x' y' \<Longrightarrow> Domainp C (f x x')" |
|
194 by (force simp: rel_fun_def) |
|
195 |
|
196 lemma right_total_semigroup_add_transfer[transfer_rule]: |
|
197 includes lifting_syntax |
|
198 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
199 shows "((A ===> A ===> A) ===> (=)) (semigroup_add_on_with (Collect (Domainp A))) class.semigroup_add" |
|
200 proof (intro rel_funI) |
|
201 fix x y assume xy[transfer_rule]: "(A ===> A ===> A) x y" |
|
202 show "semigroup_add_on_with (Collect (Domainp A)) x = class.semigroup_add y" |
|
203 unfolding semigroup_add_on_with_def class.semigroup_add_def |
|
204 by transfer (auto intro!: Domainp_apply2I[OF xy]) |
|
205 qed |
|
206 |
|
207 lemma ab_semigroup_add_on_with_transfer[transfer_rule]: |
|
208 includes lifting_syntax |
|
209 assumes [transfer_rule]: "bi_unique A" |
|
210 shows |
|
211 "(rel_set A ===> (A ===> A ===> A) ===> (=)) ab_semigroup_add_on_with ab_semigroup_add_on_with" |
|
212 unfolding ab_semigroup_add_on_with_Ball_def by transfer_prover |
|
213 |
|
214 lemma right_total_ab_semigroup_add_transfer[transfer_rule]: |
|
215 includes lifting_syntax |
|
216 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
217 shows |
|
218 "((A ===> A ===> A) ===> (=)) (ab_semigroup_add_on_with (Collect (Domainp A))) class.ab_semigroup_add" |
|
219 unfolding class.ab_semigroup_add_def class.ab_semigroup_add_axioms_def ab_semigroup_add_on_with_Ball_def |
|
220 by transfer_prover |
|
221 |
|
222 lemma comm_monoid_add_on_with_transfer[transfer_rule]: |
|
223 includes lifting_syntax |
|
224 assumes [transfer_rule]: "bi_unique A" |
|
225 shows |
|
226 "(rel_set A ===> (A ===> A ===> A) ===> A ===> (=)) comm_monoid_add_on_with comm_monoid_add_on_with" |
|
227 unfolding comm_monoid_add_on_with_Ball_def |
|
228 by transfer_prover |
|
229 |
|
230 lemma right_total_comm_monoid_add_transfer[transfer_rule]: |
|
231 includes lifting_syntax |
|
232 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
233 shows |
|
234 "((A ===> A ===> A) ===> A ===> (=)) |
|
235 (comm_monoid_add_on_with (Collect (Domainp A))) class.comm_monoid_add" |
|
236 proof (intro rel_funI) |
|
237 fix p p' z z' |
|
238 assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" |
|
239 show "comm_monoid_add_on_with (Collect (Domainp A)) p z = class.comm_monoid_add p' z'" |
|
240 unfolding class.comm_monoid_add_def class.comm_monoid_add_axioms_def comm_monoid_add_on_with_Ball_def |
|
241 apply transfer |
|
242 using \<open>A z z'\<close> |
|
243 by auto |
|
244 qed |
|
245 |
|
246 lemma ab_group_add_transfer[transfer_rule]: |
|
247 includes lifting_syntax |
|
248 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
249 shows "((A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A)===> (=)) |
|
250 (ab_group_add_on_with (Collect (Domainp A))) class.ab_group_add" |
|
251 proof (intro rel_funI) |
|
252 fix p p' z z' m m' um um' |
|
253 assume [transfer_rule]: |
|
254 "(A ===> A ===> A) p p'" "A z z'" "(A ===> A ===> A) m m'" |
|
255 and um[transfer_rule]: "(A ===> A) um um'" |
|
256 show "ab_group_add_on_with (Collect (Domainp A)) p z m um = class.ab_group_add p' z' m' um'" |
|
257 unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_Ball_def |
|
258 by transfer (use um in \<open>auto simp: rel_fun_def\<close>) |
|
259 qed |
|
260 |
|
261 lemma ab_group_add_on_with_transfer[transfer_rule]: |
|
262 includes lifting_syntax |
|
263 assumes [transfer_rule]: "right_total A" "bi_unique A" |
|
264 shows |
|
265 "(rel_set A ===> (A ===> A ===> A) ===> A ===> (A ===> A ===> A) ===> (A ===> A)===> (=)) |
|
266 ab_group_add_on_with ab_group_add_on_with" |
|
267 unfolding class.ab_group_add_def class.ab_group_add_axioms_def ab_group_add_on_with_Ball_def |
|
268 by transfer_prover |
259 |
269 |
260 lemma ex_comm_monoid_add_around_imageE: |
270 lemma ex_comm_monoid_add_around_imageE: |
261 includes lifting_syntax |
271 includes lifting_syntax |
262 assumes ex_comm: "\<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero" |
272 assumes ex_comm: "\<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero" |
263 assumes transfers: "(A ===> A ===> A) pls pls'" "A zero zero'" "Domainp (rel_set B) S" |
273 assumes transfers: "(A ===> A ===> A) pls pls'" "A zero zero'" "Domainp (rel_set B) S" |
374 show ?thesis |
384 show ?thesis |
375 by (simp add: sum_with_def * ** \<open>A zero zero'\<close>) |
385 by (simp add: sum_with_def * ** \<open>A zero zero'\<close>) |
376 qed |
386 qed |
377 qed |
387 qed |
378 |
388 |
|
389 |
379 subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations explicit\<close> |
390 subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations explicit\<close> |
380 |
391 |
381 named_theorems explicit_ab_group_add |
392 named_theorems explicit_ab_group_add |
382 |
393 |
383 lemmas [explicit_ab_group_add] = sum_with |
394 lemmas [explicit_ab_group_add] = sum_with |
384 |
395 |
385 end |
396 |
|
397 subsection \<open>Locale defining \<open>ab_group_add\<close>-Operations in a local type\<close> |
|
398 |
|
399 locale local_typedef_ab_group_add_on_with = local_typedef S s + |
|
400 ab_group_add_on_with S |
|
401 for S ::"'b set" and s::"'s itself" |
|
402 begin |
|
403 |
|
404 lemma mem_minus_lt: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> mns x y \<in> S" |
|
405 using ab_diff_conv_add_uminus[of x y] add_mem[of x "um y"] uminus_mem[of y] |
|
406 by auto |
|
407 |
|
408 context includes lifting_syntax begin |
|
409 |
|
410 definition plus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "plus_S = (rep ---> rep ---> Abs) pls" |
|
411 definition minus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "minus_S = (rep ---> rep ---> Abs) mns" |
|
412 definition uminus_S::"'s \<Rightarrow> 's" where "uminus_S = (rep ---> Abs) um" |
|
413 definition zero_S::"'s" where "zero_S = Abs z" |
|
414 |
|
415 lemma plus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) pls plus_S" |
|
416 unfolding plus_S_def |
|
417 by (auto simp: cr_S_def add_mem intro!: rel_funI) |
|
418 |
|
419 lemma minus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) mns minus_S" |
|
420 unfolding minus_S_def |
|
421 by (auto simp: cr_S_def mem_minus_lt intro!: rel_funI) |
|
422 |
|
423 lemma uminus_S_transfer[transfer_rule]: "(cr_S ===> cr_S) um uminus_S" |
|
424 unfolding uminus_S_def |
|
425 by (auto simp: cr_S_def uminus_mem intro!: rel_funI) |
|
426 |
|
427 lemma zero_S_transfer[transfer_rule]: "cr_S z zero_S" |
|
428 unfolding zero_S_def |
|
429 by (auto simp: cr_S_def zero_mem intro!: rel_funI) |
|
430 |
|
431 end |
|
432 |
|
433 sublocale type: ab_group_add plus_S "zero_S::'s" minus_S uminus_S |
|
434 apply unfold_locales |
|
435 subgoal by transfer (rule add_assoc) |
|
436 subgoal by transfer (rule add_commute) |
|
437 subgoal by transfer (rule add_zero) |
|
438 subgoal by transfer (rule ab_left_minus) |
|
439 subgoal by transfer (rule ab_diff_conv_add_uminus) |
|
440 done |
|
441 |
|
442 context includes lifting_syntax begin |
|
443 |
|
444 lemma sum_transfer[transfer_rule]: |
|
445 "((A===>cr_S) ===> rel_set A ===> cr_S) (sum_with pls z) type.sum" |
|
446 if [transfer_rule]: "bi_unique A" |
|
447 proof (safe intro!: rel_funI) |
|
448 fix f g I J |
|
449 assume fg[transfer_rule]: "(A ===> cr_S) f g" and rel_set: "rel_set A I J" |
|
450 show "cr_S (sum_with pls z f I) (type.sum g J)" |
|
451 using rel_set |
|
452 proof (induction I arbitrary: J rule: infinite_finite_induct) |
|
453 case (infinite I) |
|
454 note [transfer_rule] = infinite.prems |
|
455 from infinite.hyps have "infinite J" by transfer |
|
456 with infinite.hyps show ?case |
|
457 by (simp add: zero_S_transfer sum_with_infinite) |
|
458 next |
|
459 case [transfer_rule]: empty |
|
460 have "J = {}" by transfer rule |
|
461 then show ?case by (simp add: zero_S_transfer) |
|
462 next |
|
463 case (insert x F) |
|
464 note [transfer_rule] = insert.prems |
|
465 have [simp]: "finite J" |
|
466 by transfer (simp add: insert.hyps) |
|
467 obtain y where [transfer_rule]: "A x y" and y: "y \<in> J" |
|
468 by (meson insert.prems insertI1 rel_setD1) |
|
469 define J' where "J' = J - {y}" |
|
470 have T_def: "J = insert y J'" |
|
471 by (auto simp: J'_def y) |
|
472 define sF where "sF = sum_with pls z f F" |
|
473 define sT where "sT = type.sum g J'" |
|
474 have [simp]: "y \<notin> J'" "finite J'" |
|
475 by (auto simp: y J'_def) |
|
476 have "rel_set A (insert x F - {x}) J'" |
|
477 unfolding J'_def |
|
478 by transfer_prover |
|
479 then have "rel_set A F J'" |
|
480 using insert.hyps |
|
481 by simp |
|
482 from insert.IH[OF this] have [transfer_rule]: "cr_S sF sT" by (auto simp: sF_def sT_def) |
|
483 have f_S: "f x \<in> S" "f ` F \<subseteq> S" |
|
484 using \<open>A x y\<close> fg insert.prems |
|
485 by (auto simp: rel_fun_def cr_S_def rel_set_def) |
|
486 have "cr_S (pls (f x) sF) (plus_S (g y) sT)" by transfer_prover |
|
487 then have "cr_S (sum_with pls z f (insert x F)) (type.sum g (insert y J'))" |
|
488 by (simp add: sum_with_insert insert.hyps type.sum.insert_remove sF_def[symmetric] |
|
489 sT_def[symmetric] f_S) |
|
490 then show ?case |
|
491 by (simp add: T_def) |
|
492 qed |
|
493 qed |
|
494 |
|
495 end |
|
496 |
|
497 end |
|
498 |
|
499 |
|
500 subsection \<open>transfer theorems from \<^term>\<open>class.ab_group_add\<close> to \<^term>\<open>ab_group_add_on_with\<close>\<close> |
|
501 |
|
502 context ab_group_add_on_with begin |
|
503 |
|
504 context includes lifting_syntax assumes ltd: "\<exists>(Rep::'s \<Rightarrow> 'a) (Abs::'a \<Rightarrow> 's). type_definition Rep Abs S" begin |
|
505 |
|
506 interpretation local_typedef_ab_group_add_on_with pls z mns um S "TYPE('s)" by unfold_locales fact |
|
507 |
|
508 text\<open>Get theorem names:\<close> |
|
509 print_locale! ab_group_add |
|
510 |
|
511 lemmas lt_sum_mono_neutral_cong_left = sum.mono_neutral_cong_left |
|
512 [var_simplified explicit_ab_group_add, |
|
513 unoverload_type 'c, |
|
514 OF type.comm_monoid_add_axioms, |
|
515 untransferred] |
|
516 |
|
517 end |
|
518 |
|
519 lemmas sum_mono_neutral_cong_left = |
|
520 lt_sum_mono_neutral_cong_left |
|
521 [cancel_type_definition, |
|
522 OF carrier_ne, |
|
523 simplified pred_fun_def, simplified] |
|
524 |
|
525 end |
|
526 |
|
527 end |