# HG changeset patch
# User wenzelm
# Date 1433925568 -7200
# Node ID a197387e185497a74bf067935304b5710f9bb090
# Parent  240ad53041c9813918dd685e19edfd274b2168fd
tuned proofs;

diff -r 240ad53041c9 -r a197387e1854 src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Wed Jun 10 10:29:32 2015 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Wed Jun 10 10:39:28 2015 +0200
@@ -99,7 +99,7 @@
 
 lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
 proof -
-  have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
+  have "m = n \<longrightarrow> m + 1 \<noteq> n" for m n :: nat
       -- \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
       -- \<open>without mentioning the state space\<close>
     by simp
@@ -192,13 +192,13 @@
   also have "\<turnstile> \<dots> ?while \<lbrace>?inv \<acute>S \<acute>I \<and> \<not> \<acute>I \<noteq> n\<rbrace>"
   proof
     let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
-    have "\<And>s i. ?inv s i \<and> i \<noteq> n \<longrightarrow> ?inv (s + i) (i + 1)"
+    have "?inv s i \<and> i \<noteq> n \<longrightarrow> ?inv (s + i) (i + 1)" for s i
       by simp
     also have "\<turnstile> \<lbrace>\<acute>S + \<acute>I = ?sum (\<acute>I + 1)\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
       by hoare
     finally show "\<turnstile> \<lbrace>?inv \<acute>S \<acute>I \<and> \<acute>I \<noteq> n\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" .
   qed
-  also have "\<And>s i. s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n"
+  also have "s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n" for s i
     by simp
   finally show ?thesis .
 qed
diff -r 240ad53041c9 -r a197387e1854 src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Wed Jun 10 10:29:32 2015 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Wed Jun 10 10:39:28 2015 +0200
@@ -208,10 +208,8 @@
   let ?e = evnodd
   note hyp = \<open>card (?e t 0) = card (?e t 1)\<close>
     and at = \<open>a \<subseteq> - t\<close>
-  have card_suc:
-    "\<And>b. b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))"
+  have card_suc: "b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))" for b :: nat
   proof -
-    fix b :: nat
     assume "b < 2"
     have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un)
     also obtain i j where e: "?e a b = {(i, j)}"
@@ -230,7 +228,7 @@
       from e have "(i, j) \<in> ?e a b" by simp
       with at show "(i, j) \<notin> ?e t b" by (blast dest: evnoddD)
     qed
-    finally show "?thesis b" .
+    finally show ?thesis .
   qed
   then have "card (?e (a \<union> t) 0) = Suc (card (?e t 0))" by simp
   also from hyp have "card (?e t 0) = card (?e t 1)" .
diff -r 240ad53041c9 -r a197387e1854 src/HOL/Isar_Examples/Puzzle.thy
--- a/src/HOL/Isar_Examples/Puzzle.thy	Wed Jun 10 10:29:32 2015 +0200
+++ b/src/HOL/Isar_Examples/Puzzle.thy	Wed Jun 10 10:39:28 2015 +0200
@@ -16,52 +16,46 @@
   assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
   shows "f n = n"
 proof (rule order_antisym)
-  {
-    fix n show "n \<le> f n"
-    proof (induct "f n" arbitrary: n rule: less_induct)
-      case less
-      show "n \<le> f n"
-      proof (cases n)
-        case (Suc m)
-        from f_ax have "f (f m) < f n" by (simp only: Suc)
-        with less have "f m \<le> f (f m)" .
-        also from f_ax have "\<dots> < f n" by (simp only: Suc)
-        finally have "f m < f n" .
-        with less have "m \<le> f m" .
-        also note \<open>\<dots> < f n\<close>
-        finally have "m < f n" .
-        then have "n \<le> f n" by (simp only: Suc)
-        then show ?thesis .
-      next
-        case 0
-        then show ?thesis by simp
-      qed
+  show ge: "n \<le> f n" for n
+  proof (induct "f n" arbitrary: n rule: less_induct)
+    case less
+    show "n \<le> f n"
+    proof (cases n)
+      case (Suc m)
+      from f_ax have "f (f m) < f n" by (simp only: Suc)
+      with less have "f m \<le> f (f m)" .
+      also from f_ax have "\<dots> < f n" by (simp only: Suc)
+      finally have "f m < f n" .
+      with less have "m \<le> f m" .
+      also note \<open>\<dots> < f n\<close>
+      finally have "m < f n" .
+      then have "n \<le> f n" by (simp only: Suc)
+      then show ?thesis .
+    next
+      case 0
+      then show ?thesis by simp
     qed
-  } note ge = this
+  qed
 
-  {
-    fix m n :: nat
-    assume "m \<le> n"
-    then have "f m \<le> f n"
-    proof (induct n)
-      case 0
-      then have "m = 0" by simp
-      then show ?case by simp
+  have mono: "m \<le> n \<Longrightarrow> f m \<le> f n" for m n :: nat
+  proof (induct n)
+    case 0
+    then have "m = 0" by simp
+    then show ?case by simp
+  next
+    case (Suc n)
+    from Suc.prems show "f m \<le> f (Suc n)"
+    proof (rule le_SucE)
+      assume "m \<le> n"
+      with Suc.hyps have "f m \<le> f n" .
+      also from ge f_ax have "\<dots> < f (Suc n)"
+        by (rule le_less_trans)
+      finally show ?thesis by simp
     next
-      case (Suc n)
-      from Suc.prems show "f m \<le> f (Suc n)"
-      proof (rule le_SucE)
-        assume "m \<le> n"
-        with Suc.hyps have "f m \<le> f n" .
-        also from ge f_ax have "\<dots> < f (Suc n)"
-          by (rule le_less_trans)
-        finally show ?thesis by simp
-      next
-        assume "m = Suc n"
-        then show ?thesis by simp
-      qed
+      assume "m = Suc n"
+      then show ?thesis by simp
     qed
-  } note mono = this
+  qed
 
   show "f n \<le> n"
   proof -