src/HOL/Tools/typedef_package.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 29579 cb520b766e00
child 30345 76fd85bbf139
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/typedef_package.ML
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16126
diff changeset
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     3
21352
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
     4
Gordon/HOL-style type definitions: create a new syntactic type
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
     5
represented by a non-empty subset.
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     6
*)
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     7
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     8
signature TYPEDEF_PACKAGE =
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     9
sig
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
    10
  type info =
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    11
   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    12
    type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    13
    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    14
    Rep_induct: thm, Abs_induct: thm}
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
    15
  val get_info: theory -> string -> info option
11827
16ef206e6648 sane internal interface for add_typedef(_i);
wenzelm
parents: 11822
diff changeset
    16
  val add_typedef: bool -> string option -> bstring * string list * mixfix ->
20483
04aa552a83bc TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents: 20462
diff changeset
    17
    term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
28662
64ab5bb68d4c tuned typedef interface
haftmann
parents: 27691
diff changeset
    18
  val typedef: (bool * string) * (bstring * string list * mixfix) * term
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
    19
    * (string * string) option -> theory -> Proof.state
28662
64ab5bb68d4c tuned typedef interface
haftmann
parents: 27691
diff changeset
    20
  val typedef_cmd: (bool * string) * (bstring * string list * mixfix) * string
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
    21
    * (string * string) option -> theory -> Proof.state
25513
b7de6e23e143 interpretation for typedefs
haftmann
parents: 25495
diff changeset
    22
  val interpretation: (string -> theory -> theory) -> theory -> theory
25535
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
    23
  val setup: theory -> theory
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    24
end;
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    25
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    26
structure TypedefPackage: TYPEDEF_PACKAGE =
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    27
struct
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    28
17922
0cba8edb269e removed obsolete add_typedef_x;
wenzelm
parents: 17412
diff changeset
    29
(** type definitions **)
0cba8edb269e removed obsolete add_typedef_x;
wenzelm
parents: 17412
diff changeset
    30
0cba8edb269e removed obsolete add_typedef_x;
wenzelm
parents: 17412
diff changeset
    31
(* theory data *)
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
    32
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
    33
type info =
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    34
 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    35
  type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    36
  Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    37
  Rep_induct: thm, Abs_induct: thm};
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents: 19391
diff changeset
    38
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16126
diff changeset
    39
structure TypedefData = TheoryDataFun
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 21565
diff changeset
    40
(
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
    41
  type T = info Symtab.table;
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
    42
  val empty = Symtab.empty;
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
    43
  val copy = I;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16126
diff changeset
    44
  val extend = I;
19617
7cb4b67d4b97 avoid raw equality on type thm;
wenzelm
parents: 19585
diff changeset
    45
  fun merge _ tabs : T = Symtab.merge (K true) tabs;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 21565
diff changeset
    46
);
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
    47
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
    48
val get_info = Symtab.lookup o TypedefData.get;
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
    49
fun put_info name info = TypedefData.map (Symtab.update (name, info));
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
    50
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
    51
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
    52
(* prepare_typedef *)
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
    53
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18643
diff changeset
    54
fun err_in_typedef msg name =
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18643
diff changeset
    55
  cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
    56
21352
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
    57
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
    58
25535
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
    59
structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
    60
val interpretation = TypedefInterpretation.interpretation;
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
    61
11822
122834177ec1 improved internal interface of typedef;
wenzelm
parents: 11807
diff changeset
    62
fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    63
  let
11608
c760ea8154ee renamed theory "subset" to "Typedef";
wenzelm
parents: 11426
diff changeset
    64
    val _ = Theory.requires thy "Typedef" "typedefs";
21352
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
    65
    val ctxt = ProofContext.init thy;
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28848
diff changeset
    66
    val full = Sign.full_bname thy;
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    67
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    68
    (*rhs*)
10280
2626d4e37341 provide more theorems (see subset.thy);
wenzelm
parents: 9969
diff changeset
    69
    val full_name = full name;
21352
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
    70
    val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
    71
    val setT = Term.fastype_of set;
17280
a6917ddc864f proper treatment of polymorphic sets;
wenzelm
parents: 17261
diff changeset
    72
    val rhs_tfrees = Term.add_tfrees set [];
a6917ddc864f proper treatment of polymorphic sets;
wenzelm
parents: 17261
diff changeset
    73
    val rhs_tfreesT = Term.add_tfreesT setT [];
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    74
    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24867
