src/HOL/WF.ML
changeset 5318 72bf8039b53f
parent 5316 7a8975451a89
child 5330 8c9fadda81f4
     1.1 --- a/src/HOL/WF.ML	Fri Aug 14 12:02:35 1998 +0200
     1.2 +++ b/src/HOL/WF.ML	Fri Aug 14 12:03:01 1998 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4   *---------------------------------------------------------------------------*)
     1.5  
     1.6  Goalw [wf_def] "wf r ==> x:Q --> (? z:Q. ! y. (y,z):r --> y~:Q)";
     1.7 -bd spec 1;
     1.8 +by (dtac spec 1);
     1.9  by (etac (mp RS spec) 1);
    1.10  by (Blast_tac 1);
    1.11  val lemma1 = result();
    1.12 @@ -140,32 +140,32 @@
    1.13  \        !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
    1.14  \                                  Domain(r j) Int Range(r i) = {} \
    1.15  \     |] ==> wf(UN i:I. r i)";
    1.16 -by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
    1.17 -by(Clarify_tac 1);
    1.18 -by(rename_tac "A a" 1);
    1.19 -by(case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
    1.20 - by(Clarify_tac 1);
    1.21 - by(EVERY1[dtac bspec, atac,
    1.22 +by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
    1.23 +by (Clarify_tac 1);
    1.24 +by (rename_tac "A a" 1);
    1.25 +by (case_tac "? i:I. ? a:A. ? b:A. (b,a) : r i" 1);
    1.26 + by (Clarify_tac 1);
    1.27 + by (EVERY1[dtac bspec, atac,
    1.28             eres_inst_tac[("x","{a. a:A & (? b:A. (b,a) : r i)}")]allE]);
    1.29 - by(EVERY1[etac allE,etac impE]);
    1.30 -  by(Blast_tac 1);
    1.31 - by(Clarify_tac 1);
    1.32 - by(rename_tac "z'" 1);
    1.33 - by(res_inst_tac [("x","z'")] bexI 1);
    1.34 -  ba 2;
    1.35 - by(Clarify_tac 1);
    1.36 - by(rename_tac "j" 1);
    1.37 - by(case_tac "r j = r i" 1);
    1.38 -  by(EVERY1[etac allE,etac impE,atac]);
    1.39 -  by(Asm_full_simp_tac 1);
    1.40 -  by(Blast_tac 1);
    1.41 - by(blast_tac (claset() addEs [equalityE]) 1);
    1.42 -by(Asm_full_simp_tac 1);
    1.43 -by(case_tac "? i. i:I" 1);
    1.44 - by(Clarify_tac 1);
    1.45 - by(EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
    1.46 - by(Blast_tac 1);
    1.47 -by(Blast_tac 1);
    1.48 + by (EVERY1[etac allE,etac impE]);
    1.49 +  by (Blast_tac 1);
    1.50 + by (Clarify_tac 1);
    1.51 + by (rename_tac "z'" 1);
    1.52 + by (res_inst_tac [("x","z'")] bexI 1);
    1.53 +  by (assume_tac 2);
    1.54 + by (Clarify_tac 1);
    1.55 + by (rename_tac "j" 1);
    1.56 + by (case_tac "r j = r i" 1);
    1.57 +  by (EVERY1[etac allE,etac impE,atac]);
    1.58 +  by (Asm_full_simp_tac 1);
    1.59 +  by (Blast_tac 1);
    1.60 + by (blast_tac (claset() addEs [equalityE]) 1);
    1.61 +by (Asm_full_simp_tac 1);
    1.62 +by (case_tac "? i. i:I" 1);
    1.63 + by (Clarify_tac 1);
    1.64 + by (EVERY1[dtac bspec, atac, eres_inst_tac[("x","A")]allE]);
    1.65 + by (Blast_tac 1);
    1.66 +by (Blast_tac 1);
    1.67  qed "wf_UN";
    1.68  
    1.69  Goalw [Union_def]
    1.70 @@ -173,16 +173,16 @@
    1.71  \    !r:R.!s:R. r ~= s --> Domain r Int Range s = {} & \
    1.72  \                          Domain s Int Range r = {} \
    1.73  \ |] ==> wf(Union R)";
    1.74 -br wf_UN 1;
    1.75 -by(Blast_tac 1);
    1.76 -by(Blast_tac 1);
    1.77 +by (rtac wf_UN 1);
    1.78 +by (Blast_tac 1);
    1.79 +by (Blast_tac 1);
    1.80  qed "wf_Union";
    1.81  
    1.82  Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \
    1.83  \     |] ==> wf(r Un s)";
    1.84 -br(simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1;
    1.85 -by(Blast_tac 1);
    1.86 -by(Blast_tac 1);
    1.87 +by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1);
    1.88 +by (Blast_tac 1);
    1.89 +by (Blast_tac 1);
    1.90  qed "wf_Un";
    1.91  
    1.92  (*---------------------------------------------------------------------------
    1.93 @@ -190,12 +190,12 @@
    1.94   *---------------------------------------------------------------------------*)
    1.95  
    1.96  Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)";
    1.97 -by(asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
    1.98 -by(Clarify_tac 1);
    1.99 -by(case_tac "? p. f p : Q" 1);
   1.100 -by(eres_inst_tac [("x","{p. f p : Q}")]allE 1);
   1.101 -by(fast_tac (claset() addDs [injD]) 1);
   1.102 -by(Blast_tac 1);
   1.103 +by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1);
   1.104 +by (Clarify_tac 1);
   1.105 +by (case_tac "? p. f p : Q" 1);
   1.106 +by (eres_inst_tac [("x","{p. f p : Q}")]allE 1);
   1.107 +by (fast_tac (claset() addDs [injD]) 1);
   1.108 +by (Blast_tac 1);
   1.109  qed "wf_prod_fun_image";
   1.110  
   1.111  (*** acyclic ***)