260 val all_alpha_trms_loc = #preds alphas; |
260 val all_alpha_trms_loc = #preds alphas; |
261 val alpha_induct_loc = #raw_induct alphas; |
261 val alpha_induct_loc = #raw_induct alphas; |
262 val alpha_intros_loc = #intrs alphas; |
262 val alpha_intros_loc = #intrs alphas; |
263 val alpha_cases_loc = #elims alphas; |
263 val alpha_cases_loc = #elims alphas; |
264 val phi = ProofContext.export_morphism lthy' lthy; |
264 val phi = ProofContext.export_morphism lthy' lthy; |
265 |
265 |
266 val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc |
266 val all_alpha_trms = all_alpha_trms_loc |
267 val (all_alpha_trms', _) = Variable.importT_terms all_alpha_trms lthy |
267 |> map (Morphism.term phi) |
268 val alpha_induct = Morphism.thm phi alpha_induct_loc; |
268 |> map Type.legacy_freeze |
|
269 val alpha_induct = Morphism.thm phi alpha_induct_loc |
269 val alpha_intros = map (Morphism.thm phi) alpha_intros_loc |
270 val alpha_intros = map (Morphism.thm phi) alpha_intros_loc |
270 val alpha_cases = map (Morphism.thm phi) alpha_cases_loc |
271 val alpha_cases = map (Morphism.thm phi) alpha_cases_loc |
271 |
272 |
272 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms' |
273 val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms |
273 in |
274 in |
274 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
275 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
275 end |
276 end |
276 |
277 |
277 |
278 |
278 |
279 |
279 (** produces the distinctness theorems **) |
280 (** produces the distinctness theorems **) |
280 |
281 |
281 (* transforms the distinctness theorems of the constructors |
282 (* transforms the distinctness theorems of the constructors |
282 to "not-alphas" of the constructors *) |
283 into "not-alphas" of the constructors *) |
283 fun mk_distinct_goal ty_trm_assoc neq = |
284 fun mk_distinct_goal ty_trm_assoc neq = |
284 let |
285 let |
285 val (lhs, rhs) = |
286 val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) = |
286 neq |
287 HOLogic.dest_not (HOLogic.dest_Trueprop neq) |
287 |> HOLogic.dest_Trueprop |
288 val ty_str = fst (dest_Type (domain_type ty_eq)) |
288 |> HOLogic.dest_not |
289 in |
289 |> HOLogic.dest_eq |
290 Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs |
290 val ty = fastype_of lhs |
|
291 in |
|
292 (lookup ty_trm_assoc ty) $ lhs $ rhs |
|
293 |> HOLogic.mk_not |
291 |> HOLogic.mk_not |
294 |> HOLogic.mk_Trueprop |
292 |> HOLogic.mk_Trueprop |
295 end |
293 end |
296 |
294 |
297 fun distinct_tac cases_thms distinct_thms = |
295 fun distinct_tac cases_thms distinct_thms = |
298 rtac notI THEN' eresolve_tac cases_thms |
296 rtac notI THEN' eresolve_tac cases_thms |
299 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
297 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
300 |
298 |
301 |
299 |
302 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys = |
300 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str = |
303 let |
301 let |
304 (* proper import of type-variables does not work, |
302 val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms) |
305 since then they are replaced by new variables, messing |
|
306 up the ty_trm assoc list *) |
|
307 val distinct_thms' = map Thm.legacy_freezeT distinct_thms |
|
308 val ty_trm_assoc = alpha_tys ~~ alpha_trms |
|
309 |
303 |
310 fun mk_alpha_distinct distinct_trm = |
304 fun mk_alpha_distinct distinct_trm = |
311 let |
305 let |
312 val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt |
|
313 val goal = mk_distinct_goal ty_trm_assoc distinct_trm |
306 val goal = mk_distinct_goal ty_trm_assoc distinct_trm |
314 in |
307 in |
315 Goal.prove ctxt' [] [] goal |
308 Goal.prove ctxt [] [] goal |
316 (K (distinct_tac cases_thms distinct_thms 1)) |
309 (K (distinct_tac cases_thms distinct_thms 1)) |
317 |> singleton (Variable.export ctxt' ctxt) |
|
318 end |
310 end |
319 |
311 in |
320 in |
312 map (mk_alpha_distinct o prop_of) distinct_thms |
321 map (mk_alpha_distinct o prop_of) distinct_thms' |
|
322 |> map Thm.varifyT_global |
|
323 end |
313 end |
324 |
314 |
325 |
315 |
326 |
316 |
327 (** produces the alpha_eq_iff simplification rules **) |
317 (** produces the alpha_eq_iff simplification rules **) |
655 |
645 |
656 (* respectfulness for fv_raw / bn_raw *) |
646 (* respectfulness for fv_raw / bn_raw *) |
657 |
647 |
658 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = |
648 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = |
659 let |
649 let |
660 val arg_ty = domain_type o fastype_of |
650 val arg_ty = fst o dest_Type o domain_type o fastype_of |
661 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms |
651 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms |
662 fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y) |
652 fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y) |
663 |
653 |
664 val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs |
654 val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs |
665 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) |
655 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) |
666 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns |
656 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns |
667 |
657 |
668 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
658 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
669 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
659 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
670 |
|
671 in |
660 in |
672 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
661 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
673 (K (asm_full_simp_tac ss)) ctxt |
662 (K (asm_full_simp_tac ss)) ctxt |
674 end |
663 end |
675 |
664 |
705 asm_full_simp_tac pre_ss |
694 asm_full_simp_tac pre_ss |
706 THEN' REPEAT o (resolve_tac @{thms allI impI}) |
695 THEN' REPEAT o (resolve_tac @{thms allI impI}) |
707 THEN' resolve_tac alpha_intros |
696 THEN' resolve_tac alpha_intros |
708 THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss) |
697 THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss) |
709 end |
698 end |
710 |
|
711 |
699 |
712 fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt = |
700 fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt = |
713 let |
701 let |
714 val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms |
702 val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms |
715 |
703 |
716 fun lookup ty = |
704 fun lookup ty = |
717 case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of |
705 case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of |
718 NONE => HOLogic.eq_const ty |
706 NONE => HOLogic.eq_const ty |
719 | SOME alpha => alpha |
707 | SOME alpha => alpha |
720 |
708 |
721 fun fun_rel_app t1 t2 = |
709 fun fun_rel_app (t1, t2) = |
722 Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2 |
710 Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2 |
723 |
711 |
724 fun prep_goal trm = |
712 fun prep_goal trm = |
725 trm |
713 trm |
726 |> strip_type o fastype_of |
714 |> strip_type o fastype_of |
727 |>> map lookup |
715 |> (fn (tys, ty) => tys @ [ty]) |
728 ||> lookup |
716 |> map lookup |
729 |> uncurry (fold_rev fun_rel_app) |
717 |> foldr1 fun_rel_app |
730 |> (fn t => t $ trm $ trm) |
718 |> (fn t => t $ trm $ trm) |
731 |> Syntax.check_term ctxt |
719 |> Syntax.check_term ctxt |
732 |> HOLogic.mk_Trueprop |
720 |> HOLogic.mk_Trueprop |
733 in |
721 in |
734 Goal.prove_multi ctxt [] [] (map prep_goal constrs) |
722 Goal.prove_multi ctxt [] [] (map prep_goal constrs) |