author | blanchet |
Thu, 30 Aug 2012 09:47:46 +0200 | |
changeset 49022 | 005ce926a932 |
parent 49020 | f379cf5d71bd |
child 49028 | 487427a02bee |
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 |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
10 |
val mk_nchotomy_tac: int -> thm -> tactic |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
11 |
end; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
12 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
13 |
structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS = |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
14 |
struct |
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 |
open BNF_FP_Util |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
17 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
18 |
fun mk_nchotomy_tac n exhaust = |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
19 |
(rtac allI THEN' rtac exhaust THEN' |
49022 | 20 |
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
|
21 |
|
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
22 |
end; |