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 **)