# HG changeset patch # User Christian Urban # Date 1260191549 -3600 # Node ID ae254a6d685c1555980db4aad6b260ff893ada8e # Parent 8a1c8dc72b5cfe91950b34ef1cfe31614c6580ae final move diff -r 8a1c8dc72b5c -r ae254a6d685c Quot/quotient.ML --- /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 diff -r 8a1c8dc72b5c -r ae254a6d685c Quot/quotient_def.ML --- /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; + + diff -r 8a1c8dc72b5c -r ae254a6d685c Quot/quotient_info.ML --- /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 diff -r 8a1c8dc72b5c -r ae254a6d685c quotient.ML --- 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 diff -r 8a1c8dc72b5c -r ae254a6d685c quotient_def.ML --- 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; - - diff -r 8a1c8dc72b5c -r ae254a6d685c quotient_info.ML --- 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