67 *} |
67 *} |
68 |
68 |
69 ML {* |
69 ML {* |
70 fun define_fv_alpha_export dt binds bns ctxt = |
70 fun define_fv_alpha_export dt binds bns ctxt = |
71 let |
71 let |
72 val ((((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), alpha), ctxt') = |
72 val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') = |
73 define_fv_alpha dt binds bns ctxt; |
73 define_fv dt binds bns ctxt; |
|
74 val fv_ts_nobn = take (length bns) fv_ts_loc |
|
75 val (alpha, ctxt'') = |
|
76 define_alpha dt binds bns fv_ts_nobn ctxt'; |
74 val alpha_ts_loc = #preds alpha |
77 val alpha_ts_loc = #preds alpha |
75 val alpha_induct_loc = #induct alpha |
78 val alpha_induct_loc = #induct alpha |
76 val alpha_intros_loc = #intrs alpha; |
79 val alpha_intros_loc = #intrs alpha; |
77 val alpha_cases_loc = #elims alpha |
80 val alpha_cases_loc = #elims alpha |
78 val morphism = ProofContext.export_morphism ctxt' ctxt; |
81 val morphism = ProofContext.export_morphism ctxt'' ctxt; |
79 val fv_ts = map (Morphism.term morphism) fv_ts_loc; |
82 val fv_ts = map (Morphism.term morphism) fv_ts_loc; |
80 val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc; |
83 val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc; |
81 val fv_def = Morphism.fact morphism fv_def_loc; |
84 val fv_def = Morphism.fact morphism fv_def_loc; |
82 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; |
85 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc; |
83 val alpha_induct = Morphism.thm morphism alpha_induct_loc; |
86 val alpha_induct = Morphism.thm morphism alpha_induct_loc; |
84 val alpha_intros = Morphism.fact morphism alpha_intros_loc |
87 val alpha_intros = Morphism.fact morphism alpha_intros_loc |
85 val alpha_cases = Morphism.fact morphism alpha_cases_loc |
88 val alpha_cases = Morphism.fact morphism alpha_cases_loc |
86 in |
89 in |
87 ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt') |
90 ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'') |
88 end; |
91 end; |
89 *} |
92 *} |
90 |
93 |
91 end |
94 end |
92 |
95 |