--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Wed Jun 10 16:09:49 2015 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Wed Jun 10 17:22:35 2015 +0200
@@ -220,18 +220,13 @@
proof -
let ?sum = "\<lambda>k::nat. \<Sum>j<k. j"
let ?inv = "\<lambda>s i::nat. s = ?sum i"
-
show ?thesis
proof hoare
show "?inv 0 1" by simp
- next
- fix s i
- assume "?inv s i \<and> i \<noteq> n"
- then show "?inv (s + i) (i + 1)" by simp
- next
- fix s i
- assume "?inv s i \<and> \<not> i \<noteq> n"
- then show "s = ?sum n" by simp
+ show "?inv (s + i) (i + 1)" if "?inv s i \<and> i \<noteq> n" for s i
+ using prems by simp
+ show "s = ?sum n" if "?inv s i \<and> \<not> i \<noteq> n" for s i
+ using prems by simp
qed
qed
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Jun 10 16:09:49 2015 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Jun 10 17:22:35 2015 +0200
@@ -208,9 +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: "b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))" for b :: nat
+ have card_suc: "card (?e (a \<union> t) b) = Suc (card (?e t b))" if "b < 2" for b :: nat
proof -
- 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)}"
proof -
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Wed Jun 10 16:09:49 2015 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Wed Jun 10 17:22:35 2015 +0200
@@ -37,17 +37,12 @@
subst_term_list f1 (subst_term_list f2 ts)"
show ?thesis
proof (induct t rule: subst_term.induct)
- fix a show "?P (Var a)" by simp
- next
- fix b ts assume "?Q ts"
- then show "?P (App b ts)"
- by (simp only: subst_simps)
- next
+ show "?P (Var a)" for a by simp
+ show "?P (App b ts)" if "?Q ts" for b ts
+ using prems by (simp only: subst_simps)
show "?Q []" by simp
- next
- fix t ts
- assume "?P t" "?Q ts" then show "?Q (t # ts)"
- by (simp only: subst_simps)
+ show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
+ using prems by (simp only: subst_simps)
qed
qed