summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Fri, 06 Jan 2012 10:19:47 +0100 | |

changeset 46129 | 229fcbebf732 |

parent 46128 | 53e7cc599f58 |

child 46130 | 4821af078cd6 |

tuned proofs

src/HOL/Algebra/Divisibility.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Nominal/Examples/Standardization.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Algebra/Divisibility.thy Sun Jan 01 15:44:15 2012 +0100 +++ b/src/HOL/Algebra/Divisibility.thy Fri Jan 06 10:19:47 2012 +0100 @@ -1283,9 +1283,10 @@ assumes anunit: "a \<notin> Units G" and fs: "factors G as a" shows "length as > 0" -apply (insert fs, elim factorsE) -apply (metis Units_one_closed assms(1) foldr.simps(1) length_greater_0_conv) -done +proof - + from anunit Units_one_closed have "a \<noteq> \<one>" by auto + with fs show ?thesis by (auto elim: factorsE) +qed lemma (in monoid) unit_wfactors [simp]: assumes aunit: "a \<in> Units G" @@ -3307,182 +3308,192 @@ lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct: "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'" -apply (induct as) -apply (metis Units_one_closed essentially_equal_def foldr.simps(1) is_monoid_cancel listassoc_refl monoid_cancel.assoc_unit_r perm_refl unit_wfactors_empty wfactorsE) -apply clarsimp -proof - - fix a as ah as' - assume ih[rule_format]: - "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> - wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'" - and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G" - and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G" - and afs: "wfactors G (ah # as) a" - and afs': "wfactors G as' a" - hence ahdvda: "ah divides a" +proof (induct as) + case Nil show ?case apply auto + proof - + fix a as' + assume a: "a \<in> carrier G" + assume "wfactors G [] a" + then obtain "\<one> \<sim> a" by (auto elim: wfactorsE) + with a have "a \<in> Units G" by (auto intro: assoc_unit_r) + moreover assume "wfactors G as' a" + moreover assume "set as' \<subseteq> carrier G" + ultimately have "as' = []" by (rule unit_wfactors_empty) + then show "essentially_equal G [] as'" by simp + qed +next + case (Cons ah as) then show ?case apply clarsimp + proof - + fix a as' + assume ih [rule_format]: + "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and> + wfactors G as' a \<longrightarrow> essentially_equal G as as'" + and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G" + and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G" + and afs: "wfactors G (ah # as) a" + and afs': "wfactors G as' a" + hence ahdvda: "ah divides a" by (intro wfactors_dividesI[of "ah#as" "a"], simp+) - hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE) - from this obtain a' + hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE) + from this obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'" by auto - have a'fs: "wfactors G as a'" - apply (rule wfactorsE[OF afs], rule wfactorsI, simp) - apply (simp add: a, insert ascarr a'carr) - apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+) - done - - from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp) - with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr) - - note carr [simp] = acarr ahcarr ascarr as'carr a'carr - - note ahdvda - also from afs' - have "a divides (foldr (op \<otimes>) as' \<one>)" - by (elim wfactorsE associatedE, simp) - finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp - - with ahprime + have a'fs: "wfactors G as a'" + apply (rule wfactorsE[OF afs], rule wfactorsI, simp) + apply (simp add: a, insert ascarr a'carr) + apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+) + done + from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp) + with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr) + + note carr [simp] = acarr ahcarr ascarr as'carr a'carr + + note ahdvda + also from afs' + have "a divides (foldr (op \<otimes>) as' \<one>)" + by (elim wfactorsE associatedE, simp) + finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp + + with ahprime have "\<exists>i<length as'. ah divides as'!i" by (intro multlist_prime_pos, simp+) - from this obtain i + from this obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i" by auto - from afs' carr have irrasi: "irreducible G (as'!i)" + from afs' carr have irrasi: "irreducible G (as'!i)" by (fast intro: nth_mem[OF len] elim: wfactorsE) - from len carr + from len carr have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force) - note carr = carr asicarr - - from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE) - from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto - - with carr irrasi[simplified asi] + note carr = carr asicarr + + from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE) + from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto + + with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah" apply - - apply (elim irreducible_prodE[of "ah" "x"], assumption+) - apply (rule associatedI2[of x], assumption+) - apply (rule irreducibleE[OF ahirr], simp) - done - - note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as'] - note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]] - note carr = carr partscarr - - have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1" - apply (intro wfactors_prod_exists) - using setparts afs' by (fast elim: wfactorsE, simp) - from this obtain aa_1 - where aa1carr: "aa_1 \<in> carrier G" - and aa1fs: "wfactors G (take i as') aa_1" - by auto - - have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2" - apply (intro wfactors_prod_exists) - using setparts afs' by (fast elim: wfactorsE, simp) - from this obtain aa_2 - where aa2carr: "aa_2 \<in> carrier G" - and aa2fs: "wfactors G (drop (Suc i) as') aa_2" - by auto - - note carr = carr aa1carr[simp] aa2carr[simp] - - from aa1fs aa2fs + apply (elim irreducible_prodE[of "ah" "x"], assumption+) + apply (rule associatedI2[of x], assumption+) + apply (rule irreducibleE[OF ahirr], simp) + done + + note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as'] + note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]] + note carr = carr partscarr + + have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1" + apply (intro wfactors_prod_exists) + using setparts afs' by (fast elim: wfactorsE, simp) + from this obtain aa_1 + where aa1carr: "aa_1 \<in> carrier G" + and aa1fs: "wfactors G (take i as') aa_1" + by auto + + have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2" + apply (intro wfactors_prod_exists) + using setparts afs' by (fast elim: wfactorsE, simp) + from this obtain aa_2 + where aa2carr: "aa_2 \<in> carrier G" + and aa2fs: "wfactors G (drop (Suc i) as') aa_2" + by auto + + note carr = carr aa1carr[simp] aa2carr[simp] + + from aa1fs aa2fs have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)" by (intro wfactors_mult, simp+) - hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))" + hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))" apply (intro wfactors_mult_single) using setparts afs' by (fast intro: nth_mem[OF len] elim: wfactorsE, simp+) - from aa2carr carr aa1fs aa2fs + from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)" - apply (intro wfactors_mult_single) - apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len]) - apply (fast intro: nth_mem[OF len]) - apply fast - apply fast - apply assumption - done - with len carr aa1carr aa2carr aa1fs + apply (intro wfactors_mult_single) + apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len]) + apply (fast intro: nth_mem[OF len]) + apply fast + apply fast + apply assumption + done + with len carr aa1carr aa2carr aa1fs have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))" - apply (intro wfactors_mult) - apply fast - apply (simp, (fast intro: nth_mem[OF len])?)+ - done - - from len + apply (intro wfactors_mult) + apply fast + apply (simp, (fast intro: nth_mem[OF len])?)+ + done + + from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')" by (simp add: drop_Suc_conv_tl) - with carr + with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'" by simp - with v2 afs' carr aa1carr aa2carr nth_mem[OF len] + with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a" - apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'" "as'"]) - apply fast+ - apply (simp, fast) - done - then - have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" - apply (simp add: m_assoc[symmetric]) - apply (simp add: m_comm) - done - from carr asiah - have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)" + apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'" "as'"]) + apply fast+ + apply (simp, fast) + done + then + have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" + apply (simp add: m_assoc[symmetric]) + apply (simp add: m_comm) + done + from carr asiah + have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)" apply (intro mult_cong_l) apply (fast intro: associated_sym, simp+) - done - also note t1 - finally + done + also note t1 + finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp - with carr aa1carr aa2carr a'carr nth_mem[OF len] + with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'" by (simp add: a, fast intro: assoc_l_cancel[of ah _ a']) - note v1 - also note a' - finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp - - from a'fs this carr + note v1 + also note a' + finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp + + from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')" by (intro ih[of a']) simp - hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" - apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI) - done - - from carr - have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as') - (as' ! i # take i as' @ drop (Suc i) as')" - proof (intro essentially_equalI) - show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'" + hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')" + apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI) + done + + from carr + have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as') + (as' ! i # take i as' @ drop (Suc i) as')" + proof (intro essentially_equalI) + show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'" by simp - next show "ah # take i as' @ drop (Suc i) as' [\<sim>] - as' ! i # take i as' @ drop (Suc i) as'" - apply (simp add: list_all2_append) - apply (simp add: asiah[symmetric] ahcarr asicarr) + next + show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'" + apply (simp add: list_all2_append) + apply (simp add: asiah[symmetric] ahcarr asicarr) + done + qed + + note ee1 + also note ee2 + also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as') + (take i as' @ as' ! i # drop (Suc i) as')" + apply (intro essentially_equalI) + apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> + take i as' @ as' ! i # drop (Suc i) as'") + apply simp + apply (rule perm_append_Cons) + apply simp done + finally + have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp + then show "essentially_equal G (ah # as) as'" by (subst as', assumption) qed - - note ee1 - also note ee2 - also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as') - (take i as' @ as' ! i # drop (Suc i) as')" - apply (intro essentially_equalI) - apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~> - take i as' @ as' ! i # drop (Suc i) as'") -apply simp - apply (rule perm_append_Cons) - apply simp - done - finally - have "essentially_equal G (ah # as) - (take i as' @ as' ! i # drop (Suc i) as')" by simp - - thus "essentially_equal G (ah # as) as'" by (subst as', assumption) qed lemma (in primeness_condition_monoid) wfactors_unique:

--- a/src/HOL/Nominal/Examples/Standardization.thy Sun Jan 01 15:44:15 2012 +0100 +++ b/src/HOL/Nominal/Examples/Standardization.thy Fri Jan 06 10:19:47 2012 +0100 @@ -212,8 +212,8 @@ apply (erule allE, erule impE) prefer 2 apply (erule allE, erule impE, rule refl, erule spec) - apply simp - apply (metis add_strict_increasing le_add1 length_pos_if_in_set listsum_foldl listsum_map_remove1 nat_add_commute) + apply simp + apply (clarsimp simp add: foldr_conv_foldl [symmetric] foldr_def fold_plus_listsum_rev listsum_map_remove1) apply clarify apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)") prefer 2