138 |
138 |
139 ML {* |
139 ML {* |
140 fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = |
140 fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = |
141 let |
141 let |
142 val bn_funs' = map (fn (bn, ty, mx) => |
142 val bn_funs' = map (fn (bn, ty, mx) => |
143 (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs |
143 (raw_bind bn, SOME (replace_typ dts_env ty), mx)) bn_funs |
144 |
144 |
145 val bn_eqs' = map (fn (attr, trm) => |
145 val bn_eqs' = map (fn (attr, trm) => |
146 (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs |
146 (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs |
147 in |
147 in |
148 (bn_funs', bn_eqs') |
148 (bn_funs', bn_eqs') |
252 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
254 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
253 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
255 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
254 (bn_fun_strs ~~ bn_fun_strs') |
256 (bn_fun_strs ~~ bn_fun_strs') |
255 |
257 |
256 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
258 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
257 val raw_dt_names' = map (Long_Name.qualify thy_name) raw_dt_names |
|
258 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
259 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
259 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
260 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
260 |
261 |
261 val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
262 val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
262 val (raw_bn_funs', raw_bn_eqs', lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 |
263 |
|
264 in |
|
265 (dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1) |
|
266 end |
|
267 *} |
|
268 |
|
269 ML {* |
|
270 fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy = |
|
271 let |
|
272 val (_, lthy2) = Function.add_function raw_bn_funs raw_bn_eqs |
|
273 Function_Common.default_config (pat_completeness_simp constr_thms) lthy |
|
274 |
|
275 val (info, lthy3) = prove_termination (Local_Theory.restore lthy2) |
|
276 val {fs, simps, inducts, ...} = info; |
|
277 |
|
278 val raw_bn_induct = Rule_Cases.strict_mutual_rule lthy3 (the inducts) |
|
279 val raw_bn_eqs = the simps |
263 |
280 |
264 val raw_bn_info = |
281 val raw_bn_info = |
265 prep_bn_info lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs') |
282 prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs) |
266 in |
283 |
267 (raw_dt_full_names, raw_bclauses, raw_bn_funs', raw_bn_eqs', raw_bn_info, lthy2) |
284 in |
268 end |
285 (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3) |
269 *} |
286 end |
|
287 *} |
|
288 |
270 |
289 |
271 lemma equivp_hack: "equivp x" |
290 lemma equivp_hack: "equivp x" |
272 sorry |
291 sorry |
273 ML {* |
292 ML {* |
274 fun equivp_hack ctxt rel = |
293 fun equivp_hack ctxt rel = |
366 |
385 |
367 ML {* |
386 ML {* |
368 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
387 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
369 let |
388 let |
370 (* definition of the raw datatypes *) |
389 (* definition of the raw datatypes *) |
371 val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_info, lthy1) = |
390 val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
372 if get_STEPS lthy > 1 |
391 if get_STEPS lthy > 1 |
373 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
392 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
374 else raise TEST lthy |
393 else raise TEST lthy |
375 |
394 |
376 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names) |
395 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names) |
377 val {descr, sorts, ...} = dtinfo |
396 val {descr, sorts, ...} = dtinfo |
378 val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr |
397 val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr |
379 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr |
398 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr |
380 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames |
399 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_full_tnames |
381 |
400 |
382 val inject_thms = flat (map #inject dtinfos); |
401 val inject_thms = flat (map #inject dtinfos); |
383 val distinct_thms = flat (map #distinct dtinfos); |
402 val distinct_thms = flat (map #distinct dtinfos); |
|
403 val constr_thms = inject_thms @ distinct_thms |
384 val rel_dtinfos = List.take (dtinfos, (length dts)); |
404 val rel_dtinfos = List.take (dtinfos, (length dts)); |
385 val raw_constrs_distinct = (map #distinct rel_dtinfos); |
405 val raw_constrs_distinct = (map #distinct rel_dtinfos); |
386 val induct_thm = #induct dtinfo; |
406 val induct_thm = #induct dtinfo; |
387 val exhaust_thms = map #exhaust dtinfos; |
407 val exhaust_thms = map #exhaust dtinfos; |
|
408 |
|
409 val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy1) = |
|
410 if get_STEPS lthy0 > 1 |
|
411 then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy0 |
|
412 else raise TEST lthy0 |
|
413 |
388 |
414 |
389 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
415 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
390 val bns = raw_bn_funs ~~ bn_nos; |
416 val bns = raw_bn_funs ~~ bn_nos; |
391 |
417 |
392 (* definitions of raw permutations *) |
418 (* definitions of raw permutations *) |
405 (* definition of raw fv_functions *) |
431 (* definition of raw fv_functions *) |
406 val lthy3 = Theory_Target.init NONE thy; |
432 val lthy3 = Theory_Target.init NONE thy; |
407 |
433 |
408 val (raw_fvs, raw_fv_bns, raw_fv_defs, lthy3a) = |
434 val (raw_fvs, raw_fv_bns, raw_fv_defs, lthy3a) = |
409 if get_STEPS lthy2 > 3 |
435 if get_STEPS lthy2 > 3 |
410 then define_raw_fvs descr sorts raw_bn_info raw_bclauses lthy3 |
436 then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3 |
411 else raise TEST lthy3 |
437 else raise TEST lthy3 |
412 |
438 |
413 (* definition of raw alphas *) |
439 (* definition of raw alphas *) |
414 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
440 val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) = |
415 if get_STEPS lthy > 4 |
441 if get_STEPS lthy > 4 |