src/HOL/Isar_examples/MutilatedCheckerboard.thy

--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sun Jul 30 13:02:56 2000 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Sun Jul 30 13:03:49 2000 +0200
@@ -35,21 +35,19 @@
 proof;
   assume "t : tiling A" (is "_ : ?T");
   thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t");
-  proof induct;
-    show "?P {}"; by simp;
-
+  proof (induct (stripped) t);
+    assume "u : ?T" "{} Int u = {}"
+    thus "{} Un u : ?T" by simp;
+  next
     fix a t;
     assume "a : A" "t : ?T" "?P t" "a <= - t";
-    show "?P (a Un t)";
-    proof (intro impI);
-      assume "u : ?T" "(a Un t) Int u = {}";
-      have hyp: "t Un u: ?T"; by (blast!);
-      have "a <= - (t Un u)"; by (blast!);
-      with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
-      also; have "a Un (t Un u) = (a Un t) Un u";
-        by (simp only: Un_assoc);
-      finally; show "... : ?T"; .;
-    qed;
+    assume "u : ?T" "(a Un t) Int u = {}";
+    have hyp: "t Un u: ?T"; by (blast!);
+    have "a <= - (t Un u)"; by (blast!);
+    with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
+    also; have "a Un (t Un u) = (a Un t) Un u";
+      by (simp only: Un_assoc);
+    finally; show "... : ?T"; .;
   qed;
 qed;
 
@@ -139,7 +137,7 @@
     also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast;
     finally; show "... : domino"; .;
     from hyp; show "?B n : ?T"; .;
-    show "?a <= - ?B n"; by force;
+    show "?a <= - ?B n"; by blast;
   qed;
   finally; show "?P (Suc n)"; .;
 qed;
@@ -220,21 +218,21 @@
       "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))";
     proof -;
       fix b; assume "b < 2";
-      have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton);
-      thus "?thesis b";
-      proof (elim exE);
-	have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
-	also; fix i j; assume "?e a b = {(i, j)}";
-	also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
-	also; have "card ... = Suc (card (?e t b))";
-	proof (rule card_insert_disjoint);
-	  show "finite (?e t b)";
-            by (rule evnodd_finite, rule tiling_domino_finite);
-	  have "(i, j) : ?e a b"; by (simp!);
-	  thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD);
-	qed;
-	finally; show ?thesis; .;
+      have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
+      also; obtain i j where "?e a b = {(i, j)}";
+      proof -;
+	have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton);
+	thus ?thesis; by blast;
       qed;
+      also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
+      also; have "card ... = Suc (card (?e t b))";
+      proof (rule card_insert_disjoint);
+	show "finite (?e t b)";
+          by (rule evnodd_finite, rule tiling_domino_finite);
+	have "(i, j) : ?e a b"; by (simp!);
+	thus "(i, j) ~: ?e t b"; by (blast! dest: evnoddD);
+      qed;
+      finally; show "?thesis b"; .;
     qed;
     hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp;
     also; from hyp; have "card (?e t 0) = card (?e t 1)"; .;
@@ -276,7 +274,7 @@
         < card (?e ?t' 0)";
       proof (rule card_Diff1_less);
 	from _ fin; show "finite (?e ?t' 0)";
-          by (rule finite_subset) force;
+          by (rule finite_subset) auto;
 	show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp;
       qed;
       thus ?thesis; by simp;