2244 by fast |
2225 by fast |
2245 qed |
2226 qed |
2246 qed |
2227 qed |
2247 |
2228 |
2248 lemma (in gcd_condition_monoid) gcdof_cong_l: |
2229 lemma (in gcd_condition_monoid) gcdof_cong_l: |
2249 assumes a'a: "a' \<sim> a" |
2230 assumes "a' \<sim> a" "a gcdof b c" "a' \<in> carrier G" and carr': "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" |
2250 and agcd: "a gcdof b c" |
|
2251 and a'carr: "a' \<in> carrier G" and carr': "a \<in> carrier G" "b \<in> carrier G" "c \<in> carrier G" |
|
2252 shows "a' gcdof b c" |
2231 shows "a' gcdof b c" |
2253 proof - |
2232 proof - |
2254 note carr = a'carr carr' |
|
2255 interpret weak_lower_semilattice "division_rel G" by simp |
2233 interpret weak_lower_semilattice "division_rel G" by simp |
2256 have "is_glb (division_rel G) a' {b, c}" |
2234 have "is_glb (division_rel G) a' {b, c}" |
2257 by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd) |
2235 by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: assms gcdof_greatestLower[symmetric]) |
2258 then have "a' \<in> carrier G \<and> a' gcdof b c" |
2236 then have "a' \<in> carrier G \<and> a' gcdof b c" |
2259 by (simp add: gcdof_greatestLower carr') |
2237 by (simp add: gcdof_greatestLower carr') |
2260 then show ?thesis .. |
2238 then show ?thesis .. |
2261 qed |
2239 qed |
2262 |
2240 |
2263 lemma (in gcd_condition_monoid) gcd_closed [simp]: |
2241 lemma (in gcd_condition_monoid) gcd_closed [simp]: |
2264 assumes carr: "a \<in> carrier G" "b \<in> carrier G" |
2242 assumes "a \<in> carrier G" "b \<in> carrier G" |
2265 shows "somegcd G a b \<in> carrier G" |
2243 shows "somegcd G a b \<in> carrier G" |
2266 proof - |
2244 proof - |
2267 interpret weak_lower_semilattice "division_rel G" by simp |
2245 interpret weak_lower_semilattice "division_rel G" by simp |
2268 show ?thesis |
2246 show ?thesis |
2269 apply (simp add: somegcd_meet[OF carr]) |
2247 using assms meet_closed by (simp add: somegcd_meet) |
2270 apply (rule meet_closed[simplified], fact+) |
|
2271 done |
|
2272 qed |
2248 qed |
2273 |
2249 |
2274 lemma (in gcd_condition_monoid) gcd_isgcd: |
2250 lemma (in gcd_condition_monoid) gcd_isgcd: |
2275 assumes carr: "a \<in> carrier G" "b \<in> carrier G" |
2251 assumes "a \<in> carrier G" "b \<in> carrier G" |
2276 shows "(somegcd G a b) gcdof a b" |
2252 shows "(somegcd G a b) gcdof a b" |
2277 proof - |
2253 proof - |
2278 interpret weak_lower_semilattice "division_rel G" |
2254 interpret weak_lower_semilattice "division_rel G" |
2279 by simp |
2255 by simp |
2280 from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b" |
2256 from assms have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b" |
2281 by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet) |
2257 by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet) |
2282 then show "(somegcd G a b) gcdof a b" |
2258 then show "(somegcd G a b) gcdof a b" |
2283 by simp |
2259 by simp |
2284 qed |
2260 qed |
2285 |
2261 |
2286 lemma (in gcd_condition_monoid) gcd_exists: |
2262 lemma (in gcd_condition_monoid) gcd_exists: |
2287 assumes carr: "a \<in> carrier G" "b \<in> carrier G" |
2263 assumes "a \<in> carrier G" "b \<in> carrier G" |
2288 shows "\<exists>x\<in>carrier G. x = somegcd G a b" |
2264 shows "\<exists>x\<in>carrier G. x = somegcd G a b" |
2289 proof - |
2265 proof - |
2290 interpret weak_lower_semilattice "division_rel G" |
2266 interpret weak_lower_semilattice "division_rel G" |
2291 by simp |
2267 by simp |
2292 show ?thesis |
2268 show ?thesis |
2293 by (metis carr(1) carr(2) gcd_closed) |
2269 by (metis assms gcd_closed) |
2294 qed |
2270 qed |
2295 |
2271 |
2296 lemma (in gcd_condition_monoid) gcd_divides_l: |
2272 lemma (in gcd_condition_monoid) gcd_divides_l: |
2297 assumes carr: "a \<in> carrier G" "b \<in> carrier G" |
2273 assumes "a \<in> carrier G" "b \<in> carrier G" |
2298 shows "(somegcd G a b) divides a" |
2274 shows "(somegcd G a b) divides a" |
2299 proof - |
2275 proof - |
2300 interpret weak_lower_semilattice "division_rel G" |
2276 interpret weak_lower_semilattice "division_rel G" |
2301 by simp |
2277 by simp |
2302 show ?thesis |
2278 show ?thesis |
2303 by (metis carr(1) carr(2) gcd_isgcd isgcd_def) |
2279 by (metis assms gcd_isgcd isgcd_def) |
2304 qed |
2280 qed |
2305 |
2281 |
2306 lemma (in gcd_condition_monoid) gcd_divides_r: |
2282 lemma (in gcd_condition_monoid) gcd_divides_r: |
2307 assumes carr: "a \<in> carrier G" "b \<in> carrier G" |
2283 assumes "a \<in> carrier G" "b \<in> carrier G" |
2308 shows "(somegcd G a b) divides b" |
2284 shows "(somegcd G a b) divides b" |
2309 proof - |
2285 proof - |
2310 interpret weak_lower_semilattice "division_rel G" |
2286 interpret weak_lower_semilattice "division_rel G" |
2311 by simp |
2287 by simp |
2312 show ?thesis |
2288 show ?thesis |
2313 by (metis carr gcd_isgcd isgcd_def) |
2289 by (metis assms gcd_isgcd isgcd_def) |
2314 qed |
2290 qed |
2315 |
2291 |
2316 lemma (in gcd_condition_monoid) gcd_divides: |
2292 lemma (in gcd_condition_monoid) gcd_divides: |
2317 assumes sub: "z divides x" "z divides y" |
2293 assumes "z divides x" "z divides y" |
2318 and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
2294 and L: "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" |
2319 shows "z divides (somegcd G x y)" |
2295 shows "z divides (somegcd G x y)" |
2320 proof - |
2296 proof - |
2321 interpret weak_lower_semilattice "division_rel G" |
2297 interpret weak_lower_semilattice "division_rel G" |
2322 by simp |
2298 by simp |
2323 show ?thesis |
2299 show ?thesis |
2324 by (metis gcd_isgcd isgcd_def assms) |
2300 by (metis gcd_isgcd isgcd_def assms) |
2325 qed |
2301 qed |
2326 |
2302 |
2327 lemma (in gcd_condition_monoid) gcd_cong_l: |
2303 lemma (in gcd_condition_monoid) gcd_cong_l: |
2328 assumes xx': "x \<sim> x'" |
2304 assumes "x \<sim> x'" "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" |
2329 and carr: "x \<in> carrier G" "x' \<in> carrier G" "y \<in> carrier G" |
|
2330 shows "somegcd G x y \<sim> somegcd G x' y" |
2305 shows "somegcd G x y \<sim> somegcd G x' y" |
2331 proof - |
2306 proof - |
2332 interpret weak_lower_semilattice "division_rel G" |
2307 interpret weak_lower_semilattice "division_rel G" |
2333 by simp |
2308 by simp |
2334 show ?thesis |
2309 show ?thesis |
2335 apply (simp add: somegcd_meet carr) |
2310 using somegcd_meet assms |
2336 apply (rule meet_cong_l[simplified], fact+) |
2311 by (metis eq_object.select_convs(1) meet_cong_l partial_object.select_convs(1)) |
2337 done |
|
2338 qed |
2312 qed |
2339 |
2313 |
2340 lemma (in gcd_condition_monoid) gcd_cong_r: |
2314 lemma (in gcd_condition_monoid) gcd_cong_r: |
2341 assumes carr: "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" |
2315 assumes "y \<sim> y'" "x \<in> carrier G" "y \<in> carrier G" "y' \<in> carrier G" |
2342 and yy': "y \<sim> y'" |
|
2343 shows "somegcd G x y \<sim> somegcd G x y'" |
2316 shows "somegcd G x y \<sim> somegcd G x y'" |
2344 proof - |
2317 proof - |
2345 interpret weak_lower_semilattice "division_rel G" by simp |
2318 interpret weak_lower_semilattice "division_rel G" by simp |
2346 show ?thesis |
2319 show ?thesis |
2347 apply (simp add: somegcd_meet carr) |
2320 by (meson associated_def assms gcd_closed gcd_divides gcd_divides_l gcd_divides_r monoid.divides_trans monoid_axioms) |
2348 apply (rule meet_cong_r[simplified], fact+) |
2321 qed |
2349 done |
|
2350 qed |
|
2351 |
|
2352 (* |
|
2353 lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]: |
|
2354 assumes carr: "b \<in> carrier G" |
|
2355 shows "asc_cong (\<lambda>a. somegcd G a b)" |
|
2356 using carr |
|
2357 unfolding CONG_def |
|
2358 by clarsimp (blast intro: gcd_cong_l) |
|
2359 |
|
2360 lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]: |
|
2361 assumes carr: "a \<in> carrier G" |
|
2362 shows "asc_cong (\<lambda>b. somegcd G a b)" |
|
2363 using carr |
|
2364 unfolding CONG_def |
|
2365 by clarsimp (blast intro: gcd_cong_r) |
|
2366 |
|
2367 lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] = |
|
2368 assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r] |
|
2369 *) |
|
2370 |
2322 |
2371 lemma (in gcd_condition_monoid) gcdI: |
2323 lemma (in gcd_condition_monoid) gcdI: |
2372 assumes dvd: "a divides b" "a divides c" |
2324 assumes dvd: "a divides b" "a divides c" |
2373 and others: "\<And>y. \<lbrakk>y\<in>carrier G; y divides b; y divides c\<rbrakk> \<Longrightarrow> y divides a" |
2325 and others: "\<And>y. \<lbrakk>y\<in>carrier G; y divides b; y divides c\<rbrakk> \<Longrightarrow> y divides a" |
2374 and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G" |
2326 and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G" |
2639 by (intro prime_divides) simp+ |
2589 by (intro prime_divides) simp+ |
2640 then show ?case |
2590 then show ?case |
2641 using Cons.IH Cons.prems(1) by force |
2591 using Cons.IH Cons.prems(1) by force |
2642 qed |
2592 qed |
2643 |
2593 |
2644 |
2594 proposition (in primeness_condition_monoid) wfactors_unique: |
2645 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct: |
2595 assumes "wfactors G as a" "wfactors G as' a" |
2646 "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and> |
2596 and "a \<in> carrier G" "set as \<subseteq> carrier G" "set as' \<subseteq> carrier G" |
2647 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'" |
2597 shows "essentially_equal G as as'" |
2648 proof (induct as) |
2598 using assms |
|
2599 proof (induct as arbitrary: a as') |
2649 case Nil |
2600 case Nil |
2650 show ?case |
2601 then have "a \<sim> \<one>" |
2651 apply (clarsimp simp: wfactors_def) |
2602 by (meson Units_one_closed one_closed perm.Nil perm_wfactorsD unit_wfactors) |
2652 by (metis Units_one_closed assoc_unit_r list_update_nonempty unit_wfactors_empty unitfactor_ee wfactorsI) |
2603 then have "as' = []" |
|
2604 using Nil.prems assoc_unit_l unit_wfactors_empty by blast |
|
2605 then show ?case |
|
2606 by auto |
2653 next |
2607 next |
2654 case (Cons ah as) |
2608 case (Cons ah as) |
2655 then show ?case |
2609 then have ahdvda: "ah divides a" |
2656 proof clarsimp |
2610 using wfactors_dividesI by auto |
2657 fix a as' |
|
2658 assume ih [rule_format]: |
|
2659 "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and> |
|
2660 wfactors G as' a \<longrightarrow> essentially_equal G as as'" |
|
2661 and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G" |
|
2662 and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G" |
|
2663 and afs: "wfactors G (ah # as) a" |
|
2664 and afs': "wfactors G as' a" |
|
2665 then have ahdvda: "ah divides a" |
|
2666 by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all |
|
2667 then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'" |
2611 then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'" |
2668 by blast |
2612 by blast |
|
2613 have carr_ah: "ah \<in> carrier G" "set as \<subseteq> carrier G" |
|
2614 using Cons.prems by fastforce+ |
|
2615 have "ah \<otimes> foldr (\<otimes>) as \<one> \<sim> a" |
|
2616 by (rule wfactorsE[OF \<open>wfactors G (ah # as) a\<close>]) auto |
|
2617 then have "foldr (\<otimes>) as \<one> \<sim> a'" |
|
2618 by (metis Cons.prems(4) a a'carr assoc_l_cancel insert_subset list.set(2) monoid.multlist_closed monoid_axioms) |
|
2619 then |
2669 have a'fs: "wfactors G as a'" |
2620 have a'fs: "wfactors G as a'" |
2670 apply (rule wfactorsE[OF afs], rule wfactorsI, simp) |
2621 by (meson Cons.prems(1) set_subset_Cons subset_iff wfactorsE wfactorsI) |
2671 by (metis a a'carr ahcarr ascarr assoc_l_cancel factorsI factors_def factors_mult_single list.set_intros(1) list.set_intros(2) multlist_closed) |
2622 then have ahirr: "irreducible G ah" |
2672 from afs have ahirr: "irreducible G ah" |
2623 by (meson Cons.prems(1) list.set_intros(1) wfactorsE) |
2673 by (elim wfactorsE) simp |
2624 with Cons have ahprime: "prime G ah" |
2674 with ascarr have ahprime: "prime G ah" |
2625 by (simp add: irreducible_prime) |
2675 by (intro irreducible_prime ahcarr) |
|
2676 |
|
2677 note carr [simp] = acarr ahcarr ascarr as'carr a'carr |
|
2678 |
|
2679 note ahdvda |
2626 note ahdvda |
2680 also from afs' have "a divides (foldr (\<otimes>) as' \<one>)" |
2627 also have "a divides (foldr (\<otimes>) as' \<one>)" |
2681 by (elim wfactorsE associatedE, simp) |
2628 by (meson Cons.prems(2) associatedE wfactorsE) |
2682 finally have "ah divides (foldr (\<otimes>) as' \<one>)" |
2629 finally have "ah divides (foldr (\<otimes>) as' \<one>)" |
2683 by simp |
2630 using Cons.prems(4) by auto |
2684 with ahprime have "\<exists>i<length as'. ah divides as'!i" |
2631 with ahprime have "\<exists>i<length as'. ah divides as'!i" |
2685 by (intro multlist_prime_pos) simp_all |
2632 by (intro multlist_prime_pos) (use Cons.prems in auto) |
2686 then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i" |
2633 then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i" |
2687 by blast |
2634 by blast |
2688 from afs' carr have irrasi: "irreducible G (as'!i)" |
2635 then obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" |
2689 by (fast intro: nth_mem[OF len] elim: wfactorsE) |
|
2690 from len carr have asicarr[simp]: "as'!i \<in> carrier G" |
|
2691 unfolding set_conv_nth by force |
|
2692 note carr = carr asicarr |
|
2693 |
|
2694 from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" |
|
2695 by blast |
2636 by blast |
2696 with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah" |
2637 have irrasi: "irreducible G (as'!i)" |
2697 by (metis ahprime associatedI2 irreducible_prodE primeE) |
2638 using nth_mem[OF len] wfactorsE |
|
2639 by (metis Cons.prems(2)) |
|
2640 have asicarr[simp]: "as'!i \<in> carrier G" |
|
2641 using len \<open>set as' \<subseteq> carrier G\<close> nth_mem by blast |
|
2642 have asiah: "as'!i \<sim> ah" |
|
2643 by (metis \<open>ah \<in> carrier G\<close> \<open>x \<in> carrier G\<close> asi irrasi ahprime associatedI2 irreducible_prodE primeE) |
2698 note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as'] |
2644 note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as'] |
2699 note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]] |
|
2700 note carr = carr partscarr |
|
2701 |
|
2702 have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1" |
2645 have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1" |
2703 by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists) |
2646 using Cons |
2704 then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1" |
2647 by (metis setparts(1) subset_trans in_set_takeD wfactorsE wfactors_prod_exists) |
|
2648 then obtain aa_1 where aa1carr [simp]: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1" |
2705 by auto |
2649 by auto |
2706 |
2650 obtain aa_2 where aa2carr [simp]: "aa_2 \<in> carrier G" |
2707 have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2" |
|
2708 by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists) |
|
2709 then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G" |
|
2710 and aa2fs: "wfactors G (drop (Suc i) as') aa_2" |
2651 and aa2fs: "wfactors G (drop (Suc i) as') aa_2" |
2711 by auto |
2652 by (metis Cons.prems(2) Cons.prems(5) subset_code(1) in_set_dropD wfactors_def wfactors_prod_exists) |
2712 |
2653 |
2713 note carr = carr aa1carr[simp] aa2carr[simp] |
2654 have set_drop: "set (drop (Suc i) as') \<subseteq> carrier G" |
2714 |
2655 using Cons.prems(5) setparts(2) by blast |
2715 from aa1fs aa2fs |
2656 moreover have set_take: "set (take i as') \<subseteq> carrier G" |
2716 have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)" |
2657 using Cons.prems(5) setparts by auto |
2717 by (intro wfactors_mult, simp+) |
2658 moreover have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)" |
2718 then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))" |
2659 using aa1fs aa2fs \<open>set as' \<subseteq> carrier G\<close> by (force simp add: dest: in_set_takeD in_set_dropD) |
2719 using irrasi wfactors_mult_single by auto |
2660 ultimately have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))" |
2720 from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)" |
2661 using irrasi wfactors_mult_single |
2721 by (metis irrasi wfactors_mult_single) |
2662 by (simp add: irrasi v1 wfactors_mult_single) |
2722 with len carr aa1carr aa2carr aa1fs |
2663 have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)" |
|
2664 by (simp add: aa2fs irrasi set_drop wfactors_mult_single) |
|
2665 with len aa1carr aa2carr aa1fs |
2723 have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))" |
2666 have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))" |
2724 using wfactors_mult by auto |
2667 using wfactors_mult by (simp add: set_take set_drop) |
2725 from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')" |
2668 from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')" |
2726 by (simp add: Cons_nth_drop_Suc) |
2669 by (simp add: Cons_nth_drop_Suc) |
2727 with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'" |
2670 have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'" |
2728 by simp |
2671 using Cons.prems(5) as' by auto |
2729 with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a" |
2672 with v2 aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a" |
2730 by (metis as' ee_wfactorsD m_closed) |
2673 using Cons.prems as' comm_monoid_cancel.ee_wfactorsD is_comm_monoid_cancel by fastforce |
2731 then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" |
2674 then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" |
2732 by (metis aa1carr aa2carr asicarr m_lcomm) |
2675 by (metis aa1carr aa2carr asicarr m_lcomm) |
2733 from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)" |
2676 from asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)" |
2734 by (metis associated_sym m_closed mult_cong_l) |
2677 by (simp add: \<open>ah \<in> carrier G\<close> associated_sym mult_cong_l) |
2735 also note t1 |
2678 also note t1 |
2736 finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp |
2679 finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" |
2737 |
2680 using Cons.prems(3) carr_ah aa1carr aa2carr by blast |
2738 with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'" |
2681 with aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'" |
2739 by (simp add: a, fast intro: assoc_l_cancel[of ah _ a']) |
2682 using a assoc_l_cancel carr_ah(1) by blast |
2740 |
|
2741 note v1 |
2683 note v1 |
2742 also note a' |
2684 also note a' |
2743 finally have "wfactors G (take i as' @ drop (Suc i) as') a'" |
2685 finally have "wfactors G (take i as' @ drop (Suc i) as') a'" |
2744 by simp |
2686 by (simp add: a'carr set_drop set_take) |
2745 |
2687 from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')" |
2746 from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')" |
2688 using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto |
2747 by (intro ih[of a']) simp |
2689 with carr_ah have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" |
2748 then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" |
2690 by (auto simp: essentially_equal_def) |
2749 by (elim essentially_equalE) (fastforce intro: essentially_equalI) |
2691 have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as') |
2750 |
|
2751 from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as') |
|
2752 (as' ! i # take i as' @ drop (Suc i) as')" |
2692 (as' ! i # take i as' @ drop (Suc i) as')" |
2753 proof (intro essentially_equalI) |
2693 proof (intro essentially_equalI) |
2754 show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'" |
2694 show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'" |
2755 by simp |
2695 by simp |
2756 next |
2696 next |
2757 show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'" |
2697 show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'" |
2758 by (simp add: list_all2_append) (simp add: asiah[symmetric]) |
2698 by (simp add: asiah associated_sym set_drop set_take) |
2759 qed |
2699 qed |
2760 |
2700 |
2761 note ee1 |
2701 note ee1 |
2762 also note ee2 |
2702 also note ee2 |
2763 also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as') |
2703 also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as') |
2764 (take i as' @ as' ! i # drop (Suc i) as')" |
2704 (take i as' @ as' ! i # drop (Suc i) as')" |
2765 by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons) |
2705 by (metis Cons.prems(5) as' essentially_equalI listassoc_refl perm_append_Cons) |
2766 finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" |
2706 finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" |
2767 by simp |
2707 using Cons.prems(4) set_drop set_take by auto |
2768 then show "essentially_equal G (ah # as) as'" |
2708 then show ?case |
2769 by (subst as') |
2709 using as' by auto |
2770 qed |
2710 qed |
2771 qed |
|
2772 |
|
2773 lemma (in primeness_condition_monoid) wfactors_unique: |
|
2774 assumes "wfactors G as a" "wfactors G as' a" |
|
2775 and "a \<in> carrier G" "set as \<subseteq> carrier G" "set as' \<subseteq> carrier G" |
|
2776 shows "essentially_equal G as as'" |
|
2777 by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms) |
|
2778 |
2711 |
2779 |
2712 |
2780 subsubsection \<open>Application to factorial monoids\<close> |
2713 subsubsection \<open>Application to factorial monoids\<close> |
2781 |
2714 |
2782 text \<open>Number of factors for wellfoundedness\<close> |
2715 text \<open>Number of factors for wellfoundedness\<close> |