equal
deleted
inserted
replaced
5 Tactics for sugar on top of a BNF. |
5 Tactics for sugar on top of a BNF. |
6 *) |
6 *) |
7 |
7 |
8 signature BNF_SUGAR_TACTICS = |
8 signature BNF_SUGAR_TACTICS = |
9 sig |
9 sig |
|
10 val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic |
|
11 val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic |
10 val mk_nchotomy_tac: int -> thm -> tactic |
12 val mk_nchotomy_tac: int -> thm -> tactic |
11 val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic |
|
12 val mk_other_half_disc_disjoint_tac: thm -> tactic |
13 val mk_other_half_disc_disjoint_tac: thm -> tactic |
13 end; |
14 end; |
14 |
15 |
15 structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS = |
16 structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS = |
16 struct |
17 struct |
17 |
18 |
|
19 open BNF_Tactics |
18 open BNF_FP_Util |
20 open BNF_FP_Util |
19 |
21 |
20 fun mk_nchotomy_tac n exhaust = |
22 fun mk_nchotomy_tac n exhaust = |
21 (rtac allI THEN' rtac exhaust THEN' |
23 (rtac allI THEN' rtac exhaust THEN' |
22 EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; |
24 EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; |
28 rtac disc'_thm) 1; |
30 rtac disc'_thm) 1; |
29 |
31 |
30 fun mk_other_half_disc_disjoint_tac half_thm = |
32 fun mk_other_half_disc_disjoint_tac half_thm = |
31 (etac @{thm contrapos_pn} THEN' etac half_thm) 1; |
33 (etac @{thm contrapos_pn} THEN' etac half_thm) 1; |
32 |
34 |
|
35 fun mk_disc_exhaust_tac n exhaust discIs = |
|
36 (rtac exhaust THEN' |
|
37 EVERY' (map2 (fn k => fn discI => |
|
38 dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; |
|
39 |
33 end; |
40 end; |