51 use "nominal_function.ML" |
51 use "nominal_function.ML" |
52 use "nominal_termination.ML" |
52 use "nominal_termination.ML" |
53 |
53 |
54 ML {* |
54 ML {* |
55 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
55 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
56 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add) |
|
57 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
56 val simp_attr = Attrib.internal (K Simplifier.simp_add) |
58 val induct_attr = Attrib.internal (K Induct.induct_simp_add) |
57 val induct_attr = Attrib.internal (K Induct.induct_simp_add) |
59 *} |
58 *} |
60 |
59 |
61 section{* Interface for nominal_datatype *} |
60 section{* Interface for nominal_datatype *} |
311 val alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result |
310 val alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result |
312 |
311 |
313 val _ = trace_msg (K "Proving respectfulness...") |
312 val _ = trace_msg (K "Proving respectfulness...") |
314 val raw_funs_rsp_aux = |
313 val raw_funs_rsp_aux = |
315 raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) |
314 raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) |
316 |
315 |
317 val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux |
316 val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp) raw_funs_rsp_aux |
|
317 |
|
318 fun match_const cnst th = |
|
319 (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th = |
|
320 fst (dest_Const cnst); |
|
321 fun find_matching_rsp cnst = |
|
322 hd (filter (fn th => match_const cnst th) raw_funs_rsp); |
|
323 val raw_fv_rsp = map find_matching_rsp raw_fvs; |
|
324 val raw_bn_rsp = map find_matching_rsp raw_bns; |
|
325 val raw_fv_bn_rsp = map find_matching_rsp raw_fv_bns; |
318 |
326 |
319 val raw_size_rsp = |
327 val raw_size_rsp = |
320 raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |
328 raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |
321 |> map mk_funs_rsp |
329 |> map mk_funs_rsp |
322 |
330 |
328 val alpha_bn_rsp = |
336 val alpha_bn_rsp = |
329 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
337 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
330 |
338 |
331 val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
339 val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
332 |
340 |
333 (* noting the quot_respects lemmas *) |
|
334 val (_, lthy6) = |
|
335 Local_Theory.note ((Binding.empty, [rsp_attr]), raw_funs_rsp) lthy5 |
|
336 |
|
337 val _ = tracing (PolyML.makestring (raw_funs_rsp)) |
|
338 |
|
339 val _ = trace_msg (K "Defining the quotient types...") |
341 val _ = trace_msg (K "Defining the quotient types...") |
340 val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts |
342 val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts |
341 |
343 |
342 val (qty_infos, lthy7) = |
344 val (qty_infos, lthy7) = |
343 let |
345 let |
344 val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result |
346 val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result |
345 in |
347 in |
346 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
348 define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy5 |
347 end |
349 end |
348 |
350 |
349 val qtys = map #qtyp qty_infos |
351 val qtys = map #qtyp qty_infos |
350 val qty_full_names = map (fst o dest_Type) qtys |
352 val qty_full_names = map (fst o dest_Type) qtys |
351 val qty_names = map Long_Name.base_name qty_full_names |
353 val qty_names = map Long_Name.base_name qty_full_names |
354 val qconstrs_descrs = |
356 val qconstrs_descrs = |
355 (map2 o map2) (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) |
357 (map2 o map2) (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) |
356 (get_cnstrs dts) (map (op ~~) (raw_all_cns ~~ raw_constrs_rsp)) |
358 (get_cnstrs dts) (map (op ~~) (raw_all_cns ~~ raw_constrs_rsp)) |
357 |
359 |
358 val qbns_descr = |
360 val qbns_descr = |
359 map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns |
361 map2 (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) bn_funs (raw_bns ~~ raw_bn_rsp) |
360 |
362 |
361 val qfvs_descr = |
363 val qfvs_descr = |
362 map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_fvs |
364 map2 (fn n => fn (t, th) => ("fv_" ^ n, t, NoSyn, th)) qty_names (raw_fvs ~~ raw_fv_rsp) |
363 |
365 |
364 val qfv_bns_descr = |
366 val qfv_bns_descr = |
365 map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) |
367 map2 (fn (b, _, _) => fn (t, th) => ("fv_" ^ Variable.check_name b, t, NoSyn, th)) |
366 bn_funs raw_fv_bns |
368 bn_funs (raw_fv_bns ~~ raw_fv_bn_rsp) |
367 |
369 |
368 val qalpha_bns_descr = |
370 val qalpha_bns_descr = |
369 let |
371 let |
370 val AlphaResult {alpha_bn_trms, ...} = alpha_result |
372 val AlphaResult {alpha_bn_trms, ...} = alpha_result |
371 in |
373 in |