summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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 -