src/HOL/WF.ML
changeset 5318 72bf8039b53f
parent 5316 7a8975451a89
child 5330 8c9fadda81f4
--- a/src/HOL/WF.ML	Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/WF.ML	Fri Aug 14 12:03:01 1998 +0200
@@ -72,7 +72,7 @@
  *---------------------------------------------------------------------------*)
 
 Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
-bd spec 1;
+by (dtac spec 1);
 by (etac (mp RS spec) 1);
 by (Blast_tac 1);
 val lemma1 = result();
@@ -140,32 +140,32 @@
 \        !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
 \                                  Domain(r j) Int Range(r i) = {} \
 \     |] ==> wf(UN i:I. r i)";
-by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
-by(Clarify_tac 1);
-by(rename_tac "A a" 1);
-by(case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
- by(Clarify_tac 1);
- by(EVERY1[dtac bspec, atac,
+by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
+by (Clarify_tac 1);
+by (rename_tac "A a" 1);
+by (case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
+ by (Clarify_tac 1);
+ by (EVERY1[dtac bspec, atac,
            eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]);
- by(EVERY1[etac allE,etac impE]);
-  by(Blast_tac 1);
- by(Clarify_tac 1);
- by(rename_tac "z'" 1);
- by(res_inst_tac [("x","z'")] bexI 1);
-  ba 2;
- by(Clarify_tac 1);
- by(rename_tac "j" 1);
- by(case_tac "r j = r i" 1);
-  by(EVERY1[etac allE,etac impE,atac]);
-  by(Asm_full_simp_tac 1);
-  by(Blast_tac 1);
- by(blast_tac (claset() addEs [equalityE]) 1);
-by(Asm_full_simp_tac 1);
-by(case_tac "? i. i:I" 1);
- by(Clarify_tac 1);
- by(EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
- by(Blast_tac 1);
-by(Blast_tac 1);
+ by (EVERY1[etac allE,etac impE]);
+  by (Blast_tac 1);
+ by (Clarify_tac 1);
+ by (rename_tac "z'" 1);
+ by (res_inst_tac [("x","z'")] bexI 1);
+  by (assume_tac 2);
+ by (Clarify_tac 1);
+ by (rename_tac "j" 1);
+ by (case_tac "r j = r i" 1);
+  by (EVERY1[etac allE,etac impE,atac]);
+  by (Asm_full_simp_tac 1);
+  by (Blast_tac 1);
+ by (blast_tac (claset() addEs [equalityE]) 1);
+by (Asm_full_simp_tac 1);
+by (case_tac "? i. i:I" 1);
+ by (Clarify_tac 1);
+ by (EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
+ by (Blast_tac 1);
+by (Blast_tac 1);
 qed "wf_UN";
 
 Goalw [Union_def]
@@ -173,16 +173,16 @@
 \    !r:R.!s:R. r ~= s --> Domain r Int Range s = {} & \
 \                          Domain s Int Range r = {} \
 \ |] ==> wf(Union R)";
-br wf_UN 1;
-by(Blast_tac 1);
-by(Blast_tac 1);
+by (rtac wf_UN 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
 qed "wf_Union";
 
 Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
 \     |] ==> wf(r Un s)";
-br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
-by(Blast_tac 1);
-by(Blast_tac 1);
+by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
 qed "wf_Un";
 
 (*---------------------------------------------------------------------------
@@ -190,12 +190,12 @@
  *---------------------------------------------------------------------------*)
 
 Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
-by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
-by(Clarify_tac 1);
-by(case_tac "? p. f p : Q" 1);
-by(eres_inst_tac [("x","{p. f p : Q}")]allE 1);
-by(fast_tac (claset() addDs [injD]) 1);
-by(Blast_tac 1);
+by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
+by (Clarify_tac 1);
+by (case_tac "? p. f p : Q" 1);
+by (eres_inst_tac [("x","{p. f p : Q}")]allE 1);
+by (fast_tac (claset() addDs [injD]) 1);
+by (Blast_tac 1);
 qed "wf_prod_fun_image";
 
 (*** acyclic ***)