accomodate refined facts handling;
authorwenzelm
Tue Sep 21 17:30:55 1999 +0200 (1999-09-21 ago)
changeset 7565bfa85f429629
parent 7564 90455fa8cebe
child 7566 c5a3f980a7af
accomodate refined facts handling;
tuned;
src/HOL/Isar_examples/ExprCompiler.thy
src/HOL/Isar_examples/MultisetOrder.thy
src/HOL/Isar_examples/MutilatedCheckerboard.thy
     1.1 --- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Sep 21 17:30:11 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/ExprCompiler.thy	Tue Sep 21 17:30:55 1999 +0200
     1.3 @@ -108,23 +108,23 @@
     1.4    assume "?P xs";
     1.5    show "?P (x # xs)" (is "?Q x");
     1.6    proof (induct ?Q x type: instr);
     1.7 -    fix val; show "?Q (Const val)"; by force;
     1.8 +    fix val; show "?Q (Const val)"; by (simp!);
     1.9    next;
    1.10 -    fix adr; show "?Q (Load adr)"; by force;
    1.11 +    fix adr; show "?Q (Load adr)"; by (simp!);
    1.12    next;
    1.13 -    fix fun; show "?Q (Apply fun)"; by force;
    1.14 +    fix fun; show "?Q (Apply fun)"; by (simp!);
    1.15    qed;
    1.16  qed;
    1.17  
    1.18  lemma exec_comp:
    1.19    "ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e");
    1.20  proof (induct ?P e type: expr);
    1.21 -  fix adr; show "?P (Variable adr)"; by force;
    1.22 +  fix adr; show "?P (Variable adr)"; by (simp!);
    1.23  next;
    1.24 -  fix val; show "?P (Constant val)"; by force;
    1.25 +  fix val; show "?P (Constant val)"; by (simp!);
    1.26  next;
    1.27    fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
    1.28 -    by (force simp add: exec_append);
    1.29 +    by (simp! add: exec_append);
    1.30  qed;
    1.31  
    1.32  
     2.1 --- a/src/HOL/Isar_examples/MultisetOrder.thy	Tue Sep 21 17:30:11 1999 +0200
     2.2 +++ b/src/HOL/Isar_examples/MultisetOrder.thy	Tue Sep 21 17:30:55 1999 +0200
     2.3 @@ -40,7 +40,7 @@
     2.4        with N; have n: "N = K' + K + {#a#}"; by (simp add: union_ac);
     2.5  
     2.6        assume "M0 = K' + {#a'#}";
     2.7 -      with r; have "?R (K' + K) M0"; by simp blast;
     2.8 +      with r; have "?R (K' + K) M0"; by blast;
     2.9        with n; have ?case1; by simp; thus ?thesis; ..;
    2.10      qed;
    2.11    qed;
     3.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 21 17:30:11 1999 +0200
     3.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 21 17:30:55 1999 +0200
     3.3 @@ -38,8 +38,8 @@
     3.4      show "?P (a Un t)";
     3.5      proof (intro impI);
     3.6        assume "u : ?T" "(a Un t) Int u = {}";
     3.7 -      have hyp: "t Un u: ?T"; by blast;
     3.8 -      have "a <= - (t Un u)"; by blast;
     3.9 +      have hyp: "t Un u: ?T"; by (blast!);
    3.10 +      have "a <= - (t Un u)"; by (blast!);
    3.11        with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un);
    3.12        also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc);
    3.13        finally; show "... : ?T"; .;
    3.14 @@ -153,11 +153,11 @@
    3.15  
    3.16  lemma domino_singleton: "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
    3.17  proof -;
    3.18 -  assume "b < 2";
    3.19 +  assume b: "b < 2";
    3.20    assume "d : domino";
    3.21    thus ?thesis (is "?P d");
    3.22    proof (induct d set: domino);
    3.23 -    have b_cases: "b = 0 | b = 1"; by arith;
    3.24 +    from b; have b_cases: "b = 0 | b = 1"; by arith;
    3.25      fix i j;
    3.26      note [simp] = evnodd_empty evnodd_insert mod_Suc;
    3.27      from b_cases; show "?P {(i, j), (i, j + 1)}"; by rule auto;
    3.28 @@ -208,13 +208,13 @@
    3.29        thus "?thesis b";
    3.30        proof (elim exE);
    3.31  	have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
    3.32 -	also; fix i j; assume "?e a b = {(i, j)}";
    3.33 +	also; fix i j; assume e: "?e a b = {(i, j)}";
    3.34  	also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
    3.35  	also; have "card ... = Suc (card (?e t b))";
    3.36  	proof (rule card_insert_disjoint);
    3.37  	  show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
    3.38 -	  have "(i, j) : ?e a b"; by asm_simp;
    3.39 -	  thus "(i, j) ~: ?e t b"; by (force dest: evnoddD);
    3.40 +	  have "(i, j) : ?e a b"; by (simp!);
    3.41 +	  thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD);
    3.42  	qed;
    3.43  	finally; show ?thesis; .;
    3.44        qed;