src/HOL/GCD.thy
changeset 34973 ae634fad947e
parent 34915 7894c7dab132
child 35028 108662d50512
     1.1 --- a/src/HOL/GCD.thy	Wed Jan 27 14:03:08 2010 +0100
     1.2 +++ b/src/HOL/GCD.thy	Thu Jan 28 11:48:43 2010 +0100
     1.3 @@ -302,28 +302,22 @@
     1.4  lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
     1.5    by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
     1.6  
     1.7 -lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
     1.8 -  by (rule dvd_antisym, auto)
     1.9 -
    1.10 -lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
    1.11 -  by (auto simp add: gcd_int_def gcd_commute_nat)
    1.12 +interpretation gcd_nat!: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.13 +proof
    1.14 +qed (auto intro: dvd_antisym dvd_trans)
    1.15  
    1.16 -lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
    1.17 -  apply (rule dvd_antisym)
    1.18 -  apply (blast intro: dvd_trans)+
    1.19 -done
    1.20 +interpretation gcd_int!: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    1.21 +proof
    1.22 +qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
    1.23  
    1.24 -lemma gcd_assoc_int: "gcd (gcd (k::int) m) n = gcd k (gcd m n)"
    1.25 -  by (auto simp add: gcd_int_def gcd_assoc_nat)
    1.26 -
    1.27 -lemmas gcd_left_commute_nat =
    1.28 -  mk_left_commute[of gcd, OF gcd_assoc_nat gcd_commute_nat]
    1.29 -
    1.30 -lemmas gcd_left_commute_int =
    1.31 -  mk_left_commute[of gcd, OF gcd_assoc_int gcd_commute_int]
    1.32 +lemmas gcd_assoc_nat = gcd_nat.assoc
    1.33 +lemmas gcd_commute_nat = gcd_nat.commute
    1.34 +lemmas gcd_left_commute_nat = gcd_nat.left_commute
    1.35 +lemmas gcd_assoc_int = gcd_int.assoc
    1.36 +lemmas gcd_commute_int = gcd_int.commute
    1.37 +lemmas gcd_left_commute_int = gcd_int.left_commute
    1.38  
    1.39  lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
    1.40 -  -- {* gcd is an AC-operator *}
    1.41  
    1.42  lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
    1.43  
    1.44 @@ -1250,13 +1244,6 @@
    1.45  lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
    1.46    unfolding lcm_int_def by simp
    1.47  
    1.48 -lemma lcm_commute_nat: "lcm (m::nat) n = lcm n m"
    1.49 -  unfolding lcm_nat_def by (simp add: gcd_commute_nat ring_simps)
    1.50 -
    1.51 -lemma lcm_commute_int: "lcm (m::int) n = lcm n m"
    1.52 -  unfolding lcm_int_def by (subst lcm_commute_nat, rule refl)
    1.53 -
    1.54 -
    1.55  lemma lcm_pos_nat:
    1.56    "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
    1.57  by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
    1.58 @@ -1344,10 +1331,10 @@
    1.59  done
    1.60  
    1.61  lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
    1.62 -  by (subst lcm_commute_nat, rule lcm_dvd1_nat)
    1.63 +  using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def times.commute gcd_nat.commute)
    1.64  
    1.65  lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
    1.66 -  by (subst lcm_commute_int, rule lcm_dvd1_int)
    1.67 +  using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def times.commute gcd_nat.commute)
    1.68  
    1.69  lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
    1.70  by(metis lcm_dvd1_nat dvd_trans)
    1.71 @@ -1369,6 +1356,34 @@
    1.72      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    1.73    by (auto intro: dvd_antisym [transferred] lcm_least_int)
    1.74  
    1.75 +interpretation lcm_nat!: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.76 +proof
    1.77 +  fix n m p :: nat
    1.78 +  show "lcm (lcm n m) p = lcm n (lcm m p)"
    1.79 +    by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
    1.80 +  show "lcm m n = lcm n m"
    1.81 +    by (simp add: lcm_nat_def gcd_commute_nat ring_simps)
    1.82 +qed
    1.83 +
    1.84 +interpretation lcm_int!: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
    1.85 +proof
    1.86 +  fix n m p :: int
    1.87 +  show "lcm (lcm n m) p = lcm n (lcm m p)"
    1.88 +    by (rule lcm_unique_int [THEN iffD1]) (metis dvd_trans lcm_unique_int)
    1.89 +  show "lcm m n = lcm n m"
    1.90 +    by (simp add: lcm_int_def lcm_nat.commute)
    1.91 +qed
    1.92 +
    1.93 +lemmas lcm_assoc_nat = lcm_nat.assoc
    1.94 +lemmas lcm_commute_nat = lcm_nat.commute
    1.95 +lemmas lcm_left_commute_nat = lcm_nat.left_commute
    1.96 +lemmas lcm_assoc_int = lcm_int.assoc
    1.97 +lemmas lcm_commute_int = lcm_int.commute
    1.98 +lemmas lcm_left_commute_int = lcm_int.left_commute
    1.99 +
   1.100 +lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
   1.101 +lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
   1.102 +
   1.103  lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
   1.104    apply (rule sym)
   1.105    apply (subst lcm_unique_nat [symmetric])
   1.106 @@ -1399,18 +1414,6 @@
   1.107  lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
   1.108  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
   1.109  
   1.110 -lemma lcm_assoc_nat: "lcm (lcm n m) (p::nat) = lcm n (lcm m p)"
   1.111 -by(rule lcm_unique_nat[THEN iffD1])(metis dvd.order_trans lcm_unique_nat)
   1.112 -
   1.113 -lemma lcm_assoc_int: "lcm (lcm n m) (p::int) = lcm n (lcm m p)"
   1.114 -by(rule lcm_unique_int[THEN iffD1])(metis dvd_trans lcm_unique_int)
   1.115 -
   1.116 -lemmas lcm_left_commute_nat = mk_left_commute[of lcm, OF lcm_assoc_nat lcm_commute_nat]
   1.117 -lemmas lcm_left_commute_int = mk_left_commute[of lcm, OF lcm_assoc_int lcm_commute_int]
   1.118 -
   1.119 -lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
   1.120 -lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
   1.121 -
   1.122  lemma fun_left_comm_idem_gcd_nat: "fun_left_comm_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   1.123  proof qed (auto simp add: gcd_ac_nat)
   1.124