# HG changeset patch
# User wenzelm
# Date 1467384755 -7200
# Node ID d10eab0672f96bd79a6a06684a5b918201dca155
# Parent  65a9eb946ff2e854178becdad46b37aa481904a8
misc tuning and modernization;

diff -r 65a9eb946ff2 -r d10eab0672f9 src/HOL/Proofs/Extraction/Euclid.thy
--- a/src/HOL/Proofs/Extraction/Euclid.thy	Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Fri Jul 01 16:52:35 2016 +0200
@@ -14,8 +14,8 @@
 begin
 
 text \<open>
-A constructive version of the proof of Euclid's theorem by
-Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}.
+  A constructive version of the proof of Euclid's theorem by
+  Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}.
 \<close>
 
 lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
@@ -24,11 +24,10 @@
 lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k"
   by (induct k) auto
 
-lemma prod_mn_less_k:
-  "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
+lemma prod_mn_less_k: "0 < n \<Longrightarrow> 0 < k \<Longrightarrow> Suc 0 < m \<Longrightarrow> m * n = k \<Longrightarrow> n < k"
   by (induct m) auto
 
-lemma prime_eq: "prime (p::nat) = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
+lemma prime_eq: "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
   apply (simp add: prime_def)
   apply (rule iffI)
   apply blast
@@ -39,29 +38,25 @@
   apply (erule allE)
   apply (erule impE)
   apply assumption
-  apply (case_tac "m=0")
+  apply (case_tac "m = 0")
   apply simp
-  apply (case_tac "m=Suc 0")
+  apply (case_tac "m = Suc 0")
   apply simp
   apply simp
   done
 
-lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
+lemma prime_eq': "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p)"
   by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
 
 lemma not_prime_ex_mk:
   assumes n: "Suc 0 < n"
   shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
 proof -
-  {
-    fix k
-    from nat_eq_dec
-    have "(\<exists>m<n. n = m * k) \<or> \<not> (\<exists>m<n. n = m * k)"
-      by (rule search)
-  }
-  hence "(\<exists>k<n. \<exists>m<n. n = m * k) \<or> \<not> (\<exists>k<n. \<exists>m<n. n = m * k)"
+  from nat_eq_dec have "(\<exists>m<n. n = m * k) \<or> \<not> (\<exists>m<n. n = m * k)" for k
     by (rule search)
-  thus ?thesis
+  then have "(\<exists>k<n. \<exists>m<n. n = m * k) \<or> \<not> (\<exists>k<n. \<exists>m<n. n = m * k)"
+    by (rule search)
+  then show ?thesis
   proof
     assume "\<exists>k<n. \<exists>m<n. n = m * k"
     then obtain k m where k: "k<n" and m: "m<n" and nmk: "n = m * k"
@@ -71,7 +66,7 @@
     ultimately show ?thesis using k m nmk by iprover
   next
     assume "\<not> (\<exists>k<n. \<exists>m<n. n = m * k)"
-    hence A: "\<forall>k<n. \<forall>m<n. n \<noteq> m * k" by iprover
+    then have A: "\<forall>k<n. \<forall>m<n. n \<noteq> m * k" by iprover
     have "\<forall>m k. n = m * k \<longrightarrow> Suc 0 < m \<longrightarrow> m = n"
     proof (intro allI impI)
       fix m k
