author | blanchet |
Fri, 31 Aug 2012 15:04:03 +0200 | |
changeset 49051 | 58d3c939f91a |
parent 49050 | 9f4a7ed344b4 |
child 49052 | 3510b943dd5b |
permissions | -rw-r--r-- |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Codatatype/Tools/bnf_sugar_tactics.ML |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
4 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
5 |
Tactics for sugar on top of a BNF. |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
6 |
*) |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
7 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
8 |
signature BNF_SUGAR_TACTICS = |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
9 |
sig |
49049 | 10 |
val mk_case_cong_tac: thm -> thm list -> tactic |
49048
4e0f0f98be02
rationalized data structure for distinctness theorems
blanchet
parents:
49047
diff
changeset
|
11 |
val mk_case_disc_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic |
49030 | 12 |
val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm list -> tactic |
49029 | 13 |
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic |
14 |
val mk_half_disc_disjoint_tac: int -> thm -> thm -> tactic |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
15 |
val mk_nchotomy_tac: int -> thm -> tactic |
49028 | 16 |
val mk_other_half_disc_disjoint_tac: thm -> tactic |
49049 | 17 |
val mk_split_tac: thm -> thm list -> thm list -> thm list -> tactic |
49044 | 18 |
val mk_split_asm_tac: Proof.context -> thm -> tactic |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
19 |
end; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
20 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
21 |
structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS = |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
22 |
struct |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
23 |
|
49050 | 24 |
open BNF_Util |
49029 | 25 |
open BNF_Tactics |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
26 |
open BNF_FP_Util |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
27 |
|
49051 | 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} |
|
49031 | 33 |
|
49047 | 34 |
fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms |
49032 | 35 |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
36 |
fun mk_nchotomy_tac n exhaust = |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
37 |
(rtac allI THEN' rtac exhaust THEN' |
49022 | 38 |
EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1; |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
39 |
|
49030 | 40 |
fun mk_half_disc_disjoint_tac m discD disc'_thm = |
41 |
(dtac discD THEN' |
|
49028 | 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_disjoint_tac half_thm = |
|
47 |
(etac @{thm contrapos_pn} THEN' etac half_thm) 1; |
|
48 |
||
49029 | 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 |
||
49030 | 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' |
|
49031 | 61 |
SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN' |
49030 | 62 |
rtac refl)) 1; |
63 |
||
49050 | 64 |
fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss = |
65 |
(rtac exhaust' THEN' |
|
49051 | 66 |
EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms => EVERY' [ |
49050 | 67 |
hyp_subst_tac THEN' |
49051 | 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; |
|
49031 | 71 |
|
49049 | 72 |
fun mk_case_cong_tac exhaust' case_thms = |
49047 | 73 |
(rtac exhaust' THEN' |
74 |
EVERY' (maps (fn case_thm => [dtac sym, asm_simp_tac (ss_only [case_thm])]) case_thms)) 1; |
|
49043 | 75 |
|
76 |
val naked_ctxt = Proof_Context.init_global @{theory HOL}; |
|
77 |
||
49049 | 78 |
fun mk_split_tac exhaust' case_thms injects distincts = |
49043 | 79 |
rtac exhaust' 1 THEN |
80 |
ALLGOALS (hyp_subst_tac THEN' |
|
49047 | 81 |
simp_tac (ss_only (@{thms simp_thms} @ case_thms @ injects @ distincts))) THEN |
49045
7d9631754bba
minor fixes (for compatibility with existing datatype package)
blanchet
parents:
49044
diff
changeset
|
82 |
ALLGOALS (blast_tac naked_ctxt); |
49032 | 83 |
|
49044 | 84 |
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; |
85 |
||
86 |
fun mk_split_asm_tac ctxt split = |
|
87 |
rtac (split RS trans) 1 THEN |
|
88 |
Local_Defs.unfold_tac ctxt split_asm_thms THEN |
|
89 |
rtac refl 1; |
|
90 |
||
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
91 |
end; |