# HG changeset patch
# User wenzelm
# Date 1727023663 -7200
# Node ID eabc517e7413003fa5f8cc4db6e3fcf23e489221
# Parent  6c1146e6e79eb303c2b586feb56d9ba15db19021
misc tuning and clarification;

diff -r 6c1146e6e79e -r eabc517e7413 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sun Sep 22 17:40:28 2024 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Sep 22 18:47:43 2024 +0200
@@ -387,19 +387,27 @@
   end
 
 
-fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
+fun prove_stuff ctxt globals G0 f R0 clauses complete compat compat_store G_elim f_def =
   let
-    val Globals {h, domT, ranT, x, ...} = globals
+    val Globals {h, domT, ranT, x = x0, ...} = globals
+
+    val G = Thm.cterm_of ctxt G0
+    val R = Thm.cterm_of ctxt R0
+
+    val x = Thm.cterm_of ctxt x0
+
+    val A = Thm.ctyp_of ctxt domT
+    val B = Thm.ctyp_of ctxt ranT
+    val C = Thm.ctyp_of_cterm x
 
     val ihyp =
-      \<^instantiate>\<open>'a = \<open>Thm.ctyp_of ctxt domT\<close>
-        and 'b = \<open>Thm.ctyp_of ctxt ranT\<close>
-        and 'c = \<open>Thm.ctyp_of ctxt (fastype_of x)\<close>
-        and x = \<open>Thm.cterm_of ctxt x\<close>
-        and R = \<open>Thm.cterm_of ctxt R\<close>
-        and G = \<open>Thm.cterm_of ctxt G\<close>
+      \<^instantiate>\<open>'a = A and 'b = B and 'c = C and x and R and G
         in cprop \<open>\<And>z::'a. R z x \<Longrightarrow> \<exists>!y::'b. G z y\<close> for x :: 'c\<close>
 
+    val acc_R_x =
+      \<^instantiate>\<open>'c = C and R and x
+        in cprop \<open>Wellfounded.accp R x\<close> for x :: 'c\<close>
+
     val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0
     val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
     val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
@@ -412,16 +420,16 @@
     val (ex1s, values) =
       split_list
         (map
-          (mk_uniqueness_case ctxt globals G f ihyp ih_intro G_elim compat_store clauses repLemmas)
+          (mk_uniqueness_case ctxt globals G0 f ihyp ih_intro G_elim compat_store clauses repLemmas)
           clauses)
 
     val _ = trace_msg (K "Proving: Graph is a function")
     val graph_is_function = complete
       |> Thm.forall_elim_vars 0
       |> fold (curry op COMP) ex1s
