equal
deleted
inserted
replaced
10 sig |
10 sig |
11 val mk_collect_set_map_tac: thm list -> tactic |
11 val mk_collect_set_map_tac: thm list -> tactic |
12 val mk_in_mono_tac: int -> tactic |
12 val mk_in_mono_tac: int -> tactic |
13 val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic |
13 val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic |
14 val mk_map_id: thm -> thm |
14 val mk_map_id: thm -> thm |
|
15 val mk_map_ident: Proof.context -> thm -> thm |
15 val mk_map_comp: thm -> thm |
16 val mk_map_comp: thm -> thm |
16 val mk_map_cong_tac: Proof.context -> thm -> tactic |
17 val mk_map_cong_tac: Proof.context -> thm -> tactic |
17 val mk_set_map: thm -> thm |
18 val mk_set_map: thm -> thm |
18 |
19 |
19 val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic |
20 val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic |
41 val ord_eq_le_trans = @{thm ord_eq_le_trans}; |
42 val ord_eq_le_trans = @{thm ord_eq_le_trans}; |
42 val ord_le_eq_trans = @{thm ord_le_eq_trans}; |
43 val ord_le_eq_trans = @{thm ord_le_eq_trans}; |
43 val conversep_shift = @{thm conversep_le_swap} RS iffD1; |
44 val conversep_shift = @{thm conversep_le_swap} RS iffD1; |
44 |
45 |
45 fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply}; |
46 fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply}; |
|
47 fun mk_map_ident ctxt = unfold_thms ctxt @{thms id_def}; |
46 fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp]; |
48 fun mk_map_comp comp = @{thm comp_eq_dest_lhs} OF [mk_sym comp]; |
47 fun mk_map_cong_tac ctxt cong0 = |
49 fun mk_map_cong_tac ctxt cong0 = |
48 (hyp_subst_tac ctxt THEN' rtac cong0 THEN' |
50 (hyp_subst_tac ctxt THEN' rtac cong0 THEN' |
49 REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; |
51 REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; |
50 fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest}; |
52 fun mk_set_map set_map0 = set_map0 RS @{thm comp_eq_dest}; |