# HG changeset patch
# User haftmann
# Date 1325841587 -3600
# Node ID 229fcbebf73272b0abb311927e9f4531374ae00f
# Parent  53e7cc599f585421003ee0d22fe44b9033d65250
tuned proofs

diff -r 53e7cc599f58 -r 229fcbebf732 src/HOL/Algebra/Divisibility.thy
--- 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:
diff -r 53e7cc599f58 -r 229fcbebf732 src/HOL/Nominal/Examples/Standardization.thy
--- 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