prefer ephemeral interpretation over interpretation in proof contexts;
prefer context begin ... end blocks for often-occuring assumptions;
slightly more complete interpretations into abstract algebraic structures for gcd/lcm

--- a/src/HOL/Finite_Set.thy	Wed Dec 25 22:35:29 2013 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Dec 26 22:47:49 2013 +0100
@@ -1085,6 +1085,9 @@
   assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
 begin
 
+interpretation comp_fun_commute f
+  by default (insert comp_fun_commute, simp add: fun_eq_iff)
+
 definition F :: "'a set \<Rightarrow> 'b"
 where
   eq_fold: "F A = fold f z A"
@@ -1101,8 +1104,6 @@
   assumes "finite A" and "x \<notin> A"
   shows "F (insert x A) = f x (F A)"
 proof -
-  interpret comp_fun_commute f
-    by default (insert comp_fun_commute, simp add: fun_eq_iff)
   from fold_insert assms
   have "fold f z (insert x A) = f x (fold f z A)" by simp
   with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
@@ -1134,12 +1135,13 @@
 
 declare insert [simp del]
 
+interpretation comp_fun_idem f
+  by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
+
 lemma insert_idem [simp]:
   assumes "finite A"
   shows "F (insert x A) = f x (F A)"
 proof -
-  interpret comp_fun_idem f
-    by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
   from fold_insert_idem assms
   have "fold f z (insert x A) = f x (fold f z A)" by simp
   with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)

--- a/src/HOL/GCD.thy	Wed Dec 25 22:35:29 2013 +0100
+++ b/src/HOL/GCD.thy	Thu Dec 26 22:47:49 2013 +0100
@@ -197,14 +197,14 @@
   by (simp add: lcm_int_def)
 
 (* was gcd_0, etc. *)
-lemma gcd_0_nat [simp]: "gcd (x::nat) 0 = x"
+lemma gcd_0_nat: "gcd (x::nat) 0 = x"
   by simp
 
 (* was igcd_0, etc. *)
 lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
   by (unfold gcd_int_def, auto)
 
-lemma gcd_0_left_nat [simp]: "gcd 0 (x::nat) = x"
+lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
   by simp
 
 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
@@ -243,7 +243,7 @@
 lemma gcd_dvd1_nat [iff]: "(gcd (m::nat)) n dvd m"
   and gcd_dvd2_nat [iff]: "(gcd m n) dvd n"
   apply (induct m n rule: gcd_nat_induct)
-  apply (simp_all add: gcd_non_0_nat)
+  apply (simp_all add: gcd_non_0_nat gcd_0_nat)
   apply (blast dest: dvd_mod_imp_dvd)
 done
 
@@ -278,7 +278,7 @@
   by (rule zdvd_imp_le, auto)
 
 lemma gcd_greatest_nat: "(k::nat) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
-by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod)
+by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
 
 lemma gcd_greatest_int:
   "(k::int) dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd m n"
@@ -307,25 +307,6 @@
 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
 
-interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
-proof
-qed (auto intro: dvd_antisym dvd_trans)
-
-interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
-proof
-qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
-
-lemmas gcd_assoc_nat = gcd_nat.assoc
-lemmas gcd_commute_nat = gcd_nat.commute
-lemmas gcd_left_commute_nat = gcd_nat.left_commute
-lemmas gcd_assoc_int = gcd_int.assoc
-lemmas gcd_commute_int = gcd_int.commute
-lemmas gcd_left_commute_int = gcd_int.left_commute
-
-lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
-
-lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
-
 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   apply auto
@@ -343,18 +324,40 @@
  apply (auto intro: gcd_greatest_int)
 done
 
+interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  + gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
+apply default
+apply (auto intro: dvd_antisym dvd_trans)[4]
+apply (metis dvd.dual_order.refl gcd_unique_nat)
+apply (auto intro: dvdI elim: dvdE)
+done
+
+interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
+proof
+qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
+
+lemmas gcd_assoc_nat = gcd_nat.assoc
+lemmas gcd_commute_nat = gcd_nat.commute
+lemmas gcd_left_commute_nat = gcd_nat.left_commute
+lemmas gcd_assoc_int = gcd_int.assoc
+lemmas gcd_commute_int = gcd_int.commute
+lemmas gcd_left_commute_int = gcd_int.left_commute
+
+lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
+
+lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
+
 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
-by (metis dvd.eq_iff gcd_unique_nat)
+  by (fact gcd_nat.absorb1)
 
 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
