# HG changeset patch
# User haftmann
# Date 1289315920 -3600
# Node ID 2878445aa7d54a28a41d19d498610460360ab65f
# Parent  f208cb239da152b68fb6f5744fce0751b41cf757# Parent  89ee82ee0e0f83a074bc1daea7eb756d1eb4d842
merged

diff -r f208cb239da1 -r 2878445aa7d5 doc-src/pdfsetup.sty
--- a/doc-src/pdfsetup.sty	Tue Nov 09 14:02:14 2010 +0100
+++ b/doc-src/pdfsetup.sty	Tue Nov 09 16:18:40 2010 +0100
@@ -15,6 +15,9 @@
 \urlstyle{rm}
 \ifpdf\relax\else\renewcommand{\url}[1]{\nolinkurl{#1}}\fi
 
+\def\isaliteral#1#2{#2}
+\def\isanil{}
+
 \ifpdf
 \ifnum\pdfminorversion<5\pdfminorversion=5\fi
 \renewcommand{\isaliteral}[2]{%
diff -r f208cb239da1 -r 2878445aa7d5 etc/symbols
--- a/etc/symbols	Tue Nov 09 14:02:14 2010 +0100
+++ b/etc/symbols	Tue Nov 09 16:18:40 2010 +0100
@@ -181,7 +181,7 @@
 \<downharpoonleft>      code: 0x0021c3  font: Isabelle
 \<downharpoonright>     code: 0x0021c2  font: Isabelle
 \<upharpoonleft>        code: 0x0021bf  font: Isabelle
-\<upharpoonright>       code: 0x0021be  font: Isabelle
+#\<upharpoonright>       code: 0x0021be  font: Isabelle
 \<restriction>          code: 0x0021be  font: Isabelle
 \<Colon>                code: 0x002237  font: Isabelle
 \<up>                   code: 0x002191  font: Isabelle
diff -r f208cb239da1 -r 2878445aa7d5 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Tue Nov 09 14:02:14 2010 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Tue Nov 09 16:18:40 2010 +0100
@@ -88,11 +88,7 @@
 
 lemma prime_odd_nat: "prime (p::nat) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   unfolding prime_nat_def
-  apply (subst even_mult_two_ex)
-  apply clarify
-  apply (drule_tac x = 2 in spec)
-  apply auto
-done
+  by (metis gcd_lcm_complete_lattice_nat.bot_least nat_even_iff_2_dvd nat_neq_iff odd_1_nat)
 
 lemma prime_odd_int: "prime (p::int) \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   unfolding prime_int_def
@@ -275,10 +271,8 @@
 
 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   apply (rule prime_imp_coprime_int, assumption)
-  apply (unfold prime_int_altdef, clarify)
-  apply (drule_tac x = q in spec)
-  apply (drule_tac x = p in spec)
-  apply auto
+  apply (unfold prime_int_altdef)
+  apply (metis int_one_le_iff_zero_less zless_le)
 done
 
 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
@@ -291,11 +285,8 @@
   apply (induct n rule: nat_less_induct)
   apply (case_tac "n = 0")
   using two_is_prime_nat apply blast
-  apply (case_tac "prime n")
-  apply blast
-  apply (subgoal_tac "n > 1")
-  apply (frule (1) not_prime_eq_prod_nat)
-  apply (auto intro: dvd_mult dvd_mult2)
+  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat nat_dvd_not_less 
+               neq0_conv prime_nat_def)
 done
 
 (* An Isar version:
diff -r f208cb239da1 -r 2878445aa7d5 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Tue Nov 09 14:02:14 2010 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Tue Nov 09 16:18:40 2010 +0100
@@ -691,14 +691,9 @@
   apply (frule multiplicity_prod_prime_powers_nat [where f = "%x. f(int x)" 
     and S = "nat ` S", transferred])
   apply auto
-  apply (subst prime_int_def [symmetric])
-  apply auto
-  apply (subgoal_tac "xb >= 0")
-  apply force
-  apply (rule prime_ge_0_int)
-  apply force
-  apply (subst transfer_nat_int_set_return_embed)
-  apply (unfold nat_set_def, auto)
+  apply (metis prime_int_def)
+  apply (metis prime_ge_0_int)
+  apply (metis nat_set_def prime_ge_0_int transfer_nat_int_set_return_embed)
 done
 
 lemma multiplicity_distinct_prime_power_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow>
@@ -739,19 +734,13 @@
     "0 < (y::nat) \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   apply (simp only: prime_factors_altdef_nat)
   apply auto
-  apply (frule dvd_multiplicity_nat)
-  apply auto
-(* It is a shame that auto and arith don't get this. *)
-  apply (erule order_less_le_trans)back
-  apply assumption
+  apply (metis dvd_multiplicity_nat le_0_eq neq_zero_eq_gt_zero_nat)
 done
 
 lemma dvd_prime_factors_int [intro]:
     "0 < (y::int) \<Longrightarrow> 0 <= x \<Longrightarrow> x dvd y \<Longrightarrow> prime_factors x <= prime_factors y"
   apply (auto simp add: prime_factors_altdef_int)
-  apply (erule order_less_le_trans)
-  apply (rule dvd_multiplicity_int)
-  apply auto
+  apply (metis dvd_multiplicity_int le_0_eq neq_zero_eq_gt_zero_nat)
 done
 
 lemma multiplicity_dvd_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow> 
@@ -763,10 +752,8 @@
   apply force
   apply (subst prime_factors_altdef_nat)+
   apply auto
-(* Again, a shame that auto and arith don't get this. *)
-  apply (drule_tac x = xa in spec, auto)
-  apply (rule le_imp_power_dvd)
-  apply blast
+  apply (metis gr0I le_0_eq less_not_refl)
+  apply (metis le_imp_power_dvd)
 done
 
 lemma multiplicity_dvd_int: "0 < (x::int) \<Longrightarrow> 0 < y \<Longrightarrow> 
@@ -778,30 +765,18 @@
   apply force
   apply (subst prime_factors_altdef_int)+
   apply auto
-  apply (rule dvd_power_le)
-  apply auto
-  apply (drule_tac x = xa in spec)
-  apply (erule impE)
-  apply auto
+  apply (metis le_imp_power_dvd prime_factors_ge_0_int)
 done
 
 lemma multiplicity_dvd'_nat: "(0::nat) < x \<Longrightarrow> 
     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-  apply (cases "y = 0")
-  apply auto
-  apply (rule multiplicity_dvd_nat, auto)
-  apply (case_tac "prime p")
-  apply auto
-done
+by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
+          multiplicity_nonprime_nat neq0_conv)
 
 lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-  apply (cases "y = 0")
-  apply auto
-  apply (rule multiplicity_dvd_int, auto)
-  apply (case_tac "prime p")
-  apply auto
-done
+by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
+          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
 
 lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
     (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
@@ -820,12 +795,8 @@
   apply (rule dvd_power [where x = p and n = "multiplicity p n"])
   apply (subst (asm) prime_factors_altdef_nat, force)
   apply (rule dvd_setprod)
-  apply auto  
-  apply (subst prime_factors_altdef_nat)
-  apply (subst (asm) dvd_multiplicity_eq_nat)
   apply auto
-  apply (drule spec [where x = p])
-  apply auto
+  apply (metis One_nat_def Zero_not_Suc dvd_multiplicity_nat le0 le_antisym multiplicity_not_factor_nat multiplicity_prime_nat)  
 done
 
 lemma prime_factors_altdef2_int: 
diff -r f208cb239da1 -r 2878445aa7d5 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Nov 09 14:02:14 2010 +0100
+++ b/src/Pure/General/symbol.scala	Tue Nov 09 16:18:40 2010 +0100
@@ -146,7 +146,18 @@
       }
       (min, max)
     }
-    private val table = Map[String, String]() ++ list
+    private val table =
+    {
+      var tab = Map[String, String]()
+      for ((x, y) <- list) {
+        tab.get(x) match {
+          case None => tab += (x -> y)
+          case Some(z) =>
+            error("Duplicate mapping of \"" + x + "\" to \"" + y + "\" vs. \"" + z + "\"")
+        }
+      }
+      tab
+    }
     def recode(text: String): String =
     {
       val len = text.length
@@ -198,8 +209,9 @@
     }
 
     private val symbols: List[(String, Map[String, String])] =
-      for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
-        yield read_decl(decl)
+      Map((
+        for (decl <- symbol_decls if !empty.pattern.matcher(decl).matches)
+          yield read_decl(decl)): _*) toList
 
 
     /* misc properties */
@@ -210,9 +222,10 @@
       Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     }
 
-    val abbrevs: Map[String, String] = Map((
-      for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
-        yield (sym -> props("abbrev"))): _*)
+    val abbrevs: Map[String, String] =
+      Map((
+        for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
+          yield (sym -> props("abbrev"))): _*)
 
 
     /* main recoder methods */