--- 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 \<equiv> (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 \<equiv> my_plus x y"
+
+term MPLUS
+thm MPLUS_def
+thm MPLUS_def_raw
+
+
fun
my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
where
--- 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 \<Rightarrow> 'a \<Rightarrow> bool"
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> '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 {*
--- 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
--- /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