src/HOL/Tools/typecopy.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 37469 1436d6f28f17
child 38348 cf7b2121ad9d
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31136
diff changeset
     1
(*  Title:      HOL/Tools/typecopy.ML
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     3
20855
9f60d493c8fe clarified header comments
haftmann
parents: 20835
diff changeset
     4
Introducing copies of types using trivial typedefs; datatype-like abstraction.
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     5
*)
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     6
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31136
diff changeset
     7
signature TYPECOPY =
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
     8
sig
37469
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
     9
  type info = { vs: (string * sort) list, typ: typ, constr: string, proj: string,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    10
    constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm }
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    11
  val typecopy: binding * (string * sort) list -> typ -> binding -> binding
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20426
diff changeset
    12
    -> theory -> (string * info) * theory
25506
haftmann
parents: 25489
diff changeset
    13
  val get_info: theory -> string -> info option
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
    14
  val interpretation: (string -> theory -> theory) -> theory -> theory
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
    15
  val add_default_code: string -> theory -> theory
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    16
  val setup: theory -> theory
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    17
end;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    18
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31136
diff changeset
    19
structure Typecopy: TYPECOPY =
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    20
struct
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    21
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    22
(* theory data *)
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    23
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    24
type info = {
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    25
  vs: (string * sort) list,
37469
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    26
  typ: typ,
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    27
  constr: string,
37469
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    28
  proj: string,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    29
  constr_inject: thm,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    30
  proj_inject: thm,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    31
  constr_proj: thm,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    32
  proj_constr: thm
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    33
};
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    34
37469
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    35
structure Typecopy_Data = Theory_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    36
(
24626
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
    37
  type T = info Symtab.table;
85eceef2edc7 introduced generic concepts for theory interpretators
haftmann
parents: 24624
diff changeset
    38
  val empty = Symtab.empty;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    39
  val extend = I;
33522
737589bb9bb8 adapted Theory_Data;
wenzelm
parents: 33314
diff changeset
    40
  fun merge data = Symtab.merge (K true) data;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    41
);
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
    42
37469
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    43
val get_info = Symtab.lookup o Typecopy_Data.get;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    44
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    45
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
    46
(* interpretation of type copies *)
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    47
33314
53d49370f7af modernized functor/structures Interpretation;
wenzelm
parents: 32378
diff changeset
    48
structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =);
53d49370f7af modernized functor/structures Interpretation;
wenzelm
parents: 32378
diff changeset
    49
val interpretation = Typecopy_Interpretation.interpretation;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    50
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
    51
31735
a00292a5587d tuned interface
haftmann
parents: 31723
diff changeset
    52
(* introducing typecopies *)
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
    53
37469
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    54
fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    55
    { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    56
  let
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    57
    val exists_thm =
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    58
      UNIV_I
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    59
      |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    60
    val constr_inject = Abs_inject OF [exists_thm, exists_thm];
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    61
    val proj_constr = Abs_inverse OF [exists_thm];
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    62
    val info = {
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    63
      vs = vs,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    64
      typ = rep_type,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    65
      constr = Abs_name,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    66
      proj = Rep_name,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    67
      constr_inject = constr_inject,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    68
      proj_inject = Rep_inject,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    69
      constr_proj = Rep_inverse,
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    70
      proj_constr = proj_constr
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    71
    };
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    72
  in
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    73
    thy
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    74
    |> (Typecopy_Data.map o Symtab.update_new) (tyco, info)
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    75
    |> Typecopy_Interpretation.data tyco
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    76
    |> pair (tyco, info)
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    77
  end
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    78
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    79
fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    80
  let
28664
haftmann
parents: 28423
diff changeset
    81
    val ty = Sign.certify_typ thy raw_ty;
36610
bafd82950e24 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents: 36156
diff changeset
    82
    val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
36156
6f0a8f6b1671 explicit ProofContext.check_tfree;
wenzelm
parents: 36150
diff changeset
    83
    val vs = map (ProofContext.check_tfree ctxt) raw_vs;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    84
    val tac = Tactic.rtac UNIV_witness 1;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    85
  in
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    86
    thy
36150
123f721c9a37 typecopy: observe given sort constraints more precisely;
wenzelm
parents: 35994
diff changeset
    87
    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
37469
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    88
      (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    89
    |-> (fn (tyco, info) => add_info tyco vs info)
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    90
  end;
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    91
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
    92
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
    93
(* default code setup *)
20835
haftmann
parents: 20597
diff changeset
    94
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
    95
fun add_default_code tyco thy =
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
    96
  let
37469
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    97
    val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } =
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
    98
      get_info thy tyco;
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35842
diff changeset
    99
    val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
28423
9fc3befd8191 clarified codegen interfaces
haftmann
parents: 28394
diff changeset
   100
    val ty = Type (tyco, map TFree vs);
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   101
    val proj = Const (proj, ty --> ty_rep);
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   102
    val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   103
    val eq_lhs = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
28664
haftmann
parents: 28423
diff changeset
   104
      $ t_x $ t_y;
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   105
    val eq_rhs = HOLogic.mk_eq (proj $ t_x, proj $ t_y);
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   106
    val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (eq_lhs, eq_rhs);
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   107
    fun tac eq_thm = Class.intro_classes_tac []
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   108
      THEN (Simplifier.rewrite_goals_tac
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   109
        (map Simpdata.mk_eq [eq_thm, @{thm eq}, proj_inject]))
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   110
          THEN ALLGOALS (rtac @{thm refl});
28664
haftmann
parents: 28423
diff changeset
   111
    fun mk_eq_refl thy = @{thm HOL.eq_refl}
haftmann
parents: 28423
diff changeset
   112
      |> Thm.instantiate
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35842
diff changeset
   113
         ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], [])
28664
haftmann
parents: 28423
diff changeset
   114
      |> AxClass.unoverload thy;
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
   115
  in
25506
haftmann
parents: 25489
diff changeset
   116
    thy
28664
haftmann
parents: 28423
diff changeset
   117
    |> Code.add_datatype [constr]
37469
1436d6f28f17 cleanup of typecopy package
haftmann
parents: 36610
diff changeset
   118
    |> Code.add_eqn proj_constr
33553
35f2b30593a8 modernized structure Theory_Target;
wenzelm
parents: 33522
diff changeset
   119
    |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   120
    |> `(fn lthy => Syntax.check_term lthy eq)
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   121
    |-> (fn eq => Specification.definition
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   122
         (NONE, (Attrib.empty_binding, eq)))
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   123
    |-> (fn (_, (_, eq_thm)) =>
28664
haftmann
parents: 28423
diff changeset
   124
       Class.prove_instantiation_exit_result Morphism.thm
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   125
         (fn _ => fn eq_thm => tac eq_thm) eq_thm)
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   126
    |-> (fn eq_thm => Code.add_eqn eq_thm)
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   127
    |> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy)
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
   128
  end;
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   129
25489
5b0625f6e324 simplified interpretations
haftmann
parents: 24711
diff changeset
   130
val setup =
33314
53d49370f7af modernized functor/structures Interpretation;
wenzelm
parents: 32378
diff changeset
   131
  Typecopy_Interpretation.init
31136
85d04515abb3 tuned and generalized construction of code equations for eq; tuned interface
haftmann
parents: 31090
diff changeset
   132
  #> interpretation add_default_code
20426
9ffea7a8b31c added typecopy_package
haftmann
parents:
diff changeset
   133
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 22484
diff changeset
   134
end;