|
1 (* Title: HOL/Codatatype/Tools/bnf_wrap_tactics.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Tactics for wrapping datatypes. |
|
6 *) |
|
7 |
|
8 signature BNF_WRAP_TACTICS = |
|
9 sig |
|
10 val mk_case_cong_tac: thm -> thm list -> tactic |
|
11 val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic |
|
12 val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic |
|
13 val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic |
|
14 val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic |
|
15 val mk_nchotomy_tac: int -> thm -> tactic |
|
16 val mk_other_half_disc_exclus_tac: thm -> tactic |
|
17 val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic |
|
18 val mk_split_asm_tac: Proof.context -> thm -> tactic |
|
19 end; |
|
20 |
|
21 structure BNF_Wrap_Tactics : BNF_WRAP_TACTICS = |
|
22 struct |
|
23 |
|
24 open BNF_Util |
|
25 open BNF_Tactics |
|
26 open BNF_FP_Util |
|
27 |
|
28 fun triangle _ [] = [] |
|
29 | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss |
|
30 |
|
31 fun mk_if_P_or_not_P thm = |
|
32 thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P} |
|
33 |
|
34 fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms |
|
35 |
|
36 fun mk_nchotomy_tac n exhaust = |
|
37 (rtac allI THEN' rtac exhaust THEN' |
|
38 EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; |
|
39 |
|
40 fun mk_half_disc_exclus_tac m discD disc'_thm = |
|
41 (dtac discD THEN' |
|
42 REPEAT_DETERM_N m o etac exE THEN' |
|
43 hyp_subst_tac THEN' |
|
44 rtac disc'_thm) 1; |
|
45 |
|
46 fun mk_other_half_disc_exclus_tac half_thm = |
|
47 (etac @{thm contrapos_pn} THEN' etac half_thm) 1; |
|
48 |
|
49 fun mk_disc_exhaust_tac n exhaust discIs = |
|
50 (rtac exhaust THEN' |
|
51 EVERY' (map2 (fn k => fn discI => |
|
52 dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1; |
|
53 |
|
54 fun mk_ctr_sel_tac ctxt m discD sel_thms = |
|
55 (dtac discD THEN' |
|
56 (if m = 0 then |
|
57 atac |
|
58 else |
|
59 REPEAT_DETERM_N m o etac exE THEN' |
|
60 hyp_subst_tac THEN' |
|
61 SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' |
|
62 rtac refl)) 1; |
|
63 |
|
64 fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = |
|
65 (rtac exhaust' THEN' |
|
66 EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [ |
|
67 hyp_subst_tac THEN' |
|
68 SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN' |
|
69 rtac case_thm]) case_thms |
|
70 (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss'))) sel_thmss)) 1; |
|
71 |
|
72 fun mk_case_cong_tac exhaust' case_thms = |
|
73 (rtac exhaust' THEN' |
|
74 EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1; |
|
75 |
|
76 val naked_ctxt = Proof_Context.init_global @{theory HOL}; |
|
77 |
|
78 fun mk_split_tac exhaust' case_thms injectss distinctsss = |
|
79 rtac exhaust' 1 THEN |
|
80 ALLGOALS (fn k => |
|
81 (hyp_subst_tac THEN' |
|
82 simp_tac (ss_only (@{thms simp_thms} @ case_thms @ nth injectss (k - 1) @ |
|
83 flat (nth distinctsss (k - 1))))) k) THEN |
|
84 ALLGOALS (blast_tac naked_ctxt); |
|
85 |
|
86 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; |
|
87 |
|
88 fun mk_split_asm_tac ctxt split = |
|
89 rtac (split RS trans) 1 THEN |
|
90 Local_Defs.unfold_tac ctxt split_asm_thms THEN |
|
91 rtac refl 1; |
|
92 |
|
93 end; |