author wenzelm Wed, 10 Jun 2015 10:39:28 +0200 changeset 60410 a197387e1854 parent 60409 240ad53041c9 child 60411 8f7e1279251d
tuned proofs;
```--- 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```
```--- 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)" .```
```--- 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 -```