equal
deleted
inserted
replaced
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)); |