-      |> Thm.implies_intr (ihyp)
-      |> Thm.implies_intr (Thm.cterm_of ctxt (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
-      |> Thm.forall_intr (Thm.cterm_of ctxt x)
+      |> Thm.implies_intr ihyp
+      |> Thm.implies_intr acc_R_x
+      |> Thm.forall_intr x
       |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
       |> (fn it =>
           fold (Thm.forall_intr o Thm.cterm_of ctxt o Var)
@@ -770,55 +778,67 @@
   end
 
 
-fun mk_nest_term_rule ctxt globals R R_cases clauses =
+fun mk_nest_term_rule ctxt globals R0 R_cases clauses =
   let
-    val Globals { domT, x, z, ... } = globals
-    val acc_R = mk_acc domT R
+    val Globals { domT, x = x0, z = z0, ... } = globals
 
     val ([Rn], ctxt') = Variable.variant_fixes ["R"] ctxt
-    val R' = Free (Rn, fastype_of R)
+
+    val R = Thm.cterm_of ctxt' R0
+    val R' = Thm.cterm_of ctxt' (Free (Rn, Thm.typ_of_cterm R))
+    val Rrel = Thm.cterm_of ctxt' (Free (Rn, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))))
 
-    val Rrel = Free (Rn, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
-    val inrel_R = \<^Const>\<open>in_rel domT domT for Rrel\<close>
+    val x = Thm.cterm_of ctxt' x0
+    val z = Thm.cterm_of ctxt' z0
+
+    val A = Thm.ctyp_of ctxt' domT
+    val B = Thm.ctyp_of_cterm x
 
-    val wfR' =
-      \<^instantiate>\<open>'a = \<open>Thm.ctyp_of ctxt' domT\<close>
-        and R = \<open>Thm.cterm_of ctxt' R'\<close> in cprop \<open>wfP R\<close>\<close>
+    val acc_R_z =
+      \<^instantiate>\<open>'a = A and R and z
+        in cterm \<open>Wellfounded.accp R z\<close> for z :: 'a\<close>
 
-    (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
-    val ihyp = Logic.all_const domT $ Abs ("z", domT,
-      Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
-        HOLogic.mk_Trueprop (acc_R $ Bound 0)))
-      |> Thm.cterm_of ctxt'
+    val inrel_R =
+      \<^instantiate>\<open>'a = A and Rrel
+        in cterm \<open>in_rel Rrel\<close> for Rrel :: \<open>('a \<times> 'a) set\<close>\<close>
+
+    val wfR' = \<^instantiate>\<open>'a = A and R' in cprop \<open>wfP R'\<close>\<close>
+
+    val ihyp =
+      \<^instantiate>\<open>'a = A and 'b = B and x and R' and R
+        in cprop \<open>\<And>z::'a. R' z x \<Longrightarrow> Wellfounded.accp R z\<close> for x :: 'b\<close>
 
     val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
 
-    val R_z_x = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (R $ z $ x))
+    val R_z_x =
+      \<^instantiate>\<open>'a = A and 'b = B and R and x and z
+        in cprop \<open>R z x\<close> for x :: 'a and z :: 'b\<close>
 
-    val (hyps, cases) = fold (mk_nest_term_case ctxt' globals R' ihyp_a) clauses ([], [])
+    val (hyps, cases) =
+      fold (mk_nest_term_case ctxt' globals (Thm.term_of R') ihyp_a) clauses ([], [])
   in
     R_cases
-    |> Thm.forall_elim (Thm.cterm_of ctxt' z)
-    |> Thm.forall_elim (Thm.cterm_of ctxt' x)
-    |> Thm.forall_elim (Thm.cterm_of ctxt' (acc_R $ z))
+    |> Thm.forall_elim z
+    |> Thm.forall_elim x
+    |> Thm.forall_elim acc_R_z
     |> curry op COMP (Thm.assume R_z_x)
     |> fold_rev (curry op COMP) cases
     |> Thm.implies_intr R_z_x
-    |> Thm.forall_intr (Thm.cterm_of ctxt' z)
+    |> Thm.forall_intr z
     |> (fn it => it COMP accI)
     |> Thm.implies_intr ihyp
-    |> Thm.forall_intr (Thm.cterm_of ctxt' x)
+    |> Thm.forall_intr x
     |> (fn it => Drule.compose (it, 2, wf_induct_rule))
     |> curry op RS (Thm.assume wfR')
     |> Thm.forall_intr_vars
     |> (fn it => it COMP allI)
     |> fold Thm.implies_intr hyps
     |> Thm.implies_intr wfR'
-    |> Thm.forall_intr (Thm.cterm_of ctxt' R')
-    |> Thm.forall_elim (Thm.cterm_of ctxt' inrel_R)
+    |> Thm.forall_intr R'
+    |> Thm.forall_elim inrel_R
     |> curry op RS wf_in_rel
     |> full_simplify (put_simpset HOL_basic_ss ctxt' addsimps [in_rel_def])
-    |> Thm.forall_intr_name ("R", Thm.cterm_of ctxt' Rrel)
+    |> Thm.forall_intr_name ("R", Rrel)
   end