src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy

--- a/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy	Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy	Fri Jul 01 16:52:35 2016 +0200
@@ -10,8 +10,9 @@
 begin
 
 theorem greatest_common_divisor:
-  "\<And>n::nat. Suc m < n \<Longrightarrow> \<exists>k n1 m1. k * n1 = n \<and> k * m1 = Suc m \<and>
-     (\<forall>l l1 l2. l * l1 = n \<longrightarrow> l * l2 = Suc m \<longrightarrow> l \<le> k)"
+  "\<And>n::nat. Suc m < n \<Longrightarrow>
+    \<exists>k n1 m1. k * n1 = n \<and> k * m1 = Suc m \<and>
+    (\<forall>l l1 l2. l * l1 = n \<longrightarrow> l * l2 = Suc m \<longrightarrow> l \<le> k)"
 proof (induct m rule: nat_wf_ind)
   case (1 m n)
   from division obtain r q where h1: "n = Suc m * q + r" and h2: "r \<le> m"
@@ -21,33 +22,28 @@
     case 0
     with h1 have "Suc m * q = n" by simp
     moreover have "Suc m * 1 = Suc m" by simp
-    moreover {
-      fix l2 have "\<And>l l1. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> Suc m"
-        by (cases l2) simp_all }
+    moreover have "l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> Suc m" for l l1 l2
+      by (cases l2) simp_all
     ultimately show ?thesis by iprover
   next
     case (Suc nat)
     with h2 have h: "nat < m" by simp
     moreover from h have "Suc nat < Suc m" by simp
     ultimately have "\<exists>k m1 r1. k * m1 = Suc m \<and> k * r1 = Suc nat \<and>
-      (\<forall>l l1 l2. l * l1 = Suc m \<longrightarrow> l * l2 = Suc nat \<longrightarrow> l \<le> k)"
+        (\<forall>l l1 l2. l * l1 = Suc m \<longrightarrow> l * l2 = Suc nat \<longrightarrow> l \<le> k)"
       by (rule 1)
-    then obtain k m1 r1 where
-      h1': "k * m1 = Suc m"
+    then obtain k m1 r1 where h1': "k * m1 = Suc m"
       and h2': "k * r1 = Suc nat"
       and h3': "\<And>l l1 l2. l * l1 = Suc m \<Longrightarrow> l * l2 = Suc nat \<Longrightarrow> l \<le> k"
       by iprover
     have mn: "Suc m < n" by (rule 1)
-    from h1 h1' h2' Suc have "k * (m1 * q + r1) = n" 
+    from h1 h1' h2' Suc have "k * (m1 * q + r1) = n"
       by (simp add: add_mult_distrib2 mult.assoc [symmetric])
-    moreover have "\<And>l l1 l2. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> k"
+    moreover have "l \<le> k" if ll1n: "l * l1 = n" and ll2m: "l * l2 = Suc m" for l l1 l2
     proof -
-      fix l l1 l2
-      assume ll1n: "l * l1 = n"
-      assume ll2m: "l * l2 = Suc m"
-      moreover have "l * (l1 - l2 * q) = Suc nat"
+      have "l * (l1 - l2 * q) = Suc nat"
         by (simp add: diff_mult_distrib2 h1 Suc [symmetric] mn ll1n ll2m [symmetric])
-      ultimately show "l \<le> k" by (rule h3')
+      with ll2m show "l \<le> k" by (rule h3')
     qed
     ultimately show ?thesis using h1' by iprover
   qed
@@ -56,8 +52,8 @@
 extract greatest_common_divisor
 
 text \<open>
-The extracted program for computing the greatest common divisor is
-@{thm [display] greatest_common_divisor_def}
+  The extracted program for computing the greatest common divisor is
+  @{thm [display] greatest_common_divisor_def}
 \<close>
 
 instantiation nat :: default