1(* Title: HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML 2 Author: Martin Desharnais, TU Muenchen 3 Copyright 2014 4 5Parametricity of primitively (co)recursive functions. 6*) 7 8signature BNF_FP_REC_SUGAR_TRANSFER = 9sig 10 val set_transfer_rule_attrs: thm list -> local_theory -> local_theory 11 12 val lfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> 13 Proof.context 14 val gfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> 15 Proof.context 16end; 17 18structure BNF_FP_Rec_Sugar_Transfer : BNF_FP_REC_SUGAR_TRANSFER = 19struct 20 21open Ctr_Sugar_Util 22open Ctr_Sugar_Tactics 23open BNF_Util 24open BNF_Def 25open BNF_FP_Util 26open BNF_FP_Def_Sugar 27open BNF_FP_Rec_Sugar_Util 28open BNF_LFP_Rec_Sugar 29 30val transferN = "transfer"; 31 32val transfer_rule_attrs = @{attributes [transfer_rule]}; 33 34fun set_transfer_rule_attrs thms = 35 snd o Local_Theory.notes [(Binding.empty_atts, [(thms, transfer_rule_attrs)])]; 36 37fun mk_lfp_rec_sugar_transfer_tac ctxt def = 38 unfold_thms_tac ctxt [def] THEN HEADGOAL (Transfer.transfer_prover_tac ctxt); 39 40fun mk_gfp_rec_sugar_transfer_tac ctxt f_def corec_def type_definitions dtor_corec_transfers 41 rel_pre_defs disc_eq_cases cases case_distribs case_congs = 42 let 43 fun instantiate_with_lambda thm = 44 let 45 val prop as \<^const>\<open>Trueprop\<close> $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Var (_, fT) $ _) $ _) = 46 Thm.prop_of thm; 47 val T = range_type fT; 48 val j = Term.maxidx_of_term prop + 1; 49 val cond = Var (("x", j), HOLogic.boolT); 50 val then_branch = Var (("t", j), T); 51 val else_branch = Var (("e", j), T); 52 val lam = Term.lambda cond (mk_If cond then_branch else_branch); 53 in 54 infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt lam)] thm 55 end; 56 57 val transfer_rules = 58 @{thm Abs_transfer[OF type_definition_id_bnf_UNIV type_definition_id_bnf_UNIV]} :: 59 map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions @ 60 map (Local_Defs.unfold0 ctxt rel_pre_defs) dtor_corec_transfers; 61 val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add; 62 val ctxt' = Context.proof_map (fold add_transfer_rule transfer_rules) ctxt; 63 64 val case_distribs = map instantiate_with_lambda case_distribs; 65 val simps = case_distribs @ disc_eq_cases @ cases @ @{thms if_True if_False}; 66 val ctxt'' = put_simpset (simpset_of (ss_only simps ctxt)) ctxt'; 67 in 68 unfold_thms_tac ctxt ([f_def, corec_def] @ @{thms split_beta if_conn}) THEN 69 HEADGOAL (simp_tac (fold Simplifier.add_cong case_congs ctxt'')) THEN 70 HEADGOAL (Transfer.transfer_prover_tac ctxt') 71 end; 72 73fun massage_simple_notes base = 74 filter_out (null o #2) 75 #> map (fn (thmN, thms, f_attrs) => 76 ((Binding.qualify true base (Binding.name thmN), []), 77 map_index (fn (kk, thm) => ([thm], f_attrs kk)) thms)); 78 79fun fp_sugar_of_bnf ctxt = fp_sugar_of ctxt o (fn Type (s, _) => s) o T_of_bnf; 80 81fun bnf_depth_first_traverse ctxt f T = 82 (case T of 83 Type (s, Ts) => 84 (case bnf_of ctxt s of 85 NONE => I 86 | SOME bnf => fold (bnf_depth_first_traverse ctxt f) Ts o f bnf) 87 | _ => I); 88 89fun mk_goal lthy f = 90 let 91 val skematic_Ts = Term.add_tvarsT (fastype_of f) []; 92 93 val ((As, Bs), names_lthy) = lthy 94 |> mk_TFrees' (map snd skematic_Ts) 95 ||>> mk_TFrees' (map snd skematic_Ts); 96 97 val ((Rs, Rs'), names_lthy) = mk_Frees' "R" (map2 mk_pred2T As Bs) names_lthy; 98 99 val fA = Term.subst_TVars (map fst skematic_Ts ~~ As) f; 100 val fB = Term.subst_TVars (map fst skematic_Ts ~~ Bs) f; 101 102 val goal = mk_parametricity_goal lthy Rs fA fB; 103 val used_Rs = Term.add_frees goal []; 104 val subst = map (dest_pred2T o snd) (filter_out (member (op =) used_Rs) Rs'); 105 in 106 (goal |> Term.subst_atomic_types subst, names_lthy) 107 end; 108 109fun fp_rec_sugar_transfer_interpretation prove {transfers, fun_names, funs, fun_defs, fpTs} = 110 fold_index (fn (kk, (((transfer, fun_name), funx), fun_def)) => fn lthy => 111 if transfer then 112 (case try (map the) (map (fn Type (s, _) => bnf_of lthy s | _ => NONE) fpTs) of 113 NONE => error "No transfer rule possible" 114 | SOME bnfs => 115 (case try (prove kk bnfs funx fun_def) lthy of 116 NONE => error "Failed to prove transfer rule" 117 | SOME thm => 118 let 119 val notes = [(transferN, [thm], K @{attributes [transfer_rule]})] 120 |> massage_simple_notes fun_name; 121 in 122 snd (Local_Theory.notes notes lthy) 123 end)) 124 else 125 lthy) 126 (transfers ~~ fun_names ~~ funs ~~ fun_defs); 127 128val lfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation 129 (fn _ => fn _ => fn f => fn def => fn lthy => 130 let 131 val (goal, _) = mk_goal lthy f; 132 val vars = Variable.add_free_names lthy goal []; 133 in 134 Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} => 135 mk_lfp_rec_sugar_transfer_tac ctxt def) 136 |> Thm.close_derivation \<^here> 137 end); 138 139val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation 140 (fn kk => fn bnfs => fn f => fn def => fn lthy => 141 let 142 val fp_sugars = map (the o fp_sugar_of_bnf lthy) bnfs; 143 val (goal, _) = mk_goal lthy f; 144 val vars = Variable.add_free_names lthy goal []; 145 val (disc_eq_cases, case_thms, case_distribs, case_congs) = 146 bnf_depth_first_traverse lthy (fn bnf => 147 (case fp_sugar_of_bnf lthy bnf of 148 NONE => I 149 | SOME {fp_ctr_sugar = {ctr_sugar = {disc_eq_cases, case_thms, case_distribs, 150 case_cong, ...}, ...}, ...} => 151 (fn (disc_eq_cases0, case_thms0, case_distribs0, case_congs0) => 152 (union Thm.eq_thm disc_eq_cases disc_eq_cases0, 153 union Thm.eq_thm case_thms case_thms0, 154 union Thm.eq_thm case_distribs case_distribs0, 155 insert Thm.eq_thm case_cong case_congs0)))) 156 (fastype_of f) ([], [], [], []); 157 in 158 Goal.prove lthy vars [] goal (fn {context = ctxt, prems = _} => 159 mk_gfp_rec_sugar_transfer_tac ctxt def 160 (#co_rec_def (the (#fp_co_induct_sugar (nth fp_sugars kk)))) 161 (map (#type_definition o #absT_info) fp_sugars) 162 (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars) 163 (map (rel_def_of_bnf o #pre_bnf) fp_sugars) 164 disc_eq_cases case_thms case_distribs case_congs) 165 |> Thm.close_derivation \<^here> 166 end); 167 168val _ = Theory.setup (lfp_rec_sugar_interpretation transfer_plugin 169 lfp_rec_sugar_transfer_interpretation); 170 171end; 172