# HG changeset patch
# User paulson
# Date 905441031 -7200
# Node ID b38332431a8c311dbf9d7ec0c758d7b49333acaf
# Parent  08ca6e067ee6ccb67d1afcf21440025ff5fe1c0b
New theorem wf_not_sym and well-formed wf_asym

diff -r 08ca6e067ee6 -r b38332431a8c src/HOL/WF.ML
--- a/src/HOL/WF.ML	Thu Sep 10 17:23:16 1998 +0200
+++ b/src/HOL/WF.ML	Thu Sep 10 17:23:51 1998 +0200
@@ -36,12 +36,13 @@
            rename_last_tac a ["1"] (i+1),
            ares_tac prems i];
 
-Goal "[| wf(r);  (a,x):r;  (x,a):r |] ==> P";
-by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1);
-by (Blast_tac 1);
+Goal "wf(r) ==> ! x. (a,x):r --> (x,a)~:r";
 by (wf_ind_tac "a" [] 1);
 by (Blast_tac 1);
-qed "wf_asym";
+qed_spec_mp "wf_not_sym";
+
+(* [| wf(r);  (a,x):r;  ~P ==> (x,a):r |] ==> P *)
+bind_thm ("wf_asym", wf_not_sym RS swap);
 
 Goal "[| wf(r);  (a,a): r |] ==> P";
 by (blast_tac (claset() addEs [wf_asym]) 1);
@@ -219,10 +220,9 @@
 by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1);
 qed "wf_acyclic";
 
-Goalw [acyclic_def]
-  "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
+Goalw [acyclic_def] "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
 by (simp_tac (simpset() addsimps [trancl_insert]) 1);
-by (blast_tac (claset() addEs [make_elim rtrancl_trans]) 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
 qed "acyclic_insert";
 AddIffs [acyclic_insert];
 
diff -r 08ca6e067ee6 -r b38332431a8c src/ZF/WF.ML
--- a/src/ZF/WF.ML	Thu Sep 10 17:23:16 1998 +0200
+++ b/src/ZF/WF.ML	Thu Sep 10 17:23:51 1998 +0200
@@ -139,23 +139,34 @@
 by (Blast_tac 1);
 qed "wf_not_refl";
 
-Goal "[| wf(r);  <a,x>:r;  <x,a>:r |] ==> P";
-by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1);
-by (wf_ind_tac "a" [] 2);
-by (Blast_tac 2);
+Goal "wf(r) ==> ALL x. <a,x>:r --> <x,a> ~: r";
+by (wf_ind_tac "a" [] 1);
 by (Blast_tac 1);
-qed "wf_asym";
+qed_spec_mp "wf_not_sym";
+
+(* [| wf(r);  <a,x> : r;  ~P ==> <x,a> : r |] ==> P *)
+bind_thm ("wf_asym", wf_not_sym RS swap);
 
 Goal "[| wf[A](r); a: A |] ==> <a,a> ~: r";
 by (wf_on_ind_tac "a" [] 1);
 by (Blast_tac 1);
 qed "wf_on_not_refl";
 
-Goal "[| wf[A](r);  <a,b>:r;  <b,a>:r;  a:A;  b:A |] ==> P";
-by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1);
-by (wf_on_ind_tac "a" [] 2);
-by (Blast_tac 2);
+Goal "[| wf[A](r);  a:A;  b:A |] ==> <a,b>:r --> <b,a>~:r";
+by (res_inst_tac [("x","b")] bspec 1);
+by (assume_tac 2);
+by (wf_on_ind_tac "a" [] 1);
 by (Blast_tac 1);
+qed_spec_mp "wf_on_not_sym";
+
+(* [| wf[A](r);  <a,b> : r;  a:A;  b:A;  ~P ==> <b,a> : r |] ==> P *)
+bind_thm ("wf_on_asym", wf_on_not_sym RS swap);
+
+val prems =
+Goal "[| wf[A](r);  <a,b>:r;  ~P ==> <b,a>:r;  a:A;  b:A |] ==> P";
+by (rtac ccontr 1);
+by (rtac (wf_on_not_sym RS notE) 1);
+by (DEPTH_SOLVE (ares_tac prems 1));
 qed "wf_on_asym";
 
 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means