author | blanchet |
Tue, 03 Mar 2015 16:37:45 +0100 | |
changeset 59576 | 913c4afb0388 |
parent 59498 | 50b60f501b05 |
child 59578 | 5f56d4ff6635 |
permissions | -rw-r--r-- |
56638 | 1 |
(* Title: HOL/Tools/BNF/bnf_lfp_size.ML |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Copyright 2014 |
|
4 |
||
58315 | 5 |
Generation of size functions for datatypes. |
56638 | 6 |
*) |
7 |
||
56642
15cd15f9b40c
allow registration of custom size functions for BNF-based datatypes
blanchet
parents:
56640
diff
changeset
|
8 |
signature BNF_LFP_SIZE = |
15cd15f9b40c
allow registration of custom size functions for BNF-based datatypes
blanchet
parents:
56640
diff
changeset
|
9 |
sig |
56651 | 10 |
val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory |
11 |
val register_size_global: string -> string -> thm list -> thm list -> theory -> theory |
|
58179 | 12 |
val size_of: Proof.context -> string -> (string * (thm list * thm list)) option |
13 |
val size_of_global: theory -> string -> (string * (thm list * thm list)) option |
|
56642
15cd15f9b40c
allow registration of custom size functions for BNF-based datatypes
blanchet
parents:
56640
diff
changeset
|
14 |
end; |
15cd15f9b40c
allow registration of custom size functions for BNF-based datatypes
blanchet
parents:
56640
diff
changeset
|
15 |
|
15cd15f9b40c
allow registration of custom size functions for BNF-based datatypes
blanchet
parents:
56640
diff
changeset
|
16 |
structure BNF_LFP_Size : BNF_LFP_SIZE = |
56638 | 17 |
struct |
18 |
||
19 |
open BNF_Util |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
20 |
open BNF_Tactics |
56638 | 21 |
open BNF_Def |
58179 | 22 |
open BNF_FP_Def_Sugar |
56638 | 23 |
|
58337 | 24 |
val size_N = "size_"; |
25 |
val sizeN = "size"; |
|
58736 | 26 |
val size_genN = "size_gen"; |
58738 | 27 |
val size_gen_o_mapN = "size_gen_o_map"; |
58913 | 28 |
val size_neqN = "size_neq"; |
56638 | 29 |
|
56651 | 30 |
val nitpicksimp_attrs = @{attributes [nitpick_simp]}; |
31 |
val simp_attrs = @{attributes [simp]}; |
|
32 |
||
33 |
structure Data = Generic_Data |
|
56638 | 34 |
( |
35 |
type T = (string * (thm list * thm list)) Symtab.table; |
|
36 |
val empty = Symtab.empty; |
|
37 |
val extend = I |
|
38 |
fun merge data = Symtab.merge (K true) data; |
|
39 |
); |
|
40 |
||
58738 | 41 |
fun register_size T_name size_name size_simps size_gen_o_maps = |
42 |
Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps))))); |
|
56643
41d3596d8a64
move size hooks together, with new one preceding old one and sharing same theory data
blanchet
parents:
56642
diff
changeset
|
43 |
|
58738 | 44 |
fun register_size_global T_name size_name size_simps size_gen_o_maps = |
45 |
Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps))))); |
|
56651 | 46 |
|
58179 | 47 |
val size_of = Symtab.lookup o Data.get o Context.Proof; |
48 |
val size_of_global = Symtab.lookup o Data.get o Context.Theory; |
|
56642
15cd15f9b40c
allow registration of custom size functions for BNF-based datatypes
blanchet
parents:
56640
diff
changeset
|
49 |
|
56638 | 50 |
fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus}, |
51 |
HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; |
|
52 |
||
53 |
fun mk_to_natT T = T --> HOLogic.natT; |
|
54 |
||
58337 | 55 |
fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero; |
56638 | 56 |
|
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
57 |
fun mk_pointfull ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong); |
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
58 |
|
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
59 |
fun mk_unabs_def_unused_0 n = |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
60 |
funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
61 |
|
59576
913c4afb0388
avoid duplicate simp warning for datatypes with explicit products
blanchet
parents:
59498
diff
changeset
|
62 |
val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[unfolded apfst_def]}; |
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
63 |
|
58738 | 64 |
fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps = |
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
65 |
unfold_thms_tac ctxt [size_def] THEN |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
66 |
HEADGOAL (rtac (rec_o_map RS trans) THEN' |
58738 | 67 |
asm_simp_tac (ss_only (inj_maps @ size_maps @ size_gen_o_map_simps) ctxt)) THEN |
56645
a16d294f7e3f
prevent tactic failures by detecting and ignoring BNFs with no 'size' functions early
blanchet
parents:
56643
diff
changeset
|
68 |
IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl)); |
56638 | 69 |
|
58913 | 70 |
fun mk_size_neq ctxt cts exhaust sizes = |
71 |
HEADGOAL (rtac (Ctr_Sugar_Util.cterm_instantiate_pos (map SOME cts) exhaust)) THEN |
|
72 |
ALLGOALS (hyp_subst_tac ctxt) THEN |
|
73 |
Ctr_Sugar_Tactics.unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN |
|
74 |
ALLGOALS (REPEAT_DETERM o (rtac @{thm zero_less_Suc} ORELSE' rtac @{thm trans_less_add2})); |
|
75 |
||
58179 | 76 |
fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP, |
59145 | 77 |
fp_res = {bnfs = fp_bnfs, ...}, fp_nesting_bnfs, live_nesting_bnfs, ...} : fp_sugar) :: _) |
78 |
lthy0 = |
|
58179 | 79 |
let |
80 |
val data = Data.get (Context.Proof lthy0); |
|
56651 | 81 |
|
58179 | 82 |
val Ts = map #T fp_sugars |
83 |
val T_names = map (fst o dest_Type) Ts; |
|
84 |
val nn = length Ts; |
|
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
85 |
|
58179 | 86 |
val B_ify = Term.typ_subst_atomic (As ~~ Bs); |
56651 | 87 |
|
58461 | 88 |
val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars; |
58459 | 89 |
val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars; |
58179 | 90 |
val rec_Ts as rec_T1 :: _ = map fastype_of recs; |
91 |
val rec_arg_Ts = binder_fun_types rec_T1; |
|
92 |
val Cs = map body_type rec_Ts; |
|
93 |
val Cs_rho = map (rpair HOLogic.natT) Cs; |
|
94 |
val substCnatT = Term.subst_atomic_types Cs_rho; |
|
56651 | 95 |
|
58179 | 96 |
val f_Ts = map mk_to_natT As; |
97 |
val f_TsB = map mk_to_natT Bs; |
|
98 |
val num_As = length As; |
|
56651 | 99 |
|
58179 | 100 |
fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0); |
56651 | 101 |
|
58179 | 102 |
val f_names = variant_names num_As "f"; |
103 |
val fs = map2 (curry Free) f_names f_Ts; |
|
104 |
val fsB = map2 (curry Free) f_names f_TsB; |
|
105 |
val As_fs = As ~~ fs; |
|
56638 | 106 |
|
58179 | 107 |
val size_bs = |
108 |
map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o |
|
109 |
Long_Name.base_name) T_names; |
|
56638 | 110 |
|
58208 | 111 |
fun is_prod_C @{type_name prod} [_, T'] = member (op =) Cs T' |
112 |
| is_prod_C _ _ = false; |
|
56651 | 113 |
|
58179 | 114 |
fun mk_size_of_typ (T as TFree _) = |
115 |
pair (case AList.lookup (op =) As_fs T of |
|
116 |
SOME f => f |
|
117 |
| NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T) |
|
118 |
| mk_size_of_typ (T as Type (s, Ts)) = |
|
58208 | 119 |
if is_prod_C s Ts then |
58179 | 120 |
pair (snd_const T) |
121 |
else if exists (exists_subtype_in (As @ Cs)) Ts then |
|
122 |
(case Symtab.lookup data s of |
|
58738 | 123 |
SOME (size_name, (_, size_gen_o_maps)) => |
58179 | 124 |
let |
58738 | 125 |
val (args, size_gen_o_mapss') = fold_map mk_size_of_typ Ts []; |
58179 | 126 |
val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T); |
127 |
in |
|
58738 | 128 |
append (size_gen_o_maps :: size_gen_o_mapss') |
58179 | 129 |
#> pair (Term.list_comb (size_const, args)) |
130 |
end |
|
131 |
| _ => pair (mk_abs_zero_nat T)) |
|
132 |
else |
|
133 |
pair (mk_abs_zero_nat T); |
|
56651 | 134 |
|
58179 | 135 |
fun mk_size_of_arg t = |
136 |
mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t))); |
|
56638 | 137 |
|
58338
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
138 |
fun is_recursive_or_plain_case Ts = |
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
139 |
exists (exists_subtype_in Cs) Ts orelse forall (not o exists_subtype_in As) Ts; |
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
140 |
|
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
141 |
(* We want the size function to enjoy the following properties: |
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
142 |
|
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
143 |
1. The size of a list should coincide with its length. |
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
144 |
2. All the nonrecursive constructors of a type should have the same size. |
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
145 |
3. Each constructor through which nested recursion takes place should count as at least |
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
146 |
one in the generic size function. |
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
147 |
4. The "size" function should be definable as "size_t (%_. 0) ... (%_. 0)", where "size_t" |
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
148 |
is the generic function. |
58338
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
149 |
|
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
150 |
This explains the somewhat convoluted logic ahead. *) |
58338
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
151 |
|
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
152 |
val base_case = |
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
153 |
if forall (is_recursive_or_plain_case o binder_types) rec_arg_Ts then HOLogic.zero |
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
154 |
else HOLogic.Suc_zero; |
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
155 |
|
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
156 |
fun mk_size_arg rec_arg_T = |
58179 | 157 |
let |
158 |
val x_Ts = binder_types rec_arg_T; |
|
159 |
val m = length x_Ts; |
|
160 |
val x_names = variant_names m "x"; |
|
161 |
val xs = map2 (curry Free) x_names x_Ts; |
|
58738 | 162 |
val (summands, size_gen_o_mapss) = |
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
163 |
fold_map mk_size_of_arg xs [] |
58337 | 164 |
|>> remove (op =) HOLogic.zero; |
58179 | 165 |
val sum = |
58338
d109244b89aa
tuned definition of 'size' function to get nicer properties
blanchet
parents:
58337
diff
changeset
|
166 |
if null summands then base_case |
58179 | 167 |
else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]); |
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
168 |
in |
58738 | 169 |
append size_gen_o_mapss |
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
170 |
#> pair (fold_rev Term.lambda (map substCnatT xs) sum) |
56640
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
171 |
end; |
0a35354137a5
generate 'rec_o_map' and 'size_o_map' in size extension
blanchet
parents:
56639
diff
changeset
|
172 |
|
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
173 |
fun mk_size_rhs recx = |
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
174 |
fold_map mk_size_arg rec_arg_Ts |
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
175 |
#>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args))); |
58179 | 176 |
|
177 |
val maybe_conceal_def_binding = Thm.def_binding |
|
58208 | 178 |
#> not (Config.get lthy0 bnf_note_all) ? Binding.conceal; |
58179 | 179 |
|
58738 | 180 |
val (size_rhss, nested_size_gen_o_mapss) = fold_map mk_size_rhs recs []; |
58179 | 181 |
val size_Ts = map fastype_of size_rhss; |
182 |
||
58738 | 183 |
val nested_size_gen_o_maps_complete = forall (not o null) nested_size_gen_o_mapss; |
184 |
val nested_size_gen_o_maps = fold (union Thm.eq_thm_prop) nested_size_gen_o_mapss []; |
|
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
185 |
|
58179 | 186 |
val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0 |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58578
diff
changeset
|
187 |
|> apfst split_list o @{fold_map 2} (fn b => fn rhs => |
58179 | 188 |
Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) |
189 |
#>> apsnd snd) |
|
190 |
size_bs size_rhss |
|
191 |
||> `Local_Theory.restore; |
|
192 |
||
193 |
val phi = Proof_Context.export_morphism lthy1 lthy1'; |
|
194 |
||
195 |
val size_defs = map (Morphism.thm phi) raw_size_defs; |
|
196 |
||
197 |
val size_consts0 = map (Morphism.term phi) raw_size_consts; |
|
198 |
val size_consts = map2 retype_const_or_free size_Ts size_consts0; |
|
199 |
val size_constsB = map (Term.map_types B_ify) size_consts; |
|
200 |
||
201 |
val zeros = map mk_abs_zero_nat As; |
|
202 |
||
203 |
val overloaded_size_rhss = map (fn c => Term.list_comb (c, zeros)) size_consts; |
|
204 |
val overloaded_size_Ts = map fastype_of overloaded_size_rhss; |
|
205 |
val overloaded_size_consts = map (curry Const @{const_name size}) overloaded_size_Ts; |
|
206 |
val overloaded_size_def_bs = |
|
207 |
map (maybe_conceal_def_binding o Binding.suffix_name "_overloaded") size_bs; |
|
208 |
||
209 |
fun define_overloaded_size def_b lhs0 rhs lthy = |
|
210 |
let |
|
211 |
val Free (c, _) = Syntax.check_term lthy lhs0; |
|
212 |
val (thm, lthy') = lthy |
|
213 |
|> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs)) |
|
214 |
|-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm); |
|
215 |
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy'); |
|
216 |
val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm; |
|
217 |
in (thm', lthy') end; |
|
218 |
||
219 |
val (overloaded_size_defs, lthy2) = lthy1 |
|
220 |
|> Local_Theory.background_theory_result |
|
221 |
(Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size]) |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58578
diff
changeset
|
222 |
#> @{fold_map 3} define_overloaded_size overloaded_size_def_bs overloaded_size_consts |
58179 | 223 |
overloaded_size_rhss |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59145
diff
changeset
|
224 |
##> Class.prove_instantiation_instance (fn ctxt => Class.intro_classes_tac ctxt []) |
58179 | 225 |
##> Local_Theory.exit_global); |
56638 | 226 |
|
58179 | 227 |
val size_defs' = |
228 |
map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs; |
|
229 |
val size_defs_unused_0 = |
|
230 |
map (mk_unabs_def_unused_0 (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs; |
|
231 |
val overloaded_size_defs' = |
|
232 |
map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs; |
|
233 |
||
234 |
val all_overloaded_size_defs = overloaded_size_defs @ |
|
235 |
(Spec_Rules.retrieve lthy0 @{const size ('a)} |
|
236 |
|> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm))); |
|
237 |
||
58738 | 238 |
val nested_size_maps = map (mk_pointfull lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps; |
59576
913c4afb0388
avoid duplicate simp warning for datatypes with explicit products
blanchet
parents:
59498
diff
changeset
|
239 |
val all_inj_maps = |
913c4afb0388
avoid duplicate simp warning for datatypes with explicit products
blanchet
parents:
59498
diff
changeset
|
240 |
@{thm prod.inj_map} :: map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs) |
58179 | 241 |
|> distinct Thm.eq_thm_prop; |
242 |
||
243 |
fun derive_size_simp size_def' simp0 = |
|
244 |
(trans OF [size_def', simp0]) |
|
245 |
|> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_ident id_def o_def |
|
246 |
snd_conv} @ all_inj_maps @ nested_size_maps) lthy2) |
|
247 |
|> fold_thms lthy2 size_defs_unused_0; |
|
248 |
||
249 |
fun derive_overloaded_size_simp overloaded_size_def' simp0 = |
|
250 |
(trans OF [overloaded_size_def', simp0]) |
|
251 |
|> unfold_thms lthy2 @{thms add_0_left add_0_right} |
|
252 |
|> fold_thms lthy2 all_overloaded_size_defs; |
|
253 |
||
254 |
val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss; |
|
255 |
val size_simps = flat size_simpss; |
|
256 |
val overloaded_size_simpss = |
|
257 |
map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss; |
|
258 |
val size_thmss = map2 append size_simpss overloaded_size_simpss; |
|
58736 | 259 |
val size_gen_thmss = size_simpss |
58913 | 260 |
fun rhs_is_zero thm = |
261 |
let val Const (trueprop, _) $ (Const (eq, _) $ _ $ rhs) = prop_of thm in |
|
262 |
trueprop = @{const_name Trueprop} andalso |
|
263 |
eq = @{const_name HOL.eq} andalso |
|
264 |
rhs = HOLogic.zero |
|
265 |
end; |
|
266 |
||
267 |
val size_neq_thmss = @{map 3} (fn fp_sugar => fn size => fn size_thms => |
|
268 |
if exists rhs_is_zero size_thms then [] |
|
269 |
else |
|
270 |
let |
|
271 |
val (xs, names_lthy2) = mk_Frees "x" (binder_types (fastype_of size)) lthy2; |
|
272 |
val goal = |
|
273 |
HOLogic.mk_Trueprop (BNF_LFP_Util.mk_not_eq (list_comb (size, xs)) HOLogic.zero); |
|
274 |
val thm = |
|
275 |
Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => |
|
276 |
mk_size_neq ctxt (map (certify lthy2) xs) |
|
277 |
(#exhaust (#ctr_sugar (#fp_ctr_sugar fp_sugar))) size_thms) |
|
278 |
|> single |
|
279 |
|> Proof_Context.export names_lthy2 lthy2 |
|
280 |
|> map Thm.close_derivation; |
|
281 |
in thm end) fp_sugars overloaded_size_consts overloaded_size_simpss |
|
58179 | 282 |
|
283 |
val ABs = As ~~ Bs; |
|
284 |
val g_names = variant_names num_As "g"; |
|
285 |
val gs = map2 (curry Free) g_names (map (op -->) ABs); |
|
286 |
||
287 |
val liveness = map (op <>) ABs; |
|
288 |
val live_gs = AList.find (op =) (gs ~~ liveness) true; |
|
289 |
val live = length live_gs; |
|
290 |
||
291 |
val maps0 = map map_of_bnf fp_bnfs; |
|
292 |
||
58738 | 293 |
val size_gen_o_map_thmss = |
58732 | 294 |
if live = 0 then replicate nn [] |
58179 | 295 |
else |
296 |
let |
|
297 |
val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0; |
|
57631
959caab43a3d
use the noted theorem whenever possible, also in 'BNF_Def'
blanchet
parents:
57399
diff
changeset
|
298 |
|
58738 | 299 |
val size_gen_o_map_conds = |
300 |
if exists (can Logic.dest_implies o Thm.prop_of) nested_size_gen_o_maps then |
|
58179 | 301 |
map (HOLogic.mk_Trueprop o mk_inj) live_gs |
302 |
else |
|
303 |
[]; |
|
304 |
||
305 |
val fsizes = map (fn size_constB => Term.list_comb (size_constB, fsB)) size_constsB; |
|
58738 | 306 |
val size_gen_o_map_lhss = map2 (curry HOLogic.mk_comp) fsizes gmaps; |
57631
959caab43a3d
use the noted theorem whenever possible, also in 'BNF_Def'
blanchet
parents:
57399
diff
changeset
|
307 |
|
58179 | 308 |
val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) => |
309 |
if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs; |
|
58738 | 310 |
val size_gen_o_map_rhss = map (fn c => Term.list_comb (c, fgs)) size_consts; |
58179 | 311 |
|
58738 | 312 |
val size_gen_o_map_goals = |
58179 | 313 |
map2 (fold_rev (fold_rev Logic.all) [fsB, gs] o |
58738 | 314 |
curry Logic.list_implies size_gen_o_map_conds o HOLogic.mk_Trueprop oo |
315 |
curry HOLogic.mk_eq) size_gen_o_map_lhss size_gen_o_map_rhss; |
|
58179 | 316 |
|
58734 | 317 |
val rec_o_maps = |
318 |
fold_rev (curry (op @) o (#co_rec_o_maps o #fp_co_induct_sugar)) fp_sugars []; |
|
58732 | 319 |
|
58738 | 320 |
val size_gen_o_map_thmss = |
321 |
if nested_size_gen_o_maps_complete then |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58578
diff
changeset
|
322 |
@{map 3} (fn goal => fn size_def => fn rec_o_map => |
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
323 |
Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => |
58738 | 324 |
mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) |
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
325 |
|> Thm.close_derivation |
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
326 |
|> single) |
58738 | 327 |
size_gen_o_map_goals size_defs rec_o_maps |
58355
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
328 |
else |
9a041a55ee95
syntactic check to determine when to prove 'nested_size_o_map'
blanchet
parents:
58353
diff
changeset
|
329 |
replicate nn []; |
58179 | 330 |
in |
58738 | 331 |
size_gen_o_map_thmss |
58179 | 332 |
end; |
333 |
||
58335
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset
|
334 |
(* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *) |
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset
|
335 |
val code_attrs = Code.add_default_eqn_attrib; |
a5a3b576fcfb
generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents:
58315
diff
changeset
|
336 |
|
58179 | 337 |
val massage_multi_notes = |
338 |
maps (fn (thmN, thmss, attrs) => |
|
339 |
map2 (fn T_name => fn thms => |
|
340 |
((Binding.qualify true (Long_Name.base_name T_name) (Binding.name thmN), attrs), |
|
341 |
[(thms, [])])) |
|
342 |
T_names thmss) |
|
343 |
#> filter_out (null o fst o hd o snd); |
|
344 |
||
345 |
val notes = |
|
58732 | 346 |
[(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs), |
58736 | 347 |
(size_genN, size_gen_thmss, []), |
58913 | 348 |
(size_gen_o_mapN, size_gen_o_map_thmss, []), |
349 |
(size_neqN, size_neq_thmss, [])] |
|
58179 | 350 |
|> massage_multi_notes; |
351 |
||
352 |
val (noted, lthy3) = |
|
353 |
lthy2 |
|
354 |
|> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps) |
|
355 |
|> Local_Theory.notes notes; |
|
356 |
||
357 |
val phi0 = substitute_noted_thm noted; |
|
358 |
in |
|
359 |
lthy3 |
|
360 |
|> Local_Theory.declaration {syntax = false, pervasive = true} |
|
361 |
(fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) => |
|
362 |
Symtab.update (T_name, (size_name, |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58916
diff
changeset
|
363 |
apply2 (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_gen_o_map_thmss)))) |
58179 | 364 |
T_names size_consts)) |
365 |
end |
|
366 |
| generate_datatype_size _ lthy = lthy; |
|
367 |
||
58659
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58634
diff
changeset
|
368 |
val size_plugin = Plugin_Name.declare_setup @{binding size}; |
6c9821c32dd5
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
wenzelm
parents:
58634
diff
changeset
|
369 |
val _ = Theory.setup (fp_sugars_interpretation size_plugin generate_datatype_size); |
56638 | 370 |
|
371 |
end; |