# HG changeset patch
# User wenzelm
# Date 1723119858 -7200
# Node ID 28e8d402a9ba67db0cb8eb7af67d5568ac39d17c
# Parent  cbfc1058df7c9a53edf9e51aa5bbe720beb95b7b
clarified signature;

diff -r cbfc1058df7c -r 28e8d402a9ba src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Aug 07 20:56:31 2024 +0200
+++ b/src/HOL/Lifting.thy	Thu Aug 08 14:24:18 2024 +0200
@@ -25,12 +25,13 @@
 
 subsection \<open>Quotient Predicate\<close>
 
-definition
-  "Quotient R Abs Rep T \<longleftrightarrow>
-     (\<forall>a. Abs (Rep a) = a) \<and>
-     (\<forall>a. R (Rep a) (Rep a)) \<and>
-     (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
-     T = (\<lambda>x y. R x x \<and> Abs x = y)"
+definition Quotient :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+  where
+    "Quotient R Abs Rep T \<longleftrightarrow>
+      (\<forall>a. Abs (Rep a) = a) \<and>
+      (\<forall>a. R (Rep a) (Rep a)) \<and>
+      (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s) \<and>
+      T = (\<lambda>x y. R x x \<and> Abs x = y)"
 
 lemma QuotientI:
   assumes "\<And>a. Abs (Rep a) = a"
diff -r cbfc1058df7c -r 28e8d402a9ba src/HOL/Tools/Lifting/lifting_bnf.ML
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Aug 07 20:56:31 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Thu Aug 08 14:24:18 2024 +0200
@@ -11,6 +11,7 @@
 structure Lifting_BNF : LIFTING_BNF =
 struct
 
+open Lifting_Util
 open BNF_Util
 open BNF_Def
 open Transfer_BNF
@@ -38,13 +39,6 @@
       hyp_subst_tac ctxt, rtac ctxt refl] i
   end
 
-fun mk_Quotient args =
-  let
-    val argTs = map fastype_of args
-  in
-    list_comb (Const (\<^const_name>\<open>Quotient\<close>, argTs ---> HOLogic.boolT), args)
-  end
-
 fun prove_Quotient_map bnf ctxt =
   let
     val live = live_of_bnf bnf
@@ -57,12 +51,13 @@
       |> @{fold_map 2} mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss)
       |>> `transpose
    
-    val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss
+    val assms = argss |> map (fn [rel, abs, rep, cr] =>
+      HOLogic.mk_Trueprop (mk_Quotient (rel, abs, rep, cr)))
     val R_rel = list_comb (mk_rel_of_bnf Ds As As bnf, nth argss' 0)
     val Abs_map = list_comb (mk_map_of_bnf Ds As Bs bnf, nth argss' 1)
     val Rep_map = list_comb (mk_map_of_bnf Ds Bs As bnf, nth argss' 2)
     val T_rel = list_comb (mk_rel_of_bnf Ds As Bs bnf, nth argss' 3)
-    val concl = mk_Quotient [R_rel, Abs_map, Rep_map, T_rel] |> HOLogic.mk_Trueprop
+    val concl = HOLogic.mk_Trueprop (mk_Quotient (R_rel, Abs_map, Rep_map, T_rel))
     val goal = Logic.list_implies (assms, concl)
   in
     Goal.prove_sorry ctxt'' [] [] goal
diff -r cbfc1058df7c -r 28e8d402a9ba src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Wed Aug 07 20:56:31 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Thu Aug 08 14:24:18 2024 +0200
@@ -7,6 +7,7 @@
 signature LIFTING_UTIL =
 sig
   val MRSL: thm list * thm -> thm
+  val mk_Quotient: term * term * term * term -> term
   val dest_Quotient: term -> term * term * term * term
 
   val quot_thm_rel: thm -> term
@@ -40,8 +41,11 @@
 
 fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
 
-fun dest_Quotient (Const (\<^const_name>\<open>Quotient\<close>, _) $ rel $ abs $ rep $ cr)
-      = (rel, abs, rep, cr)
+fun mk_Quotient (rel, abs, rep, cr) =
+  let val \<^Type>\<open>fun A B\<close> = fastype_of abs
+  in \<^Const>\<open>Quotient A B for rel abs rep cr\<close> end
+
+fun dest_Quotient \<^Const_>\<open>Quotient _ _ for rel abs rep cr\<close> = (rel, abs, rep, cr)
   | dest_Quotient t = raise TERM ("dest_Quotient", [t])
 
 (*