238 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info |
238 val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info |
239 |
239 |
240 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
240 val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) |
241 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
241 (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) |
242 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
242 val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros) |
243 |
243 |
244 val (alphas, lthy') = Inductive.add_inductive_i |
244 val (alphas, lthy') = Inductive.add_inductive_i |
245 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
245 {quiet_mode = true, verbose = false, alt_name = Binding.empty, |
246 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
246 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} |
247 all_alpha_names [] all_alpha_intros [] lthy |
247 all_alpha_names [] all_alpha_intros [] lthy |
248 |
248 |
250 val alpha_induct_loc = #raw_induct alphas; |
250 val alpha_induct_loc = #raw_induct alphas; |
251 val alpha_intros_loc = #intrs alphas; |
251 val alpha_intros_loc = #intrs alphas; |
252 val alpha_cases_loc = #elims alphas; |
252 val alpha_cases_loc = #elims alphas; |
253 val phi = ProofContext.export_morphism lthy' lthy; |
253 val phi = ProofContext.export_morphism lthy' lthy; |
254 |
254 |
255 val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc; |
255 val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc |
|
256 val (all_alpha_trms', _) = Variable.importT_terms all_alpha_trms lthy |
256 val alpha_induct = Morphism.thm phi alpha_induct_loc; |
257 val alpha_induct = Morphism.thm phi alpha_induct_loc; |
257 val alpha_intros = map (Morphism.thm phi) alpha_intros_loc |
258 val alpha_intros = map (Morphism.thm phi) alpha_intros_loc |
258 val alpha_cases = map (Morphism.thm phi) alpha_cases_loc |
259 val alpha_cases = map (Morphism.thm phi) alpha_cases_loc |
259 |
260 |
260 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms |
261 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms' |
261 in |
262 in |
262 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
263 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
263 end |
264 end |
264 |
265 |
265 |
266 |
287 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
288 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
288 |
289 |
289 |
290 |
290 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys = |
291 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys = |
291 let |
292 let |
|
293 (* proper import of type-variables does not work, |
|
294 since ther are replaced by new variables, messing |
|
295 up the ty_term assoc list *) |
|
296 val distinct_thms' = map Thm.legacy_freezeT distinct_thms |
292 val ty_trm_assoc = alpha_tys ~~ alpha_trms |
297 val ty_trm_assoc = alpha_tys ~~ alpha_trms |
293 |
298 |
294 fun mk_alpha_distinct distinct_trm = |
299 fun mk_alpha_distinct distinct_trm = |
295 let |
300 let |
296 val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt |
301 val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt |
297 val goal = mk_distinct_goal ty_trm_assoc trm' |
302 val goal = mk_distinct_goal ty_trm_assoc distinct_trm |
298 in |
303 in |
299 Goal.prove ctxt' [] [] goal |
304 Goal.prove ctxt' [] [] goal |
300 (K (distinct_tac cases_thms distinct_thms 1)) |
305 (K (distinct_tac cases_thms distinct_thms 1)) |
301 |> singleton (Variable.export ctxt' ctxt) |
306 |> singleton (Variable.export ctxt' ctxt) |
302 end |
307 end |
303 |
308 |
304 in |
309 in |
305 map (mk_alpha_distinct o prop_of) distinct_thms |
310 map (mk_alpha_distinct o prop_of) distinct_thms' |
|
311 |> map Thm.varifyT_global |
306 end |
312 end |
307 |
313 |
308 |
314 |
309 |
315 |
310 (** produces the alpha_eq_iff simplification rules **) |
316 (** produces the alpha_eq_iff simplification rules **) |