src/HOL/WF.ML
changeset 5452 b38332431a8c
parent 5337 2f7d09a927c4
child 5521 7970832271cc
     1.1 --- a/src/HOL/WF.ML	Thu Sep 10 17:23:16 1998 +0200
     1.2 +++ b/src/HOL/WF.ML	Thu Sep 10 17:23:51 1998 +0200
     1.3 @@ -36,12 +36,13 @@
     1.4             rename_last_tac a ["1"] (i+1),
     1.5             ares_tac prems i];
     1.6  
     1.7 -Goal "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
     1.8 -by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
     1.9 -by (Blast_tac 1);
    1.10 +Goal "wf(r) ==> ! x. (a,x):r --> (x,a)~:r";
    1.11  by (wf_ind_tac "a" [] 1);
    1.12  by (Blast_tac 1);
    1.13 -qed "wf_asym";
    1.14 +qed_spec_mp "wf_not_sym";
    1.15 +
    1.16 +(* [| wf(r);  (a,x):r;  ~P ==> (x,a):r |] ==> P *)
    1.17 +bind_thm ("wf_asym", wf_not_sym RS swap);
    1.18  
    1.19  Goal "[| wf(r);  (a,a): r |] ==> P";
    1.20  by (blast_tac (claset() addEs [wf_asym]) 1);
    1.21 @@ -219,10 +220,9 @@
    1.22  by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1);
    1.23  qed "wf_acyclic";
    1.24  
    1.25 -Goalw [acyclic_def]
    1.26 -  "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
    1.27 +Goalw [acyclic_def] "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
    1.28  by (simp_tac (simpset() addsimps [trancl_insert]) 1);
    1.29 -by (blast_tac (claset() addEs [make_elim rtrancl_trans]) 1);
    1.30 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
    1.31  qed "acyclic_insert";
    1.32  AddIffs [acyclic_insert];
    1.33