# 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