1.1 --- a/src/HOL/Algebra/Divisibility.thy Sun Jan 01 15:44:15 2012 +0100
1.2 +++ b/src/HOL/Algebra/Divisibility.thy Fri Jan 06 10:19:47 2012 +0100
1.3 @@ -1283,9 +1283,10 @@
1.4 assumes anunit: "a \<notin> Units G"
1.5 and fs: "factors G as a"
1.6 shows "length as > 0"
1.7 -apply (insert fs, elim factorsE)
1.8 -apply (metis Units_one_closed assms(1) foldr.simps(1) length_greater_0_conv)
1.9 -done
1.10 +proof -
1.11 + from anunit Units_one_closed have "a \<noteq> \<one>" by auto
1.12 + with fs show ?thesis by (auto elim: factorsE)
1.13 +qed
1.14
1.15 lemma (in monoid) unit_wfactors [simp]:
1.16 assumes aunit: "a \<in> Units G"
1.17 @@ -3307,182 +3308,192 @@
1.18 lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
1.19 "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>
1.20 wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
1.21 -apply (induct as)
1.22 -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)
1.23 -apply clarsimp
1.24 -proof -
1.25 - fix a as ah as'
1.26 - assume ih[rule_format]:
1.27 - "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and>
1.28 - wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
1.29 - and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
1.30 - and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
1.31 - and afs: "wfactors G (ah # as) a"
1.32 - and afs': "wfactors G as' a"
1.33 - hence ahdvda: "ah divides a"
1.34 +proof (induct as)
1.35 + case Nil show ?case apply auto
1.36 + proof -
1.37 + fix a as'
1.38 + assume a: "a \<in> carrier G"
1.39 + assume "wfactors G [] a"
1.40 + then obtain "\<one> \<sim> a" by (auto elim: wfactorsE)
1.41 + with a have "a \<in> Units G" by (auto intro: assoc_unit_r)
1.42 + moreover assume "wfactors G as' a"
1.43 + moreover assume "set as' \<subseteq> carrier G"
1.44 + ultimately have "as' = []" by (rule unit_wfactors_empty)
1.45 + then show "essentially_equal G [] as'" by simp
1.46 + qed
1.47 +next
1.48 + case (Cons ah as) then show ?case apply clarsimp
1.49 + proof -
1.50 + fix a as'
1.51 + assume ih [rule_format]:
1.52 + "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>
1.53 + wfactors G as' a \<longrightarrow> essentially_equal G as as'"
1.54 + and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
1.55 + and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
1.56 + and afs: "wfactors G (ah # as) a"
1.57 + and afs': "wfactors G as' a"
1.58 + hence ahdvda: "ah divides a"
1.59 by (intro wfactors_dividesI[of "ah#as" "a"], simp+)
1.60 - hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
1.61 - from this obtain a'
1.62 + hence "\<exists>a'\<in> carrier G. a = ah \<otimes> a'" by (fast elim: dividesE)
1.63 + from this obtain a'
1.64 where a'carr: "a' \<in> carrier G"
1.65 and a: "a = ah \<otimes> a'"
1.66 by auto
1.67 - have a'fs: "wfactors G as a'"
1.68 - apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
1.69 - apply (simp add: a, insert ascarr a'carr)
1.70 - apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
1.71 - done
1.72 -
1.73 - from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp)
1.74 - with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr)
1.75 -
1.76 - note carr [simp] = acarr ahcarr ascarr as'carr a'carr
1.77 -
1.78 - note ahdvda
1.79 - also from afs'
1.80 - have "a divides (foldr (op \<otimes>) as' \<one>)"
1.81 - by (elim wfactorsE associatedE, simp)
1.82 - finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp
1.83 -
1.84 - with ahprime
1.85 + have a'fs: "wfactors G as a'"
1.86 + apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
1.87 + apply (simp add: a, insert ascarr a'carr)
1.88 + apply (intro assoc_l_cancel[of ah _ a'] multlist_closed ahcarr, assumption+)
1.89 + done
1.90 + from afs have ahirr: "irreducible G ah" by (elim wfactorsE, simp)
1.91 + with ascarr have ahprime: "prime G ah" by (intro irreducible_prime ahcarr)
1.92 +
1.93 + note carr [simp] = acarr ahcarr ascarr as'carr a'carr
1.94 +
1.95 + note ahdvda
1.96 + also from afs'
1.97 + have "a divides (foldr (op \<otimes>) as' \<one>)"
1.98 + by (elim wfactorsE associatedE, simp)
1.99 + finally have "ah divides (foldr (op \<otimes>) as' \<one>)" by simp
1.100 +
1.101 + with ahprime
1.102 have "\<exists>i<length as'. ah divides as'!i"
1.103 by (intro multlist_prime_pos, simp+)
1.104 - from this obtain i
1.105 + from this obtain i
1.106 where len: "i<length as'" and ahdvd: "ah divides as'!i"
1.107 by auto
1.108 - from afs' carr have irrasi: "irreducible G (as'!i)"
1.109 + from afs' carr have irrasi: "irreducible G (as'!i)"
1.110 by (fast intro: nth_mem[OF len] elim: wfactorsE)
1.111 - from len carr
1.112 + from len carr
1.113 have asicarr[simp]: "as'!i \<in> carrier G" by (unfold set_conv_nth, force)
1.114 - note carr = carr asicarr
1.115 -
1.116 - from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
1.117 - from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
1.118 -
1.119 - with carr irrasi[simplified asi]
1.120 + note carr = carr asicarr
1.121 +
1.122 + from ahdvd have "\<exists>x \<in> carrier G. as'!i = ah \<otimes> x" by (fast elim: dividesE)
1.123 + from this obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x" by auto
1.124 +
1.125 + with carr irrasi[simplified asi]
1.126 have asiah: "as'!i \<sim> ah" apply -
1.127 - apply (elim irreducible_prodE[of "ah" "x"], assumption+)
1.128 - apply (rule associatedI2[of x], assumption+)
1.129 - apply (rule irreducibleE[OF ahirr], simp)
1.130 - done
1.131 -
1.132 - note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
1.133 - note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
1.134 - note carr = carr partscarr
1.135 -
1.136 - have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
1.137 - apply (intro wfactors_prod_exists)
1.138 - using setparts afs' by (fast elim: wfactorsE, simp)
1.139 - from this obtain aa_1
1.140 - where aa1carr: "aa_1 \<in> carrier G"
1.141 - and aa1fs: "wfactors G (take i as') aa_1"
1.142 - by auto
1.143 -
1.144 - have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
1.145 - apply (intro wfactors_prod_exists)
1.146 - using setparts afs' by (fast elim: wfactorsE, simp)
1.147 - from this obtain aa_2
1.148 - where aa2carr: "aa_2 \<in> carrier G"
1.149 - and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
1.150 - by auto
1.151 -
1.152 - note carr = carr aa1carr[simp] aa2carr[simp]
1.153 -
1.154 - from aa1fs aa2fs
1.155 + apply (elim irreducible_prodE[of "ah" "x"], assumption+)
1.156 + apply (rule associatedI2[of x], assumption+)
1.157 + apply (rule irreducibleE[OF ahirr], simp)
1.158 + done
1.159 +
1.160 + note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
1.161 + note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
1.162 + note carr = carr partscarr
1.163 +
1.164 + have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
1.165 + apply (intro wfactors_prod_exists)
1.166 + using setparts afs' by (fast elim: wfactorsE, simp)
1.167 + from this obtain aa_1
1.168 + where aa1carr: "aa_1 \<in> carrier G"
1.169 + and aa1fs: "wfactors G (take i as') aa_1"
1.170 + by auto
1.171 +
1.172 + have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
1.173 + apply (intro wfactors_prod_exists)
1.174 + using setparts afs' by (fast elim: wfactorsE, simp)
1.175 + from this obtain aa_2
1.176 + where aa2carr: "aa_2 \<in> carrier G"
1.177 + and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
1.178 + by auto
1.179 +
1.180 + note carr = carr aa1carr[simp] aa2carr[simp]
1.181 +
1.182 + from aa1fs aa2fs
1.183 have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
1.184 by (intro wfactors_mult, simp+)
1.185 - hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
1.186 + hence v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
1.187 apply (intro wfactors_mult_single)
1.188 using setparts afs'
1.189 by (fast intro: nth_mem[OF len] elim: wfactorsE, simp+)
1.190
1.191 - from aa2carr carr aa1fs aa2fs
1.192 + from aa2carr carr aa1fs aa2fs
1.193 have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
1.194 - apply (intro wfactors_mult_single)
1.195 - apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])
1.196 - apply (fast intro: nth_mem[OF len])
1.197 - apply fast
1.198 - apply fast
1.199 - apply assumption
1.200 - done
1.201 - with len carr aa1carr aa2carr aa1fs
1.202 + apply (intro wfactors_mult_single)
1.203 + apply (rule wfactorsE[OF afs'], fast intro: nth_mem[OF len])
1.204 + apply (fast intro: nth_mem[OF len])
1.205 + apply fast
1.206 + apply fast
1.207 + apply assumption
1.208 + done
1.209 + with len carr aa1carr aa2carr aa1fs
1.210 have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
1.211 - apply (intro wfactors_mult)
1.212 - apply fast
1.213 - apply (simp, (fast intro: nth_mem[OF len])?)+
1.214 - done
1.215 -
1.216 - from len
1.217 + apply (intro wfactors_mult)
1.218 + apply fast
1.219 + apply (simp, (fast intro: nth_mem[OF len])?)+
1.220 + done
1.221 +
1.222 + from len
1.223 have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
1.224 by (simp add: drop_Suc_conv_tl)
1.225 - with carr
1.226 + with carr
1.227 have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
1.228 by simp
1.229
1.230 - with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
1.231 + with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
1.232 have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
1.233 - apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'" "as'"])
1.234 - apply fast+
1.235 - apply (simp, fast)
1.236 - done
1.237 - then
1.238 - have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
1.239 - apply (simp add: m_assoc[symmetric])
1.240 - apply (simp add: m_comm)
1.241 - done
1.242 - from carr asiah
1.243 - have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
1.244 + apply (intro ee_wfactorsD[of "take i as' @ as'!i # drop (Suc i) as'" "as'"])
1.245 + apply fast+
1.246 + apply (simp, fast)
1.247 + done
1.248 + then
1.249 + have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
1.250 + apply (simp add: m_assoc[symmetric])
1.251 + apply (simp add: m_comm)
1.252 + done
1.253 + from carr asiah
1.254 + have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
1.255 apply (intro mult_cong_l)
1.256 apply (fast intro: associated_sym, simp+)
1.257 - done
1.258 - also note t1
1.259 - finally
1.260 + done
1.261 + also note t1
1.262 + finally
1.263 have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
1.264
1.265 - with carr aa1carr aa2carr a'carr nth_mem[OF len]
1.266 + with carr aa1carr aa2carr a'carr nth_mem[OF len]
1.267 have a': "aa_1 \<otimes> aa_2 \<sim> a'"
1.268 by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])
1.269
1.270 - note v1
1.271 - also note a'
1.272 - finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp
1.273 -
1.274 - from a'fs this carr
1.275 + note v1
1.276 + also note a'
1.277 + finally have "wfactors G (take i as' @ drop (Suc i) as') a'" by simp
1.278 +
1.279 + from a'fs this carr
1.280 have "essentially_equal G as (take i as' @ drop (Suc i) as')"
1.281 by (intro ih[of a']) simp
1.282
1.283 - hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
1.284 - apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI)
1.285 - done
1.286 -
1.287 - from carr
1.288 - have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
1.289 - (as' ! i # take i as' @ drop (Suc i) as')"
1.290 - proof (intro essentially_equalI)
1.291 - show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
1.292 + hence ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
1.293 + apply (elim essentially_equalE) apply (fastforce intro: essentially_equalI)
1.294 + done
1.295 +
1.296 + from carr
1.297 + have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
1.298 + (as' ! i # take i as' @ drop (Suc i) as')"
1.299 + proof (intro essentially_equalI)
1.300 + show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
1.301 by simp
1.302 - next show "ah # take i as' @ drop (Suc i) as' [\<sim>]
1.303 - as' ! i # take i as' @ drop (Suc i) as'"
1.304 - apply (simp add: list_all2_append)
1.305 - apply (simp add: asiah[symmetric] ahcarr asicarr)
1.306 + next
1.307 + show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
1.308 + apply (simp add: list_all2_append)
1.309 + apply (simp add: asiah[symmetric] ahcarr asicarr)
1.310 + done
1.311 + qed
1.312 +
1.313 + note ee1
1.314 + also note ee2
1.315 + also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
1.316 + (take i as' @ as' ! i # drop (Suc i) as')"
1.317 + apply (intro essentially_equalI)
1.318 + apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
1.319 + take i as' @ as' ! i # drop (Suc i) as'")
1.320 + apply simp
1.321 + apply (rule perm_append_Cons)
1.322 + apply simp
1.323 done
1.324 + finally
1.325 + have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')" by simp
1.326 + then show "essentially_equal G (ah # as) as'" by (subst as', assumption)
1.327 qed
1.328 -
1.329 - note ee1
1.330 - also note ee2
1.331 - also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
1.332 - (take i as' @ as' ! i # drop (Suc i) as')"
1.333 - apply (intro essentially_equalI)
1.334 - apply (subgoal_tac "as' ! i # take i as' @ drop (Suc i) as' <~~>
1.335 - take i as' @ as' ! i # drop (Suc i) as'")
1.336 -apply simp
1.337 - apply (rule perm_append_Cons)
1.338 - apply simp
1.339 - done
1.340 - finally
1.341 - have "essentially_equal G (ah # as)
1.342 - (take i as' @ as' ! i # drop (Suc i) as')" by simp
1.343 -
1.344 - thus "essentially_equal G (ah # as) as'" by (subst as', assumption)
1.345 qed
1.346
1.347 lemma (in primeness_condition_monoid) wfactors_unique:
2.1 --- a/src/HOL/Nominal/Examples/Standardization.thy Sun Jan 01 15:44:15 2012 +0100
2.2 +++ b/src/HOL/Nominal/Examples/Standardization.thy Fri Jan 06 10:19:47 2012 +0100
2.3 @@ -212,8 +212,8 @@
2.4 apply (erule allE, erule impE)
2.5 prefer 2
2.6 apply (erule allE, erule impE, rule refl, erule spec)
2.7 - apply simp
2.8 - apply (metis add_strict_increasing le_add1 length_pos_if_in_set listsum_foldl listsum_map_remove1 nat_add_commute)
2.9 + apply simp
2.10 + apply (clarsimp simp add: foldr_conv_foldl [symmetric] foldr_def fold_plus_listsum_rev listsum_map_remove1)
2.11 apply clarify
2.12 apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
2.13 prefer 2