# HG changeset patch
# User wenzelm
# Date 1662405209 -7200
# Node ID 28ddebb43d93ff206bd019ecb156184502d6dd3f
# Parent  24c9f56aa03520d808126a6471f1d947006ed35d
show goal instantiation, notably for 'schematic_goal' command (inactive by default);

diff -r 24c9f56aa035 -r 28ddebb43d93 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Sep 05 20:22:13 2022 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Sep 05 21:13:29 2022 +0200
@@ -601,6 +601,7 @@
   register_config_bool Thm.show_consts #>
   register_config_bool Thm.show_hyps #>
   register_config_bool Thm.show_tags #>
+  register_config_bool Proof_Display.show_goal_inst #>
   register_config_bool Proof_Display.show_results #>
   register_config_bool Pattern.unify_trace_failure #>
   register_config_int Unify.trace_bound #>
diff -r 24c9f56aa035 -r 28ddebb43d93 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Sep 05 20:22:13 2022 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Sep 05 21:13:29 2022 +0200
@@ -382,10 +382,17 @@
 
     val prt_facts = Proof_Display.pretty_goal_facts ctxt;
 
-    fun prt_goal (SOME (_, {statement = _, using, goal, before_qed = _, after_qed = _})) =
-          pretty_sep
-            (prt_facts "using" (if mode <> Backward orelse null using then NONE else SOME using))
-            ([Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal)
+    fun prt_goal (SOME (_, goal)) =
+          let
+            val {statement = (_, propss, _), using, goal, before_qed = _, after_qed = _} = goal;
+            val head = [Proof_Display.pretty_goal_header goal];
+            val body = Goal_Display.pretty_goals ctxt goal;
+            val foot = Proof_Display.pretty_goal_inst ctxt propss goal;
+          in
+            pretty_sep
+              (prt_facts "using" (if mode <> Backward orelse null using then NONE else SOME using))
+              (head @ body @ foot)
+          end
       | prt_goal NONE = [];
 
     val prt_ctxt =
diff -r 24c9f56aa035 -r 28ddebb43d93 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Mon Sep 05 20:22:13 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon Sep 05 21:13:29 2022 +0200
@@ -20,6 +20,8 @@
   val pretty_goal_header: thm -> Pretty.T
   val string_of_goal: Proof.context -> thm -> string
   val pretty_goal_facts: Proof.context -> string -> thm list option -> Pretty.T list
+  val show_goal_inst: bool Config.T
+  val pretty_goal_inst: Proof.context -> term list list -> thm -> Pretty.T list
   val method_error: string -> Position.T ->
     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
   val show_results: bool Config.T
@@ -247,6 +249,63 @@
          Proof_Context.pretty_fact ctxt ("", ths)];
 
 
+(* goal instantiation *)
+
+val show_goal_inst = Config.declare_bool ("show_goal_inst", \<^here>) (K false);
+
+fun pretty_goal_inst ctxt propss goal =
+  let
+    val title = "instantiation:";
+
+    fun prt_inst env =
+      if Envir.is_empty env then []
+      else
+        let
+          val prt_type = Syntax.pretty_typ ctxt;
+          val prt_term = Syntax.pretty_term ctxt;
+
+          fun instT v =
+            let
+              val T = TVar v;
+              val T' = Envir.norm_type (Envir.type_env env) T;
+            in if T = T' then NONE else SOME (prt_type T, prt_type T') end;
+
+          fun inst v =
+            let
+              val t = Var v;
+              val t' = Envir.norm_term env t;
+            in if t aconv t' then NONE else SOME (prt_term t, prt_term t') end;
+
+          fun prt_eq (x, y) = Pretty.block [x, Pretty.str " =", Pretty.brk 1, y];
+
+          val prts =
+            ((fold o fold) Term.add_tvars propss [] |> sort Term_Ord.tvar_ord |> map_filter instT) @
+            ((fold o fold) Term.add_vars propss [] |> sort Term_Ord.var_ord |> map_filter inst);
+        in if null prts then [] else [Pretty.big_list title (map prt_eq prts)] end;
+
+    fun prt_failed prt = [Pretty.block [Pretty.str title, Pretty.brk 1, prt]];
+
+    fun goal_matcher () =
+      let
+        val concl = Logic.unprotect (Thm.concl_of goal);
+        val goal_propss = filter_out null propss;
+        val results =
+          Logic.dest_conjunction_balanced (length goal_propss) concl
+          |> map2 Logic.dest_conjunction_balanced (map length goal_propss);
+      in
+        Unify.matcher (Context.Proof ctxt)
+          (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (flat results)
+      end;
+  in
+    if Config.get ctxt show_goal_inst then
+      (case Exn.interruptible_capture goal_matcher () of
+        Exn.Res (SOME env) => prt_inst env
+      | Exn.Res NONE => prt_failed (Pretty.mark_str (Markup.bad (), "FAILED"))
+      | Exn.Exn exn => prt_failed (Runtime.pretty_exn exn))
+    else []
+  end;
+
+
 (* method_error *)
 
 fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>