@@ -99,11 +94,11 @@
     qed
     with n have "prime n"
       by (simp only: prime_eq' One_nat_def simp_thms)
-    thus ?thesis ..
+    then show ?thesis ..
   qed
 qed
 
-lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact (n::nat)"
+lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
 proof (induct n rule: nat_induct)
   case 0
   then show ?case by simp
@@ -124,30 +119,30 @@
 qed
 
 lemma dvd_prod [iff]: "n dvd (\<Prod>m::nat \<in># mset (n # ns). m)"
-  by (simp add: msetprod_Un msetprod_singleton)
+  by (simp add: msetprod_Un)
 
-definition all_prime :: "nat list \<Rightarrow> bool" where
-  "all_prime ps \<longleftrightarrow> (\<forall>p\<in>set ps. prime p)"
+definition all_prime :: "nat list \<Rightarrow> bool"
+  where "all_prime ps \<longleftrightarrow> (\<forall>p\<in>set ps. prime p)"
 
 lemma all_prime_simps:
   "all_prime []"
   "all_prime (p # ps) \<longleftrightarrow> prime p \<and> all_prime ps"
   by (simp_all add: all_prime_def)
 
-lemma all_prime_append:
-  "all_prime (ps @ qs) \<longleftrightarrow> all_prime ps \<and> all_prime qs"
+lemma all_prime_append: "all_prime (ps @ qs) \<longleftrightarrow> all_prime ps \<and> all_prime qs"
   by (simp add: all_prime_def ball_Un)
 
 lemma split_all_prime:
   assumes "all_prime ms" and "all_prime ns"
-  shows "\<exists>qs. all_prime qs \<and> (\<Prod>m::nat \<in># mset qs. m) =
-    (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
+  shows "\<exists>qs. all_prime qs \<and>
+    (\<Prod>m::nat \<in># mset qs. m) = (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
+  (is "\<exists>qs. ?P qs \<and> ?Q qs")
 proof -
   from assms have "all_prime (ms @ ns)"
     by (simp add: all_prime_append)
-  moreover from assms have "(\<Prod>m::nat \<in># mset (ms @ ns). m) =
-    (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
-    by (simp add: msetprod_Un)
+  moreover
+  have "(\<Prod>m::nat \<in># mset (ms @ ns). m) = (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
+    using assms by (simp add: msetprod_Un)
   ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
   then show ?thesis ..
 qed
@@ -155,8 +150,10 @@
 lemma all_prime_nempty_g_one:
   assumes "all_prime ps" and "ps \<noteq> []"
   shows "Suc 0 < (\<Prod>m::nat \<in># mset ps. m)"
-  using \<open>ps \<noteq> []\<close> \<open>all_prime ps\<close> unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
-    (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
+  using \<open>ps \<noteq> []\<close> \<open>all_prime ps\<close>
+  unfolding One_nat_def [symmetric]
+  by (induct ps rule: list_nonempty_induct)
+    (simp_all add: all_prime_simps msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
 
 lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = n)"
 proof (induct n rule: nat_wf_ind)
@@ -165,14 +162,17 @@
   have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
     by (rule not_prime_ex_mk)
   then show ?case
-  proof 
+  proof
     assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
     then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
-      and kn: "k < n" and nmk: "n = m * k" by iprover
-    from mn and m have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = m" by (rule 1)
+      and kn: "k < n" and nmk: "n = m * k"
+      by iprover
+    from mn and m have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = m"
+      by (rule 1)
     then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(\<Prod>m::nat \<in># mset ps1. m) = m"
       by iprover
-    from kn and k have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = k" by (rule 1)
+    from kn and k have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = k"
+      by (rule 1)
     then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(\<Prod>m::nat \<in># mset ps2. m) = k"
       by iprover
     from \<open>all_prime ps1\<close> \<open>all_prime ps2\<close>
@@ -192,27 +192,27 @@
   assumes N: "(1::nat) < n"
   shows "\<exists>p. prime p \<and> p dvd n"
 proof -
-  from N obtain ps where "all_prime ps"
-    and prod_ps: "n = (\<Prod>m::nat \<in># mset ps. m)" using factor_exists
-    by simp iprover
+  from N obtain ps where "all_prime ps" and prod_ps: "n = (\<Prod>m::nat \<in># mset ps. m)"
+    using factor_exists by simp iprover
   with N have "ps \<noteq> []"
-    by (auto simp add: all_prime_nempty_g_one msetprod_empty)
-  then obtain p qs where ps: "ps = p # qs" by (cases ps) simp
-  with \<open>all_prime ps\<close> have "prime p" by (simp add: all_prime_simps)
-  moreover from \<open>all_prime ps\<close> ps prod_ps
-  have "p dvd n" by (simp only: dvd_prod)
+    by (auto simp add: all_prime_nempty_g_one)
+  then obtain p qs where ps: "ps = p # qs"
+    by (cases ps) simp
+  with \<open>all_prime ps\<close> have "prime p"
+    by (simp add: all_prime_simps)
+  moreover from \<open>all_prime ps\<close> ps prod_ps have "p dvd n"
+    by (simp only: dvd_prod)
   ultimately show ?thesis by iprover
 qed
 
-text \<open>
-Euclid's theorem: there are infinitely many primes.
-\<close>
+text \<open>Euclid's theorem: there are infinitely many primes.\<close>
 
-lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
+lemma Euclid: "\<exists>p. prime p \<and> n < p"
 proof -
   let ?k = "fact n + (1::nat)"
   have "1 < ?k" by simp
-  then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover
+  then obtain p where prime: "prime p" and dvd: "p dvd ?k"
+    using prime_factor_exists by iprover
   have "n < p"
   proof -
     have "\<not> p \<le> n"
@@ -232,10 +232,10 @@
 extract Euclid
 
 text \<open>
-The program extracted from the proof of Euclid's theorem looks as follows.
-@{thm [display] Euclid_def}
-The program corresponding to the proof of the factorization theorem is
-@{thm [display] factor_exists_def}
+  The program extracted from the proof of Euclid's theorem looks as follows.
+  @{thm [display] Euclid_def}
+  The program corresponding to the proof of the factorization theorem is
+  @{thm [display] factor_exists_def}
 \<close>
 
 instantiation nat :: default
@@ -256,9 +256,10 @@
 
 end
 
-primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
+primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
+where
   "iterate 0 f x = []"
-  | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
+| "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
 
 lemma "factor_exists 1007 = [53, 19]" by eval
 lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
diff -r 65a9eb946ff2 -r d10eab0672f9 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
diff -r 65a9eb946ff2 -r d10eab0672f9 src/HOL/Proofs/Extraction/Higman.thy
--- a/src/HOL/Proofs/Extraction/Higman.thy	Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Fri Jul 01 16:52:35 2016 +0200
@@ -18,43 +18,44 @@
 
 inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
 where
-   emb0 [Pure.intro]: "emb [] bs"
- | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
- | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
+  emb0 [Pure.intro]: "emb [] bs"
+| emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
+| emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
 
 inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"
   for v :: "letter list"
 where
-   L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"
- | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"
+  L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"
+| L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"
 
 inductive good :: "letter list list \<Rightarrow> bool"
 where
-    good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"
-  | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"
+  good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"
+| good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"
 
 inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
   for a :: letter
 where
-    R0 [Pure.intro]: "R a [] []"
-  | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"
+  R0 [Pure.intro]: "R a [] []"
+| R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"
 
 inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
   for a :: letter
 where
-    T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"
-  | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"
-  | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"
+  T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"
+| T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"
+| T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"
 
 inductive bar :: "letter list list \<Rightarrow> bool"
 where
-    bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"
-  | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"
+  bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"
+| bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"
 
-theorem prop1: "bar ([] # ws)" by iprover
+theorem prop1: "bar ([] # ws)"
+  by iprover
 
 theorem lemma1: "L as ws \<Longrightarrow> L (a # as) ws"
-  by (erule L.induct, iprover+)
+  by (erule L.induct) iprover+
 
 lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"
   apply (induct set: R)
@@ -123,7 +124,7 @@
   apply simp
   done
 
-lemma letter_neq: "(a::letter) \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b"
+lemma letter_neq: "a \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b" for a b c :: letter
   apply (case_tac a)
   apply (case_tac b)
   apply (case_tac c, simp, simp)
@@ -133,7 +134,7 @@
   apply (case_tac c, simp, simp)
   done
 
-lemma letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b"
+lemma letter_eq_dec: "a = b \<or> a \<noteq> b" for a b :: letter
   apply (case_tac a)
   apply (case_tac b)
   apply simp
@@ -145,42 +146,46 @@
 
 theorem prop2:
   assumes ab: "a \<noteq> b" and bar: "bar xs"
-  shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar
+  shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
+  using bar
 proof induct
-  fix xs zs assume "T a xs zs" and "good xs"
-  hence "good zs" by (rule lemma3)
+  fix xs zs
+  assume "T a xs zs" and "good xs"
+  then have "good zs" by (rule lemma3)
   then show "bar zs" by (rule bar1)
 next
   fix xs ys
   assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
   assume "bar ys"
-  thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
+  then show "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
   proof induct
-    fix ys zs assume "T b ys zs" and "good ys"
+    fix ys zs
+    assume "T b ys zs" and "good ys"
     then have "good zs" by (rule lemma3)
     then show "bar zs" by (rule bar1)
   next
-    fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"
-    and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"
+    fix ys zs
+    assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"
+      and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"
     show "bar zs"
     proof (rule bar2)
       fix w
       show "bar (w # zs)"
       proof (cases w)
         case Nil
-        thus ?thesis by simp (rule prop1)
+        then show ?thesis by simp (rule prop1)
       next
         case (Cons c cs)
         from letter_eq_dec show ?thesis
         proof
           assume ca: "c = a"
           from ab have "bar ((a # cs) # zs)" by (iprover intro: I ys Ta Tb)
-          thus ?thesis by (simp add: Cons ca)
+          then show ?thesis by (simp add: Cons ca)
         next
           assume "c \<noteq> a"
           with ab have cb: "c = b" by (rule letter_neq)
           from ab have "bar ((b # cs) # zs)" by (iprover intro: I' Ta Tb)
-          thus ?thesis by (simp add: Cons cb)
+          then show ?thesis by (simp add: Cons cb)
         qed
       qed
     qed
@@ -189,7 +194,8 @@
 
 theorem prop3:
   assumes bar: "bar xs"
-  shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar
+  shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs"
+  using bar
 proof induct
   fix xs zs
   assume "R a xs zs" and "good xs"
@@ -198,7 +204,7 @@
 next
   fix xs zs
   assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs"
-  and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs"
+    and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs"
   show "bar zs"
   proof (rule bar2)
     fix w
@@ -211,11 +217,11 @@
       from letter_eq_dec show ?case
       proof
         assume "c = a"
-        thus ?thesis by (iprover intro: I [simplified] R)
+        then show ?thesis by (iprover intro: I [simplified] R)
       next
         from R xsn have T: "T a xs zs" by (rule lemma4)
         assume "c \<noteq> a"
-        thus ?thesis by (iprover intro: prop2 Cons xsb xsn R T)
+        then show ?thesis by (iprover intro: prop2 Cons xsb xsn R T)
       qed
     qed
   qed
@@ -229,58 +235,60 @@
     show "bar [[]]" by (rule prop1)
   next
     fix c cs assume "bar [cs]"
-    thus "bar [c # cs]" by (rule prop3) (simp, iprover)
+    then show "bar [c # cs]" by (rule prop3) (simp, iprover)
   qed
 qed
 
-primrec
-  is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
+primrec is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
 where
-    "is_prefix [] f = True"
-  | "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"
+  "is_prefix [] f = True"
+| "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"
 
 theorem L_idx:
   assumes L: "L w ws"
-  shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws" using L
+  shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws"
+  using L
 proof induct
   case (L0 v ws)
-  hence "emb (f (length ws)) w" by simp
+  then have "emb (f (length ws)) w" by simp
   moreover have "length ws < length (v # ws)" by simp
   ultimately show ?case by iprover
 next
   case (L1 ws v)
   then obtain i where emb: "emb (f i) w" and "i < length ws"
     by simp iprover
-  hence "i < length (v # ws)" by simp
+  then have "i < length (v # ws)" by simp
   with emb show ?case by iprover
 qed
 
 theorem good_idx:
   assumes good: "good ws"
-  shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using good
+  shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j"
+  using good
 proof induct
   case (good0 w ws)
-  hence "w = f (length ws)" and "is_prefix ws f" by simp_all
+  then have "w = f (length ws)" and "is_prefix ws f" by simp_all
   with good0 show ?case by (iprover dest: L_idx)
 next
   case (good1 ws w)
-  thus ?case by simp
+  then show ?case by simp
 qed
 
 theorem bar_idx:
   assumes bar: "bar ws"
-  shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using bar
+  shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j"
+  using bar
 proof induct
   case (bar1 ws)
-  thus ?case by (rule good_idx)
+  then show ?case by (rule good_idx)
 next
   case (bar2 ws)
-  hence "is_prefix (f (length ws) # ws) f" by simp
-  thus ?case by (rule bar2)
+  then have "is_prefix (f (length ws) # ws) f" by simp
+  then show ?case by (rule bar2)
 qed
 
 text \<open>
-Strong version: yields indices of words that can be embedded into each other.
+  Strong version: yields indices of words that can be embedded into each other.
 \<close>
 
 theorem higman_idx: "\<exists>(i::nat) j. emb (f i) (f j) \<and> i < j"
@@ -290,26 +298,25 @@
 qed
 
 text \<open>
-Weak version: only yield sequence containing words
-that can be embedded into each other.
+  Weak version: only yield sequence containing words
+  that can be embedded into each other.
 \<close>
 
 theorem good_prefix_lemma:
   assumes bar: "bar ws"
-  shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> good vs" using bar
+  shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> good vs"
+  using bar
 proof induct
   case bar1
-  thus ?case by iprover
+  then show ?case by iprover
 next
   case (bar2 ws)
   from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp
-  thus ?case by (iprover intro: bar2)
+  then show ?case by (iprover intro: bar2)
 qed
 
 theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> good vs"
   using higman
   by (rule good_prefix_lemma) simp+
 
-(*<*)
 end
-(*>*)
diff -r 65a9eb946ff2 -r d10eab0672f9 src/HOL/Proofs/Extraction/Higman_Extraction.thy
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Fri Jul 01 16:52:35 2016 +0200
@@ -3,13 +3,11 @@
     Author:     Monika Seisenberger, LMU Muenchen
 *)
 
-(*<*)
+subsection \<open>Extracting the program\<close>
+
 theory Higman_Extraction
 imports Higman "~~/src/HOL/Library/State_Monad" Random
 begin
-(*>*)
-
-subsection \<open>Extracting the program\<close>
 
 declare R.induct [ind_realizer]
 declare T.induct [ind_realizer]
@@ -48,7 +46,8 @@
 
 end
 
-function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed"
+where
   "mk_word_aux k = exec {
      i \<leftarrow> Random.range 10;
      (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
@@ -57,54 +56,58 @@
        ls \<leftarrow> mk_word_aux (Suc k);
        Pair (l # ls)
      })}"
-by pat_completeness auto
-termination by (relation "measure ((op -) 1001)") auto
+  by pat_completeness auto
+termination
+  by (relation "measure ((op -) 1001)") auto
 
-definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
-  "mk_word = mk_word_aux 0"
+definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed"
+  where "mk_word = mk_word_aux 0"
 
-primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed"
+where
   "mk_word_s 0 = mk_word"
-  | "mk_word_s (Suc n) = exec {
-       _ \<leftarrow> mk_word;
-       mk_word_s n
-     }"
+| "mk_word_s (Suc n) = exec {
+     _ \<leftarrow> mk_word;
+     mk_word_s n
+   }"
 
-definition g1 :: "nat \<Rightarrow> letter list" where
-  "g1 s = fst (mk_word_s s (20000, 1))"
+definition g1 :: "nat \<Rightarrow> letter list"
+  where "g1 s = fst (mk_word_s s (20000, 1))"
 
-definition g2 :: "nat \<Rightarrow> letter list" where
-  "g2 s = fst (mk_word_s s (50000, 1))"
+definition g2 :: "nat \<Rightarrow> letter list"
+  where "g2 s = fst (mk_word_s s (50000, 1))"
 
-fun f1 :: "nat \<Rightarrow> letter list" where
+fun f1 :: "nat \<Rightarrow> letter list"
+where
   "f1 0 = [A, A]"
-  | "f1 (Suc 0) = [B]"
-  | "f1 (Suc (Suc 0)) = [A, B]"
-  | "f1 _ = []"
+| "f1 (Suc 0) = [B]"
+| "f1 (Suc (Suc 0)) = [A, B]"
+| "f1 _ = []"
 
-fun f2 :: "nat \<Rightarrow> letter list" where
+fun f2 :: "nat \<Rightarrow> letter list"
+where
   "f2 0 = [A, A]"
-  | "f2 (Suc 0) = [B]"
-  | "f2 (Suc (Suc 0)) = [B, A]"
-  | "f2 _ = []"
+| "f2 (Suc 0) = [B]"
+| "f2 (Suc (Suc 0)) = [B, A]"
+| "f2 _ = []"
 
 ML_val \<open>
-local
-  val higman_idx = @{code higman_idx};
-  val g1 = @{code g1};
-  val g2 = @{code g2};
-  val f1 = @{code f1};
-  val f2 = @{code f2};
-in
-  val (i1, j1) = higman_idx g1;
-  val (v1, w1) = (g1 i1, g1 j1);
-  val (i2, j2) = higman_idx g2;
-  val (v2, w2) = (g2 i2, g2 j2);
-  val (i3, j3) = higman_idx f1;
-  val (v3, w3) = (f1 i3, f1 j3);
-  val (i4, j4) = higman_idx f2;
-  val (v4, w4) = (f2 i4, f2 j4);
-end;
+  local
+    val higman_idx = @{code higman_idx};
+    val g1 = @{code g1};
+    val g2 = @{code g2};
+    val f1 = @{code f1};
+    val f2 = @{code f2};
+  in
+    val (i1, j1) = higman_idx g1;
+    val (v1, w1) = (g1 i1, g1 j1);
+    val (i2, j2) = higman_idx g2;
+    val (v2, w2) = (g2 i2, g2 j2);
+    val (i3, j3) = higman_idx f1;
+    val (v3, w3) = (f1 i3, f1 j3);
+    val (i4, j4) = higman_idx f2;
+    val (v4, w4) = (f2 i4, f2 j4);
+  end;
 \<close>
 
 end
diff -r 65a9eb946ff2 -r d10eab0672f9 src/HOL/Proofs/Extraction/Pigeonhole.thy
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy	Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy	Fri Jul 01 16:52:35 2016 +0200
@@ -9,131 +9,126 @@
 begin
 
 text \<open>
-We formalize two proofs of the pigeonhole principle, which lead
-to extracted programs of quite different complexity. The original
-formalization of these proofs in {\sc Nuprl} is due to
-Aleksey Nogin @{cite "Nogin-ENTCS-2000"}.
+  We formalize two proofs of the pigeonhole principle, which lead
+  to extracted programs of quite different complexity. The original
+  formalization of these proofs in {\sc Nuprl} is due to
+  Aleksey Nogin @{cite "Nogin-ENTCS-2000"}.
 
-This proof yields a polynomial program.
+  This proof yields a polynomial program.
 \<close>
 
 theorem pigeonhole:
   "\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j"
 proof (induct n)
   case 0
-  hence "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp
-  thus ?case by iprover
+  then have "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp
+  then show ?case by iprover
 next
   case (Suc n)
-  {
-    fix k
-    have
-      "k \<le> Suc (Suc n) \<Longrightarrow>
-      (\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow>
-      (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)"
-    proof (induct k)
-      case 0
-      let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
-      have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)"
-      proof
-        assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
-        then obtain i j where i: "i \<le> Suc n" and j: "j < i"
-          and f: "?f i = ?f j" by iprover
-        from j have i_nz: "Suc 0 \<le> i" by simp
-        from i have iSSn: "i \<le> Suc (Suc n)" by simp
-        have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp
+  have r:
+    "k \<le> Suc (Suc n) \<Longrightarrow>
+    (\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow>
+    (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)" for k
+  proof (induct k)
+    case 0
+    let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
+    have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)"
+    proof
+      assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
+      then obtain i j where i: "i \<le> Suc n" and j: "j < i" and f: "?f i = ?f j"
+        by iprover
+      from j have i_nz: "Suc 0 \<le> i" by simp
+      from i have iSSn: "i \<le> Suc (Suc n)" by simp
+      have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp
+      show False
+      proof cases
+        assume fi: "f i = Suc n"
+        show False
+        proof cases
+          assume fj: "f j = Suc n"
+          from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0)
+          moreover from fi have "f i = f j"
+            by (simp add: fj [symmetric])
+          ultimately show ?thesis ..
+        next
+          from i and j have "j < Suc (Suc n)" by simp
+          with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j"
+            by (rule 0)
+          moreover assume "f j \<noteq> Suc n"
+          with fi and f have "f (Suc (Suc n)) = f j" by simp
+          ultimately show False ..
+        qed
+      next
+        assume fi: "f i \<noteq> Suc n"
         show False
         proof cases
-          assume fi: "f i = Suc n"
-          show False
-          proof cases
-            assume fj: "f j = Suc n"
-            from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0)
-            moreover from fi have "f i = f j"
-              by (simp add: fj [symmetric])
-            ultimately show ?thesis ..
-          next
-            from i and j have "j < Suc (Suc n)" by simp
-            with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j"
-              by (rule 0)
-            moreover assume "f j \<noteq> Suc n"
-            with fi and f have "f (Suc (Suc n)) = f j" by simp
-            ultimately show False ..
+          from i have "i < Suc (Suc n)" by simp
+          with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i"
+            by (rule 0)
+          moreover assume "f j = Suc n"
+          with fi and f have "f (Suc (Suc n)) = f i" by simp
+          ultimately show False ..
+        next
+          from i_nz and iSSn and j
+          have "f i \<noteq> f j" by (rule 0)
+          moreover assume "f j \<noteq> Suc n"
+          with fi and f have "f i = f j" by simp
+          ultimately show False ..
+        qed
+      qed
+    qed
+    moreover have "?f i \<le> n" if "i \<le> Suc n" for i
+    proof -
+      from that have i: "i < Suc (Suc n)" by simp
+      have "f (Suc (Suc n)) \<noteq> f i"
+        by (rule 0) (simp_all add: i)
+      moreover have "f (Suc (Suc n)) \<le> Suc n"
+        by (rule Suc) simp
+      moreover from i have "i \<le> Suc (Suc n)" by simp
+      then have "f i \<le> Suc n" by (rule Suc)
+      ultimately show ?thesis
+        by simp
+    qed
+    then have "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
+      by (rule Suc)
+    ultimately show ?case ..
+  next
+    case (Suc k)
+    from search [OF nat_eq_dec] show ?case
+    proof
+      assume "\<exists>j<Suc k. f (Suc k) = f j"
+      then show ?case by (iprover intro: le_refl)
+    next
+      assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)"
+      have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j"
+      proof (rule Suc)
+        from Suc show "k \<le> Suc (Suc n)" by simp
+        fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)"
+          and j: "j < i"
+        show "f i \<noteq> f j"
+        proof cases
+          assume eq: "i = Suc k"
+          show ?thesis
+          proof
+            assume "f i = f j"
+            then have "f (Suc k) = f j" by (simp add: eq)
+            with nex and j and eq show False by iprover
           qed
         next
-          assume fi: "f i \<noteq> Suc n"
-          show False
-          proof cases
-            from i have "i < Suc (Suc n)" by simp
-            with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i"
-              by (rule 0)
-            moreover assume "f j = Suc n"
-            with fi and f have "f (Suc (Suc n)) = f i" by simp
-            ultimately show False ..
-          next
-            from i_nz and iSSn and j
-            have "f i \<noteq> f j" by (rule 0)
-            moreover assume "f j \<noteq> Suc n"
-            with fi and f have "f i = f j" by simp
-            ultimately show False ..
-          qed
+          assume "i \<noteq> Suc k"
+          with k have "Suc (Suc k) \<le> i" by simp
+          then show ?thesis using i and j by (rule Suc)
         qed
       qed
-      moreover have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
-      proof -
-        fix i assume "i \<le> Suc n"
-        hence i: "i < Suc (Suc n)" by simp
-        have "f (Suc (Suc n)) \<noteq> f i"
-          by (rule 0) (simp_all add: i)
-        moreover have "f (Suc (Suc n)) \<le> Suc n"
-          by (rule Suc) simp
-        moreover from i have "i \<le> Suc (Suc n)" by simp
-        hence "f i \<le> Suc n" by (rule Suc)
-        ultimately show "?thesis i"
-          by simp
-      qed
-      hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
-        by (rule Suc)
-      ultimately show ?case ..
-    next
-      case (Suc k)
-      from search [OF nat_eq_dec] show ?case
-      proof
-        assume "\<exists>j<Suc k. f (Suc k) = f j"
-        thus ?case by (iprover intro: le_refl)
-      next
-        assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)"
-        have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j"
-        proof (rule Suc)
-          from Suc show "k \<le> Suc (Suc n)" by simp
-          fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)"
-            and j: "j < i"
-          show "f i \<noteq> f j"
-          proof cases
-            assume eq: "i = Suc k"
-            show ?thesis
-            proof
-              assume "f i = f j"
-              hence "f (Suc k) = f j" by (simp add: eq)
-              with nex and j and eq show False by iprover
-            qed
-          next
-            assume "i \<noteq> Suc k"
-            with k have "Suc (Suc k) \<le> i" by simp
-            thus ?thesis using i and j by (rule Suc)
-          qed
-        qed
-        thus ?thesis by (iprover intro: le_SucI)
-      qed
+      then show ?thesis by (iprover intro: le_SucI)
     qed
