author | blanchet |
Thu, 30 Aug 2012 14:27:26 +0200 | |
changeset 49029 | f0ecfa9575a9 |
parent 49028 | 487427a02bee |
child 49030 | d0f4f113e43d |
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 |
49029 | 10 |
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic |
11 |
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
|
12 |
val mk_nchotomy_tac: int -> thm -> tactic |
49028 | 13 |
val mk_other_half_disc_disjoint_tac: thm -> tactic |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
14 |
end; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
15 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
16 |
structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS = |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
17 |
struct |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
18 |
|
49029 | 19 |
open BNF_Tactics |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
20 |
open BNF_FP_Util |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
21 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
22 |
fun mk_nchotomy_tac n exhaust = |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
23 |
(rtac allI THEN' rtac exhaust THEN' |
49022 | 24 |
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
|
25 |
|
49028 | 26 |
fun mk_half_disc_disjoint_tac m disc_def disc'_thm = |
27 |
(dtac (disc_def RS iffD1) THEN' |
|
28 |
REPEAT_DETERM_N m o etac exE THEN' |
|
29 |
hyp_subst_tac THEN' |
|
30 |
rtac disc'_thm) 1; |
|
31 |
||
32 |
fun mk_other_half_disc_disjoint_tac half_thm = |
|
33 |
(etac @{thm contrapos_pn} THEN' etac half_thm) 1; |
|
34 |
||
49029 | 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 |
||
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
40 |
end; |