# HG changeset patch # User Christian Urban # Date 1256510681 -3600 # Node ID 929bc55efff709eb3b93dca199ed82ffddfdeaa0 # Parent f3c192574d2a5334981933be2e74dcb971706317 added code for declaring map-functions diff -r f3c192574d2a -r 929bc55efff7 QuotMain.thy --- a/QuotMain.thy Sun Oct 25 01:31:04 2009 +0200 +++ b/QuotMain.thy Sun Oct 25 23:44:41 2009 +0100 @@ -3,17 +3,6 @@ uses ("quotient.ML") begin -definition - EQ_TRUE -where - "EQ_TRUE X \ (X = True)" - -lemma test: "EQ_TRUE ?X" - unfolding EQ_TRUE_def - by (rule refl) - -thm test - locale QUOT_TYPE = fixes R :: "'a \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" @@ -155,14 +144,17 @@ section {* type definition for the quotient type *} +ML {* Toplevel.theory *} + use "quotient.ML" -(* mapfuns for some standard types *) -setup {* - maps_update @{type_name "list"} {mapfun = @{const_name "map"}, relfun = @{const_name "LIST_REL"}} #> - maps_update @{type_name "*"} {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #> - maps_update @{type_name "fun"} {mapfun = @{const_name "fun_map"}, relfun = @{const_name "FUN_REL"}} -*} +declare [[map list = (map, LIST_REL)]] +declare [[map * = (prod_fun, prod_rel)]] +declare [[map "fun" = (fun_map, FUN_REL)]] + +ML {* maps_lookup @{theory} "List.list" *} +ML {* maps_lookup @{theory} "*" *} +ML {* maps_lookup @{theory} "fun" *} ML {* val no_vars = Thm.rule_attribute (fn context => fn th => @@ -175,6 +167,10 @@ section {* lifting of constants *} ML {* + +*} + +ML {* (* calculates the aggregate abs and rep functions for a given type; repF is for constants' arguments; absF is for constants; function types need to be treated specially, since repF and absF diff -r f3c192574d2a -r 929bc55efff7 QuotTest.thy --- a/QuotTest.thy Sun Oct 25 01:31:04 2009 +0200 +++ b/QuotTest.thy Sun Oct 25 23:44:41 2009 +0100 @@ -13,13 +13,13 @@ where r_eq: "EQUIV RR" -ML {* print_quotdata @{context} *} +print_quotients quotient qtrm = trm / "RR" apply(rule r_eq) done -ML {* print_quotdata @{context} *} +print_quotients typ qtrm term Rep_qtrm @@ -51,6 +51,7 @@ apply(rule r_eq') done +print_quotients print_theorems term ABS_qtrm' @@ -72,6 +73,13 @@ quotient qt = "t" / "Rt" by (rule t_eq) +print_quotients + +ML {* +Toplevel.context_of; +Toplevel.keep +*} + ML {* get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \ qt) \ qt) \ qt) list) * nat"} |> fst @@ -130,6 +138,7 @@ apply(rule t_eq') done +print_quotients print_theorems local_setup {* diff -r f3c192574d2a -r 929bc55efff7 quotient.ML --- a/quotient.ML Sun Oct 25 01:31:04 2009 +0200 +++ b/quotient.ML Sun Oct 25 23:44:41 2009 +0100 @@ -7,7 +7,8 @@ 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: string -> maps_info -> theory -> theory + 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: theory -> quotient_info list val quotdata_update_thy: (typ * typ * term) -> theory -> theory @@ -31,7 +32,32 @@ fun merge _ = Symtab.merge (K true)) val maps_lookup = Symtab.lookup o MapsData.get -fun maps_update k v = MapsData.map (Symtab.update (k, v)) +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 *) @@ -42,31 +68,35 @@ val empty = [] val copy = I val extend = I - fun merge _ = (op @)) + fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *) val quotdata_lookup = QuotData.get -fun quotdata_update_thy (qty, rty, rel) = - QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) +fun quotdata_update_thy (qty, rty, rel) thy = + QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) thy -fun quotdata_update (qty, rty, rel) = - ProofContext.theory (quotdata_update_thy (qty, rty, rel)) +fun quotdata_update (qty, rty, rel) ctxt = + ProofContext.theory (quotdata_update_thy (qty, rty, rel)) ctxt fun print_quotdata ctxt = let - val quots = QuotData.get (ProofContext.theory_of ctxt) fun prt_quot {qtyp, rtyp, rel} = - Pretty.block [Pretty.str ("quotient:"), - Pretty.brk 2, Syntax.pretty_typ ctxt qtyp, - Pretty.brk 2, Syntax.pretty_typ ctxt rtyp, - Pretty.brk 2, Syntax.pretty_term ctxt rel] + 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]) in - [Pretty.big_list "quotients:" (map prt_quot quots)] - |> Pretty.chunks |> Pretty.writeln + QuotData.get (ProofContext.theory_of ctxt) + |> map prt_quot + |> Pretty.big_list "quotients:" + |> Pretty.writeln end val _ = - OuterSyntax.improper_command "print_quotients" "print quotient types of this theory" + OuterSyntax.improper_command "print_quotients" "print out all quotients" OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of))) @@ -200,7 +230,6 @@ val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name - (* storing the quot-info *) val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2 @@ -248,14 +277,14 @@ fun mk_quotient_type quot_list lthy = let - fun get_goal (rty, rel) = + fun mk_goal (rty, rel) = let val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} in (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), []) end - val goals = map (get_goal o snd) quot_list + val goals = map (mk_goal o snd) quot_list fun after_qed thms lthy = fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd