src/HOL/WF_Rel.ML
changeset 4751 6fbd9838ccae
parent 4749 35b47e36e615
child 5069 3ea049f7979d
equal deleted inserted replaced
4750:f83cd6a06676 4751:6fbd9838ccae
   116 by (split_all_tac 1);
   116 by (split_all_tac 1);
   117 by (Asm_full_simp_tac 1);
   117 by (Asm_full_simp_tac 1);
   118 qed_spec_mp "finite_acyclic_wf";
   118 qed_spec_mp "finite_acyclic_wf";
   119 
   119 
   120 qed_goal "finite_acyclic_wf_converse" thy 
   120 qed_goal "finite_acyclic_wf_converse" thy 
   121  "X. finite r; acyclic r  wf (r^-1)" (K [
   121  "!!X. [|finite r; acyclic r|] ==> wf (r^-1)" (K [
   122 	etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
   122 	etac (finite_converse RS iffD2 RS finite_acyclic_wf) 1,
   123 	etac (acyclic_converse RS iffD2) 1]);
   123 	etac (acyclic_converse RS iffD2) 1]);
   124 
   124 
   125 goal thy "!!r. finite r ==> wf r = acyclic r";
   125 goal thy "!!r. finite r ==> wf r = acyclic r";
   126 by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);
   126 by (blast_tac (claset() addIs [finite_acyclic_wf,wf_acyclic]) 1);