--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Feb 16 19:30:53 2018 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Feb 16 19:58:42 2018 +0100
@@ -61,11 +61,11 @@
val (_, prop') = Local_Defs.cert_def lthy (K []) prop
val (_, newrhs) = Local_Defs.abs_def prop'
- val ((trm, (_ , def_thm)), lthy') =
+ val ((qconst, (_ , def)), lthy') =
Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
- (* data storage *)
- val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
+ fun qconst_data phi =
+ Quotient_Info.transform_quotconsts phi {qconst = qconst, rconst = rhs, def = def}
fun qualify defname suffix = Binding.name suffix
|> Binding.qualify true defname
@@ -76,14 +76,14 @@
val lthy'' = lthy'
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi =>
- (case Quotient_Info.transform_quotconsts phi qconst_data of
+ (case qconst_data phi of
qcinfo as {qconst = Const (c, _), ...} =>
Quotient_Info.update_quotconsts (c, qcinfo)
| _ => I))
|> (snd oo Local_Theory.note)
((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
in
- (qconst_data, lthy'')
+ (qconst_data Morphism.identity, lthy'')
end
fun mk_readable_rsp_thm_eq tm lthy =
--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Feb 16 19:30:53 2018 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Feb 16 19:58:42 2018 +0100
@@ -111,9 +111,9 @@
(Scan.lift @{keyword "("} |--
Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
Attrib.thm --| Scan.lift @{keyword ")"}) >>
- (fn (tyname, (relname, qthm)) =>
- let val minfo = {relmap = relname, quot_thm = qthm}
- in Thm.declaration_attribute (fn _ => map_quotmaps (Symtab.update (tyname, minfo))) end))
+ (fn (tyname, (relmap, quot_thm)) =>
+ let val minfo = {relmap = relmap, quot_thm = quot_thm}
+ in Thm.declaration_attribute (K (map_quotmaps (Symtab.update (tyname, minfo)))) end))
"declaration of map information")
fun print_quotmaps ctxt =
@@ -201,8 +201,8 @@
fun lookup_quotconsts_global thy t =
let
val (name, qty) = dest_Const t
- fun matches (x: quotconsts) =
- let val (name', qty') = dest_Const (#qconst x);
+ fun matches ({qconst, ...}: quotconsts) =
+ let val (name', qty') = dest_Const qconst;
in name = name' andalso Sign.typ_instance thy (qty, qty') end
in
(case Symtab.lookup (get_quotconsts (Context.Theory thy)) name of
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Feb 16 19:30:53 2018 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Feb 16 19:58:42 2018 +0100
@@ -154,7 +154,6 @@
fun regularize_tac ctxt =
let
- val thy = Proof_Context.theory_of ctxt
val simpset =
mk_minimal_simpset ctxt
addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Feb 16 19:30:53 2018 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Feb 16 19:58:42 2018 +0100
@@ -83,7 +83,7 @@
val thy = Proof_Context.theory_of ctxt
in
(case Quotient_Info.lookup_quotients_global thy s of
- SOME qdata => (#rtyp qdata, #qtyp qdata)
+ SOME {rtyp, qtyp, ...} => (rtyp, qtyp)
| NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
end
@@ -104,12 +104,9 @@
| mk_dummyT (Free (c, _)) = Free (c, dummyT)
| mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable"
in
- case Quotient_Info.lookup_abs_rep ctxt qty_str of
- SOME abs_rep =>
- mk_dummyT (case flag of
- AbsF => #abs abs_rep
- | RepF => #rep abs_rep)
- | NONE => error ("No abs/rep terms for " ^ quote qty_str)
+ (case Quotient_Info.lookup_abs_rep ctxt qty_str of
+ SOME {abs, rep} => mk_dummyT (case flag of AbsF => abs | RepF => rep)
+ | NONE => error ("No abs/rep terms for " ^ quote qty_str))
end
(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
@@ -273,14 +270,14 @@
fun mk_rel_compose (trm1, trm2) =
Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
-fun get_relmap thy s =
- (case Quotient_Info.lookup_quotmaps thy s of
- SOME map_data => Const (#relmap map_data, dummyT)
+fun get_relmap ctxt s =
+ (case Quotient_Info.lookup_quotmaps ctxt s of
+ SOME {relmap, ...} => Const (relmap, dummyT)
| NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
-fun get_equiv_rel thy s =
- (case Quotient_Info.lookup_quotients thy s of
- SOME qdata => #equiv_rel qdata
+fun get_equiv_rel ctxt s =
+ (case Quotient_Info.lookup_quotients ctxt s of
+ SOME {equiv_rel, ...} => equiv_rel
| NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")"))
fun equiv_match_err ctxt ty_pat ty =
@@ -342,7 +339,7 @@
val thy = Proof_Context.theory_of ctxt
in
(case Quotient_Info.lookup_quotients ctxt s of
- SOME qdata => Thm.transfer thy (#quot_thm qdata)
+ SOME {quot_thm, ...} => Thm.transfer thy quot_thm
| NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."))
end
@@ -351,7 +348,7 @@
val thy = Proof_Context.theory_of ctxt
in
(case Quotient_Info.lookup_quotmaps ctxt s of
- SOME map_data => Thm.transfer thy (#quot_thm map_data)
+ SOME {quot_thm, ...} => Thm.transfer thy quot_thm
| NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
end
@@ -497,7 +494,7 @@
else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys)
else
(case Quotient_Info.lookup_quotients_global thy qs of
- SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
+ SOME {rtyp, ...} => Sign.typ_instance thy (rT, rtyp)
| NONE => false)
| _ => false)
end
@@ -626,7 +623,7 @@
let
val rtrm' =
(case Quotient_Info.lookup_quotconsts_global thy qtrm of
- SOME qconst_info => #rconst qconst_info
+ SOME {rconst, ...} => rconst
| NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
in
if Pattern.matches thy (rtrm', rtrm)
@@ -858,5 +855,4 @@
fun derive_rtrm ctxt qtys qtrm =
subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
-
end;
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Feb 16 19:30:53 2018 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Feb 16 19:58:42 2018 +0100
@@ -141,17 +141,18 @@
val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o Thm.prop_of) quot_thm
val (qtyp, rtyp) = (dest_funT o fastype_of) rep
val qty_full_name = (fst o dest_Type) qtyp
- val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
- quot_thm = quot_thm }
- fun quot_info phi = Quotient_Info.transform_quotients phi quotients
- val abs_rep = {abs = abs, rep = rep}
- fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep
+ fun quotients phi =
+ Quotient_Info.transform_quotients phi
+ {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
+ quot_thm = quot_thm}
+ fun abs_rep phi =
+ Quotient_Info.transform_abs_rep phi {abs = abs, rep = rep}
in
lthy
- |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Quotient_Info.update_quotients (qty_full_name, quot_info phi)
- #> Quotient_Info.update_abs_rep (qty_full_name, abs_rep_info phi))
- |> setup_lifting_package quot_thm equiv_thm opt_par_thm
+ |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+ Quotient_Info.update_quotients (qty_full_name, quotients phi) #>
+ Quotient_Info.update_abs_rep (qty_full_name, abs_rep phi))
+ |> setup_lifting_package quot_thm equiv_thm opt_par_thm
end
(* main function for constructing a quotient type *)