--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/quotient.ML Mon Dec 07 14:12:29 2009 +0100
@@ -0,0 +1,253 @@
+signature QUOTIENT =
+sig
+ exception LIFT_MATCH of string
+
+ val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
+ val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
+
+end;
+
+structure Quotient: QUOTIENT =
+struct
+
+exception LIFT_MATCH of string
+
+(* wrappers for define, note and theorem_i *)
+fun define (name, mx, rhs) lthy =
+let
+ val ((rhs, (_ , thm)), lthy') =
+ Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
+in
+ ((rhs, thm), lthy')
+end
+
+fun note (name, thm, attrs) lthy =
+let
+ val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
+in
+ (thm', lthy')
+end
+
+fun internal_attr at = Attrib.internal (K at)
+
+fun theorem after_qed goals ctxt =
+let
+ val goals' = map (rpair []) goals
+ fun after_qed' thms = after_qed (the_single thms)
+in
+ Proof.theorem_i NONE after_qed' [goals'] ctxt
+end
+
+
+(* definition of quotient types *)
+(********************************)
+
+(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
+fun typedef_term rel rty lthy =
+let
+ val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)]
+ |> Variable.variant_frees lthy [rel]
+ |> map Free
+in
+ lambda c
+ (HOLogic.exists_const rty $
+ lambda x (HOLogic.mk_eq (c, (rel $ x))))
+end
+
+(* makes the new type definitions and proves non-emptyness*)
+fun typedef_make (qty_name, mx, rel, rty) lthy =
+let
+ val typedef_tac =
+ EVERY1 [rewrite_goal_tac @{thms mem_def},
+ rtac @{thm exI},
+ rtac @{thm exI},
+ rtac @{thm refl}]
+ val tfrees = map fst (Term.add_tfreesT rty [])
+in
+ Local_Theory.theory_result
+ (Typedef.add_typedef false NONE
+ (qty_name, tfrees, mx)
+ (typedef_term rel rty lthy)
+ NONE typedef_tac) lthy
+end
+
+(* tactic to prove the QUOT_TYPE theorem for the new type *)
+fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
+let
+ val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}]
+ val rep_thm = #Rep typedef_info |> unfold_mem
+ val rep_inv = #Rep_inverse typedef_info
+ val abs_inv = #Abs_inverse typedef_info |> unfold_mem
+ val rep_inj = #Rep_inject typedef_info
+in
+ EVERY1 [rtac @{thm QUOT_TYPE.intro},
+ rtac equiv_thm,
+ rtac rep_thm,
+ rtac rep_inv,
+ rtac abs_inv,
+ rtac @{thm exI},
+ rtac @{thm refl},
+ rtac rep_inj]
+end
+
+(* proves the QUOT_TYPE theorem *)
+fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
+let
+ val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
+ val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
+ |> Syntax.check_term lthy
+in
+ Goal.prove lthy [] [] goal
+ (K (typedef_quot_type_tac equiv_thm typedef_info))
+end
+
+(* proves the quotient theorem *)
+fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
+let
+ val quotient_const = Const (@{const_name "Quotient"}, dummyT)
+ val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
+ |> Syntax.check_term lthy
+
+ val typedef_quotient_thm_tac =
+ EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
+ rtac @{thm QUOT_TYPE.Quotient},
+ rtac quot_type_thm]
+in
+ Goal.prove lthy [] [] goal
+ (K typedef_quotient_thm_tac)
+end
+
+(* main function for constructing the quotient type *)
+fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy =
+let
+ (* generates typedef *)
+ val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
+
+ (* abs and rep functions *)
+ val abs_ty = #abs_type typedef_info
+ val rep_ty = #rep_type typedef_info
+ val abs_name = #Abs_name typedef_info
+ val rep_name = #Rep_name typedef_info
+ val abs = Const (abs_name, rep_ty --> abs_ty)
+ val rep = Const (rep_name, abs_ty --> rep_ty)
+
+ (* ABS and REP definitions *)
+ val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
+ val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
+ val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs)
+ val REP_trm = Syntax.check_term lthy1 (REP_const $ rep)
+ val ABS_name = Binding.prefix_name "ABS_" qty_name
+ val REP_name = Binding.prefix_name "REP_" qty_name
+ val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
+ lthy1 |> define (ABS_name, NoSyn, ABS_trm)
+ ||>> define (REP_name, NoSyn, REP_trm)
+
+ (* quot_type theorem *)
+ val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2
+ val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
+
+ (* quotient theorem *)
+ 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 qty_str = fst (Term.dest_Type abs_ty)
+ val lthy3 = quotdata_update qty_str
+ (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
+ (* FIXME: varifyT should not be used *)
+ (* FIXME: the relation needs to be a string, since its type needs *)
+ (* FIXME: to recalculated in for example REGULARIZE *)
+
+ (* storing of the equiv_thm under a name *)
+ val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm,
+ [internal_attr equiv_rules_add]) lthy3
+
+ (* interpretation *)
+ val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
+ val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;
+ val eqn1i = Thm.prop_of (symmetric eqn1pre)
+ val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;
+ val eqn2i = Thm.prop_of (symmetric eqn2pre)
+
+ val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));
+ val exp_term = Morphism.term exp_morphism;
+ val exp = Morphism.thm exp_morphism;
+
+ val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
+ ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
+ val mthdt = Method.Basic (fn _ => mthd)
+ val bymt = Proof.global_terminal_proof (mthdt, NONE)
+ val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
+ Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
+in
+ lthy6
+ |> note (quot_thm_name, quot_thm, [])
+ ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add])
+ ||> Local_Theory.theory (fn thy =>
+ let
+ val global_eqns = map exp_term [eqn2i, eqn1i];
+ (* Not sure if the following context should not be used *)
+ val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
+ val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
+ in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
+end
+
+
+
+
+(* interface and syntax setup *)
+
+(* the ML-interface takes a list of 4-tuples consisting of *)
+(* *)
+(* - the name of the quotient type *)
+(* - its mixfix annotation *)
+(* - the type to be quotient *)
+(* - the relation according to which the type is quotient *)
+
+fun quotient_type quot_list lthy =
+let
+ fun mk_goal (rty, rel) =
+ let
+ val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+ in
+ HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
+ end
+
+ val goals = map (mk_goal o snd) quot_list
+
+ fun after_qed thms lthy =
+ fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
+in
+ theorem after_qed goals lthy
+end
+
+fun quotient_type_cmd spec lthy =
+let
+ fun parse_spec (((qty_str, mx), rty_str), rel_str) =
+ let
+ val qty_name = Binding.name qty_str
+ val rty = Syntax.read_typ lthy rty_str
+ val rel = Syntax.read_term lthy rel_str
+ in
+ ((qty_name, mx), (rty, rel))
+ end
+in
+ quotient_type (map parse_spec spec) lthy
+end
+
+val quotspec_parser =
+ OuterParse.and_list1
+ (OuterParse.short_ident -- OuterParse.opt_infix --
+ (OuterParse.$$$ "=" |-- OuterParse.typ) --
+ (OuterParse.$$$ "/" |-- OuterParse.term))
+
+val _ = OuterKeyword.keyword "/"
+
+val _ =
+ OuterSyntax.local_theory_to_proof "quotient"
+ "quotient type definitions (requires equivalence proofs)"
+ OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+
+end; (* structure *)
+
+open Quotient
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/quotient_def.ML Mon Dec 07 14:12:29 2009 +0100
@@ -0,0 +1,140 @@
+
+signature QUOTIENT_DEF =
+sig
+ datatype flag = absF | repF
+ val get_fun: flag -> Proof.context -> typ * typ -> term
+ val make_def: binding -> typ -> mixfix -> Attrib.binding -> term ->
+ Proof.context -> (term * thm) * local_theory
+
+ val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) ->
+ local_theory -> (term * thm) * local_theory
+ val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
+ local_theory -> local_theory
+end;
+
+structure Quotient_Def: QUOTIENT_DEF =
+struct
+
+(* wrapper for define *)
+fun define name mx attr rhs lthy =
+let
+ val ((rhs, (_ , thm)), lthy') =
+ Local_Theory.define ((name, mx), (attr, rhs)) lthy
+in
+ ((rhs, thm), lthy')
+end
+
+datatype flag = absF | repF
+
+fun negF absF = repF
+ | negF repF = absF
+
+fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
+
+fun get_fun_aux lthy s fs =
+ case (maps_lookup (ProofContext.theory_of lthy) s) of
+ SOME info => list_comb (Const (#mapfun info, dummyT), fs)
+ | NONE => raise
+ (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))
+
+fun get_const flag lthy _ qty =
+(* FIXME: check here that _ and qty are related *)
+let
+ val thy = ProofContext.theory_of lthy
+ val qty_name = Long_Name.base_name (fst (dest_Type qty))
+in
+ case flag of
+ absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
+ | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
+end
+
+
+(* 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
+ change *)
+
+fun get_fun flag lthy (rty, qty) =
+ if rty = qty then mk_identity qty else
+ case (rty, qty) of
+ (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
+ let
+ val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
+ val fs_ty2 = get_fun flag lthy (ty2, ty2')
+ in
+ get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
+ end
+ | (Type (s, []), Type (s', [])) =>
+ if s = s'
+ then mk_identity qty
+ else get_const flag lthy rty qty
+ | (Type (s, tys), Type (s', tys')) =>
+ if s = s'
+ then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys'))
+ else get_const flag lthy rty qty
+ | (TFree x, TFree x') =>
+ if x = x'
+ then mk_identity qty
+ else raise (LIFT_MATCH "get_fun")
+ | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
+ | _ => raise (LIFT_MATCH "get_fun")
+
+fun make_def qconst_bname qty mx attr rhs lthy =
+let
+ val absrep_trm = get_fun absF lthy (fastype_of rhs, qty) $ rhs
+ |> Syntax.check_term lthy
+
+ val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
+
+ fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
+ val lthy'' = Local_Theory.declaration true
+ (fn phi =>
+ let
+ val qconst_str = fst (Term.dest_Const (Morphism.term phi trm))
+ in
+ qconsts_update_gen qconst_str (qcinfo phi)
+ end) lthy'
+in
+ ((trm, thm), lthy'')
+end
+
+(* interface and syntax setup *)
+
+(* the ML-interface takes a 5-tuple consisting of *)
+(* *)
+(* - the name of the constant to be lifted *)
+(* - its type *)
+(* - its mixfix annotation *)
+(* - a meta-equation defining the constant, *)
+(* and the attributes of for this meta-equality *)
+
+fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
+let
+ val (_, prop') = LocalDefs.cert_def lthy prop
+ val (_, rhs) = Primitive_Defs.abs_def prop'
+in
+ make_def bind qty mx attr rhs lthy
+end
+
+fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy =
+let
+ val qty = Syntax.read_typ lthy qtystr
+ val prop = Syntax.read_prop lthy propstr
+in
+ quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
+end
+
+val quotdef_parser =
+ (OuterParse.binding --
+ (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ --
+ OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
+ (SpecParse.opt_thm_name ":" -- OuterParse.prop)
+
+val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
+ OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
+
+end; (* structure *)
+
+open Quotient_Def;
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/quotient_info.ML Mon Dec 07 14:12:29 2009 +0100
@@ -0,0 +1,204 @@
+signature QUOTIENT_INFO =
+sig
+ exception NotFound
+
+ 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_quotinfo: Proof.context -> unit
+ val quotdata_lookup_thy: theory -> string -> quotient_info option
+ val quotdata_lookup: Proof.context -> string -> quotient_info option
+ 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
+
+ type qconsts_info = {qconst: term, rconst: term, def: thm}
+ val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
+ val qconsts_lookup: theory -> string -> qconsts_info
+ 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
+ val print_qconstinfo: Proof.context -> unit
+
+ val equiv_rules_get: Proof.context -> thm list
+ val equiv_rules_add: attribute
+ val rsp_rules_get: Proof.context -> thm list
+ val quotient_rules_get: Proof.context -> thm list
+ val quotient_rules_add: attribute
+end;
+
+structure Quotient_Info: QUOTIENT_INFO =
+struct
+
+exception NotFound
+
+(* data containers *)
+(*******************)
+
+(* info about map- and rel-functions *)
+type maps_info = {mapfun: string, relfun: string}
+
+structure MapsData = Theory_Data
+ (type T = maps_info Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ val 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 quotient types *)
+type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
+
+structure QuotData = Theory_Data
+ (type T = quotient_info Symtab.table
+ val empty = Symtab.empty
+ 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)
+
+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 qty_name (qty, rty, rel, equiv_thm) =
+ ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
+
+fun quotdata_dest thy =
+ map snd (Symtab.dest (QuotData.get thy))
+
+fun print_quotinfo 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)
+ |> Symtab.dest
+ |> map (prt_quot o snd)
+ |> Pretty.big_list "quotients:"
+ |> Pretty.writeln
+end
+
+val _ =
+ OuterSyntax.improper_command "print_quotients" "print out all quotients"
+ OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
+
+
+(* info about quotient constants *)
+type qconsts_info = {qconst: term, rconst: term, def: thm}
+
+structure QConstsData = Theory_Data
+ (type T = qconsts_info Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ val merge = Symtab.merge (K true))
+
+fun qconsts_transfer phi {qconst, rconst, def} =
+ {qconst = Morphism.term phi qconst,
+ rconst = Morphism.term phi rconst,
+ def = Morphism.thm phi def}
+
+fun qconsts_lookup thy str =
+ case Symtab.lookup (QConstsData.get thy) str of
+ SOME info => info
+ | NONE => raise NotFound
+
+fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
+fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
+
+fun qconsts_dest thy =
+ map snd (Symtab.dest (QConstsData.get thy))
+
+(* We don't print the definition *)
+fun print_qconstinfo ctxt =
+let
+ fun prt_qconst {qconst, rconst, def} =
+ Pretty.block (separate (Pretty.brk 1)
+ [Syntax.pretty_term ctxt qconst,
+ Pretty.str ":=",
+ Syntax.pretty_term ctxt rconst])
+in
+ QConstsData.get (ProofContext.theory_of ctxt)
+ |> Symtab.dest
+ |> map (prt_qconst o snd)
+ |> Pretty.big_list "quotient constants:"
+ |> Pretty.writeln
+end
+
+val _ =
+ OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants"
+ OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
+
+(* equivalence relation theorems *)
+structure EquivRules = Named_Thms
+ (val name = "quotient_equiv"
+ val description = "Equivalence relation theorems.")
+
+val equiv_rules_get = EquivRules.get
+val equiv_rules_add = EquivRules.add
+
+(* respectfulness theorems *)
+structure RspRules = Named_Thms
+ (val name = "quotient_rsp"
+ val description = "Respectfulness theorems.")
+
+val rsp_rules_get = RspRules.get
+
+(* quotient theorems *)
+structure QuotientRules = Named_Thms
+ (val name = "quotient_thm"
+ val description = "Quotient theorems.")
+
+val quotient_rules_get = QuotientRules.get
+val quotient_rules_add = QuotientRules.add
+
+(* setup of the theorem lists *)
+val _ = Context.>> (Context.map_theory
+ (EquivRules.setup #>
+ RspRules.setup #>
+ QuotientRules.setup))
+
+end; (* structure *)
+
+open Quotient_Info
--- a/quotient.ML Mon Dec 07 14:09:50 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,253 +0,0 @@
-signature QUOTIENT =
-sig
- exception LIFT_MATCH of string
-
- val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
- val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
-
-end;
-
-structure Quotient: QUOTIENT =
-struct
-
-exception LIFT_MATCH of string
-
-(* wrappers for define, note and theorem_i *)
-fun define (name, mx, rhs) lthy =
-let
- val ((rhs, (_ , thm)), lthy') =
- Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
-in
- ((rhs, thm), lthy')
-end
-
-fun note (name, thm, attrs) lthy =
-let
- val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
-in
- (thm', lthy')
-end
-
-fun internal_attr at = Attrib.internal (K at)
-
-fun theorem after_qed goals ctxt =
-let
- val goals' = map (rpair []) goals
- fun after_qed' thms = after_qed (the_single thms)
-in
- Proof.theorem_i NONE after_qed' [goals'] ctxt
-end
-
-
-(* definition of quotient types *)
-(********************************)
-
-(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
-fun typedef_term rel rty lthy =
-let
- val [x, c] = [("x", rty), ("c", HOLogic.mk_setT rty)]
- |> Variable.variant_frees lthy [rel]
- |> map Free
-in
- lambda c
- (HOLogic.exists_const rty $
- lambda x (HOLogic.mk_eq (c, (rel $ x))))
-end
-
-(* makes the new type definitions and proves non-emptyness*)
-fun typedef_make (qty_name, mx, rel, rty) lthy =
-let
- val typedef_tac =
- EVERY1 [rewrite_goal_tac @{thms mem_def},
- rtac @{thm exI},
- rtac @{thm exI},
- rtac @{thm refl}]
- val tfrees = map fst (Term.add_tfreesT rty [])
-in
- Local_Theory.theory_result
- (Typedef.add_typedef false NONE
- (qty_name, tfrees, mx)
- (typedef_term rel rty lthy)
- NONE typedef_tac) lthy
-end
-
-(* tactic to prove the QUOT_TYPE theorem for the new type *)
-fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) =
-let
- val unfold_mem = MetaSimplifier.rewrite_rule [@{thm mem_def}]
- val rep_thm = #Rep typedef_info |> unfold_mem
- val rep_inv = #Rep_inverse typedef_info
- val abs_inv = #Abs_inverse typedef_info |> unfold_mem
- val rep_inj = #Rep_inject typedef_info
-in
- EVERY1 [rtac @{thm QUOT_TYPE.intro},
- rtac equiv_thm,
- rtac rep_thm,
- rtac rep_inv,
- rtac abs_inv,
- rtac @{thm exI},
- rtac @{thm refl},
- rtac rep_inj]
-end
-
-(* proves the QUOT_TYPE theorem *)
-fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
-let
- val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
- val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
- |> Syntax.check_term lthy
-in
- Goal.prove lthy [] [] goal
- (K (typedef_quot_type_tac equiv_thm typedef_info))
-end
-
-(* proves the quotient theorem *)
-fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy =
-let
- val quotient_const = Const (@{const_name "Quotient"}, dummyT)
- val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep)
- |> Syntax.check_term lthy
-
- val typedef_quotient_thm_tac =
- EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]),
- rtac @{thm QUOT_TYPE.Quotient},
- rtac quot_type_thm]
-in
- Goal.prove lthy [] [] goal
- (K typedef_quotient_thm_tac)
-end
-
-(* main function for constructing the quotient type *)
-fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy =
-let
- (* generates typedef *)
- val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
-
- (* abs and rep functions *)
- val abs_ty = #abs_type typedef_info
- val rep_ty = #rep_type typedef_info
- val abs_name = #Abs_name typedef_info
- val rep_name = #Rep_name typedef_info
- val abs = Const (abs_name, rep_ty --> abs_ty)
- val rep = Const (rep_name, abs_ty --> rep_ty)
-
- (* ABS and REP definitions *)
- val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
- val REP_const = Const (@{const_name "QUOT_TYPE.REP"}, dummyT )
- val ABS_trm = Syntax.check_term lthy1 (ABS_const $ rel $ abs)
- val REP_trm = Syntax.check_term lthy1 (REP_const $ rep)
- val ABS_name = Binding.prefix_name "ABS_" qty_name
- val REP_name = Binding.prefix_name "REP_" qty_name
- val (((ABS, ABS_def), (REP, REP_def)), lthy2) =
- lthy1 |> define (ABS_name, NoSyn, ABS_trm)
- ||>> define (REP_name, NoSyn, REP_trm)
-
- (* quot_type theorem *)
- val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy2
- val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
-
- (* quotient theorem *)
- 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 qty_str = fst (Term.dest_Type abs_ty)
- val lthy3 = quotdata_update qty_str
- (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
- (* FIXME: varifyT should not be used *)
- (* FIXME: the relation needs to be a string, since its type needs *)
- (* FIXME: to recalculated in for example REGULARIZE *)
-
- (* storing of the equiv_thm under a name *)
- val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm,
- [internal_attr equiv_rules_add]) lthy3
-
- (* interpretation *)
- val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
- val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;
- val eqn1i = Thm.prop_of (symmetric eqn1pre)
- val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;
- val eqn2i = Thm.prop_of (symmetric eqn2pre)
-
- val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));
- val exp_term = Morphism.term exp_morphism;
- val exp = Morphism.thm exp_morphism;
-
- val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
- ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
- val mthdt = Method.Basic (fn _ => mthd)
- val bymt = Proof.global_terminal_proof (mthdt, NONE)
- val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
- Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
-in
- lthy6
- |> note (quot_thm_name, quot_thm, [])
- ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add])
- ||> Local_Theory.theory (fn thy =>
- let
- val global_eqns = map exp_term [eqn2i, eqn1i];
- (* Not sure if the following context should not be used *)
- val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
- val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
- in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
-end
-
-
-
-
-(* interface and syntax setup *)
-
-(* the ML-interface takes a list of 4-tuples consisting of *)
-(* *)
-(* - the name of the quotient type *)
-(* - its mixfix annotation *)
-(* - the type to be quotient *)
-(* - the relation according to which the type is quotient *)
-
-fun quotient_type quot_list lthy =
-let
- fun mk_goal (rty, rel) =
- let
- val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
- in
- HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
- end
-
- val goals = map (mk_goal o snd) quot_list
-
- fun after_qed thms lthy =
- fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
-in
- theorem after_qed goals lthy
-end
-
-fun quotient_type_cmd spec lthy =
-let
- fun parse_spec (((qty_str, mx), rty_str), rel_str) =
- let
- val qty_name = Binding.name qty_str
- val rty = Syntax.read_typ lthy rty_str
- val rel = Syntax.read_term lthy rel_str
- in
- ((qty_name, mx), (rty, rel))
- end
-in
- quotient_type (map parse_spec spec) lthy
-end
-
-val quotspec_parser =
- OuterParse.and_list1
- (OuterParse.short_ident -- OuterParse.opt_infix --
- (OuterParse.$$$ "=" |-- OuterParse.typ) --
- (OuterParse.$$$ "/" |-- OuterParse.term))
-
-val _ = OuterKeyword.keyword "/"
-
-val _ =
- OuterSyntax.local_theory_to_proof "quotient"
- "quotient type definitions (requires equivalence proofs)"
- OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
-
-end; (* structure *)
-
-open Quotient
--- a/quotient_def.ML Mon Dec 07 14:09:50 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,140 +0,0 @@
-
-signature QUOTIENT_DEF =
-sig
- datatype flag = absF | repF
- val get_fun: flag -> Proof.context -> typ * typ -> term
- val make_def: binding -> typ -> mixfix -> Attrib.binding -> term ->
- Proof.context -> (term * thm) * local_theory
-
- val quotdef: (binding * typ * mixfix) * (Attrib.binding * term) ->
- local_theory -> (term * thm) * local_theory
- val quotdef_cmd: (binding * string * mixfix) * (Attrib.binding * string) ->
- local_theory -> local_theory
-end;
-
-structure Quotient_Def: QUOTIENT_DEF =
-struct
-
-(* wrapper for define *)
-fun define name mx attr rhs lthy =
-let
- val ((rhs, (_ , thm)), lthy') =
- Local_Theory.define ((name, mx), (attr, rhs)) lthy
-in
- ((rhs, thm), lthy')
-end
-
-datatype flag = absF | repF
-
-fun negF absF = repF
- | negF repF = absF
-
-fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
-
-fun get_fun_aux lthy s fs =
- case (maps_lookup (ProofContext.theory_of lthy) s) of
- SOME info => list_comb (Const (#mapfun info, dummyT), fs)
- | NONE => raise
- (LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]))
-
-fun get_const flag lthy _ qty =
-(* FIXME: check here that _ and qty are related *)
-let
- val thy = ProofContext.theory_of lthy
- val qty_name = Long_Name.base_name (fst (dest_Type qty))
-in
- case flag of
- absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
- | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
-end
-
-
-(* 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
- change *)
-
-fun get_fun flag lthy (rty, qty) =
- if rty = qty then mk_identity qty else
- case (rty, qty) of
- (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
- let
- val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
- val fs_ty2 = get_fun flag lthy (ty2, ty2')
- in
- get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
- end
- | (Type (s, []), Type (s', [])) =>
- if s = s'
- then mk_identity qty
- else get_const flag lthy rty qty
- | (Type (s, tys), Type (s', tys')) =>
- if s = s'
- then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys'))
- else get_const flag lthy rty qty
- | (TFree x, TFree x') =>
- if x = x'
- then mk_identity qty
- else raise (LIFT_MATCH "get_fun")
- | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun")
- | _ => raise (LIFT_MATCH "get_fun")
-
-fun make_def qconst_bname qty mx attr rhs lthy =
-let
- val absrep_trm = get_fun absF lthy (fastype_of rhs, qty) $ rhs
- |> Syntax.check_term lthy
-
- val ((trm, thm), lthy') = define qconst_bname mx attr absrep_trm lthy
-
- fun qcinfo phi = qconsts_transfer phi {qconst = trm, rconst = rhs, def = thm}
- val lthy'' = Local_Theory.declaration true
- (fn phi =>
- let
- val qconst_str = fst (Term.dest_Const (Morphism.term phi trm))
- in
- qconsts_update_gen qconst_str (qcinfo phi)
- end) lthy'
-in
- ((trm, thm), lthy'')
-end
-
-(* interface and syntax setup *)
-
-(* the ML-interface takes a 5-tuple consisting of *)
-(* *)
-(* - the name of the constant to be lifted *)
-(* - its type *)
-(* - its mixfix annotation *)
-(* - a meta-equation defining the constant, *)
-(* and the attributes of for this meta-equality *)
-
-fun quotdef ((bind, qty, mx), (attr, prop)) lthy =
-let
- val (_, prop') = LocalDefs.cert_def lthy prop
- val (_, rhs) = Primitive_Defs.abs_def prop'
-in
- make_def bind qty mx attr rhs lthy
-end
-
-fun quotdef_cmd ((bind, qtystr, mx), (attr, propstr)) lthy =
-let
- val qty = Syntax.read_typ lthy qtystr
- val prop = Syntax.read_prop lthy propstr
-in
- quotdef ((bind, qty, mx), (attr, prop)) lthy |> snd
-end
-
-val quotdef_parser =
- (OuterParse.binding --
- (OuterParse.$$$ "::" |-- OuterParse.!!! (OuterParse.typ --
- OuterParse.opt_mixfix' --| OuterParse.where_)) >> OuterParse.triple2) --
- (SpecParse.opt_thm_name ":" -- OuterParse.prop)
-
-val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants"
- OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
-
-end; (* structure *)
-
-open Quotient_Def;
-
-
--- a/quotient_info.ML Mon Dec 07 14:09:50 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,204 +0,0 @@
-signature QUOTIENT_INFO =
-sig
- exception NotFound
-
- 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_quotinfo: Proof.context -> unit
- val quotdata_lookup_thy: theory -> string -> quotient_info option
- val quotdata_lookup: Proof.context -> string -> quotient_info option
- 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
-
- type qconsts_info = {qconst: term, rconst: term, def: thm}
- val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
- val qconsts_lookup: theory -> string -> qconsts_info
- 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
- val print_qconstinfo: Proof.context -> unit
-
- val equiv_rules_get: Proof.context -> thm list
- val equiv_rules_add: attribute
- val rsp_rules_get: Proof.context -> thm list
- val quotient_rules_get: Proof.context -> thm list
- val quotient_rules_add: attribute
-end;
-
-structure Quotient_Info: QUOTIENT_INFO =
-struct
-
-exception NotFound
-
-(* data containers *)
-(*******************)
-
-(* info about map- and rel-functions *)
-type maps_info = {mapfun: string, relfun: string}
-
-structure MapsData = Theory_Data
- (type T = maps_info Symtab.table
- val empty = Symtab.empty
- val extend = I
- val 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 quotient types *)
-type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
-
-structure QuotData = Theory_Data
- (type T = quotient_info Symtab.table
- val empty = Symtab.empty
- 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)
-
-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 qty_name (qty, rty, rel, equiv_thm) =
- ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
-
-fun quotdata_dest thy =
- map snd (Symtab.dest (QuotData.get thy))
-
-fun print_quotinfo 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)
- |> Symtab.dest
- |> map (prt_quot o snd)
- |> Pretty.big_list "quotients:"
- |> Pretty.writeln
-end
-
-val _ =
- OuterSyntax.improper_command "print_quotients" "print out all quotients"
- OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
-
-
-(* info about quotient constants *)
-type qconsts_info = {qconst: term, rconst: term, def: thm}
-
-structure QConstsData = Theory_Data
- (type T = qconsts_info Symtab.table
- val empty = Symtab.empty
- val extend = I
- val merge = Symtab.merge (K true))
-
-fun qconsts_transfer phi {qconst, rconst, def} =
- {qconst = Morphism.term phi qconst,
- rconst = Morphism.term phi rconst,
- def = Morphism.thm phi def}
-
-fun qconsts_lookup thy str =
- case Symtab.lookup (QConstsData.get thy) str of
- SOME info => info
- | NONE => raise NotFound
-
-fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
-fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
-
-fun qconsts_dest thy =
- map snd (Symtab.dest (QConstsData.get thy))
-
-(* We don't print the definition *)
-fun print_qconstinfo ctxt =
-let
- fun prt_qconst {qconst, rconst, def} =
- Pretty.block (separate (Pretty.brk 1)
- [Syntax.pretty_term ctxt qconst,
- Pretty.str ":=",
- Syntax.pretty_term ctxt rconst])
-in
- QConstsData.get (ProofContext.theory_of ctxt)
- |> Symtab.dest
- |> map (prt_qconst o snd)
- |> Pretty.big_list "quotient constants:"
- |> Pretty.writeln
-end
-
-val _ =
- OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants"
- OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
-
-(* equivalence relation theorems *)
-structure EquivRules = Named_Thms
- (val name = "quotient_equiv"
- val description = "Equivalence relation theorems.")
-
-val equiv_rules_get = EquivRules.get
-val equiv_rules_add = EquivRules.add
-
-(* respectfulness theorems *)
-structure RspRules = Named_Thms
- (val name = "quotient_rsp"
- val description = "Respectfulness theorems.")
-
-val rsp_rules_get = RspRules.get
-
-(* quotient theorems *)
-structure QuotientRules = Named_Thms
- (val name = "quotient_thm"
- val description = "Quotient theorems.")
-
-val quotient_rules_get = QuotientRules.get
-val quotient_rules_add = QuotientRules.add
-
-(* setup of the theorem lists *)
-val _ = Context.>> (Context.map_theory
- (EquivRules.setup #>
- RspRules.setup #>
- QuotientRules.setup))
-
-end; (* structure *)
-
-open Quotient_Info