# HG changeset patch # User wenzelm # Date 1268955829 -3600 # Node ID 01d7c4ba9050475e32b4047f9b35c2d74271fad3 # Parent a601da1056b3e526b85909ee64afd32969224815 allow sort constraints in HOL/typedef and related HOLCF variants; diff -r a601da1056b3 -r 01d7c4ba9050 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Fri Mar 19 00:42:17 2010 +0100 +++ b/src/HOL/Tools/typedef.ML Fri Mar 19 00:43:49 2010 +0100 @@ -17,13 +17,13 @@ val get_info_global: theory -> string -> info list val interpretation: (string -> theory -> theory) -> theory -> theory val setup: theory -> theory - val add_typedef: bool -> binding option -> binding * string list * mixfix -> + val add_typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory - val add_typedef_global: bool -> binding option -> binding * string list * mixfix -> + val add_typedef_global: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory - val typedef: (bool * binding) * (binding * string list * mixfix) * term * + val typedef: (bool * binding) * (binding * (string * sort) list * mixfix) * term * (binding * binding) option -> local_theory -> Proof.state - val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string * + val typedef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> local_theory -> Proof.state end; @@ -127,7 +127,7 @@ (* prepare_typedef *) -fun prepare_typedef prep_term def_set name (tname, vs, mx) raw_set opt_morphs lthy = +fun prepare_typedef prep_term def_set name (tname, raw_args, mx) raw_set opt_morphs lthy = let val full_name = Local_Theory.full_name lthy name; val bname = Binding.name_of name; @@ -135,7 +135,7 @@ (* rhs *) - val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, map (rpair dummyS) vs, mx); + val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, raw_args, mx); val set = prep_term tmp_lthy raw_set; val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set; @@ -149,7 +149,7 @@ (* lhs *) - val args = map (fn a => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) vs; + val args = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args; val (newT, typedecl_lthy) = lthy |> Typedecl.typedecl (tname, args, mx) ||> Variable.declare_term set; @@ -275,17 +275,18 @@ local -fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) lthy = +fun gen_typedef prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) lthy = let + val args = map (apsnd (prep_constraint lthy)) raw_args; val ((goal, goal_pat, typedef_result), lthy') = - prepare_typedef prep_term def name typ set opt_morphs lthy; + prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy; fun after_qed [[th]] = snd o typedef_result th; in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] lthy' end; in -val typedef = gen_typedef Syntax.check_term; -val typedef_cmd = gen_typedef Syntax.read_term; +val typedef = gen_typedef Syntax.check_term (K I); +val typedef_cmd = gen_typedef Syntax.read_term Typedecl.read_constraint; end; @@ -303,10 +304,10 @@ (Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- + (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)) - >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) => - typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs))); + >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => + typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs))); end; diff -r a601da1056b3 -r 01d7c4ba9050 src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Fri Mar 19 00:42:17 2010 +0100 +++ b/src/HOLCF/Tools/pcpodef.ML Fri Mar 19 00:43:49 2010 +0100 @@ -14,23 +14,27 @@ { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm, Rep_defined: thm, Abs_defined: thm } - val add_podef: bool -> binding option -> binding * string list * mixfix -> + val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> theory -> (Typedef.info * thm) * theory - val add_cpodef: bool -> binding option -> binding * string list * mixfix -> + val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic * tactic -> theory -> (Typedef.info * cpo_info) * theory - val add_pcpodef: bool -> binding option -> binding * string list * mixfix -> + val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic * tactic -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory - val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term + val cpodef_proof: (bool * binding) + * (binding * (string * sort) list * mixfix) * term * (binding * binding) option -> theory -> Proof.state - val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string + val cpodef_proof_cmd: (bool * binding) + * (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> theory -> Proof.state - val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term + val pcpodef_proof: (bool * binding) + * (binding * (string * sort) list * mixfix) * term * (binding * binding) option -> theory -> Proof.state - val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string + val pcpodef_proof_cmd: (bool * binding) + * (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> theory -> Proof.state end; @@ -153,21 +157,23 @@ fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); -fun prepare prep_term name (tname, vs, mx) raw_set opt_morphs thy = +fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy = let val _ = Theory.requires thy "Pcpodef" "pcpodefs"; - val ctxt = ProofContext.init thy; (*rhs*) - val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; + val (_, tmp_lthy) = + thy |> Theory.copy |> Theory_Target.init NONE + |> Typedecl.predeclare_constraints (tname, raw_args, mx); + val set = prep_term tmp_lthy raw_set; + val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set; + val setT = Term.fastype_of set; - val rhs_tfrees = Term.add_tfrees set []; val oldT = HOLogic.dest_setT setT handle TYPE _ => - error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); + error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_lthy setT)); (*lhs*) - val defS = Sign.defaultS thy; - val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; + val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args; val full_tname = Sign.full_name thy tname; val newT = Type (full_tname, map TFree lhs_tfrees); @@ -206,7 +212,7 @@ (prep_term: Proof.context -> 'a -> term) (def: bool) (name: binding) - (typ: binding * string list * mixfix) + (typ: binding * (string * sort) list * mixfix) (raw_set: 'a) (opt_morphs: (binding * binding) option) (thy: theory) @@ -239,7 +245,7 @@ (prep_term: Proof.context -> 'a -> term) (def: bool) (name: binding) - (typ: binding * string list * mixfix) + (typ: binding * (string * sort) list * mixfix) (raw_set: 'a) (opt_morphs: (binding * binding) option) (thy: theory) @@ -306,27 +312,33 @@ local -fun gen_cpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy = +fun gen_cpodef_proof prep_term prep_constraint + ((def, name), (b, raw_args, mx), set, opt_morphs) thy = let + val ctxt = ProofContext.init thy; + val args = map (apsnd (prep_constraint ctxt)) raw_args; val (goal1, goal2, make_result) = - prepare_cpodef prep_term def name typ set opt_morphs thy; + prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy; fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2); - in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end; + in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end; -fun gen_pcpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy = +fun gen_pcpodef_proof prep_term prep_constraint + ((def, name), (b, raw_args, mx), set, opt_morphs) thy = let + val ctxt = ProofContext.init thy; + val args = map (apsnd (prep_constraint ctxt)) raw_args; val (goal1, goal2, make_result) = - prepare_pcpodef prep_term def name typ set opt_morphs thy; + prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy; fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2); - in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end; + in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end; in -fun cpodef_proof x = gen_cpodef_proof Syntax.check_term x; -fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term x; +fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x; +fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x; -fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term x; -fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term x; +fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x; +fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x; end; @@ -340,12 +352,12 @@ Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- + (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); -fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) = +fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) = (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) - ((def, the_default t opt_name), (t, vs, mx), A, morphs); + ((def, the_default t opt_name), (t, args, mx), A, morphs); val _ = OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal diff -r a601da1056b3 -r 01d7c4ba9050 src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Fri Mar 19 00:42:17 2010 +0100 +++ b/src/HOLCF/Tools/repdef.ML Fri Mar 19 00:43:49 2010 +0100 @@ -9,11 +9,11 @@ type rep_info = { emb_def: thm, prj_def: thm, approx_def: thm, REP: thm } - val add_repdef: bool -> binding option -> binding * string list * mixfix -> + val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> theory -> (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory - val repdef_cmd: (bool * binding) * (binding * string list * mixfix) * string + val repdef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> theory -> theory end; @@ -55,25 +55,27 @@ (prep_term: Proof.context -> 'a -> term) (def: bool) (name: binding) - (typ as (tname, vs, mx) : binding * string list * mixfix) + (typ as (tname, raw_args, mx) : binding * (string * sort) list * mixfix) (raw_defl: 'a) (opt_morphs: (binding * binding) option) (thy: theory) : (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory = let val _ = Theory.requires thy "Representable" "repdefs"; - val ctxt = ProofContext.init thy; (*rhs*) - val defl = prep_term (ctxt |> fold declare_type_name vs) raw_defl; + val (_, tmp_lthy) = + thy |> Theory.copy |> Theory_Target.init NONE + |> Typedecl.predeclare_constraints (tname, raw_args, mx); + val defl = prep_term tmp_lthy raw_defl; + val tmp_lthy' = tmp_lthy |> Variable.declare_constraints defl; + val deflT = Term.fastype_of defl; val _ = if deflT = @{typ "udom alg_defl"} then () - else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ ctxt deflT)); - val rhs_tfrees = Term.add_tfrees defl []; + else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT)); (*lhs*) - val defS = Sign.defaultS thy; - val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; + val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args; val lhs_sorts = map snd lhs_tfrees; val full_tname = Sign.full_name thy tname; val newT = Type (full_tname, map TFree lhs_tfrees); @@ -152,8 +154,12 @@ gen_add_repdef Syntax.check_term def name typ defl opt_morphs thy end; -fun repdef_cmd ((def, name), typ, A, morphs) = - snd o gen_add_repdef Syntax.read_term def name typ A morphs; +fun repdef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy = + let + val ctxt = ProofContext.init thy; + val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args; + in snd (gen_add_repdef Syntax.read_term def name (b, args, mx) A morphs thy) end; + (** outer syntax **) @@ -163,11 +169,11 @@ Scan.optional (P.$$$ "(" |-- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) -- - (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- + (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) -- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); -fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = - repdef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs); +fun mk_repdef ((((((def, opt_name), (args, t)), mx), A), morphs)) = + repdef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs); val _ = OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl