author | blanchet |
Tue, 01 Oct 2013 14:05:25 +0200 | |
changeset 54006 | 9fe1bd54d437 |
parent 54003 | c4343c31f86d |
child 54009 | f138452e8265 |
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_lfp_compat.ML |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, 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 |
Compatibility layer with the old datatype package. |
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_LFP_COMPAT = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
sig |
53309 | 10 |
val datatype_new_compat_cmd : string list -> local_theory -> local_theory |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
11 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
12 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
13 |
structure BNF_LFP_Compat : BNF_LFP_COMPAT = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
14 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
15 |
|
54006 | 16 |
open Ctr_Sugar |
53303
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 |
open BNF_FP_Def_Sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
20 |
open BNF_FP_N2M_Sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
21 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
22 |
fun dtyp_of_typ _ (TFree a) = Datatype_Aux.DtTFree a |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
23 |
| dtyp_of_typ recTs (T as Type (s, Ts)) = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
24 |
(case find_index (curry (op =) T) recTs of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
25 |
~1 => Datatype_Aux.DtType (s, map (dtyp_of_typ recTs) Ts) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
26 |
| kk => Datatype_Aux.DtRec kk); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
27 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
28 |
val compatN = "compat_"; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
29 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
30 |
(* TODO: graceful failure for local datatypes -- perhaps by making the command global *) |
53309 | 31 |
fun datatype_new_compat_cmd raw_fpT_names lthy = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
32 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
33 |
val thy = Proof_Context.theory_of lthy; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
34 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
35 |
fun not_datatype s = error (quote s ^ " is not a new-style datatype"); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
36 |
fun not_mutually_recursive ss = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
37 |
error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes"); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
38 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
39 |
val (fpT_names as fpT_name1 :: _) = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
40 |
map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
41 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
42 |
val Ss = Sign.arity_sorts thy fpT_name1 HOLogic.typeS; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
43 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
44 |
val (unsorted_As, _) = lthy |> mk_TFrees (length Ss); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
45 |
val As = map2 resort_tfree Ss unsorted_As; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
46 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
47 |
fun lfp_sugar_of s = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
48 |
(case fp_sugar_of lthy s of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
49 |
SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
50 |
| _ => not_datatype s); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
51 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
52 |
val fp_sugar0 as {fp_res = {Ts = fpTs0, ...}, ...} = lfp_sugar_of fpT_name1; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
53 |
val fpT_names' = map (fst o dest_Type) fpTs0; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
54 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
55 |
val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
56 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
57 |
val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names'; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
58 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
59 |
fun add_nested_types_of (T as Type (s, _)) seen = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
60 |
if member (op =) seen T orelse s = @{type_name fun} then |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
61 |
seen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
62 |
else |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
63 |
(case try lfp_sugar_of s of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
64 |
SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
65 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
66 |
val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) []; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
67 |
val substT = Term.typ_subst_TVars rho; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
68 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
69 |
val mutual_Ts = map substT mutual_Ts0; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
70 |
|
53901 | 71 |
fun add_interesting_subtypes (U as Type (_, Us)) = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
72 |
(case filter (exists_subtype_in mutual_Ts) Us of [] => I |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
73 |
| Us' => insert (op =) U #> fold add_interesting_subtypes Us') |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
74 |
| add_interesting_subtypes _ = I; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
75 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
76 |
val ctrs = maps #ctrs ctr_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
77 |
val ctr_Ts = maps (binder_types o substT o fastype_of) ctrs |> distinct (op =); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
78 |
val subTs = fold add_interesting_subtypes ctr_Ts []; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
79 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
80 |
fold add_nested_types_of subTs (seen @ mutual_Ts) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
81 |
end |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
82 |
| NONE => error ("Unsupported recursion via type constructor " ^ quote s ^ |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
83 |
" not associated with new-style datatype (cf. \"datatype_new\")")); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
84 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
85 |
val Ts = add_nested_types_of fpT1 []; |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
86 |
val b_names = map base_name_of_typ Ts; |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
87 |
val compat_b_names = map (prefix compatN) b_names; |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
88 |
val compat_bs = map Binding.name compat_b_names; |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
89 |
val common_name = compatN ^ mk_common_name b_names; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
90 |
val nn_fp = length fpTs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
91 |
val nn = length Ts; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
92 |
val get_indices = K []; |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
93 |
val fp_sugars0 = if nn = 1 then [fp_sugar0] else map (lfp_sugar_of o fst o dest_Type) Ts; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
94 |
val callssss = pad_and_indexify_calls fp_sugars0 nn []; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
95 |
val has_nested = nn > nn_fp; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
96 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
97 |
val ((fp_sugars, (lfp_sugar_thms, _)), lthy) = |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
98 |
mutualize_fp_sugars false has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0 |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
99 |
lthy; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
100 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
101 |
val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
102 |
fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
103 |
val inducts = conj_dests nn induct; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
104 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
105 |
val frozen_Ts = map Type.legacy_freeze_type Ts; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
106 |
val mk_dtyp = dtyp_of_typ frozen_Ts; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
107 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
108 |
fun mk_ctr_descr (Const (s, T)) = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
109 |
(s, map mk_dtyp (binder_types (Type.legacy_freeze_type T))); |
54003 | 110 |
fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
111 |
(index, (T_name, map mk_dtyp Ts, map mk_ctr_descr ctrs)); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
112 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
113 |
val descr = map3 mk_typ_descr (0 upto nn - 1) frozen_Ts ctr_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
114 |
val recs = map (fst o dest_Const o co_rec_of) co_iterss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
115 |
val rec_thms = flat (map co_rec_of iter_thmsss); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
116 |
|
54003 | 117 |
fun mk_info ({T = Type (T_name0, _), index, ...} : fp_sugar) = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
118 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
119 |
val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
120 |
split, split_asm, ...} = nth ctr_sugars index; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
121 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
122 |
(T_name0, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
123 |
{index = index, descr = descr, inject = injects, distinct = distincts, induct = induct, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
124 |
inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
125 |
rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
126 |
case_cong = case_cong, weak_case_cong = weak_case_cong, split = split, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
127 |
split_asm = split_asm}) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
128 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
129 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
130 |
val infos = map mk_info (take nn_fp fp_sugars); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
131 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
132 |
val all_notes = |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
133 |
(case lfp_sugar_thms of |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
134 |
NONE => [] |
53808 | 135 |
| SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) => |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
136 |
let |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
137 |
val common_notes = |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
138 |
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
139 |
|> filter_out (null o #2) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
140 |
|> map (fn (thmN, thms, attrs) => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
141 |
((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
142 |
|
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
143 |
val notes = |
53747
a8253329ebe9
took out spurious attributes (no need for several code equations / simps for thesame constants)
blanchet
parents:
53746
diff
changeset
|
144 |
[(foldN, fold_thmss, []), |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
145 |
(inductN, map single induct_thms, induct_attrs), |
53747
a8253329ebe9
took out spurious attributes (no need for several code equations / simps for thesame constants)
blanchet
parents:
53746
diff
changeset
|
146 |
(recN, rec_thmss, [])] |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
147 |
|> filter_out (null o #2) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
148 |
|> maps (fn (thmN, thmss, attrs) => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
149 |
if forall null thmss then |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
150 |
[] |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
151 |
else |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
152 |
map2 (fn b_name => fn thms => |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
153 |
((Binding.qualify true b_name (Binding.name thmN), attrs), [(thms, [])])) |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
154 |
compat_b_names thmss); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
155 |
in |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
156 |
common_notes @ notes |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
157 |
end); |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
158 |
|
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
159 |
val register_interpret = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
160 |
Datatype_Data.register infos |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
161 |
#> Datatype_Data.interpretation_data (Datatype_Aux.default_config, map fst infos) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
162 |
in |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
163 |
lthy |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
164 |
|> Local_Theory.raw_theory register_interpret |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53309
diff
changeset
|
165 |
|> Local_Theory.notes all_notes |> snd |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
166 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
167 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
168 |
val _ = |
53309 | 169 |
Outer_Syntax.local_theory @{command_spec "datatype_new_compat"} |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
170 |
"register a new-style datatype as an old-style datatype" |
53309 | 171 |
(Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
172 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
173 |
end; |