allow sort constraints in HOL/typedef and related HOLCF variants;
authorwenzelm
Fri Mar 19 00:43:49 2010 +0100 (2010-03-19)
changeset 3584001d7c4ba9050
parent 35839 a601da1056b3
child 35841 94f901e4969a
allow sort constraints in HOL/typedef and related HOLCF variants;
src/HOL/Tools/typedef.ML
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tools/repdef.ML
     1.1 --- a/src/HOL/Tools/typedef.ML	Fri Mar 19 00:42:17 2010 +0100
     1.2 +++ b/src/HOL/Tools/typedef.ML	Fri Mar 19 00:43:49 2010 +0100
     1.3 @@ -17,13 +17,13 @@
     1.4    val get_info_global: theory -> string -> info list
     1.5    val interpretation: (string -> theory -> theory) -> theory -> theory
     1.6    val setup: theory -> theory
     1.7 -  val add_typedef: bool -> binding option -> binding * string list * mixfix ->
     1.8 +  val add_typedef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     1.9      term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
    1.10 -  val add_typedef_global: bool -> binding option -> binding * string list * mixfix ->
    1.11 +  val add_typedef_global: bool -> binding option -> binding * (string * sort) list * mixfix ->
    1.12      term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
    1.13 -  val typedef: (bool * binding) * (binding * string list * mixfix) * term *
    1.14 +  val typedef: (bool * binding) * (binding * (string * sort) list * mixfix) * term *
    1.15      (binding * binding) option -> local_theory -> Proof.state
    1.16 -  val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string *
    1.17 +  val typedef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string *
    1.18      (binding * binding) option -> local_theory -> Proof.state
    1.19  end;
    1.20  
    1.21 @@ -127,7 +127,7 @@
    1.22  
    1.23  (* prepare_typedef *)
    1.24  
    1.25 -fun prepare_typedef prep_term def_set name (tname, vs, mx) raw_set opt_morphs lthy =
    1.26 +fun prepare_typedef prep_term def_set name (tname, raw_args, mx) raw_set opt_morphs lthy =
    1.27    let
    1.28      val full_name = Local_Theory.full_name lthy name;
    1.29      val bname = Binding.name_of name;
    1.30 @@ -135,7 +135,7 @@
    1.31  
    1.32      (* rhs *)
    1.33  
    1.34 -    val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, map (rpair dummyS) vs, mx);
    1.35 +    val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, raw_args, mx);
    1.36      val set = prep_term tmp_lthy raw_set;
    1.37      val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
    1.38  
    1.39 @@ -149,7 +149,7 @@
    1.40  
    1.41      (* lhs *)
    1.42  
    1.43 -    val args = map (fn a => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) vs;
    1.44 +    val args = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
    1.45      val (newT, typedecl_lthy) = lthy
    1.46        |> Typedecl.typedecl (tname, args, mx)
    1.47        ||> Variable.declare_term set;
    1.48 @@ -275,17 +275,18 @@
    1.49  
    1.50  local
    1.51  
    1.52 -fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) lthy =
    1.53 +fun gen_typedef prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) lthy =
    1.54    let
    1.55 +    val args = map (apsnd (prep_constraint lthy)) raw_args;
    1.56      val ((goal, goal_pat, typedef_result), lthy') =
    1.57 -      prepare_typedef prep_term def name typ set opt_morphs lthy;
    1.58 +      prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
    1.59      fun after_qed [[th]] = snd o typedef_result th;
    1.60    in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] lthy' end;
    1.61  
    1.62  in
    1.63  
    1.64 -val typedef = gen_typedef Syntax.check_term;
    1.65 -val typedef_cmd = gen_typedef Syntax.read_term;
    1.66 +val typedef = gen_typedef Syntax.check_term (K I);
    1.67 +val typedef_cmd = gen_typedef Syntax.read_term Typedecl.read_constraint;
    1.68  
    1.69  end;
    1.70  
    1.71 @@ -303,10 +304,10 @@
    1.72      (Scan.optional (P.$$$ "(" |--
    1.73          ((P.$$$ "open" >> K false) -- Scan.option P.binding ||
    1.74            P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
    1.75 -      (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
    1.76 +      (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
    1.77        Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
    1.78 -    >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) =>
    1.79 -        typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs)));
    1.80 +    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
    1.81 +        typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
    1.82  
    1.83  end;
    1.84  
     2.1 --- a/src/HOLCF/Tools/pcpodef.ML	Fri Mar 19 00:42:17 2010 +0100
     2.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Fri Mar 19 00:43:49 2010 +0100
     2.3 @@ -14,23 +14,27 @@
     2.4      { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
     2.5        Rep_defined: thm, Abs_defined: thm }
     2.6  
     2.7 -  val add_podef: bool -> binding option -> binding * string list * mixfix ->
     2.8 +  val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     2.9      term -> (binding * binding) option -> tactic -> theory ->
    2.10      (Typedef.info * thm) * theory
    2.11 -  val add_cpodef: bool -> binding option -> binding * string list * mixfix ->
    2.12 +  val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
    2.13      term -> (binding * binding) option -> tactic * tactic -> theory ->
    2.14      (Typedef.info * cpo_info) * theory
    2.15 -  val add_pcpodef: bool -> binding option -> binding * string list * mixfix ->
    2.16 +  val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
    2.17      term -> (binding * binding) option -> tactic * tactic -> theory ->
    2.18      (Typedef.info * cpo_info * pcpo_info) * theory
    2.19  
    2.20 -  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    2.21 +  val cpodef_proof: (bool * binding)
    2.22 +    * (binding * (string * sort) list * mixfix) * term
    2.23      * (binding * binding) option -> theory -> Proof.state
    2.24 -  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    2.25 +  val cpodef_proof_cmd: (bool * binding)
    2.26 +    * (binding * (string * string option) list * mixfix) * string
    2.27      * (binding * binding) option -> theory -> Proof.state
    2.28 -  val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    2.29 +  val pcpodef_proof: (bool * binding)
    2.30 +    * (binding * (string * sort) list * mixfix) * term
    2.31      * (binding * binding) option -> theory -> Proof.state
    2.32 -  val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    2.33 +  val pcpodef_proof_cmd: (bool * binding)
    2.34 +    * (binding * (string * string option) list * mixfix) * string
    2.35      * (binding * binding) option -> theory -> Proof.state
    2.36  end;
    2.37  
    2.38 @@ -153,21 +157,23 @@
    2.39  fun declare_type_name a =
    2.40    Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
    2.41  
    2.42 -fun prepare prep_term name (tname, vs, mx) raw_set opt_morphs thy =
    2.43 +fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
    2.44    let
    2.45      val _ = Theory.requires thy "Pcpodef" "pcpodefs";
    2.46 -    val ctxt = ProofContext.init thy;
    2.47  
    2.48      (*rhs*)
    2.49 -    val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
    2.50 +    val (_, tmp_lthy) =
    2.51 +      thy |> Theory.copy |> Theory_Target.init NONE
    2.52 +      |> Typedecl.predeclare_constraints (tname, raw_args, mx);
    2.53 +    val set = prep_term tmp_lthy raw_set;
    2.54 +    val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set;
    2.55 +
    2.56      val setT = Term.fastype_of set;
    2.57 -    val rhs_tfrees = Term.add_tfrees set [];
    2.58      val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    2.59 -      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
    2.60 +      error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_lthy setT));
    2.61  
    2.62      (*lhs*)
    2.63 -    val defS = Sign.defaultS thy;
    2.64 -    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
    2.65 +    val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
    2.66      val full_tname = Sign.full_name thy tname;
    2.67      val newT = Type (full_tname, map TFree lhs_tfrees);
    2.68  
    2.69 @@ -206,7 +212,7 @@
    2.70        (prep_term: Proof.context -> 'a -> term)
    2.71        (def: bool)
    2.72        (name: binding)
    2.73 -      (typ: binding * string list * mixfix)
    2.74 +      (typ: binding * (string * sort) list * mixfix)
    2.75        (raw_set: 'a)
    2.76        (opt_morphs: (binding * binding) option)
    2.77        (thy: theory)
    2.78 @@ -239,7 +245,7 @@
    2.79        (prep_term: Proof.context -> 'a -> term)
    2.80        (def: bool)
    2.81        (name: binding)
    2.82 -      (typ: binding * string list * mixfix)
    2.83 +      (typ: binding * (string * sort) list * mixfix)
    2.84        (raw_set: 'a)
    2.85        (opt_morphs: (binding * binding) option)
    2.86        (thy: theory)
    2.87 @@ -306,27 +312,33 @@
    2.88  
    2.89  local
    2.90  
    2.91 -fun gen_cpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy =
    2.92 +fun gen_cpodef_proof prep_term prep_constraint
    2.93 +    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
    2.94    let
    2.95 +    val ctxt = ProofContext.init thy;
    2.96 +    val args = map (apsnd (prep_constraint ctxt)) raw_args;
    2.97      val (goal1, goal2, make_result) =
    2.98 -      prepare_cpodef prep_term def name typ set opt_morphs thy;
    2.99 +      prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
   2.100      fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
   2.101 -  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
   2.102 +  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
   2.103  
   2.104 -fun gen_pcpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy =
   2.105 +fun gen_pcpodef_proof prep_term prep_constraint
   2.106 +    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
   2.107    let
   2.108 +    val ctxt = ProofContext.init thy;
   2.109 +    val args = map (apsnd (prep_constraint ctxt)) raw_args;
   2.110      val (goal1, goal2, make_result) =
   2.111 -      prepare_pcpodef prep_term def name typ set opt_morphs thy;
   2.112 +      prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
   2.113      fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
   2.114 -  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
   2.115 +  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
   2.116  
   2.117  in
   2.118  
   2.119 -fun cpodef_proof x = gen_cpodef_proof Syntax.check_term x;
   2.120 -fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term x;
   2.121 +fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x;
   2.122 +fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x;
   2.123  
   2.124 -fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term x;
   2.125 -fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term x;
   2.126 +fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x;
   2.127 +fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x;
   2.128  
   2.129  end;
   2.130  
   2.131 @@ -340,12 +352,12 @@
   2.132    Scan.optional (P.$$$ "(" |--
   2.133        ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
   2.134          --| P.$$$ ")") (true, NONE) --
   2.135 -    (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
   2.136 +    (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
   2.137      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
   2.138  
   2.139 -fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
   2.140 +fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   2.141    (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
   2.142 -    ((def, the_default t opt_name), (t, vs, mx), A, morphs);
   2.143 +    ((def, the_default t opt_name), (t, args, mx), A, morphs);
   2.144  
   2.145  val _ =
   2.146    OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
     3.1 --- a/src/HOLCF/Tools/repdef.ML	Fri Mar 19 00:42:17 2010 +0100
     3.2 +++ b/src/HOLCF/Tools/repdef.ML	Fri Mar 19 00:43:49 2010 +0100
     3.3 @@ -9,11 +9,11 @@
     3.4    type rep_info =
     3.5      { emb_def: thm, prj_def: thm, approx_def: thm, REP: thm }
     3.6  
     3.7 -  val add_repdef: bool -> binding option -> binding * string list * mixfix ->
     3.8 +  val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     3.9      term -> (binding * binding) option -> theory ->
    3.10      (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory
    3.11  
    3.12 -  val repdef_cmd: (bool * binding) * (binding * string list * mixfix) * string
    3.13 +  val repdef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string
    3.14      * (binding * binding) option -> theory -> theory
    3.15  end;
    3.16  
    3.17 @@ -55,25 +55,27 @@
    3.18        (prep_term: Proof.context -> 'a -> term)
    3.19        (def: bool)
    3.20        (name: binding)
    3.21 -      (typ as (tname, vs, mx) : binding * string list * mixfix)
    3.22 +      (typ as (tname, raw_args, mx) : binding * (string * sort) list * mixfix)
    3.23        (raw_defl: 'a)
    3.24        (opt_morphs: (binding * binding) option)
    3.25        (thy: theory)
    3.26      : (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory =
    3.27    let
    3.28      val _ = Theory.requires thy "Representable" "repdefs";
    3.29 -    val ctxt = ProofContext.init thy;
    3.30  
    3.31      (*rhs*)
    3.32 -    val defl = prep_term (ctxt |> fold declare_type_name vs) raw_defl;
    3.33 +    val (_, tmp_lthy) =
    3.34 +      thy |> Theory.copy |> Theory_Target.init NONE
    3.35 +      |> Typedecl.predeclare_constraints (tname, raw_args, mx);
    3.36 +    val defl = prep_term tmp_lthy raw_defl;
    3.37 +    val tmp_lthy' = tmp_lthy |> Variable.declare_constraints defl;
    3.38 +
    3.39      val deflT = Term.fastype_of defl;
    3.40      val _ = if deflT = @{typ "udom alg_defl"} then ()
    3.41 -            else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ ctxt deflT));
    3.42 -    val rhs_tfrees = Term.add_tfrees defl [];
    3.43 +            else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT));
    3.44  
    3.45      (*lhs*)
    3.46 -    val defS = Sign.defaultS thy;
    3.47 -    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
    3.48 +    val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args;
    3.49      val lhs_sorts = map snd lhs_tfrees;
    3.50      val full_tname = Sign.full_name thy tname;
    3.51      val newT = Type (full_tname, map TFree lhs_tfrees);
    3.52 @@ -152,8 +154,12 @@
    3.53      gen_add_repdef Syntax.check_term def name typ defl opt_morphs thy
    3.54    end;
    3.55  
    3.56 -fun repdef_cmd ((def, name), typ, A, morphs) =
    3.57 -  snd o gen_add_repdef Syntax.read_term def name typ A morphs;
    3.58 +fun repdef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy =
    3.59 +  let
    3.60 +    val ctxt = ProofContext.init thy;
    3.61 +    val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args;
    3.62 +  in snd (gen_add_repdef Syntax.read_term def name (b, args, mx) A morphs thy) end;
    3.63 +
    3.64  
    3.65  (** outer syntax **)
    3.66  
    3.67 @@ -163,11 +169,11 @@
    3.68    Scan.optional (P.$$$ "(" |--
    3.69        ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
    3.70          --| P.$$$ ")") (true, NONE) --
    3.71 -    (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
    3.72 +    (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
    3.73      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
    3.74  
    3.75 -fun mk_repdef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
    3.76 -  repdef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs);
    3.77 +fun mk_repdef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
    3.78 +  repdef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs);
    3.79  
    3.80  val _ =
    3.81    OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl