added lemmas; tuned
authornipkow
Sat Jun 20 13:34:54 2009 +0200 (2009-06-20)
changeset 31730d74830dc3e4a
parent 31729 b9299916d618
child 31731 7ffc1a901eea
added lemmas; tuned
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/GCD.thy
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sat Jun 20 01:53:39 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sat Jun 20 13:34:54 2009 +0200
     1.3 @@ -1106,18 +1106,18 @@
     1.4    let ?d = "\<delta> (And p q)"
     1.5    from prems int_lcm_pos have dp: "?d >0" by simp
     1.6    have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp
     1.7 -  hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp del:int_lcm_dvd1)
     1.8 +  hence th: "d\<delta> p ?d" using delta_mono prems(3-4) by(simp only: iszlfm.simps)
     1.9    have "\<delta> q dvd \<delta> (And p q)" using prems by simp
    1.10 -  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:int_lcm_dvd2)
    1.11 +  hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps)
    1.12    from th th' dp show ?case by simp
    1.13  next
    1.14    case (2 p q)  
    1.15    let ?d = "\<delta> (And p q)"
    1.16    from prems int_lcm_pos have dp: "?d >0" by simp
    1.17    have "\<delta> p dvd \<delta> (And p q)" using prems by simp
    1.18 -  hence th: "d\<delta> p ?d" using delta_mono prems by(simp del:int_lcm_dvd1)
    1.19 +  hence th: "d\<delta> p ?d" using delta_mono prems by(simp only: iszlfm.simps)
    1.20    have "\<delta> q dvd \<delta> (And p q)" using prems by simp
    1.21 -  hence th': "d\<delta> q ?d" using delta_mono prems by(simp del:int_lcm_dvd2)
    1.22 +  hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps)
    1.23    from th th' dp show ?case by simp
    1.24  qed simp_all
    1.25  
     2.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Jun 20 01:53:39 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sat Jun 20 13:34:54 2009 +0200
     2.3 @@ -2129,18 +2129,18 @@
     2.4    from prems int_lcm_pos have dp: "?d >0" by simp
     2.5    have d1: "\<delta> p dvd \<delta> (And p q)" using prems by simp 
     2.6     hence th: "d\<delta> p ?d" 
     2.7 -     using delta_mono prems by (auto simp del: int_lcm_dvd1)
     2.8 +     using delta_mono prems by(simp only: iszlfm.simps) blast
     2.9    have "\<delta> q dvd \<delta> (And p q)" using prems  by simp 
    2.10 -  hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: int_lcm_dvd2)
    2.11 +  hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast
    2.12    from th th' dp show ?case by simp 
    2.13  next
    2.14    case (2 p q)  
    2.15    let ?d = "\<delta> (And p q)"
    2.16    from prems int_lcm_pos have dp: "?d >0" by simp
    2.17    have "\<delta> p dvd \<delta> (And p q)" using prems by simp hence th: "d\<delta> p ?d" using delta_mono prems 
    2.18 -    by (auto simp del: int_lcm_dvd1)
    2.19 -  have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by (auto simp del: int_lcm_dvd2)
    2.20 -  from th th' dp show ?case by simp 
    2.21 +    by(simp only: iszlfm.simps) blast
    2.22 +  have "\<delta> q dvd \<delta> (And p q)" using prems by simp hence th': "d\<delta> q ?d" using delta_mono prems by(simp only: iszlfm.simps) blast
    2.23 +  from th th' dp show ?case by simp
    2.24  qed simp_all
    2.25  
    2.26  
     3.1 --- a/src/HOL/GCD.thy	Sat Jun 20 01:53:39 2009 +0200
     3.2 +++ b/src/HOL/GCD.thy	Sat Jun 20 13:34:54 2009 +0200
     3.3 @@ -283,6 +283,18 @@
     3.4    apply auto
     3.5  done
     3.6  
     3.7 +lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
     3.8 +by(metis nat_gcd_dvd1 dvd_trans)
     3.9 +
    3.10 +lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
    3.11 +by(metis nat_gcd_dvd2 dvd_trans)
    3.12 +
    3.13 +lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
    3.14 +by(metis int_gcd_dvd1 dvd_trans)
    3.15 +
    3.16 +lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
    3.17 +by(metis int_gcd_dvd2 dvd_trans)
    3.18 +
    3.19  lemma nat_gcd_le1 [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
    3.20    by (rule dvd_imp_le, auto)
    3.21  
    3.22 @@ -1386,7 +1398,7 @@
    3.23    using prems apply auto
    3.24  done
    3.25  
    3.26 -lemma nat_lcm_dvd1 [iff]: "(m::nat) dvd lcm m n"
    3.27 +lemma nat_lcm_dvd1: "(m::nat) dvd lcm m n"
    3.28  proof (cases m)
    3.29    case 0 then show ?thesis by simp
    3.30  next
    3.31 @@ -1407,7 +1419,7 @@
    3.32    qed
    3.33  qed
    3.34  
    3.35 -lemma int_lcm_dvd1 [iff]: "(m::int) dvd lcm m n"
    3.36 +lemma int_lcm_dvd1: "(m::int) dvd lcm m n"
    3.37    apply (subst int_lcm_abs)
    3.38    apply (rule dvd_trans)
    3.39    prefer 2
    3.40 @@ -1415,27 +1427,27 @@
    3.41    apply auto
    3.42  done
    3.43  
    3.44 -lemma nat_lcm_dvd2 [iff]: "(n::nat) dvd lcm m n"
    3.45 +lemma nat_lcm_dvd2: "(n::nat) dvd lcm m n"
    3.46    by (subst nat_lcm_commute, rule nat_lcm_dvd1)
    3.47  
    3.48 -lemma int_lcm_dvd2 [iff]: "(n::int) dvd lcm m n"
    3.49 +lemma int_lcm_dvd2: "(n::int) dvd lcm m n"
    3.50    by (subst int_lcm_commute, rule int_lcm_dvd1)
    3.51  
    3.52 -lemma dvd_lcm_if_dvd1_nat: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
    3.53 +lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
    3.54  by(metis nat_lcm_dvd1 dvd_trans)
    3.55  
    3.56 -lemma dvd_lcm_if_dvd2_nat: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
    3.57 +lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
    3.58  by(metis nat_lcm_dvd2 dvd_trans)
    3.59  
    3.60 -lemma dvd_lcm_if_dvd1_int: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
    3.61 +lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
    3.62  by(metis int_lcm_dvd1 dvd_trans)
    3.63  
    3.64 -lemma dvd_lcm_if_dvd2_int: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
    3.65 +lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
    3.66  by(metis int_lcm_dvd2 dvd_trans)
    3.67  
    3.68  lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and>
    3.69      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    3.70 -  by (auto intro: dvd_anti_sym nat_lcm_least)
    3.71 +  by (auto intro: dvd_anti_sym nat_lcm_least nat_lcm_dvd1 nat_lcm_dvd2)
    3.72  
    3.73  lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
    3.74      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"