diff changeset
    75
      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    76
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    77
    (*lhs*)
17280
a6917ddc864f proper treatment of polymorphic sets;
wenzelm
parents: 17261
diff changeset
    78
    val defS = Sign.defaultS thy;
19473
wenzelm
parents: 19459
diff changeset
    79
    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
17280
a6917ddc864f proper treatment of polymorphic sets;
wenzelm
parents: 17261
diff changeset
    80
    val args_setT = lhs_tfrees
a6917ddc864f proper treatment of polymorphic sets;
wenzelm
parents: 17261
diff changeset
    81
      |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
a6917ddc864f proper treatment of polymorphic sets;
wenzelm
parents: 17261
diff changeset
    82
      |> map TFree;
a6917ddc864f proper treatment of polymorphic sets;
wenzelm
parents: 17261
diff changeset
    83
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    84
    val tname = Syntax.type_name t mx;
10280
2626d4e37341 provide more theorems (see subset.thy);
wenzelm
parents: 9969
diff changeset
    85
    val full_tname = full tname;
2626d4e37341 provide more theorems (see subset.thy);
wenzelm
parents: 9969
diff changeset
    86
    val newT = Type (full_tname, map TFree lhs_tfrees);
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    87
19473
wenzelm
parents: 19459
diff changeset
    88
    val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
19391
4812d28c90a6 Term.itselfT;
wenzelm
parents: 19342
diff changeset
    89
    val setT' = map Term.itselfT args_setT ---> setT;
17280
a6917ddc864f proper treatment of polymorphic sets;
wenzelm
parents: 17261
diff changeset
    90
    val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
10280
2626d4e37341 provide more theorems (see subset.thy);
wenzelm
parents: 9969
diff changeset
    91
    val RepC = Const (full Rep_name, newT --> oldT);
2626d4e37341 provide more theorems (see subset.thy);
wenzelm
parents: 9969
diff changeset
    92
    val AbsC = Const (full Abs_name, oldT --> newT);
2626d4e37341 provide more theorems (see subset.thy);
wenzelm
parents: 9969
diff changeset
    93
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    94
    (*inhabitance*)
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    95
    fun mk_inhabited A =
29054
6f61794f1ff7 logically separate typedef axiomatization from constant definition
krauss
parents: 29053
diff changeset
    96
      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    97
    val set' = if def then setC else set;
29062
6f8a100325b6 recovered goal_pat;
wenzelm
parents: 29061
diff changeset
    98
    val goal' = mk_inhabited set';
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    99
    val goal = mk_inhabited set;
29062
6f8a100325b6 recovered goal_pat;
wenzelm
parents: 29061
diff changeset
   100
    val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   101
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   102
    (*axiomatization*)
10280
2626d4e37341 provide more theorems (see subset.thy);
wenzelm
parents: 9969
diff changeset
   103
    val typedef_name = "type_definition_" ^ name;