-  }
-  note r = this
+  qed
   show ?case by (rule r) simp_all
 qed
 
 text \<open>
-The following proof, although quite elegant from a mathematical point of view,
-leads to an exponential program:
+  The following proof, although quite elegant from a mathematical point of view,
+  leads to an exponential program:
 \<close>
 
 theorem pigeonhole_slow:
@@ -149,10 +144,10 @@
   from search [OF nat_eq_dec] show ?case
   proof
     assume "\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j"
-    thus ?case by (iprover intro: le_refl)
+    then show ?case by (iprover intro: le_refl)
   next
     assume "\<not> (\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j)"
-    hence nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by iprover
+    then have nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by iprover
     let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
     have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
     proof -
@@ -171,7 +166,7 @@
         with False show ?thesis by simp
       qed
     qed
-    hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc)
+    then have "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc)
     then obtain i j where i: "i \<le> Suc n" and ji: "j < i" and f: "?f i = ?f j"
       by iprover
     have "f i = f j"
@@ -206,16 +201,16 @@
 extract pigeonhole pigeonhole_slow
 
 text \<open>
-The programs extracted from the above proofs look as follows:
-@{thm [display] pigeonhole_def}
-@{thm [display] pigeonhole_slow_def}
-The program for searching for an element in an array is
-@{thm [display,eta_contract=false] search_def}
-The correctness statement for @{term "pigeonhole"} is
-@{thm [display] pigeonhole_correctness [no_vars]}
+  The programs extracted from the above proofs look as follows:
+  @{thm [display] pigeonhole_def}
+  @{thm [display] pigeonhole_slow_def}
+  The program for searching for an element in an array is
+  @{thm [display,eta_contract=false] search_def}
+  The correctness statement for @{term "pigeonhole"} is
+  @{thm [display] pigeonhole_correctness [no_vars]}
 
