src/HOL/BNF/Tools/bnf_comp_tactics.ML
changeset 54841 af71b753c459
parent 54189 c0186a0d8cb3
equal deleted inserted replaced
54840:fac0c76bbda2 54841:af71b753c459
    29   val lift_in_alt_tac: tactic
    29   val lift_in_alt_tac: tactic
    30   val mk_lift_set_bd_tac: thm -> tactic
    30   val mk_lift_set_bd_tac: thm -> tactic
    31 
    31 
    32   val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic
    32   val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic
    33 
    33 
    34   val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
    34   val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
    35   val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
    35   val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
    36   val mk_simple_wit_tac: thm list -> tactic
    36   val mk_simple_wit_tac: thm list -> tactic
    37 end;
    37 end;
    38 
    38 
    39 structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
    39 structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
   239 fun mk_permute_in_alt_tac src dest =
   239 fun mk_permute_in_alt_tac src dest =
   240   (rtac @{thm Collect_cong} THEN'
   240   (rtac @{thm Collect_cong} THEN'
   241   mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
   241   mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
   242     dest src) 1;
   242     dest src) 1;
   243 
   243 
   244 fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
   244 fun mk_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
   245   (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
   245   EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1;
   246   WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
       
   247   TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
       
   248 
   246 
   249 fun mk_simple_rel_OO_Grp_tac rel_OO_Grp in_alt_thm =
   247 fun mk_simple_rel_OO_Grp_tac rel_OO_Grp in_alt_thm =
   250   rtac (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
   248   rtac (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
   251 
   249 
   252 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
   250 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));