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;