7 |
7 |
8 signature NOMINAL_DT_ALPHA = |
8 signature NOMINAL_DT_ALPHA = |
9 sig |
9 sig |
10 val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
10 val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info -> |
11 bclause list list list -> term list -> Proof.context -> |
11 bclause list list list -> term list -> Proof.context -> |
12 term list * thm list * thm list * thm * local_theory |
12 term list * term list * thm list * thm list * thm * local_theory |
13 end |
13 end |
14 |
14 |
15 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
15 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
16 struct |
16 struct |
17 |
17 |
217 val (alphas, lthy') = Inductive.add_inductive_i |
217 val (alphas, lthy') = Inductive.add_inductive_i |
218 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
218 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
219 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
219 coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} |
220 all_alpha_names [] all_alpha_intros [] lthy |
220 all_alpha_names [] all_alpha_intros [] lthy |
221 |
221 |
222 val alpha_trms_loc = #preds alphas; |
222 val all_alpha_trms_loc = #preds alphas; |
223 val alpha_induct_loc = #raw_induct alphas; |
223 val alpha_induct_loc = #raw_induct alphas; |
224 val alpha_intros_loc = #intrs alphas; |
224 val alpha_intros_loc = #intrs alphas; |
225 val alpha_cases_loc = #elims alphas; |
225 val alpha_cases_loc = #elims alphas; |
226 val phi = ProofContext.export_morphism lthy' lthy; |
226 val phi = ProofContext.export_morphism lthy' lthy; |
227 |
227 |
228 val alpha_trms = map (Morphism.term phi) alpha_trms_loc; |
228 val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc; |
229 val alpha_induct = Morphism.thm phi alpha_induct_loc; |
229 val alpha_induct = Morphism.thm phi alpha_induct_loc; |
230 val alpha_intros = map (Morphism.thm phi) alpha_intros_loc |
230 val alpha_intros = map (Morphism.thm phi) alpha_intros_loc |
231 val alpha_cases = map (Morphism.thm phi) alpha_cases_loc |
231 val alpha_cases = map (Morphism.thm phi) alpha_cases_loc |
232 in |
232 |
233 (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
233 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms |
|
234 in |
|
235 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
234 end |
236 end |
235 |
237 |
236 end (* structure *) |
238 end (* structure *) |
237 |
239 |