hooks for foundational terms: protection of foundational terms during simplification

--- a/NEWS	Wed Apr 22 19:22:43 2020 +0200
+++ b/NEWS	Tue Apr 21 07:28:17 2020 +0000
@@ -24,6 +24,11 @@
 INCOMPATIBILITY.
 
 
+*** Pure ***
+
+* Definitions in locales produce rule which can be added as congruence
+rule to protect foundational terms during simplification.
+
 
 New in Isabelle2020 (April 2020)
 --------------------------------

--- a/src/Pure/Isar/generic_target.ML	Wed Apr 22 19:22:43 2020 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Apr 21 07:28:17 2020 +0000
@@ -18,6 +18,8 @@
     term list * term list -> local_theory -> (term * thm) * local_theory
   val background_declaration: declaration -> local_theory -> local_theory
   val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
+  val add_foundation_interpretation: (binding * (term * term list) -> Context.generic -> Context.generic) ->
+    theory -> theory
 
   (*nested local theories primitives*)
   val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list
@@ -163,9 +165,32 @@
 
 (** background primitives **)
 
+structure Foundation_Interpretations = Theory_Data
+(
+  type T = (binding * (term * term list) -> Context.generic -> Context.generic) Inttab.table;
+  val empty = Inttab.empty;
+  val extend = I;
+  val merge = Inttab.merge (K true);
+);
+
+fun add_foundation_interpretation f =
+  Foundation_Interpretations.map (Inttab.update_new (serial (), f));
+
+fun foundation_interpretation binding_const_params lthy =
+  let
+    val interps = Foundation_Interpretations.get (Proof_Context.theory_of lthy);
+    val interp = Inttab.fold (fn (_, f) => f binding_const_params) interps;
+  in
+    lthy
+    |> Local_Theory.background_theory (Context.theory_map interp)
+    |> Local_Theory.map_contexts (K (Context.proof_map interp))
+  end;
+
 fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
     val params = type_params @ term_params;
+    val target_params = type_params
+      @ take_prefix is_Free (Variable.export_terms lthy (Local_Theory.target_of lthy) term_params);
     val mx' = check_mixfix_global (b, null params) mx;
 
     val (const, lthy2) = lthy
@@ -175,7 +200,8 @@
     val ((_, def), lthy3) = lthy2
       |> Local_Theory.background_theory_result
         (Thm.add_def (Proof_Context.defs_context lthy2) false false
-          (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
+          (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)))
+      ||> foundation_interpretation (b, (const, target_params));
   in ((lhs, def), lthy3) end;
 
 fun background_declaration decl lthy =

--- a/src/Pure/simplifier.ML	Wed Apr 22 19:22:43 2020 +0200
+++ b/src/Pure/simplifier.ML	Tue Apr 21 07:28:17 2020 +0000
@@ -158,6 +158,34 @@
 end;
 
 
+(** congruence rule to protect foundational terms of local definitions **)
+
+local
+
+fun make_cong ctxt = Thm.close_derivation \<^here> o Thm.reflexive
+  o Thm.cterm_of ctxt o Logic.varify_global o list_comb;
+
+fun add_cong (const_binding, (const, target_params)) gthy =
+  if null target_params
+  then gthy
+  else
+    let
+      val cong = make_cong (Context.proof_of gthy) (const, target_params)
+      val cong_binding = Binding.qualify_name true const_binding "cong"
+    in
+      gthy
+      |> Attrib.generic_notes Thm.theoremK
+           [((cong_binding, []), [([cong], [])])]
+      |> snd
+    end;
+
+in
+
+val _ = Theory.setup (Generic_Target.add_foundation_interpretation add_cong);
+
+end;
+
+
 
 (** pretty_simpset **)