src/FOL/IFOL.ML
changeset 793 0b5c5f568d74
parent 779 4ab9176b45b7
child 821 650ee089809b
equal deleted inserted replaced
792:5d2a7634da46 793:0b5c5f568d74
   148   [ (cut_facts_tac prems 1),
   148   [ (cut_facts_tac prems 1),
   149     (REPEAT  (ares_tac [iffI,conjI] 1
   149     (REPEAT  (ares_tac [iffI,conjI] 1
   150       ORELSE  eresolve_tac [iffE,conjE,mp] 1
   150       ORELSE  eresolve_tac [iffE,conjE,mp] 1
   151       ORELSE  iff_tac prems 1)) ]);
   151       ORELSE  iff_tac prems 1)) ]);
   152 
   152 
       
   153 (*Reversed congruence rule!   Used in ZF/Order*)
       
   154 qed_goal "conj_cong2" IFOL.thy 
       
   155     "[| P <-> P';  P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')"
       
   156  (fn prems =>
       
   157   [ (cut_facts_tac prems 1),
       
   158     (REPEAT  (ares_tac [iffI,conjI] 1
       
   159       ORELSE  eresolve_tac [iffE,conjE,mp] 1
       
   160       ORELSE  iff_tac prems 1)) ]);
       
   161 
   153 qed_goal "disj_cong" IFOL.thy 
   162 qed_goal "disj_cong" IFOL.thy 
   154     "[| P <-> P';  Q <-> Q' |] ==> (P|Q) <-> (P'|Q')"
   163     "[| P <-> P';  Q <-> Q' |] ==> (P|Q) <-> (P'|Q')"
   155  (fn prems =>
   164  (fn prems =>
   156   [ (cut_facts_tac prems 1),
   165   [ (cut_facts_tac prems 1),
   157     (REPEAT  (eresolve_tac [iffE,disjE,disjI1,disjI2] 1
   166     (REPEAT  (eresolve_tac [iffE,disjE,disjI1,disjI2] 1