equal
deleted
inserted
replaced
255 |
255 |
256 val all_alpha_trms_loc = #preds alpha_info; |
256 val all_alpha_trms_loc = #preds alpha_info; |
257 val alpha_raw_induct_loc = #raw_induct alpha_info; |
257 val alpha_raw_induct_loc = #raw_induct alpha_info; |
258 val alpha_intros_loc = #intrs alpha_info; |
258 val alpha_intros_loc = #intrs alpha_info; |
259 val alpha_cases_loc = #elims alpha_info; |
259 val alpha_cases_loc = #elims alpha_info; |
260 val phi = ProofContext.export_morphism lthy' lthy; |
260 val phi = Proof_Context.export_morphism lthy' lthy; |
261 |
261 |
262 val all_alpha_trms = all_alpha_trms_loc |
262 val all_alpha_trms = all_alpha_trms_loc |
263 |> map (Morphism.term phi) |
263 |> map (Morphism.term phi) |
264 |> map Type.legacy_freeze |
264 |> map Type.legacy_freeze |
265 val alpha_raw_induct = Morphism.thm phi alpha_raw_induct_loc |
265 val alpha_raw_induct = Morphism.thm phi alpha_raw_induct_loc |
316 (DETERM o (rtac induct_thm) |
316 (DETERM o (rtac induct_thm) |
317 THEN_ALL_NEW |
317 THEN_ALL_NEW |
318 (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt]))) |
318 (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt]))) |
319 in |
319 in |
320 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
320 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
321 |> singleton (ProofContext.export ctxt' ctxt) |
321 |> singleton (Proof_Context.export ctxt' ctxt) |
322 |> Datatype_Aux.split_conj_thm |
322 |> Datatype_Aux.split_conj_thm |
323 |> map Datatype_Aux.split_conj_thm |
323 |> map Datatype_Aux.split_conj_thm |
324 |> flat |
324 |> flat |
325 |> filter_out (is_true o concl_of) |
325 |> filter_out (is_true o concl_of) |
326 |> map zero_var_indexes |
326 |> map zero_var_indexes |
362 HEADGOAL |
362 HEADGOAL |
363 (DETERM o (rtac alpha_induct_thm) |
363 (DETERM o (rtac alpha_induct_thm) |
364 THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt]) |
364 THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt]) |
365 in |
365 in |
366 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
366 Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) |
367 |> singleton (ProofContext.export ctxt' ctxt) |
367 |> singleton (Proof_Context.export ctxt' ctxt) |
368 |> Datatype_Aux.split_conj_thm |
368 |> Datatype_Aux.split_conj_thm |
369 |> map (fn th => th RS mp) |
369 |> map (fn th => th RS mp) |
370 |> map Datatype_Aux.split_conj_thm |
370 |> map Datatype_Aux.split_conj_thm |
371 |> flat |
371 |> flat |
372 |> filter_out (is_true o concl_of) |
372 |> filter_out (is_true o concl_of) |
828 |
828 |
829 val goals = map mk_prop perm_bns |
829 val goals = map mk_prop perm_bns |
830 in |
830 in |
831 alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct |
831 alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct |
832 (raw_prove_perm_bn_tac alpha_result simps) ctxt |
832 (raw_prove_perm_bn_tac alpha_result simps) ctxt |
833 |> ProofContext.export ctxt' ctxt |
833 |> Proof_Context.export ctxt' ctxt |
834 |> map atomize |
834 |> map atomize |
835 |> map single |
835 |> map single |
836 |> map (curry (op OF) perm_bn_rsp) |
836 |> map (curry (op OF) perm_bn_rsp) |
837 end |
837 end |
838 |
838 |