src/ZF/WF.ML
changeset 485 5e00a676a211
parent 443 10884e64c241
child 494 3686157a5a51
equal deleted inserted replaced
484:70b789956bd3 485:5e00a676a211
    93 fun wf_ind_tac a prems i = 
    93 fun wf_ind_tac a prems i = 
    94     EVERY [res_inst_tac [("a",a)] wf_induct i,
    94     EVERY [res_inst_tac [("a",a)] wf_induct i,
    95 	   rename_last_tac a ["1"] (i+1),
    95 	   rename_last_tac a ["1"] (i+1),
    96 	   ares_tac prems i];
    96 	   ares_tac prems i];
    97 
    97 
    98 (*The form of this rule is designed to match wfI2*)
    98 (*The form of this rule is designed to match wfI*)
    99 val wfr::amem::prems = goal WF.thy
    99 val wfr::amem::prems = goal WF.thy
   100     "[| wf(r);  a:A;  field(r)<=A;  \
   100     "[| wf(r);  a:A;  field(r)<=A;  \
   101 \       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
   101 \       !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) \
   102 \    |]  ==>  P(a)";
   102 \    |]  ==>  P(a)";
   103 by (rtac (amem RS rev_mp) 1);
   103 by (rtac (amem RS rev_mp) 1);
   131 \       !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
   131 \       !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A  \
   132 \              |] ==> y:B |] \
   132 \              |] ==> y:B |] \
   133 \    ==>  wf(r)";
   133 \    ==>  wf(r)";
   134 by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1);
   134 by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1);
   135 by (REPEAT (ares_tac [indhyp] 1));
   135 by (REPEAT (ares_tac [indhyp] 1));
   136 val wfI2 = result();
   136 val wfI = result();
   137 
   137 
   138 
   138 
   139 (*** Properties of well-founded relations ***)
   139 (*** Properties of well-founded relations ***)
   140 
   140 
   141 goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";
   141 goal WF.thy "!!r. wf(r) ==> <a,a> ~: r";