-In order to analyze the speed of the above programs,
-we generate ML code from them.
+  In order to analyze the speed of the above programs,
+  we generate ML code from them.
 \<close>
 
 instantiation nat :: default
@@ -236,14 +231,11 @@
 
 end
 
-definition
-  "test n u = pigeonhole (nat_of_integer n) (\<lambda>m. m - 1)"
-definition
-  "test' n u = pigeonhole_slow (nat_of_integer n) (\<lambda>m. m - 1)"
-definition
-  "test'' u = pigeonhole 8 (List.nth [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
+definition "test n u = pigeonhole (nat_of_integer n) (\<lambda>m. m - 1)"
+definition "test' n u = pigeonhole_slow (nat_of_integer n) (\<lambda>m. m - 1)"
+definition "test'' u = pigeonhole 8 (List.nth [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
 
-ML_val "timeit (@{code test} 10)" 
+ML_val "timeit (@{code test} 10)"
 ML_val "timeit (@{code test'} 10)"
 ML_val "timeit (@{code test} 20)"
 ML_val "timeit (@{code test'} 20)"
diff -r 65a9eb946ff2 -r d10eab0672f9 src/HOL/Proofs/Extraction/QuotRem.thy
--- a/src/HOL/Proofs/Extraction/QuotRem.thy	Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/QuotRem.thy	Fri Jul 01 16:52:35 2016 +0200
@@ -14,7 +14,7 @@
 proof (induct a)
   case 0
   have "0 = Suc b * 0 + 0 \<and> 0 \<le> b" by simp
