# HG changeset patch # User Cezary Kaliszyk # Date 1257253485 -3600 # Node ID c18308f60f0ef1434ad4a44d687a63525857522e # Parent 5f3b364d476554f9fa1dfd6821608db932d87d34# Parent d0581fbc096c7a3423be2a25c99148079a6355b8 merge diff -r 5f3b364d4765 -r c18308f60f0e IntEx.thy --- a/IntEx.thy Tue Nov 03 14:04:21 2009 +0100 +++ b/IntEx.thy Tue Nov 03 14:04:45 2009 +0100 @@ -19,7 +19,6 @@ where "ZERO \ (0::nat, 0::nat)" -thm ZERO_def quotient_def (for my_int) ONE::"my_int" @@ -42,6 +41,14 @@ term PLUS thm PLUS_def +definition + "MPLUS x y \ my_plus x y" + +term MPLUS +thm MPLUS_def +thm MPLUS_def_raw + + fun my_neg :: "(nat \ nat) \ (nat \ nat)" where diff -r 5f3b364d4765 -r c18308f60f0e QuotMain.thy --- a/QuotMain.thy Tue Nov 03 14:04:21 2009 +0100 +++ b/QuotMain.thy Tue Nov 03 14:04:45 2009 +0100 @@ -1,8 +1,11 @@ theory QuotMain imports QuotScript QuotList Prove -uses ("quotient.ML") +uses ("quotient_info.ML") + ("quotient.ML") begin +ML {* Attrib.empty_binding *} + locale QUOT_TYPE = fixes R :: "'a \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" @@ -137,6 +140,7 @@ section {* type definition for the quotient type *} +use "quotient_info.ML" use "quotient.ML" declare [[map list = (map, LIST_REL)]] @@ -300,11 +304,11 @@ fun build_qenv lthy qtys = let val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) - val tsig = Sign.tsig_of (ProofContext.theory_of lthy) + val thy = ProofContext.theory_of lthy fun find_assoc ((qty', rty')::rest) qty = let - val inst = Type.typ_match tsig (qty', qty) Vartab.empty + val inst = Sign.typ_match thy (qty', qty) Vartab.empty in (Envir.norm_type inst qty, Envir.norm_type inst rty') end @@ -319,32 +323,40 @@ end *} + ML {* -val qd_parser = - (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- - (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop)) +fun quotdef_cmd qenv ((bind, qty_, mx), (attr, prop)) lthy = +let + val (lhs_, rhs) = Logic.dest_equals prop +in + make_const_def bind rhs mx qenv lthy +end *} ML {* -fun parse_qd_spec (qtystrs, ((bind, tystr, mx), (attr__, propstr))) lthy = +val quotdef_parser = + Scan.option (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- + (SpecParse.constdecl -- (SpecParse.opt_thm_name ":" -- + OuterParse.prop)) >> OuterParse.triple2 +*} + +ML {* +fun quotdef (qtystrs, (bind, tystr, mx), (attr, propstr)) lthy = let - val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs + val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) (the qtystrs) val qenv = build_qenv lthy qtys - val qty = Syntax.parse_typ lthy (the tystr) |> Syntax.check_typ lthy + val qty = Option.map (Syntax.check_typ lthy o Syntax.parse_typ lthy) tystr val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy - val (lhs, rhs) = Logic.dest_equals prop in - make_const_def bind rhs mx qenv lthy |> snd + quotdef_cmd qenv ((bind, qty, mx), (attr, prop)) lthy |> snd end *} ML {* val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" - OuterKeyword.thy_decl (qd_parser >> parse_qd_spec) + OuterKeyword.thy_decl (quotdef_parser >> quotdef) *} -(* ML {* show_all_types := true *} *) - section {* ATOMIZE *} text {* diff -r 5f3b364d4765 -r c18308f60f0e quotient.ML --- a/quotient.ML Tue Nov 03 14:04:21 2009 +0100 +++ b/quotient.ML Tue Nov 03 14:04:45 2009 +0100 @@ -1,112 +1,14 @@ signature QUOTIENT = sig - type maps_info = {mapfun: string, relfun: string} - type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory val note: binding * thm -> local_theory -> thm * local_theory - val maps_lookup: theory -> string -> maps_info option - val maps_update_thy: string -> maps_info -> theory -> theory - val maps_update: string -> maps_info -> Proof.context -> Proof.context - val print_quotdata: Proof.context -> unit - val quotdata_lookup_thy: theory -> quotient_info list - val quotdata_lookup: Proof.context -> quotient_info list - val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory - val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context end; structure Quotient: QUOTIENT = struct -(* data containers *) -(*******************) - -(* info about map- and rel-functions *) -type maps_info = {mapfun: string, relfun: string} - -structure MapsData = TheoryDataFun - (type T = maps_info Symtab.table - val empty = Symtab.empty - val copy = I - val extend = I - fun merge _ = Symtab.merge (K true)) - -val maps_lookup = Symtab.lookup o MapsData.get - - -fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) -fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) - -fun maps_attribute_aux s minfo = Thm.declaration_attribute - (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) - -(* attribute to be used in declare statements *) -fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = -let - val thy = ProofContext.theory_of ctxt - val tyname = Sign.intern_type thy tystr - val mapname = Sign.intern_const thy mapstr - val relname = Sign.intern_const thy relstr -in - maps_attribute_aux tyname {mapfun = mapname, relfun = relname} -end - -val maps_attr_parser = - Args.context -- Scan.lift - ((Args.name --| OuterParse.$$$ "=") -- - (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- - Args.name --| OuterParse.$$$ ")")) - -val _ = Context.>> (Context.map_theory - (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) - "declaration of map information")) - - -(* info about the quotient types *) -type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} - -structure QuotData = TheoryDataFun - (type T = quotient_info list - val empty = [] - val copy = I - val extend = I - fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) - -val quotdata_lookup_thy = QuotData.get -val quotdata_lookup = QuotData.get o ProofContext.theory_of - -fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = - QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy - -fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = - ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt - -fun print_quotdata ctxt = -let - fun prt_quot {qtyp, rtyp, 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, - Pretty.str ("equiv. thm:"), - Syntax.pretty_term ctxt (prop_of equiv_thm)]) -in - QuotData.get (ProofContext.theory_of ctxt) - |> map prt_quot - |> Pretty.big_list "quotients:" - |> Pretty.writeln -end - -val _ = - OuterSyntax.improper_command "print_quotients" "print out all quotients" - OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) - - - (* wrappers for define, note and theorem_i *) fun define (name, mx, rhs) lthy = let diff -r 5f3b364d4765 -r c18308f60f0e quotient_info.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/quotient_info.ML Tue Nov 03 14:04:45 2009 +0100 @@ -0,0 +1,107 @@ +signature QUOTIENT_INFO = +sig + type maps_info = {mapfun: string, relfun: string} + val maps_lookup: theory -> string -> maps_info option + val maps_update_thy: string -> maps_info -> theory -> theory + val maps_update: string -> maps_info -> Proof.context -> Proof.context + + type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} + val print_quotdata: Proof.context -> unit + val quotdata_lookup_thy: theory -> quotient_info list + val quotdata_lookup: Proof.context -> quotient_info list + val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory + val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context +end; + +structure Quotient_Info: QUOTIENT_INFO = +struct + +(* data containers *) +(*******************) + +(* info about map- and rel-functions *) +type maps_info = {mapfun: string, relfun: string} + +structure MapsData = TheoryDataFun + (type T = maps_info Symtab.table + val empty = Symtab.empty + val copy = I + val extend = I + fun merge _ = Symtab.merge (K true)) + +val maps_lookup = Symtab.lookup o MapsData.get + + +fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo)) +fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo) + +fun maps_attribute_aux s minfo = Thm.declaration_attribute + (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo)) + +(* attribute to be used in declare statements *) +fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = +let + val thy = ProofContext.theory_of ctxt + val tyname = Sign.intern_type thy tystr + val mapname = Sign.intern_const thy mapstr + val relname = Sign.intern_const thy relstr +in + maps_attribute_aux tyname {mapfun = mapname, relfun = relname} +end + +val maps_attr_parser = + Args.context -- Scan.lift + ((Args.name --| OuterParse.$$$ "=") -- + (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- + Args.name --| OuterParse.$$$ ")")) + +val _ = Context.>> (Context.map_theory + (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) + "declaration of map information")) + + +(* info about the quotient types *) +type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm} + +structure QuotData = TheoryDataFun + (type T = quotient_info list + val empty = [] + val copy = I + val extend = I + fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) + +val quotdata_lookup_thy = QuotData.get +val quotdata_lookup = QuotData.get o ProofContext.theory_of + +fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = + QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy + +fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = + ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt + +fun print_quotdata ctxt = +let + fun prt_quot {qtyp, rtyp, 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, + Pretty.str ("equiv. thm:"), + Syntax.pretty_term ctxt (prop_of equiv_thm)]) +in + QuotData.get (ProofContext.theory_of ctxt) + |> map prt_quot + |> Pretty.big_list "quotients:" + |> Pretty.writeln +end + +val _ = + OuterSyntax.improper_command "print_quotients" "print out all quotients" + OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) + +end; (* structure *) + +open Quotient_Info \ No newline at end of file