src/HOL/Isar_examples/MutilatedCheckerboard.thy
 changeset 7565 bfa85f429629 parent 7480 0a0e0dbe1269 child 7761 7fab9592384f
```     1.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 21 17:30:11 1999 +0200
1.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 21 17:30:55 1999 +0200
1.3 @@ -38,8 +38,8 @@
1.4      show "?P (a Un t)";
1.5      proof (intro impI);
1.6        assume "u : ?T" "(a Un t) Int u = {}";
1.7 -      have hyp: "t Un u: ?T"; by blast;
1.8 -      have "a <= - (t Un u)"; by blast;
1.9 +      have hyp: "t Un u: ?T"; by (blast!);
1.10 +      have "a <= - (t Un u)"; by (blast!);
1.11        with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
1.12        also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc);
1.13        finally; show "... : ?T"; .;
1.14 @@ -153,11 +153,11 @@
1.15
1.16  lemma domino_singleton: "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
1.17  proof -;
1.18 -  assume "b < 2";
1.19 +  assume b: "b < 2";
1.20    assume "d : domino";
1.21    thus ?thesis (is "?P d");
1.22    proof (induct d set: domino);
1.23 -    have b_cases: "b = 0 | b = 1"; by arith;
1.24 +    from b; have b_cases: "b = 0 | b = 1"; by arith;
1.25      fix i j;
1.26      note [simp] = evnodd_empty evnodd_insert mod_Suc;
1.27      from b_cases; show "?P {(i, j), (i, j + 1)}"; by rule auto;
1.28 @@ -208,13 +208,13 @@
1.29        thus "?thesis b";
1.30        proof (elim exE);
1.31  	have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
1.32 -	also; fix i j; assume "?e a b = {(i, j)}";
1.33 +	also; fix i j; assume e: "?e a b = {(i, j)}";
1.34  	also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
1.35  	also; have "card ... = Suc (card (?e t b))";
1.36  	proof (rule card_insert_disjoint);
1.37  	  show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
1.38 -	  have "(i, j) : ?e a b"; by asm_simp;
1.39 -	  thus "(i, j) ~: ?e t b"; by (force dest: evnoddD);
1.40 +	  have "(i, j) : ?e a b"; by (simp!);
1.41 +	  thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD);
1.42  	qed;
1.43  	finally; show ?thesis; .;
1.44        qed;
```