--- 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 -