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