|
1 (* Title: HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Tactics for wrapping existing freely generated type's constructors. |
|
6 *) |
|
7 |
|
8 signature BNF_CTR_SUGAR_TACTICS = |
|
9 sig |
|
10 val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic |
|
11 val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic |
|
12 val mk_case_conv_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list -> |
|
13 tactic |
|
14 val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic |
|
15 val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic |
|
16 val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list -> |
|
17 thm list list list -> thm list list list -> tactic |
|
18 val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic |
|
19 val mk_nchotomy_tac: int -> thm -> tactic |
|
20 val mk_other_half_disc_exclude_tac: thm -> tactic |
|
21 val mk_split_tac: Proof.context -> |
|
22 thm -> thm list -> thm list list -> thm list list list -> tactic |
|
23 val mk_split_asm_tac: Proof.context -> thm -> tactic |
|
24 val mk_unique_disc_def_tac: int -> thm -> tactic |
|
25 end; |
|
26 |
|
27 structure BNF_Ctr_Sugar_Tactics : BNF_CTR_SUGAR_TACTICS = |
|
28 struct |
|
29 |
|
30 open BNF_Util |
|
31 open BNF_Tactics |
|
32 |
|
33 val meta_mp = @{thm meta_mp}; |
|
34 |
|
35 fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P}); |
|
36 |
|
37 fun mk_nchotomy_tac n exhaust = |
|
38 (rtac allI THEN' rtac exhaust THEN' |
|
39 EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; |
|
40 |
|
41 fun mk_unique_disc_def_tac m uexhaust = |
|
42 EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1; |
|
43 |
|
44 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust = |
|
45 EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans), |
|
46 rtac @{thm iffI_np}, REPEAT_DETERM o etac exE, |
|
47 hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, |
|
48 rtac distinct, rtac uexhaust] @ |
|
49 (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac]) |
|
50 |> k = 1 ? swap |> op @)) 1; |
|
51 |
|
52 fun mk_half_disc_exclude_tac m discD disc' = |
|
53 (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' rtac disc') 1; |
|
54 |
|
55 fun mk_other_half_disc_exclude_tac half = (etac @{thm contrapos_pn} THEN' etac half) 1; |
|
56 |
|
57 fun mk_disc_exhaust_tac n exhaust discIs = |
|
58 (rtac exhaust THEN' |
|
59 EVERY' (map2 (fn k => fn discI => |
|
60 dtac discI THEN' select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) discIs)) 1; |
|
61 |
|
62 fun mk_collapse_tac ctxt m discD sels = |
|
63 (dtac discD THEN' |
|
64 (if m = 0 then |
|
65 atac |
|
66 else |
|
67 REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN' |
|
68 SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1; |
|
69 |
|
70 fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss |
|
71 disc_excludesss' = |
|
72 if ms = [0] then |
|
73 (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN' |
|
74 TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac]) 1 |
|
75 else |
|
76 let val ks = 1 upto n in |
|
77 (rtac udisc_exhaust THEN' |
|
78 EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => |
|
79 fn uuncollapse => |
|
80 EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, |
|
81 rtac sym, rtac vdisc_exhaust, |
|
82 EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse => |
|
83 EVERY' |
|
84 (if k' = k then |
|
85 [rtac (vuncollapse RS trans), TRY o atac] @ |
|
86 (if m = 0 then |
|
87 [rtac refl] |
|
88 else |
|
89 [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac], |
|
90 REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, |
|
91 asm_simp_tac (ss_only [] ctxt)]) |
|
92 else |
|
93 [dtac (the_single (if k = n then disc_excludes else disc_excludes')), |
|
94 etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}), |
|
95 atac, atac])) |
|
96 ks disc_excludess disc_excludess' uncollapses)]) |
|
97 ks ms disc_excludesss disc_excludesss' uncollapses)) 1 |
|
98 end; |
|
99 |
|
100 fun mk_case_conv_tac ctxt n uexhaust cases discss' selss = |
|
101 (rtac uexhaust THEN' |
|
102 EVERY' (map3 (fn casex => fn if_discs => fn sels => |
|
103 EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex]) |
|
104 cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1; |
|
105 |
|
106 fun mk_case_cong_tac ctxt uexhaust cases = |
|
107 (rtac uexhaust THEN' |
|
108 EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)) 1; |
|
109 |
|
110 val naked_ctxt = @{theory_context HOL}; |
|
111 |
|
112 (* TODO: More precise "simp_thms"; get rid of "blast_tac" *) |
|
113 fun mk_split_tac ctxt uexhaust cases injectss distinctsss = |
|
114 rtac uexhaust 1 THEN |
|
115 ALLGOALS (fn k => (hyp_subst_tac THEN' |
|
116 simp_tac (ss_only (@{thms simp_thms} @ cases @ nth injectss (k - 1) @ |
|
117 flat (nth distinctsss (k - 1))) ctxt)) k) THEN |
|
118 ALLGOALS (blast_tac naked_ctxt); |
|
119 |
|
120 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; |
|
121 |
|
122 fun mk_split_asm_tac ctxt split = |
|
123 rtac (split RS trans) 1 THEN unfold_thms_tac ctxt split_asm_thms THEN rtac refl 1; |
|
124 |
|
125 end; |