-  thus ?case by iprover
+  then show ?case by iprover
 next
   case (Suc a)
   then obtain r q where I: "a = Suc b * q + r" and "r \<le> b" by iprover
@@ -22,12 +22,12 @@
   proof
     assume "r = b"
     with I have "Suc a = Suc b * (Suc q) + 0 \<and> 0 \<le> b" by simp
-    thus ?case by iprover
+    then show ?case by iprover
   next
     assume "r \<noteq> b"
     with \<open>r \<le> b\<close> have "r < b" by (simp add: order_less_le)
     with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp
-    thus ?case by iprover
+    then show ?case by iprover
   qed
 qed
 
diff -r 65a9eb946ff2 -r d10eab0672f9 src/HOL/Proofs/Extraction/Util.thy
--- a/src/HOL/Proofs/Extraction/Util.thy	Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Util.thy	Fri Jul 01 16:52:35 2016 +0200
@@ -8,9 +8,7 @@
 imports "~~/src/HOL/Library/Old_Datatype"
 begin
 
-text \<open>
-Decidability of equality on natural numbers.
-\<close>
+text \<open>Decidability of equality on natural numbers.\<close>
 
 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
   apply (induct m)
@@ -20,8 +18,8 @@
   done
 
 text \<open>
-Well-founded induction on natural numbers, derived using the standard
-structural induction rule.
+  Well-founded induction on natural numbers, derived using the standard
+  structural induction rule.
 \<close>
 
 lemma nat_wf_ind:
