# HG changeset patch # User Christian Urban # Date 1261606922 -3600 # Node ID da75568e7f124962789d2bfcd99e28941765bf11 # Parent 06e17083e90bd8339fa0edb702c9c73945641a57 renamed some fields in the info records diff -r 06e17083e90b -r da75568e7f12 Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Wed Dec 23 22:42:30 2009 +0100 +++ b/Quot/Examples/FSet3.thy Wed Dec 23 23:22:02 2009 +0100 @@ -12,6 +12,8 @@ unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def by auto +(* FIXME-TODO: because of beta-reduction, one cannot give the *) +(* FIXME-TODO: relation as a term or abbreviation *) quotient_type fset = "'a list" / "list_eq" by (rule list_eq_equivp) diff -r 06e17083e90b -r da75568e7f12 Quot/quotient_info.ML --- a/Quot/quotient_info.ML Wed Dec 23 22:42:30 2009 +0100 +++ b/Quot/quotient_info.ML Wed Dec 23 23:22:02 2009 +0100 @@ -2,15 +2,15 @@ sig exception NotFound - type maps_info = {mapfun: string, relfun: string} - val maps_lookup: theory -> string -> maps_info (* raises NotFound *) + type maps_info = {mapfun: string, relmap: string} + val maps_lookup: theory -> string -> maps_info (* raises NotFound *) val maps_update_thy: string -> maps_info -> theory -> theory val maps_update: string -> maps_info -> Proof.context -> Proof.context val print_mapsinfo: Proof.context -> unit - type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} - val quotdata_lookup_thy: theory -> string -> quotient_info option - val quotdata_lookup: Proof.context -> string -> quotient_info option + type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} + val quotdata_lookup_thy: theory -> string -> quotient_info (* raises NotFound *) + val quotdata_lookup: Proof.context -> string -> quotient_info (* raises NotFound *) val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context val quotdata_dest: theory -> quotient_info list @@ -18,7 +18,7 @@ type qconsts_info = {qconst: term, rconst: term, def: thm} val qconsts_transfer: morphism -> qconsts_info -> qconsts_info - val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) + val qconsts_lookup: theory -> term -> qconsts_info (* raises NotFound *) val qconsts_update_thy: string -> qconsts_info -> theory -> theory val qconsts_update_gen: string -> qconsts_info -> Context.generic -> Context.generic val qconsts_dest: theory -> qconsts_info list @@ -43,7 +43,7 @@ (*******************) (* info about map- and rel-functions for a type *) -type maps_info = {mapfun: string, relfun: string} +type maps_info = {mapfun: string, relmap: string} structure MapsData = Theory_Data (type T = maps_info Symtab.table @@ -73,7 +73,7 @@ fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt) val _ = map sanity_check [mapname, relname] in - maps_attribute_aux tyname {mapfun = mapname, relfun = relname} + maps_attribute_aux tyname {mapfun = mapname, relmap = relname} end val maps_attr_parser = @@ -88,12 +88,12 @@ fun print_mapsinfo ctxt = let - fun prt_map (ty_name, {mapfun, relfun}) = + fun prt_map (ty_name, {mapfun, relmap}) = Pretty.block (Library.separate (Pretty.brk 2) (map Pretty.str ["type:", ty_name, - "map fun:", mapfun, - "relation map:", relfun])) + "map:", mapfun, + "relation map:", relmap])) in MapsData.get (ProofContext.theory_of ctxt) |> Symtab.dest @@ -104,7 +104,7 @@ (* info about quotient types *) -type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} +type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm} structure QuotData = Theory_Data (type T = quotient_info Symtab.table @@ -112,13 +112,19 @@ val extend = I val merge = Symtab.merge (K true)) -fun quotdata_lookup_thy thy str = - Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str) +fun quotdata_lookup_thy thy s = + case Symtab.lookup (QuotData.get thy) (Sign.intern_type thy s) of + SOME qinfo => qinfo + | NONE => raise NotFound val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of -fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) = - QuotData.map (Symtab.update (qty_name, {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm})) +fun quotdata_update_thy qty_name (qty, rty, equiv_rel, equiv_thm) = +let + val qinfo = {qtyp = qty, rtyp = rty, equiv_rel = equiv_rel, equiv_thm = equiv_thm} +in + QuotData.map (Symtab.update (qty_name, qinfo)) +end fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm)) @@ -128,14 +134,14 @@ fun print_quotinfo ctxt = let - fun prt_quot {qtyp, rtyp, rel, equiv_thm} = + fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} = Pretty.block (Library.separate (Pretty.brk 2) [Pretty.str "quotient type:", Syntax.pretty_typ ctxt qtyp, Pretty.str "raw type:", Syntax.pretty_typ ctxt rtyp, Pretty.str "relation:", - Syntax.pretty_term ctxt rel, + Syntax.pretty_term ctxt equiv_rel, Pretty.str "equiv. thm:", Syntax.pretty_term ctxt (prop_of equiv_thm)]) in diff -r 06e17083e90b -r da75568e7f12 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Wed Dec 23 22:42:30 2009 +0100 +++ b/Quot/quotient_term.ML Wed Dec 23 23:22:02 2009 +0100 @@ -45,9 +45,9 @@ let val thy = ProofContext.theory_of ctxt val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."]) - val info = maps_lookup thy ty_str handle NotFound => raise exc + val mapfun = #mapfun (maps_lookup thy ty_str) handle NotFound => raise exc in - Const (#mapfun info, dummyT) + Const (mapfun, dummyT) end fun get_absrep_const flag ctxt _ qty = @@ -145,23 +145,24 @@ if s = s' then let - val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) - val map_info = maps_lookup thy s handle NotFound => raise exc + val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s ^ ")") + val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc val args = map (mk_resp_arg ctxt) (tys ~~ tys') in - list_comb (Const (#relfun map_info, dummyT), args) + list_comb (Const (relmap, dummyT), args) end else - let - val SOME qinfo = quotdata_lookup_thy thy s' + let + val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") + val equiv_rel = #equiv_rel (quotdata_lookup_thy thy s') handle NotFound => raise exc (* FIXME: check in this case that the rty and qty *) (* FIXME: correspond to each other *) (* we need to instantiate the TVars in the relation *) val thy = ProofContext.theory_of ctxt - val forced_rel = force_typ thy (#rel qinfo) (rty --> rty --> @{typ bool}) + val forced_equiv_rel = force_typ thy equiv_rel (rty --> rty --> @{typ bool}) in - forced_rel + forced_equiv_rel end | _ => HOLogic.eq_const rty (* FIXME: check that the types correspond to each other? *)