src/HOL/GCD.thy
changeset 32960 69916a850301
parent 32879 7f5ce7af45fd
child 33197 de6285ebcc05
     1.1 --- a/src/HOL/GCD.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1190,35 +1190,35 @@
     1.4       moreover
     1.5       {assume db: "d=b"
     1.6         from prems have ?thesis apply simp
     1.7 -	 apply (rule exI[where x = b], simp)
     1.8 -	 apply (rule exI[where x = b])
     1.9 -	by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
    1.10 +         apply (rule exI[where x = b], simp)
    1.11 +         apply (rule exI[where x = b])
    1.12 +        by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
    1.13      moreover
    1.14      {assume db: "d < b"
    1.15 -	{assume "x=0" hence ?thesis  using prems by simp }
    1.16 -	moreover
    1.17 -	{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
    1.18 -	  from db have "d \<le> b - 1" by simp
    1.19 -	  hence "d*b \<le> b*(b - 1)" by simp
    1.20 -	  with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
    1.21 -	  have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
    1.22 -	  from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
    1.23 +        {assume "x=0" hence ?thesis  using prems by simp }
    1.24 +        moreover
    1.25 +        {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
    1.26 +          from db have "d \<le> b - 1" by simp
    1.27 +          hence "d*b \<le> b*(b - 1)" by simp
    1.28 +          with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
    1.29 +          have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
    1.30 +          from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
    1.31              by simp
    1.32 -	  hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
    1.33 -	    by (simp only: mult_assoc right_distrib)
    1.34 -	  hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
    1.35 +          hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
    1.36 +            by (simp only: mult_assoc right_distrib)
    1.37 +          hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
    1.38              by algebra
    1.39 -	  hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
    1.40 -	  hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
    1.41 -	    by (simp only: diff_add_assoc[OF dble, of d, symmetric])
    1.42 -	  hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
    1.43 -	    by (simp only: diff_mult_distrib2 add_commute mult_ac)
    1.44 -	  hence ?thesis using H(1,2)
    1.45 -	    apply -
    1.46 -	    apply (rule exI[where x=d], simp)
    1.47 -	    apply (rule exI[where x="(b - 1) * y"])
    1.48 -	    by (rule exI[where x="x*(b - 1) - d"], simp)}
    1.49 -	ultimately have ?thesis by blast}
    1.50 +          hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
    1.51 +          hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
    1.52 +            by (simp only: diff_add_assoc[OF dble, of d, symmetric])
    1.53 +          hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
    1.54 +            by (simp only: diff_mult_distrib2 add_commute mult_ac)
    1.55 +          hence ?thesis using H(1,2)
    1.56 +            apply -
    1.57 +            apply (rule exI[where x=d], simp)
    1.58 +            apply (rule exI[where x="(b - 1) * y"])
    1.59 +            by (rule exI[where x="x*(b - 1) - d"], simp)}
    1.60 +        ultimately have ?thesis by blast}
    1.61      ultimately have ?thesis by blast}
    1.62    ultimately have ?thesis by blast}
    1.63   ultimately show ?thesis by blast
    1.64 @@ -1653,23 +1653,23 @@
    1.65      next
    1.66        assume "M\<noteq>{0}"
    1.67        with `M\<noteq>{}` assms show ?thesis
    1.68 -	apply(subst Gcd_remove0_nat[OF assms])
    1.69 -	apply(simp add:GCD_def)
    1.70 -	apply(subst divisors_remove0_nat)
    1.71 -	apply(simp add:LCM_def)
    1.72 -	apply rule
    1.73 -	 apply rule
    1.74 -	 apply(subst Gcd_eq_Max)
    1.75 -	    apply simp
    1.76 -	   apply blast
    1.77 -	  apply blast
    1.78 -	 apply(rule Lcm_eq_Max_nat)
    1.79 -	    apply simp
    1.80 -	   apply blast
    1.81 -	  apply fastsimp
    1.82 -	 apply clarsimp
    1.83 -	apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
    1.84 -	done
    1.85 +        apply(subst Gcd_remove0_nat[OF assms])
    1.86 +        apply(simp add:GCD_def)
    1.87 +        apply(subst divisors_remove0_nat)
    1.88 +        apply(simp add:LCM_def)
    1.89 +        apply rule
    1.90 +         apply rule
    1.91 +         apply(subst Gcd_eq_Max)
    1.92 +            apply simp
    1.93 +           apply blast
    1.94 +          apply blast
    1.95 +         apply(rule Lcm_eq_Max_nat)
    1.96 +            apply simp
    1.97 +           apply blast
    1.98 +          apply fastsimp
    1.99 +         apply clarsimp
   1.100 +        apply(fastsimp intro: finite_divisors_nat intro!: finite_INT)
   1.101 +        done
   1.102      qed
   1.103    qed
   1.104  qed