added flag to 'typedef' to allow concealed definitions
authorblanchet
Mon Sep 08 23:04:18 2014 +0200 (2014-09-08)
changeset 582391c5bc387bd4c
parent 58238 a701907d621e
child 58240 b05ed697708e
added flag to 'typedef' to allow concealed definitions
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/Import/import_rule.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/BNF/bnf_util.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typedef.ML
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Sep 08 23:04:18 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon Sep 08 23:04:18 2014 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4    let
     1.5      val name = #1 typ
     1.6      val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
     1.7 -      |> Typedef.add_typedef_global typ set opt_morphs tac
     1.8 +      |> Typedef.add_typedef_global false typ set opt_morphs tac
     1.9      val oldT = #rep_type (#1 info)
    1.10      val newT = #abs_type (#1 info)
    1.11      val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
     2.1 --- a/src/HOL/Import/import_rule.ML	Mon Sep 08 23:04:18 2014 +0200
     2.2 +++ b/src/HOL/Import/import_rule.ML	Mon Sep 08 23:04:18 2014 +0200
     2.3 @@ -221,7 +221,7 @@
     2.4      val tfrees = Term.add_tfrees c []
     2.5      val tnames = sort_strings (map fst tfrees)
     2.6      val ((_, typedef_info), thy') =
     2.7 -     Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
     2.8 +     Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
     2.9         (SOME (Binding.name rep_name, Binding.name abs_name)) (rtac th2 1) thy
    2.10      val aty = #abs_type (#1 typedef_info)
    2.11      val th = freezeT (#type_definition (#2 typedef_info))
     3.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
     3.3 @@ -574,7 +574,7 @@
     3.4      val (typedefs, thy6) =
     3.5        thy4
     3.6        |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
     3.7 -          Typedef.add_typedef_global
     3.8 +          Typedef.add_typedef_global false
     3.9              (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
    3.10              (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    3.11                 Const (cname, U --> HOLogic.boolT)) NONE
     4.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 08 23:04:18 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Sep 08 23:04:18 2014 +0200
     4.3 @@ -324,7 +324,7 @@
     4.4      val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
     4.5      val ((name, info), (lthy, lthy_old)) =
     4.6        lthy
     4.7 -      |> Typedef.add_typedef (b', Ts, mx) set opt_morphs tac
     4.8 +      |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
     4.9        ||> `Local_Theory.restore;
    4.10      val phi = Proof_Context.export_morphism lthy_old lthy;
    4.11    in
     5.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
     5.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
     5.3 @@ -186,7 +186,7 @@
     5.4        |> Sign.parent_path
     5.5        |> fold_map
     5.6          (fn (((name, mx), tvs), c) =>
     5.7 -          Typedef.add_typedef_global (name, tvs, mx)
     5.8 +          Typedef.add_typedef_global false (name, tvs, mx)
     5.9              (Collect $ Const (c, UnivT')) NONE
    5.10              (rtac exI 1 THEN rtac CollectI 1 THEN
    5.11                QUIET_BREADTH_FIRST (has_fewer_prems 1)
     6.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Mon Sep 08 23:04:18 2014 +0200
     6.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Sep 08 23:04:18 2014 +0200
     6.3 @@ -45,7 +45,7 @@
     6.4      val typedef_tac =
     6.5        EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
     6.6    in
     6.7 -    Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
     6.8 +    Typedef.add_typedef false (qty_name, map (rpair dummyS) vs, mx)
     6.9        (typedef_term rel rty lthy) NONE typedef_tac lthy
    6.10    end
    6.11  
     7.1 --- a/src/HOL/Tools/record.ML	Mon Sep 08 23:04:18 2014 +0200
     7.2 +++ b/src/HOL/Tools/record.ML	Mon Sep 08 23:04:18 2014 +0200
     7.3 @@ -111,7 +111,7 @@
     7.4      val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
     7.5    in
     7.6      thy
     7.7 -    |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
     7.8 +    |> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn)
     7.9          (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
    7.10      |-> (fn (tyco, info) => get_typedef_info tyco vs info)
    7.11    end;
     8.1 --- a/src/HOL/Tools/typedef.ML	Mon Sep 08 23:04:18 2014 +0200
     8.2 +++ b/src/HOL/Tools/typedef.ML	Mon Sep 08 23:04:18 2014 +0200
     8.3 @@ -16,10 +16,9 @@
     8.4    val get_info: Proof.context -> string -> info list
     8.5    val get_info_global: theory -> string -> info list
     8.6    val interpretation: (string -> theory -> theory) -> theory -> theory
     8.7 -  val setup: theory -> theory
     8.8 -  val add_typedef: binding * (string * sort) list * mixfix ->
     8.9 +  val add_typedef: bool -> binding * (string * sort) list * mixfix ->
    8.10      term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
    8.11 -  val add_typedef_global: binding * (string * sort) list * mixfix ->
    8.12 +  val add_typedef_global: bool -> binding * (string * sort) list * mixfix ->
    8.13      term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
    8.14    val typedef: (binding * (string * sort) list * mixfix) * term *
    8.15      (binding * binding) option -> local_theory -> Proof.state
    8.16 @@ -83,7 +82,7 @@
    8.17  
    8.18  fun interpretation f = Typedef_Interpretation.interpretation (with_repaired_path f);
    8.19  
    8.20 -val setup = Typedef_Interpretation.init;
    8.21 +val _ = Theory.setup Typedef_Interpretation.init;
    8.22  
    8.23  
    8.24  (* primitive typedef axiomatization -- for fresh typedecl *)
    8.25 @@ -136,8 +135,9 @@
    8.26  
    8.27  (* prepare_typedef *)
    8.28  
    8.29 -fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
    8.30 +fun prepare_typedef conceal prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
    8.31    let
    8.32 +    val concealed_name = name |> conceal ? Binding.conceal;
    8.33      val bname = Binding.name_of name;
    8.34  
    8.35  
    8.36 @@ -169,10 +169,11 @@
    8.37  
    8.38      val (Rep_name, Abs_name) =
    8.39        (case opt_morphs of
    8.40 -        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
    8.41 +        NONE => (Binding.prefix_name "Rep_" concealed_name,
    8.42 +          Binding.prefix_name "Abs_" concealed_name)
    8.43        | SOME morphs => morphs);
    8.44  
    8.45 -    val typedef_name = Binding.prefix_name "type_definition_" name;
    8.46 +    val typedef_name = Binding.prefix_name "type_definition_" concealed_name;
    8.47  
    8.48      val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
    8.49        |> primitive_typedef typedef_name newT oldT Rep_name Abs_name set;
    8.50 @@ -239,18 +240,18 @@
    8.51  
    8.52  (* add_typedef: tactic interface *)
    8.53  
    8.54 -fun add_typedef typ set opt_morphs tac lthy =
    8.55 +fun add_typedef conceal typ set opt_morphs tac lthy =
    8.56    let
    8.57      val ((goal, _, typedef_result), lthy') =
    8.58 -      prepare_typedef Syntax.check_term typ set opt_morphs lthy;
    8.59 +      prepare_typedef conceal Syntax.check_term typ set opt_morphs lthy;
    8.60      val inhabited =
    8.61        Goal.prove lthy' [] [] goal (K tac)
    8.62        |> Goal.norm_result lthy' |> Thm.close_derivation;
    8.63    in typedef_result inhabited lthy' end;
    8.64  
    8.65 -fun add_typedef_global typ set opt_morphs tac =
    8.66 +fun add_typedef_global conceal typ set opt_morphs tac =
    8.67    Named_Target.theory_init
    8.68 -  #> add_typedef typ set opt_morphs tac
    8.69 +  #> add_typedef conceal typ set opt_morphs tac
    8.70    #> Local_Theory.exit_result_global (apsnd o transform_info);
    8.71  
    8.72  
    8.73 @@ -262,7 +263,7 @@
    8.74    let
    8.75      val args = map (apsnd (prep_constraint lthy)) raw_args;
    8.76      val ((goal, goal_pat, typedef_result), lthy') =
    8.77 -      prepare_typedef prep_term (b, args, mx) set opt_morphs lthy;
    8.78 +      prepare_typedef false prep_term (b, args, mx) set opt_morphs lthy;
    8.79      fun after_qed [[th]] = snd o typedef_result th;
    8.80    in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
    8.81  
     9.1 --- a/src/HOL/Typedef.thy	Mon Sep 08 23:04:18 2014 +0200
     9.2 +++ b/src/HOL/Typedef.thy	Mon Sep 08 23:04:18 2014 +0200
     9.3 @@ -108,6 +108,6 @@
     9.4  
     9.5  end
     9.6  
     9.7 -ML_file "Tools/typedef.ML" setup Typedef.setup
     9.8 +ML_file "Tools/typedef.ML"
     9.9  
    9.10  end