# HG changeset patch # User wenzelm # Date 1518807522 -3600 # Node ID 3b94553353ae628202d3d3d2cae4df857e02a2d5 # Parent b7d90c4a3897ffbc0622b692ac94a976a229874e tuned; diff -r b7d90c4a3897 -r 3b94553353ae src/HOL/Tools/Quotient/quotient_def.ML --- 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 = diff -r b7d90c4a3897 -r 3b94553353ae src/HOL/Tools/Quotient/quotient_info.ML --- 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 diff -r b7d90c4a3897 -r 3b94553353ae src/HOL/Tools/Quotient/quotient_tacs.ML --- 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} diff -r b7d90c4a3897 -r 3b94553353ae src/HOL/Tools/Quotient/quotient_term.ML --- 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; diff -r b7d90c4a3897 -r 3b94553353ae src/HOL/Tools/Quotient/quotient_type.ML --- 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 *)