6 Tactics for definition of bounded natural functors. |
6 Tactics for definition of bounded natural functors. |
7 *) |
7 *) |
8 |
8 |
9 signature BNF_DEF_TACTICS = |
9 signature BNF_DEF_TACTICS = |
10 sig |
10 sig |
11 val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic |
11 val mk_collect_set_natural_tac: thm list -> tactic |
12 val mk_id': thm -> thm |
12 val mk_id': thm -> thm |
13 val mk_comp': thm -> thm |
13 val mk_comp': thm -> thm |
14 val mk_in_mono_tac: int -> tactic |
14 val mk_in_mono_tac: int -> tactic |
15 val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic |
15 val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic |
16 val mk_set_natural': thm -> thm |
16 val mk_set_natural': thm -> thm |
42 REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN |
42 REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN |
43 REPEAT_DETERM_N (n - 1) |
43 REPEAT_DETERM_N (n - 1) |
44 ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN |
44 ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN |
45 (etac subset_trans THEN' atac) 1; |
45 (etac subset_trans THEN' atac) 1; |
46 |
46 |
47 fun mk_collect_set_natural_tac ctxt set_naturals = |
47 fun mk_collect_set_natural_tac set_naturals = |
48 substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1; |
48 (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' |
|
49 EVERY' (map (fn set_natural => |
|
50 rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN' |
|
51 rtac set_natural) set_naturals) THEN' |
|
52 rtac @{thm image_empty}) 1; |
49 |
53 |
50 fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals = |
54 fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals = |
51 if null set_naturals then |
55 if null set_naturals then |
52 EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 |
56 EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1 |
53 else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, |
57 else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull}, |