--- 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"
--- 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
--- 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])
(*