src/HOL/Tools/BNF/bnf_lfp_tactics.ML
changeset 63568 e63c8f2fbd28
parent 63312 d75d1e399698
child 67399 eab6ce8368fa
equal deleted inserted replaced
63567:41037360dcb7 63568:e63c8f2fbd28
   431         rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym),
   431         rtac ctxt (thm RS (infer_instantiate' ctxt [NONE, NONE, SOME ct] arg_cong) RS sym),
   432         EVERY' (map (fn Abs_inverse =>
   432         EVERY' (map (fn Abs_inverse =>
   433           EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
   433           EVERY' [rtac ctxt (o_apply RS trans RS ballI), etac ctxt (set_mp RS Abs_inverse),
   434             assume_tac ctxt])
   434             assume_tac ctxt])
   435         Abs_inverses)])
   435         Abs_inverses)])
   436     (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;;
   436     (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;
   437 
   437 
   438 fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor =
   438 fun mk_mor_fold_tac ctxt cT ct fold_defs ex_mor mor =
   439   (EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN'
   439   (EVERY' (map (stac ctxt) fold_defs) THEN' EVERY' [rtac ctxt rev_mp, rtac ctxt ex_mor, rtac ctxt impI] THEN'
   440   REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN'
   440   REPEAT_DETERM_N (length fold_defs) o etac ctxt exE THEN'
   441   rtac ctxt (Thm.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;
   441   rtac ctxt (Thm.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac ctxt mor) 1;