|
(* Title: HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML
Author: Martin Desharnais, TU Muenchen
Copyright 2014
Parametricity of primitively (co)recursive functions.
*)
signature BNF_FP_REC_SUGAR_TRANSFER =
sig
val set_transfer_rule_attrs: thm list -> local_theory -> local_theory
val lfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
Proof.context
val gfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
Proof.context
end;
structure BNF_FP_Rec_Sugar_Transfer : BNF_FP_REC_SUGAR_TRANSFER =
struct
open Ctr_Sugar_Util
open Ctr_Sugar_Tactics
open BNF_Util
open BNF_Def
open BNF_FP_Util
open BNF_FP_Def_Sugar
open BNF_FP_Rec_Sugar_Util
open BNF_LFP_Rec_Sugar
val transferN = "transfer";
val transfer_rule_attrs = @{attributes [transfer_rule]};
fun set_transfer_rule_attrs thms =
snd o Local_Theory.notes [(Binding.empty_atts, [(thms, transfer_rule_attrs)])];
fun mk_lfp_rec_sugar_transfer_tac ctxt def =
unfold_thms_tac ctxt [def] THEN HEADGOAL (Transfer.transfer_prover_tac ctxt);
fun mk_gfp_rec_sugar_transfer_tac ctxt f_def corec_def type_definitions dtor_corec_transfers
rel_pre_defs disc_eq_cases cases case_distribs case_congs =
let
fun instantiate_with_lambda thm =
let
val prop as \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) =
Thm.prop_of thm;
val T = range_type fT;
val j = Term.maxidx_of_term prop + 1;
val cond = Var (("x", j), HOLogic.boolT);
val then_branch = Var (("t", j), T);
val else_branch = Var (("e", j), T);
val lam = Term.lambda cond (mk_If cond then_branch else_branch);
in
infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt lam)] thm
end;
val transfer_rules =
@{thm Abs_transfer[OF type_definition_id_bnf_UNIV type_definition_id_bnf_UNIV]} ::
map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions @
map (Local_Defs.unfold0 ctxt rel_pre_defs) dtor_corec_transfers;
val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add;
val ctxt' = Context.proof_map (fold add_transfer_rule transfer_rules) ctxt;
val case_distribs = map instantiate_with_lambda case_distribs;
val simps = case_distribs @ disc_eq_cases @ cases @ @{thms if_True if_False};
val ctxt'' = put_simpset (simpset_of (ss_only simps ctxt)) ctxt';
in
unfold_thms_tac ctxt ([f_def, corec_def] @ @{thms split_beta if_conn}) THEN
HEADGOAL (simp_tac (fold Simplifier.add_cong case_congs ctxt'')) THEN
HEADGOAL (Transfer.transfer_prover_tac ctxt')
end;
fun massage_simple_notes base =
filter_out (null o #2)
#> map (fn (thmN, thms, f_attrs) =>
((Binding.qualify true base (Binding.name thmN), []),
map_index (fn (kk, thm) => ([thm], f_attrs kk)) thms));
fun fp_sugar_of_bnf ctxt = fp_sugar_of ctxt o (fn Type (s, _) => s) o T_of_bnf;
fun bnf_depth_first_traverse ctxt f T =
(case T of
Type (s, Ts) =>
(case bnf_of ctxt s of
NONE => I
| SOME bnf => fold (bnf_depth_first_traverse ctxt f) Ts o f bnf)
| _ => I);
fun mk_goal lthy f =
let
val skematic_Ts = Term.add_tvarsT (fastype_of f) [];
val ((As, Bs), names_lthy) = lthy
|> mk_TFrees' (map snd skematic_Ts)
||>> mk_TFrees' (map snd skematic_Ts);
val ((Rs, Rs'), names_lthy) = mk_Frees' "R" (map2 mk_pred2T As Bs) names_lthy;
val fA = Term.subst_TVars (map fst skematic_Ts ~~ As) f;
val fB = Term.subst_TVars (map fst skematic_Ts ~~ Bs) f;
val goal = mk_parametricity_goal lthy Rs fA fB;
val used_Rs = Term.add_frees goal [];
val subst = map (dest_pred2T o snd) (filter_out (member (op =) used_Rs) Rs');
in
(goal |> Term.subst_atomic_types subst, names_lthy)
end;
fun fp_rec_sugar_transfer_interpretation prove {transfers, fun_names, funs, fun_defs, fpTs} =
fold_index (fn (kk, (((transfer, fun_name), funx), fun_def)) => fn lthy =>
if transfer then
(case try (map the) (map (fn Type (s, _) => bnf_of lthy s | _ => NONE) fpTs) of
NONE => error "No transfer rule possible"
| SOME bnfs =>
(case try (prove kk bnfs funx fun_def) lthy of
NONE => error "Failed to prove transfer rule"
| SOME thm =>
let
val notes = [(transferN, [thm], K @{attributes [transfer_rule]})]
|> massage_simple_notes fun_name;
in
snd (Local_Theory.notes notes lthy)
end))
else
lthy)
(transfers ~~ fun_names ~~ funs ~~ fun_defs);
val lfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
(fn _ => fn _ => fn f => fn def => fn lthy =>
let
val (goal, _) = mk_goal lthy f;
val vars = Variable.add_free_names lthy goal [];
in
Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_lfp_rec_sugar_transfer_tac ctxt def)
|> Thm.close_derivation \<^here>
end);
val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
(fn kk => fn bnfs => fn f => fn def => fn lthy =>
let
val fp_sugars = map (the o fp_sugar_of_bnf lthy) bnfs;
val (goal, _) = mk_goal lthy f;
val vars = Variable.add_free_names lthy goal [];
val (disc_eq_cases, case_thms, case_distribs, case_congs) =
bnf_depth_first_traverse lthy (fn bnf =>
(case fp_sugar_of_bnf lthy bnf of
NONE => I
| SOME {fp_ctr_sugar = {ctr_sugar = {disc_eq_cases, case_thms, case_distribs,
case_cong, ...}, ...}, ...} =>
(fn (disc_eq_cases0, case_thms0, case_distribs0, case_congs0) =>
(union Thm.eq_thm disc_eq_cases disc_eq_cases0,
union Thm.eq_thm case_thms case_thms0,
union Thm.eq_thm case_distribs case_distribs0,
insert Thm.eq_thm case_cong case_congs0))))
(fastype_of f) ([], [], [], []);
in
Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} =>
mk_gfp_rec_sugar_transfer_tac ctxt def
(#co_rec_def (the (#fp_co_induct_sugar (nth fp_sugars kk))))
(map (#type_definition o #absT_info) fp_sugars)
(maps (#xtor_co_rec_transfers o #fp_res) fp_sugars)
(map (rel_def_of_bnf o #pre_bnf) fp_sugars)
disc_eq_cases case_thms case_distribs case_congs)
|> Thm.close_derivation \<^here>
end);
val _ = Theory.setup (lfp_rec_sugar_interpretation transfer_plugin
lfp_rec_sugar_transfer_interpretation);
end;
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
