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.70 -	apply(subst divisors_remove0_nat)
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.87 +        apply(subst divisors_remove0_nat)
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
```