1(* Title: HOL/Types_To_Sets/Examples/Group_On_With.thy 2 Author: Fabian Immler, TU M��nchen 3*) 4theory Group_On_With 5imports 6 Prerequisites 7 "../Types_To_Sets" 8begin 9 10subsection \<open>\<^emph>\<open>on\<close> carrier set \<^emph>\<open>with\<close> explicit group operations\<close> 11 12locale semigroup_add_on_with = 13 fixes S::"'a set" and pls::"'a\<Rightarrow>'a\<Rightarrow>'a" 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)" 15 assumes add_mem: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> pls a b \<in> S" 16 17locale ab_semigroup_add_on_with = semigroup_add_on_with + 18 assumes add_commute: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> pls a b = pls b a" 19 20locale comm_monoid_add_on_with = ab_semigroup_add_on_with + 21 fixes z 22 assumes add_zero: "a \<in> S \<Longrightarrow> pls z a = a" 23 assumes zero_mem: "z \<in> S" 24begin 25 26lemma carrier_ne: "S \<noteq> {}" using zero_mem by auto 27 28end 29 30definition "sum_with pls z f S = 31 (if \<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls z then 32 Finite_Set.fold (pls o f) z S else z)" 33 34lemma sum_with_empty[simp]: "sum_with pls z f {} = z" 35 by (auto simp: sum_with_def) 36 37lemma sum_with_cases[case_names comm zero]: 38 "P (sum_with pls z f 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)" 40 "(\<And>C. comm_monoid_add_on_with C pls z \<Longrightarrow> (\<exists>s\<in>S. f s \<notin> C)) \<Longrightarrow> P z" 41 using that 42 by (auto simp: sum_with_def) 43 44context comm_monoid_add_on_with begin 45 46lemma sum_with_infinite: "infinite A \<Longrightarrow> sum_with pls z g A = z" 47 by (induction rule: sum_with_cases) auto 48 49context begin 50 51private abbreviation "pls' \<equiv> \<lambda>x y. pls (if x \<in> S then x else z) (if y \<in> S then y else z)" 52 53lemma fold_pls'_mem: "Finite_Set.fold (pls' \<circ> g) z A \<in> S" 54 if "g ` A \<subseteq> S" 55proof cases 56 assume A: "finite A" 57 interpret comp_fun_commute "pls' o g" 58 using that 59 using add_assoc add_commute add_mem zero_mem 60 by unfold_locales auto 61 from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" . 62 from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"] 63 add_assoc add_commute add_mem zero_mem 64 show ?thesis 65 by auto 66qed (use add_assoc add_commute add_mem zero_mem in simp) 67 68lemma fold_pls'_eq: "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A" 69 if "g ` A \<subseteq> S" 70 using add_assoc add_commute add_mem zero_mem that 71 by (intro fold_closed_eq[where B=S]) auto 72 73lemma sum_with_mem: "sum_with pls z g A \<in> S" if "g ` A \<subseteq> S" 74proof - 75 interpret comp_fun_commute "pls' o g" 76 using add_assoc add_commute add_mem zero_mem that 77 by unfold_locales auto 78 have "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z" 79 using that comm_monoid_add_on_with_axioms by auto 80 then show ?thesis 81 using fold_pls'_mem[OF that] 82 by (simp add: sum_with_def fold_pls'_eq that) 83qed 84 85lemma sum_with_insert: 86 "sum_with pls z g (insert x A) = pls (g x) (sum_with pls z g A)" 87 if g_into: "g x \<in> S" "g ` A \<subseteq> S" 88 and A: "finite A" and x: "x \<notin> A" 89proof - 90 interpret comp_fun_commute "pls' o g" 91 using add_assoc add_commute add_mem zero_mem g_into 92 by unfold_locales auto 93 have "Finite_Set.fold (pls \<circ> g) z (insert x A) = Finite_Set.fold (pls' \<circ> g) z (insert x A)" 94 using g_into 95 by (subst fold_pls'_eq) auto 96 also have "\<dots> = pls' (g x) (Finite_Set.fold (pls' \<circ> g) z A)" 97 unfolding fold_insert[OF A x] 98 by (auto simp: o_def) 99 also have "\<dots> = pls (g x) (Finite_Set.fold (pls' \<circ> g) z A)" 100 proof - 101 from fold_graph_fold[OF A] have "fold_graph (pls' \<circ> g) z A (Finite_Set.fold (pls' \<circ> g) z A)" . 102 from fold_graph_closed_lemma[OF this, of S "pls' \<circ> g"] add_assoc add_commute add_mem zero_mem 103 have "Finite_Set.fold (pls' \<circ> g) z A \<in> S" 104 by auto 105 then show ?thesis 106 using g_into by auto 107 qed 108 also have "Finite_Set.fold (pls' \<circ> g) z A = Finite_Set.fold (pls \<circ> g) z A" 109 using g_into 110 by (subst fold_pls'_eq) auto 111 finally 112 have "Finite_Set.fold (pls \<circ> g) z (insert x A) = pls (g x) (Finite_Set.fold (pls \<circ> g) z A)" . 113 moreover 114 have "\<exists>C. g ` insert x A \<subseteq> C \<and> comm_monoid_add_on_with C pls z" 115 "\<exists>C. g ` A \<subseteq> C \<and> comm_monoid_add_on_with C pls z" 116 using that (1,2) comm_monoid_add_on_with_axioms by auto 117 ultimately show ?thesis 118 by (simp add: sum_with_def) 119qed 120 121end 122 123end 124 125locale 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 132subsection \<open>obvious instances (by type class constraints)\<close> 133 134lemma 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 137lemma 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 141lemma 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 145lemma 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 148lemma 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 152lemma 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 156lemma 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 161lemma 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 164lemma sum_with: "sum f S = sum_with (+) 0 f S" 165proof (induction rule: sum_with_cases) 166 case (comm C) 167 then show ?case 168 unfolding sum.eq_fold 169 by simp 170next 171 case zero 172 from zero[OF comm_monoid_add_on_with] 173 show ?case by simp 174qed 175 176 177subsection \<open>transfer rules\<close> 178 179lemma 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 186lemma 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 191lemma 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 196lemma 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" 200proof (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]) 205qed 206 207lemma 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 214lemma 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 222lemma 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 230lemma 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" 236proof (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 244qed 245 246lemma 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" 251proof (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>) 259qed 260 261lemma 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 269 270lemma ex_comm_monoid_add_around_imageE: 271 includes lifting_syntax 272 assumes ex_comm: "\<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero" 273 assumes transfers: "(A ===> A ===> A) pls pls'" "A zero zero'" "Domainp (rel_set B) S" 274 and in_dom: "\<And>x. x \<in> S \<Longrightarrow> Domainp A (f x)" 275 obtains C where "comm_monoid_add_on_with C pls zero" "f ` S \<subseteq> C" "Domainp (rel_set A) C" 276proof - 277 from ex_comm obtain C0 where C0: "f ` S \<subseteq> C0" and comm: "comm_monoid_add_on_with C0 pls zero" 278 by auto 279 define C where "C = C0 \<inter> Collect (Domainp A)" 280 have "comm_monoid_add_on_with C pls zero" 281 using comm Domainp_apply2I[OF \<open>(A ===> A ===> A) pls pls'\<close>] \<open>A zero zero'\<close> 282 by (auto simp: comm_monoid_add_on_with_Ball_def ab_semigroup_add_on_with_Ball_def 283 semigroup_add_on_with_def C_def) 284 moreover have "f ` S \<subseteq> C" using C0 285 by (auto simp: C_def in_dom) 286 moreover have "Domainp (rel_set A) C" by (auto simp: C_def Domainp_set) 287 ultimately show ?thesis .. 288qed 289 290lemma sum_with_transfer[transfer_rule]: 291 includes lifting_syntax 292 assumes [transfer_rule]: "right_total A" "bi_unique A" "bi_unique B" 293 shows "((A ===> A ===> A) ===> A ===> (B ===> A) ===> rel_set B ===> A) 294 sum_with sum_with" 295proof (safe intro!: rel_funI) 296 fix pls pls' zero zero' f g S T 297 assume transfer_pls[transfer_rule]: "(A ===> A ===> A) pls pls'" 298 and transfer_zero[transfer_rule]: "A zero zero'" 299 assume transfer_g[transfer_rule]: "(B ===> A) f g" 300 and transfer_T[transfer_rule]: "rel_set B S T" 301 show "A (sum_with pls zero f S) (sum_with pls' zero' g T)" 302 proof cases 303 assume ex_comm: "\<exists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero" 304 have Domains: "Domainp (rel_set B) S" "(\<And>x. x \<in> S \<Longrightarrow> Domainp A (f x))" 305 using transfer_T transfer_g 306 by auto (meson Domainp_applyI rel_set_def) 307 from ex_comm_monoid_add_around_imageE[OF ex_comm transfer_pls transfer_zero Domains] 308 obtain C where comm: "comm_monoid_add_on_with C pls zero" 309 and C: "f ` S \<subseteq> C" 310 and "Domainp (rel_set A) C" 311 by auto 312 then obtain C' where [transfer_rule]: "rel_set A C C'" by auto 313 interpret comm: comm_monoid_add_on_with C pls zero by fact 314 have C': "g ` T \<subseteq> C'" 315 by transfer (rule C) 316 have comm': "comm_monoid_add_on_with C' pls' zero'" 317 by transfer (rule comm) 318 then interpret comm': comm_monoid_add_on_with C' pls' zero' . 319 from C' comm' have ex_comm': "\<exists>C. g ` T \<subseteq> C \<and> comm_monoid_add_on_with C pls' zero'" by auto 320 show ?thesis 321 using transfer_T C C' 322 proof (induction S arbitrary: T rule: infinite_finite_induct) 323 case (infinite S) 324 note [transfer_rule] = infinite.prems 325 from infinite.hyps have "infinite T" by transfer 326 then show ?case by (simp add: sum_with_def infinite.hyps \<open>A zero zero'\<close>) 327 next 328 case [transfer_rule]: empty 329 have "T = {}" by transfer rule 330 then show ?case by (simp add: sum_with_def \<open>A zero zero'\<close>) 331 next 332 case (insert x F) 333 note [transfer_rule] = insert.prems(1) 334 have [simp]: "finite T" 335 by transfer (simp add: insert.hyps) 336 obtain y where [transfer_rule]: "B x y" and y: "y \<in> T" 337 by (meson insert.prems insertI1 rel_setD1) 338 define T' where "T' = T - {y}" 339 have T_def: "T = insert y T'" 340 by (auto simp: T'_def y) 341 define sF where "sF = sum_with pls zero f F" 342 define sT where "sT = sum_with pls' zero' g T'" 343 have [simp]: "y \<notin> T'" "finite T'" 344 by (auto simp: y T'_def) 345 have "rel_set B (insert x F - {x}) T'" 346 unfolding T'_def 347 by transfer_prover 348 then have transfer_T'[transfer_rule]: "rel_set B F T'" 349 using insert.hyps 350 by simp 351 from insert.prems have "f ` F \<subseteq> C" "g ` T' \<subseteq> C'" 352 by (auto simp: T'_def) 353 from insert.IH[OF transfer_T' this] have [transfer_rule]: "A sF sT" by (auto simp: sF_def sT_def o_def) 354 have rew: "(sum_with pls zero f (insert x F)) = pls (f x) (sum_with pls zero f F)" 355 apply (subst comm.sum_with_insert) 356 subgoal using insert.prems by auto 357 subgoal using insert.prems by auto 358 subgoal by fact 359 subgoal by fact 360 subgoal by auto 361 done 362 have rew': "(sum_with pls' zero' g (insert y T')) = pls' (g y) (sum_with pls' zero' g T')" 363 apply (subst comm'.sum_with_insert) 364 subgoal 365 apply transfer 366 using insert.prems by auto 367 subgoal 368 apply transfer 369 using insert.prems by auto 370 subgoal by fact 371 subgoal by fact 372 subgoal by auto 373 done 374 have "A (sum_with pls zero f (insert x F)) (sum_with pls' zero' g (insert y T'))" 375 unfolding sT_def[symmetric] sF_def[symmetric] rew rew' 376 by transfer_prover 377 then show ?case 378 by (simp add: T_def) 379 qed 380 next 381 assume *: "\<nexists>C. f ` S \<subseteq> C \<and> comm_monoid_add_on_with C pls zero" 382 then have **: "\<nexists>C'. g ` T \<subseteq> C' \<and> comm_monoid_add_on_with C' pls' zero'" 383 by transfer simp 384 show ?thesis 385 by (simp add: sum_with_def * ** \<open>A zero zero'\<close>) 386 qed 387qed 388 389 390subsection \<open>Rewrite rules to make \<open>ab_group_add\<close> operations explicit\<close> 391 392named_theorems explicit_ab_group_add 393 394lemmas [explicit_ab_group_add] = sum_with 395 396 397subsection \<open>Locale defining \<open>ab_group_add\<close>-Operations in a local type\<close> 398 399locale 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" 402begin 403 404lemma 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 408context includes lifting_syntax begin 409 410definition plus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "plus_S = (rep ---> rep ---> Abs) pls" 411definition minus_S::"'s \<Rightarrow> 's \<Rightarrow> 's" where "minus_S = (rep ---> rep ---> Abs) mns" 412definition uminus_S::"'s \<Rightarrow> 's" where "uminus_S = (rep ---> Abs) um" 413definition zero_S::"'s" where "zero_S = Abs z" 414 415lemma 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 419lemma 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 423lemma 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 427lemma 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 431end 432 433sublocale 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 442context includes lifting_syntax begin 443 444lemma 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" 447proof (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 493qed 494 495end 496 497end 498 499 500subsection \<open>transfer theorems from \<^term>\<open>class.ab_group_add\<close> to \<^term>\<open>ab_group_add_on_with\<close>\<close> 501 502context ab_group_add_on_with begin 503 504context includes lifting_syntax assumes ltd: "\<exists>(Rep::'s \<Rightarrow> 'a) (Abs::'a \<Rightarrow> 's). type_definition Rep Abs S" begin 505 506interpretation local_typedef_ab_group_add_on_with pls z mns um S "TYPE('s)" by unfold_locales fact 507 508text\<open>Get theorem names:\<close> 509print_locale! ab_group_add 510 511lemmas 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 517end 518 519lemmas 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 525end 526 527end