--- a/src/HOL/Isar_examples/ExprCompiler.thy Tue Sep 21 17:30:11 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Tue Sep 21 17:30:55 1999 +0200
@@ -108,23 +108,23 @@
assume "?P xs";
show "?P (x # xs)" (is "?Q x");
proof (induct ?Q x type: instr);
- fix val; show "?Q (Const val)"; by force;
+ fix val; show "?Q (Const val)"; by (simp!);
next;
- fix adr; show "?Q (Load adr)"; by force;
+ fix adr; show "?Q (Load adr)"; by (simp!);
next;
- fix fun; show "?Q (Apply fun)"; by force;
+ fix fun; show "?Q (Apply fun)"; by (simp!);
qed;
qed;
lemma exec_comp:
"ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e");
proof (induct ?P e type: expr);
- fix adr; show "?P (Variable adr)"; by force;
+ fix adr; show "?P (Variable adr)"; by (simp!);
next;
- fix val; show "?P (Constant val)"; by force;
+ fix val; show "?P (Constant val)"; by (simp!);
next;
fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
- by (force simp add: exec_append);
+ by (simp! add: exec_append);
qed;
--- a/src/HOL/Isar_examples/MultisetOrder.thy Tue Sep 21 17:30:11 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy Tue Sep 21 17:30:55 1999 +0200
@@ -40,7 +40,7 @@
with N; have n: "N = K' + K + {#a#}"; by (simp add: union_ac);
assume "M0 = K' + {#a'#}";
- with r; have "?R (K' + K) M0"; by simp blast;
+ with r; have "?R (K' + K) M0"; by blast;
with n; have ?case1; by simp; thus ?thesis; ..;
qed;
qed;
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Tue Sep 21 17:30:11 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Tue Sep 21 17:30:55 1999 +0200
@@ -38,8 +38,8 @@
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;
+ 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"; .;
@@ -153,11 +153,11 @@
lemma domino_singleton: "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
proof -;
- assume "b < 2";
+ assume b: "b < 2";
assume "d : domino";
thus ?thesis (is "?P d");
proof (induct d set: domino);
- have b_cases: "b = 0 | b = 1"; by arith;
+ from b; have b_cases: "b = 0 | b = 1"; by arith;
fix i j;
note [simp] = evnodd_empty evnodd_insert mod_Suc;
from b_cases; show "?P {(i, j), (i, j + 1)}"; by rule auto;
@@ -208,13 +208,13 @@
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; fix i j; assume e: "?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 asm_simp;
- thus "(i, j) ~: ?e t b"; by (force dest: evnoddD);
+ have "(i, j) : ?e a b"; by (simp!);
+ thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD);
qed;
finally; show ?thesis; .;
qed;