equal
deleted
inserted
replaced
269 let |
269 let |
270 val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info |
270 val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info |
271 in |
271 in |
272 raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) |
272 raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) |
273 (Local_Theory.restore lthy_tmp) |
273 (Local_Theory.restore lthy_tmp) |
274 |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]}) |
274 |> map (rewrite_rule (Local_Theory.restore lthy_tmp) |
|
275 @{thms permute_nat_def[THEN eq_reflection]}) |
275 |> map (fn thm => thm RS @{thm sym}) |
276 |> map (fn thm => thm RS @{thm sym}) |
276 end |
277 end |
277 |
278 |
278 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
279 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
279 |
280 |
300 |
301 |
301 val _ = trace_msg (K "Proving respectfulness...") |
302 val _ = trace_msg (K "Proving respectfulness...") |
302 val raw_funs_rsp_aux = |
303 val raw_funs_rsp_aux = |
303 raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) |
304 raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) |
304 |
305 |
305 val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp) raw_funs_rsp_aux |
306 val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp lthy5) raw_funs_rsp_aux |
306 |
307 |
307 fun match_const cnst th = |
308 fun match_const cnst th = |
308 (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th = |
309 (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th = |
309 fst (dest_Const cnst); |
310 fst (dest_Const cnst); |
310 fun find_matching_rsp cnst = |
311 fun find_matching_rsp cnst = |
313 val raw_bn_rsp = map find_matching_rsp raw_bns; |
314 val raw_bn_rsp = map find_matching_rsp raw_bns; |
314 val raw_fv_bn_rsp = map find_matching_rsp raw_fv_bns; |
315 val raw_fv_bn_rsp = map find_matching_rsp raw_fv_bns; |
315 |
316 |
316 val raw_size_rsp = |
317 val raw_size_rsp = |
317 raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |
318 raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt) |
318 |> map mk_funs_rsp |
319 |> map (mk_funs_rsp lthy5) |
319 |
320 |
320 val raw_constrs_rsp = |
321 val raw_constrs_rsp = |
321 raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux) |
322 raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux) |
322 |
323 |
323 val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt |
324 val alpha_permute_rsp = map (mk_alpha_permute_rsp lthy5) alpha_eqvt |
324 |
325 |
325 val alpha_bn_rsp = |
326 val alpha_bn_rsp = |
326 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
327 raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms |
327 |
328 |
328 val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
329 val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps |
742 val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} |
743 val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"} |
743 "declaration of nominal datatypes" |
744 "declaration of nominal datatypes" |
744 (main_parser >> nominal_datatype2_cmd) |
745 (main_parser >> nominal_datatype2_cmd) |
745 *} |
746 *} |
746 |
747 |
747 end |
748 |
|
749 end |
|
750 |
|
751 |
|
752 |