@@ -31,7 +29,7 @@
   show "\<And>y. y < z \<Longrightarrow> P y"
   proof (induct z)
     case 0
-    thus ?case by simp
+    then show ?case by simp
   next
     case (Suc n y)
     from nat_eq_dec show ?case
@@ -43,23 +41,22 @@
     next
       assume "n \<noteq> y"
       with Suc have "y < n" by simp
-      thus ?case by (rule Suc)
+      then show ?case by (rule Suc)
     qed
   qed
 qed
 
-text \<open>
-Bounded search for a natural number satisfying a decidable predicate.
-\<close>
+text \<open>Bounded search for a natural number satisfying a decidable predicate.\<close>
 
 lemma search:
   assumes dec: "\<And>x::nat. P x \<or> \<not> P x"
   shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)"
 proof (induct y)
-  case 0 show ?case by simp
+  case 0
+  show ?case by simp
 next
   case (Suc z)
-  thus ?case
+  then show ?case
   proof
     assume "\<exists>x<z. P x"
     then obtain x where le: "x < z" and P: "P x" by iprover
@@ -89,7 +86,7 @@
         with P have "\<exists>x<z. P x" by iprover
         with nex show False ..
       qed
-      thus ?case by iprover
+      then show ?case by iprover
     qed
   qed
 qed
