src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML

 Parametricity of primitively (co)recursive functions.
 *)
 
 signature BNF_FP_REC_SUGAR_TRANSFER =
 sig
-  val primrec_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
+  val lfp_rec_sugar_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context ->
     Proof.context
-  val primcorec_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> 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_Tactics
 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";
 
-fun mk_primrec_transfer_tac ctxt def =
+fun mk_lfp_rec_sugar_transfer_tac ctxt def =
   Ctr_Sugar_Tactics.unfold_thms_tac ctxt [def] THEN
   HEADGOAL (Transfer.transfer_prover_tac ctxt);
 
-fun mk_primcorec_transfer_tac apply_transfer ctxt f_def corec_def type_definitions
+fun mk_gfp_rec_sugar_transfer_tac apply_transfer 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 = Thm.prop_of thm;

         if_all_bnfs lthy fpTs
           (fn bnfs => fn () => prove n bnfs f_names f def lthy)
           (fn () => error "Function is not parametric" (*FIXME: wording*)) ())
     (transfers ~~ fun_names ~~ funs ~~ fun_defs) lthy;
 
-fun prim_co_rec_transfer_interpretation prove =
+fun fp_rec_sugar_transfer_interpretation prove =
   prove_parametricity_if_bnf (fn n => fn bnfs => fn f_name => fn f => fn def => fn lthy =>
     (case try (prove n bnfs f def) lthy of
       NONE => error "Failed to prove parametricity"
     | SOME thm =>
       let

           |> massage_simple_notes f_name;
       in
         snd (Local_Theory.notes notes lthy)
       end));
 
-val primrec_transfer_interpretation = prim_co_rec_transfer_interpretation
+val lfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
   (fn _ => fn _ => fn f => fn def => fn lthy =>
      let val (goal, names_lthy) = mk_goal lthy f in
        Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} =>
-         mk_primrec_transfer_tac ctxt def)
+         mk_lfp_rec_sugar_transfer_tac ctxt def)
        |> singleton (Proof_Context.export names_lthy lthy)
        |> Thm.close_derivation
      end);
 
-val primcorec_transfer_interpretation = prim_co_rec_transfer_interpretation
+val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
   (fn n => fn bnfs => fn f => fn def => fn lthy =>
      let
        val fp_sugars = map (the o fp_sugar_of_bnf lthy) bnfs;
        val (goal, names_lthy) = mk_goal lthy f;
        val (disc_eq_cases, case_thms, case_distribs, case_congs) =

              Option.map (add_thms quad) (fp_sugar_of_bnf lthy bnf)
              |> the_default quad
            end) (fastype_of f) ([], [], [], []);
      in
        Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} =>
-         mk_primcorec_transfer_tac true ctxt def
+         mk_gfp_rec_sugar_transfer_tac true ctxt def
          (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars n)))
          (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)
        |> singleton (Proof_Context.export names_lthy lthy)
        |> Thm.close_derivation
      end);
 
-val _ = Theory.setup (BNF_LFP_Rec_Sugar.primrec_interpretation Transfer_BNF.transfer_plugin
-  primrec_transfer_interpretation);
+val _ = Theory.setup (lfp_rec_sugar_interpretation Transfer_BNF.transfer_plugin
+  lfp_rec_sugar_transfer_interpretation);
 
 end;