-by (metis dvd.eq_iff gcd_unique_nat)
+  by (fact gcd_nat.absorb2)
 
-lemma gcd_proj1_if_dvd_int[simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
-by (metis abs_dvd_iff abs_eq_0 gcd_0_left_int gcd_abs_int gcd_unique_int)
+lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
+  by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
 
-lemma gcd_proj2_if_dvd_int[simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
-by (metis gcd_proj1_if_dvd_int gcd_commute_int)
-
+lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
+  by (metis gcd_proj1_if_dvd_int gcd_commute_int)
 
 text {*
   \medskip Multiplication laws
@@ -1391,12 +1394,17 @@
   by (auto intro: dvd_antisym [transferred] lcm_least_int)
 
 interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
+  + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
 proof
   fix n m p :: nat
   show "lcm (lcm n m) p = lcm n (lcm m p)"
     by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
   show "lcm m n = lcm n m"
     by (simp add: lcm_nat_def gcd_commute_nat field_simps)
+  show "lcm m m = m"
+    by (metis dvd.order_refl lcm_unique_nat)
+  show "lcm m 1 = m"
+    by (metis dvd.dual_order.refl lcm_unique_nat one_dvd)
 qed
 
 interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
@@ -1478,10 +1486,6 @@
 
 subsection {* The complete divisibility lattice *}
 
-lemma semilattice_neutr_set_lcm_one_nat:
-  "semilattice_neutr_set lcm (1::nat)"
-  by default simp_all
-
 interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
 proof
   case goal3 thus ?case by(metis gcd_unique_nat)
@@ -1508,28 +1512,19 @@
 definition
   "Lcm (M::nat set) = (if finite M then semilattice_neutr_set.F lcm 1 M else 0)"
 
+interpretation semilattice_neutr_set lcm "1::nat" ..
+
 lemma Lcm_nat_infinite:
   "\<not> finite M \<Longrightarrow> Lcm M = (0::nat)"
   by (simp add: Lcm_nat_def)
 
 lemma Lcm_nat_empty:
   "Lcm {} = (1::nat)"
-proof -
-  interpret semilattice_neutr_set lcm "1::nat"
-    by (fact semilattice_neutr_set_lcm_one_nat)
-  show ?thesis by (simp add: Lcm_nat_def)
-qed
+  by (simp add: Lcm_nat_def)
 
 lemma Lcm_nat_insert:
   "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
-proof (cases "finite M")
-  interpret semilattice_neutr_set lcm "1::nat"
-    by (fact semilattice_neutr_set_lcm_one_nat)
-  case True
-  then show ?thesis by (simp add: Lcm_nat_def)
-next
-  case False then show ?thesis by (simp add: Lcm_nat_infinite)
-qed
+  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
 
 definition
   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
@@ -1587,7 +1582,7 @@
 qed
 
 lemma Lcm_empty_nat: "Lcm {} = (1::nat)"
-  by (fact gcd_lcm_complete_lattice_nat.Sup_empty) (* already simp *)
+  by (fact Lcm_nat_empty)
 
 lemma Gcd_empty_nat: "Gcd {} = (0::nat)"
   by (fact gcd_lcm_complete_lattice_nat.Inf_empty) (* already simp *)
@@ -1688,6 +1683,7 @@
 lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
 
+
 subsubsection {* Setwise gcd and lcm for integers *}
 
 instantiation int :: Gcd

--- a/src/HOL/Quotient.thy	Wed Dec 25 22:35:29 2013 +0100
+++ b/src/HOL/Quotient.thy	Thu Dec 26 22:47:49 2013 +0100
@@ -46,75 +46,94 @@
   shows "Quotient3 R Abs Rep"
   using assms unfolding Quotient3_def by blast
 
-lemma Quotient3_abs_rep:
+context
+  fixes R Abs Rep
   assumes a: "Quotient3 R Abs Rep"
-  shows "Abs (Rep a) = a"
+begin
+
+lemma Quotient3_abs_rep:
+  "Abs (Rep a) = a"
   using a
   unfolding Quotient3_def
   by simp
 
 lemma Quotient3_rep_reflp:
-  assumes a: "Quotient3 R Abs Rep"
-  shows "R (Rep a) (Rep a)"
+  "R (Rep a) (Rep a)"
   using a
   unfolding Quotient3_def
   by blast
 
 lemma Quotient3_rel:
-  assumes a: "Quotient3 R Abs Rep"
-  shows "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
+  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
   using a
   unfolding Quotient3_def
   by blast
 
 lemma Quotient3_refl1: 
-  assumes a: "Quotient3 R Abs Rep" 
-  shows "R r s \<Longrightarrow> R r r"
+  "R r s \<Longrightarrow> R r r"
   using a unfolding Quotient3_def 
   by fast
 
 lemma Quotient3_refl2: 
-  assumes a: "Quotient3 R Abs Rep" 
-  shows "R r s \<Longrightarrow> R s s"
+  "R r s \<Longrightarrow> R s s"
   using a unfolding Quotient3_def 
   by fast
 
 lemma Quotient3_rel_rep:
-  assumes a: "Quotient3 R Abs Rep"
-  shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
+  "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
   using a
   unfolding Quotient3_def
   by metis
 
 lemma Quotient3_rep_abs:
-  assumes a: "Quotient3 R Abs Rep"
-  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
+  "R r r \<Longrightarrow> R (Rep (Abs r)) r"
   using a unfolding Quotient3_def
   by blast
 
 lemma Quotient3_rel_abs:
-  assumes a: "Quotient3 R Abs Rep"
-  shows "R r s \<Longrightarrow> Abs r = Abs s"
+  "R r s \<Longrightarrow> Abs r = Abs s"
   using a unfolding Quotient3_def
   by blast
 
 lemma Quotient3_symp:
-  assumes a: "Quotient3 R Abs Rep"
-  shows "symp R"
+  "symp R"
   using a unfolding Quotient3_def using sympI by metis
 
 lemma Quotient3_transp:
-  assumes a: "Quotient3 R Abs Rep"
-  shows "transp R"
+  "transp R"
   using a unfolding Quotient3_def using transpI by (metis (full_types))
 
 lemma Quotient3_part_equivp:
-  assumes a: "Quotient3 R Abs Rep"
-  shows "part_equivp R"
-by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp a part_equivpI)
+  "part_equivp R"
+  by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI)
+
+lemma abs_o_rep:
+  "Abs o Rep = id"
+  unfolding fun_eq_iff
+  by (simp add: Quotient3_abs_rep)
+
+lemma equals_rsp:
+  assumes b: "R xa xb" "R ya yb"
+  shows "R xa ya = R xb yb"
+  using b Quotient3_symp Quotient3_transp
+  by (blast elim: sympE transpE)
+
+lemma rep_abs_rsp:
+  assumes b: "R x1 x2"
+  shows "R x1 (Rep (Abs x2))"
+  using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
+  by metis
+
+lemma rep_abs_rsp_left:
+  assumes b: "R x1 x2"
+  shows "R (Rep (Abs x1)) x2"
+  using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
+  by metis
+
+end
 
 lemma identity_quotient3:
-  shows "Quotient3 (op =) id id"
+  "Quotient3 (op =) id id"
   unfolding Quotient3_def id_def
   by blast
 
@@ -157,19 +176,6 @@
  ultimately show ?thesis by (intro Quotient3I) (assumption+)
 qed
 
-lemma abs_o_rep:
-  assumes a: "Quotient3 R Abs Rep"
-  shows "Abs o Rep = id"
-  unfolding fun_eq_iff
-  by (simp add: Quotient3_abs_rep[OF a])
-
-lemma equals_rsp:
-  assumes q: "Quotient3 R Abs Rep"
-  and     a: "R xa xb" "R ya yb"
-  shows "R xa ya = R xb yb"
-  using a Quotient3_symp[OF q] Quotient3_transp[OF q]
-  by (blast elim: sympE transpE)
-
 lemma lambda_prs:
   assumes q1: "Quotient3 R1 Abs1 Rep1"
   and     q2: "Quotient3 R2 Abs2 Rep2"
@@ -186,20 +192,6 @@
   using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
   by simp
 
-lemma rep_abs_rsp:
-  assumes q: "Quotient3 R Abs Rep"
-  and     a: "R x1 x2"
-  shows "R x1 (Rep (Abs x2))"
-  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
-  by metis
-
-lemma rep_abs_rsp_left:
-  assumes q: "Quotient3 R Abs Rep"
-  and     a: "R x1 x2"
-  shows "R (Rep (Abs x1)) x2"
-  using a Quotient3_rel[OF q] Quotient3_abs_rep[OF q] Quotient3_rep_reflp[OF q]
-  by metis
-
 text{*
   In the following theorem R1 can be instantiated with anything,
   but we know some of the types of the Rep and Abs functions;