diff -r 65a9eb946ff2 -r d10eab0672f9 src/HOL/Proofs/Extraction/Warshall.thy
--- a/src/HOL/Proofs/Extraction/Warshall.thy	Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Fri Jul 01 16:52:35 2016 +0200
@@ -15,34 +15,27 @@
 
 datatype b = T | F
 
-primrec
-  is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
-where
-    "is_path' r x [] z = (r x z = T)"
-  | "is_path' r x (y # ys) z = (r x y = T \<and> is_path' r y ys z)"
-
-definition
-  is_path :: "(nat \<Rightarrow> nat \<Rightarrow> b) \<Rightarrow> (nat * nat list * nat) \<Rightarrow>
-    nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+primrec is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
 where
-  "is_path r p i j k \<longleftrightarrow> fst p = j \<and> snd (snd p) = k \<and>
-     list_all (\<lambda>x. x < i) (fst (snd p)) \<and>
-     is_path' r (fst p) (fst (snd p)) (snd (snd p))"
+  "is_path' r x [] z \<longleftrightarrow> r x z = T"
+| "is_path' r x (y # ys) z \<longleftrightarrow> r x y = T \<and> is_path' r y ys z"
 
-definition
-  conc :: "('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a)"
-where
-  "conc p q = (fst p, fst (snd p) @ fst q # fst (snd q), snd (snd q))"
+definition is_path :: "(nat \<Rightarrow> nat \<Rightarrow> b) \<Rightarrow> (nat * nat list * nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+  where "is_path r p i j k \<longleftrightarrow>
+    fst p = j \<and> snd (snd p) = k \<and>
+    list_all (\<lambda>x. x < i) (fst (snd p)) \<and>
+    is_path' r (fst p) (fst (snd p)) (snd (snd p))"
 
-theorem is_path'_snoc [simp]:
-  "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
+definition conc :: "'a \<times> 'a list \<times> 'a \<Rightarrow> 'a \<times> 'a list \<times> 'a \<Rightarrow> 'a \<times> 'a list * 'a"
+  where "conc p q = (fst p, fst (snd p) @ fst q # fst (snd q), snd (snd q))"
+
+theorem is_path'_snoc [simp]: "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
   by (induct ys) simp+
 
 theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \<longleftrightarrow> P x \<and> list_all P xs"
-  by (induct xs, simp+, iprover)
+  by (induct xs) (simp+, iprover)
 
-theorem list_all_lemma: 
-  "list_all P xs \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> list_all Q xs"
+theorem list_all_lemma: "list_all P xs \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> list_all Q xs"
 proof -
   assume PQ: "\<And>x. P x \<Longrightarrow> Q x"
   show "list_all P xs \<Longrightarrow> list_all Q xs"
@@ -51,7 +44,7 @@
     show ?case by simp
   next
     case (Cons y ys)
-    hence Py: "P y" by simp
+    then have Py: "P y" by simp
     from Cons have Pys: "list_all P ys" by simp
     show ?case
       by simp (rule conjI PQ Py Cons Pys)+
@@ -59,7 +52,7 @@
 qed
 
 theorem lemma1: "\<And>p. is_path r p i j k \<Longrightarrow> is_path r p (Suc i) j k"
-  apply (unfold is_path_def)
+  unfolding is_path_def
   apply (simp cong add: conj_cong add: split_paired_all)
   apply (erule conjE)+
   apply (erule list_all_lemma)
@@ -67,7 +60,7 @@
   done
 
 theorem lemma2: "\<And>p. is_path r p 0 j k \<Longrightarrow> r j k = T"
-  apply (unfold is_path_def)
+  unfolding is_path_def
   apply (simp cong add: conj_cong add: split_paired_all)
   apply (case_tac "aa")
   apply simp+
@@ -80,11 +73,11 @@
   show "\<And>j. is_path' r j xs i \<Longrightarrow> is_path' r j (xs @ i # ys) k"
   proof (induct xs)
     case (Nil j)
