author wenzelm Wed, 10 Jun 2015 17:22:35 +0200 changeset 60416 e1ff959f4f1b parent 60415 9d37b2330ee3 child 60417 014d77e5c1ab
tuned proofs;
```--- 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
```