2626d4e37341 provide more theorems (see subset.thy);
wenzelm
parents: 9969
diff changeset
   104
    val typedefC =
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   105
      Const (@{const_name type_definition},
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   106
        (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   107
    val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   108
    val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   109
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   110
    (*set definition*)
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   111
    fun add_def theory =
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   112
      if def then
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   113
        theory
29053
077fb9b16119 add def before setting up goal
krauss
parents: 29052
diff changeset
   114
        |> Sign.add_consts_i [(name, setT', NoSyn)]
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29264
diff changeset
   115
        |> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name)
cb520b766e00 binding replaces bstring
haftmann
parents: 29264
diff changeset
   116
            (PrimitiveDefs.mk_defpair (setC, set)))]
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
   117
        |-> (fn [th] => pair (SOME th))
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   118
      else (NONE, theory);
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   119
    fun contract_def NONE th = th
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   120
      | contract_def (SOME def_eq) th =
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   121
          let
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   122
            val cert = Thm.cterm_of (Thm.theory_of_thm def_eq);
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   123
            val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal');
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   124
          in Drule.standard (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
18358
0a733e11021a re-oriented some result tuples in PureThy
haftmann
parents: 17956
diff changeset
   125
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   126
    fun typedef_result inhabited =
25495
98f3596bec44 ObjectLogic.typedecl;
wenzelm
parents: 25458
diff changeset
   127
      ObjectLogic.typedecl (t, vs, mx)
25458
ba8f5e4fa336 separated typedecl module, providing typedecl command with interpretation
haftmann
parents: 24926
diff changeset
   128
      #> snd
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24509
diff changeset
   129
      #> Sign.add_consts_i
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   130
        [(Rep_name, newT --> oldT, NoSyn),
29053
077fb9b16119 add def before setting up goal
krauss
parents: 29052
diff changeset
   131
         (Abs_name, oldT --> newT, NoSyn)]
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   132
      #> add_def
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   133
      #-> (fn set_def =>
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29264
diff changeset
   134
        PureThy.add_axioms [((Binding.name typedef_name, typedef_prop),
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   135
          [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   136
        ##>> pair set_def)
21352
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
   137
      ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
   138
      ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   139
      #-> (fn ([type_definition], set_def) => fn thy1 =>
11822
122834177ec1 improved internal interface of typedef;
wenzelm
parents: 11807
diff changeset
   140
        let
122834177ec1 improved internal interface of typedef;
wenzelm
parents: 11807
diff changeset
   141
          fun make th = Drule.standard (th OF [type_definition]);
18377
0e1d025d57b3 oriented result pairs in PureThy
haftmann
parents: 18358
diff changeset
   142
          val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
   143
              Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
   144
            thy1
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24509
diff changeset
   145
            |> Sign.add_path name
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12043
diff changeset
   146
            |> PureThy.add_thms
29579
cb520b766e00 binding replaces bstring
haftmann
parents: 29264
diff changeset
   147
              ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []),
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   148
                ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   149
                ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   150
                ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   151
                ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []),
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   152
                ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}),
24861
cc669ca5f382 tuned Induct interface: prefer pred'' over set'';
wenzelm
parents: 24830
diff changeset
   153
                  [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   154
                ((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}),
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 24712
diff changeset
   155
                  [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   156
                ((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}),
24861
cc669ca5f382 tuned Induct interface: prefer pred'' over set'';
wenzelm
parents: 24830
diff changeset
   157
                  [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   158
                ((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}),
24830
a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents: 24712
diff changeset
   159
                  [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24509
diff changeset
   160
            ||> Sign.parent_path;
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
   161
          val info = {rep_type = oldT, abs_type = newT,
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
   162
            Rep_name = full Rep_name, Abs_name = full Abs_name,
28848
9a02932efb91 explicit inhabitance proof
haftmann
parents: 28662
diff changeset
   163
              inhabited = inhabited, type_definition = type_definition, set_def = set_def,
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
   164
              Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
   165
              Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
11822
122834177ec1 improved internal interface of typedef;
wenzelm
parents: 11807
diff changeset
   166
            Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
25535
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
   167
        in
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
   168
          thy2
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
   169
          |> put_info full_tname info
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
   170
          |> TypedefInterpretation.data full_tname
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
   171
          |> pair (full_tname, info)
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
   172
        end);
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   173
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   174
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   175
    (* errors *)
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   176
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   177
    fun show_names pairs = commas_quote (map fst pairs);
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   178
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   179
    val illegal_vars =
29264
4ea3358fac3f use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 29062
diff changeset
   180
      if null (Term.add_vars set []) andalso null (Term.add_tvars set []) then []
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   181
      else ["Illegal schematic variable(s) on rhs"];
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   182
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   183
    val dup_lhs_tfrees =
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18928
diff changeset
   184
      (case duplicates (op =) lhs_tfrees of [] => []
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   185
      | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   186
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   187
    val extra_rhs_tfrees =
17280
a6917ddc864f proper treatment of polymorphic sets;
wenzelm
parents: 17261
diff changeset
   188
      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => []
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   189
      | extras => ["Extra type variables on rhs: " ^ show_names extras]);
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   190
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   191
    val illegal_frees =
29264
4ea3358fac3f use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 29062
diff changeset
   192
      (case Term.add_frees set [] of [] => []
4ea3358fac3f use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 29062
diff changeset
   193
      | xs => ["Illegal variables on rhs: " ^ show_names xs]);
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   194
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   195
    val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
11426
f280d4b29a2c abtract non-emptiness statements (no longer use Eps);
wenzelm
parents: 10697
diff changeset
   196
    val _ = if null errs then () else error (cat_lines errs);
f280d4b29a2c abtract non-emptiness statements (no longer use Eps);
wenzelm
parents: 10697
diff changeset
   197
f280d4b29a2c abtract non-emptiness statements (no longer use Eps);
wenzelm
parents: 10697
diff changeset
   198
    (*test theory errors now!*)
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   199
    val test_thy = Theory.copy thy;
21352
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
   200
    val _ = test_thy
19342
094a1c071c8e added functions for definitional code generation
haftmann
parents: 18964
diff changeset
   201
      |> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal);
11426
f280d4b29a2c abtract non-emptiness statements (no longer use Eps);
wenzelm
parents: 10697
diff changeset
   202
29062
6f8a100325b6 recovered goal_pat;
wenzelm
parents: 29061
diff changeset
   203
  in (set, goal, goal_pat, typedef_result) end
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18643
diff changeset
   204
  handle ERROR msg => err_in_typedef msg name;
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   205
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   206
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   207
(* add_typedef: tactic interface *)
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   208
28662
64ab5bb68d4c tuned typedef interface
haftmann
parents: 27691
diff changeset
   209
fun add_typedef def opt_name typ set opt_morphs tac thy =
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   210
  let
17922
0cba8edb269e removed obsolete add_typedef_x;
wenzelm
parents: 17412
diff changeset
   211
    val name = the_default (#1 typ) opt_name;
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   212
    val (set, goal, _, typedef_result) =
28662
64ab5bb68d4c tuned typedef interface
haftmann
parents: 27691
diff changeset
   213
      prepare_typedef Syntax.check_term def name typ set opt_morphs thy;
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   214
    val inhabited = Goal.prove_global thy [] [] goal (K tac)
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   215
      handle ERROR msg => cat_error msg
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   216
        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
   217
  in typedef_result inhabited thy end;
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   218
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   219
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   220
(* typedef: proof interface *)
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   221
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   222
local
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   223
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   224
fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy =
11822
122834177ec1 improved internal interface of typedef;
wenzelm
parents: 11807
diff changeset
   225
  let
29062
6f8a100325b6 recovered goal_pat;
wenzelm
parents: 29061
diff changeset
   226
    val (_, goal, goal_pat, typedef_result) =
13443
1c3327c348b3 typedef: "open" option;
wenzelm
parents: 13413
diff changeset
   227
      prepare_typedef prep_term def name typ set opt_morphs thy;
21352
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
   228
    fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
29062
6f8a100325b6 recovered goal_pat;
wenzelm
parents: 29061
diff changeset
   229
  in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end;
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   230
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   231
in
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   232
28662
64ab5bb68d4c tuned typedef interface
haftmann
parents: 27691
diff changeset
   233
val typedef = gen_typedef Syntax.check_term;
64ab5bb68d4c tuned typedef interface
haftmann
parents: 27691
diff changeset
   234
val typedef_cmd = gen_typedef Syntax.read_term;
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   235
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
   236
end;
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
   237
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
   238
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
   239
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   240
(** outer syntax **)
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   241
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   242
local structure P = OuterParse in
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   243
27353
71c4dd53d4cb moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 26939
diff changeset
   244
val _ = OuterKeyword.keyword "morphisms";
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24861
diff changeset
   245
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   246
val typedef_decl =
16126
3ba9eb7ea366 fixed outer syntax: allow type_args with parentheses;
wenzelm
parents: 15570
diff changeset
   247
  Scan.optional (P.$$$ "(" |--
3ba9eb7ea366 fixed outer syntax: allow type_args with parentheses;
wenzelm
parents: 15570
diff changeset
   248
      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
3ba9eb7ea366 fixed outer syntax: allow type_args with parentheses;
wenzelm
parents: 15570
diff changeset
   249
        --| P.$$$ ")") (true, NONE) --
11744
3a4625eaead0 'morphisms' spec;
wenzelm
parents: 11740
diff changeset
   250
    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
12876
a70df1e5bf10 got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents: 12694
diff changeset
   251
    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
6357
12448b8f92fb named witnesses: PureThy.get_thmss;
wenzelm
parents: 6092
diff changeset
   252
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   253
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
28662
64ab5bb68d4c tuned typedef interface
haftmann
parents: 27691
diff changeset
   254
  typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
6357
12448b8f92fb named witnesses: PureThy.get_thmss;
wenzelm
parents: 6092
diff changeset
   255
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24861
diff changeset
   256
val _ =
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   257
  OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   258
    OuterKeyword.thy_goal
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   259
    (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
6357
12448b8f92fb named witnesses: PureThy.get_thmss;
wenzelm
parents: 6092
diff changeset
   260
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   261
end;
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   262
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   263
25535
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
   264
val setup = TypedefInterpretation.init;
4975b7529a14 interpretation of typedefs
haftmann
parents: 25513
diff changeset
   265
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   266
end;