-    hence "r j i = T" by simp
+    then have "r j i = T" by simp
     with pys show ?case by simp
   next
     case (Cons z zs j)
-    hence jzr: "r j z = T" by simp
+    then have jzr: "r j z = T" by simp
     from Cons have pzs: "is_path' r z zs i" by simp
     show ?case
       by simp (rule conjI jzr Cons pzs)+
@@ -93,7 +86,7 @@
 
 theorem lemma3:
   "\<And>p q. is_path r p i j i \<Longrightarrow> is_path r q i i k \<Longrightarrow>
-   is_path r (conc p q) (Suc i) j k"
+    is_path r (conc p q) (Suc i) j k"
   apply (unfold is_path_def conc_def)
   apply (simp cong add: conj_cong add: split_paired_all)
   apply (erule conjE)+
@@ -108,8 +101,8 @@
   done
 
 theorem lemma5:
-  "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> ~ is_path r p i j k \<Longrightarrow>
-   (\<exists>q. is_path r q i j i) \<and> (\<exists>q'. is_path r q' i i k)"
+  "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> \<not> is_path r p i j k \<Longrightarrow>
+    (\<exists>q. is_path r q i j i) \<and> (\<exists>q'. is_path r q' i i k)"
 proof (simp cong add: conj_cong add: split_paired_all is_path_def, (erule conjE)+)
   fix xs
   assume asms:
@@ -124,7 +117,7 @@
     \<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i" (is "PROP ?ih xs")
     proof (induct xs)
       case Nil
-      thus ?case by simp
+      then show ?case by simp
     next
       case (Cons a as j)
       show ?case
@@ -133,7 +126,7 @@
         show ?thesis
         proof
           from True and Cons have "r j i = T" by simp
-          thus "list_all (\<lambda>x. x < i) [] \<and> is_path' r j [] i" by simp
+          then show "list_all (\<lambda>x. x < i) [] \<and> is_path' r j [] i" by simp
         qed
       next
         case False
@@ -157,7 +150,7 @@
       \<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k" (is "PROP ?ih xs")
     proof (induct xs rule: rev_induct)
       case Nil
-      thus ?case by simp
+      then show ?case by simp
     next
       case (snoc a as k)
       show ?case
@@ -166,7 +159,7 @@
         show ?thesis
         proof
           from True and snoc have "r i k = T" by simp
-          thus "list_all (\<lambda>x. x < i) [] \<and> is_path' r i [] k" by simp
+          then show "list_all (\<lambda>x. x < i) [] \<and> is_path' r i [] k" by simp
         qed
       next
         case False
@@ -191,30 +184,29 @@
 
 theorem lemma5':
   "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> \<not> is_path r p i j k \<Longrightarrow>
-   \<not> (\<forall>q. \<not> is_path r q i j i) \<and> \<not> (\<forall>q'. \<not> is_path r q' i i k)"
+    \<not> (\<forall>q. \<not> is_path r q i j i) \<and> \<not> (\<forall>q'. \<not> is_path r q' i i k)"
   by (iprover dest: lemma5)
 
-theorem warshall: 
-  "\<And>j k. \<not> (\<exists>p. is_path r p i j k) \<or> (\<exists>p. is_path r p i j k)"
+theorem warshall: "\<And>j k. \<not> (\<exists>p. is_path r p i j k) \<or> (\<exists>p. is_path r p i j k)"
 proof (induct i)
   case (0 j k)
   show ?case
   proof (cases "r j k")
     assume "r j k = T"
-    hence "is_path r (j, [], k) 0 j k"
+    then have "is_path r (j, [], k) 0 j k"
       by (simp add: is_path_def)
-    hence "\<exists>p. is_path r p 0 j k" ..
-    thus ?thesis ..
+    then have "\<exists>p. is_path r p 0 j k" ..
+    then show ?thesis ..
   next
     assume "r j k = F"
-    hence "r j k ~= T" by simp
-    hence "\<not> (\<exists>p. is_path r p 0 j k)"
+    then have "r j k \<noteq> T" by simp
+    then have "\<not> (\<exists>p. is_path r p 0 j k)"
       by (iprover dest: lemma2)
-    thus ?thesis ..
+    then show ?thesis ..
   qed
 next
   case (Suc i j k)
-  thus ?case
+  then show ?case
   proof
     assume h1: "\<not> (\<exists>p. is_path r p i j k)"
     from Suc show ?case
@@ -222,7 +214,7 @@
       assume "\<not> (\<exists>p. is_path r p i j i)"
       with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)"
         by (iprover dest: lemma5')
-      thus ?case ..
+      then show ?case ..
     next
       assume "\<exists>p. is_path r p i j i"
       then obtain p where h2: "is_path r p i j i" ..
@@ -231,21 +223,21 @@
         assume "\<not> (\<exists>p. is_path r p i i k)"
         with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)"
           by (iprover dest: lemma5')
-        thus ?case ..
+        then show ?case ..
       next
         assume "\<exists>q. is_path r q i i k"
         then obtain q where "is_path r q i i k" ..
         with h2 have "is_path r (conc p q) (Suc i) j k" 
           by (rule lemma3)
-        hence "\<exists>pq. is_path r pq (Suc i) j k" ..
-        thus ?case ..
+        then have "\<exists>pq. is_path r pq (Suc i) j k" ..
+        then show ?case ..
       qed
     qed
   next
     assume "\<exists>p. is_path r p i j k"
-    hence "\<exists>p. is_path r p (Suc i) j k"
+    then have "\<exists>p. is_path r p (Suc i) j k"
       by (iprover intro: lemma1)
-    thus ?case ..
+    then show ?case ..
   qed
 qed