author | blanchet |
Fri, 30 Aug 2013 11:27:23 +0200 | |
changeset 53303 | ae49b835ca01 |
permissions | -rw-r--r-- |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/BNF/Tools/bnf_fp_n2m_tactics.ML |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
3 |
Copyright 2013 |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
4 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
5 |
Tactics for mutualization of nested (co)datatypes. |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
6 |
*) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
7 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
8 |
signature BNF_FP_N2M_TACTICS = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
sig |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
10 |
val mk_rel_xtor_co_induct_tactic: BNF_FP_Util.fp_kind -> thm list -> thm list -> thm list -> |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
11 |
{prems: thm list, context: Proof.context} -> tactic |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
12 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
13 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
14 |
structure BNF_FP_N2M_Tactics : BNF_FP_N2M_TACTICS = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
15 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
16 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
17 |
open BNF_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
18 |
open BNF_FP_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
19 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
20 |
fun mk_rel_xtor_co_induct_tactic fp co_inducts rel_defs rel_monos |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
21 |
{context = ctxt, prems = raw_C_IHs} = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
22 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
23 |
val unfolds = map (fn def => unfold_thms ctxt (id_apply :: no_reflexive [def])) rel_defs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
24 |
val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
25 |
val C_IHs = map2 (curry op |>) folded_C_IHs unfolds; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
26 |
val C_IH_monos = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
27 |
map3 (fn C_IH => fn mono => fn unfold => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
28 |
(mono RSN (2, @{thm rev_predicate2D}), C_IH) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
29 |
|> fp = Greatest_FP ? swap |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
30 |
|> op RS |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
31 |
|> unfold) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
32 |
folded_C_IHs rel_monos unfolds; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
33 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
34 |
HEADGOAL (CONJ_WRAP_GEN' (rtac @{thm context_conjI}) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
35 |
(fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN' |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
36 |
REPEAT_ALL_NEW (FIRST' [eresolve_tac C_IHs, eresolve_tac C_IH_monos, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
37 |
rtac @{thm order_refl}, atac, resolve_tac co_inducts]))) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
38 |
co_inducts) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
39 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
40 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
41 |
end; |