src/HOL/Tools/typedef_package.ML
author wenzelm
Wed Jun 25 17:38:32 2008 +0200 (2008-06-25)
changeset 27353 71c4dd53d4cb
parent 26939 1035c89b4c02
child 27691 ce171cbd4b93
permissions -rw-r--r--
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
     1 (*  Title:      HOL/Tools/typedef_package.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     4 
     5 Gordon/HOL-style type definitions: create a new syntactic type
     6 represented by a non-empty subset.
     7 *)
     8 
     9 signature TYPEDEF_PACKAGE =
    10 sig
    11   type info =
    12    {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
    13     type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    14     Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm,
    15     Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
    16   val get_info: theory -> string -> info option
    17   val add_typedef: bool -> string option -> bstring * string list * mixfix ->
    18     string -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
    19   val add_typedef_i: bool -> string option -> bstring * string list * mixfix ->
    20     term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
    21   val typedef: (bool * string) * (bstring * string list * mixfix) * string
    22     * (string * string) option -> theory -> Proof.state
    23   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
    24     * (string * string) option -> theory -> Proof.state
    25   val interpretation: (string -> theory -> theory) -> theory -> theory
    26   val setup: theory -> theory
    27 end;
    28 
    29 structure TypedefPackage: TYPEDEF_PACKAGE =
    30 struct
    31 
    32 (** theory context references **)
    33 
    34 val type_definitionN = "Typedef.type_definition";
    35 
    36 val Rep = thm "type_definition.Rep";
    37 val Rep_inverse = thm "type_definition.Rep_inverse";
    38 val Abs_inverse = thm "type_definition.Abs_inverse";
    39 val Rep_inject = thm "type_definition.Rep_inject";
    40 val Abs_inject = thm "type_definition.Abs_inject";
    41 val Rep_cases = thm "type_definition.Rep_cases";
    42 val Abs_cases = thm "type_definition.Abs_cases";
    43 val Rep_induct = thm "type_definition.Rep_induct";
    44 val Abs_induct = thm "type_definition.Abs_induct";
    45 
    46 
    47 
    48 (** type definitions **)
    49 
    50 (* theory data *)
    51 
    52 type info =
    53  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
    54   type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    55   Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm,
    56   Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
    57 
    58 structure TypedefData = TheoryDataFun
    59 (
    60   type T = info Symtab.table;
    61   val empty = Symtab.empty;
    62   val copy = I;
    63   val extend = I;
    64   fun merge _ tabs : T = Symtab.merge (K true) tabs;
    65 );
    66 
    67 val get_info = Symtab.lookup o TypedefData.get;
    68 fun put_info name info = TypedefData.map (Symtab.update (name, info));
    69 
    70 
    71 (* prepare_typedef *)
    72 
    73 fun err_in_typedef msg name =
    74   cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
    75 
    76 fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
    77 
    78 structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
    79 val interpretation = TypedefInterpretation.interpretation;
    80 
    81 fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
    82   let
    83     val _ = Theory.requires thy "Typedef" "typedefs";
    84     val ctxt = ProofContext.init thy;
    85     val full = Sign.full_name thy;
    86 
    87     (*rhs*)
    88     val full_name = full name;
    89     val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
    90     val setT = Term.fastype_of set;
    91     val rhs_tfrees = Term.add_tfrees set [];
    92     val rhs_tfreesT = Term.add_tfreesT setT [];
    93     val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    94       error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
    95     fun mk_nonempty A =
    96       HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
    97     val goal = mk_nonempty set;
    98     val goal_pat = mk_nonempty (Var (the_default (name, 0) (Syntax.read_variable name), setT));
    99 
   100     (*lhs*)
   101     val defS = Sign.defaultS thy;
   102     val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
   103     val args_setT = lhs_tfrees
   104       |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
   105       |> map TFree;
   106 
   107     val tname = Syntax.type_name t mx;
   108     val full_tname = full tname;
   109     val newT = Type (full_tname, map TFree lhs_tfrees);
   110 
   111     val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
   112     val setT' = map Term.itselfT args_setT ---> setT;
   113     val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
   114     val RepC = Const (full Rep_name, newT --> oldT);
   115     val AbsC = Const (full Abs_name, oldT --> newT);
   116     val x_new = Free ("x", newT);
   117     val y_old = Free ("y", oldT);
   118 
   119     val set' = if def then setC else set;
   120 
   121     val typedef_name = "type_definition_" ^ name;
   122     val typedefC =
   123       Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
   124     val typedef_prop =
   125       Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
   126     val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
   127 
   128     fun add_def eq thy =
   129       if def then
   130         thy
   131         |> PureThy.add_defs_i false [Thm.no_attributes eq]
   132         |-> (fn [th] => pair (SOME th))
   133       else (NONE, thy);
   134 
   135     fun typedef_result nonempty =
   136       ObjectLogic.typedecl (t, vs, mx)
   137       #> snd
   138       #> Sign.add_consts_i
   139        ((if def then [(name, setT', NoSyn)] else []) @
   140         [(Rep_name, newT --> oldT, NoSyn),
   141          (Abs_name, oldT --> newT, NoSyn)])
   142       #> add_def (PrimitiveDefs.mk_defpair (setC, set))
   143       ##>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
   144           [apsnd (fn cond_axm => nonempty RS cond_axm)])]
   145       ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
   146       ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
   147       #-> (fn (set_def, [type_definition]) => fn thy1 =>
   148         let
   149           fun make th = Drule.standard (th OF [type_definition]);
   150           val abs_inject = make Abs_inject;
   151           val abs_inverse = make Abs_inverse;
   152           val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
   153               Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
   154             thy1
   155             |> Sign.add_path name
   156             |> PureThy.add_thms
   157               ([((Rep_name, make Rep), []),
   158                 ((Rep_name ^ "_inverse", make Rep_inverse), []),
   159                 ((Abs_name ^ "_inverse", abs_inverse), []),
   160                 ((Rep_name ^ "_inject", make Rep_inject), []),
   161                 ((Abs_name ^ "_inject", abs_inject), []),
   162                 ((Rep_name ^ "_cases", make Rep_cases),
   163                   [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
   164                 ((Abs_name ^ "_cases", make Abs_cases),
   165                   [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
   166                 ((Rep_name ^ "_induct", make Rep_induct),
   167                   [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
   168                 ((Abs_name ^ "_induct", make Abs_induct),
   169                   [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
   170             ||> Sign.parent_path;
   171           val info = {rep_type = oldT, abs_type = newT,
   172             Rep_name = full Rep_name, Abs_name = full Abs_name,
   173               type_definition = type_definition, set_def = set_def,
   174               Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
   175               Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
   176             Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
   177         in
   178           thy2
   179           |> put_info full_tname info
   180           |> TypedefInterpretation.data full_tname
   181           |> pair (full_tname, info)
   182         end);
   183 
   184 
   185     (* errors *)
   186 
   187     fun show_names pairs = commas_quote (map fst pairs);
   188 
   189     val illegal_vars =
   190       if null (term_vars set) andalso null (term_tvars set) then []
   191       else ["Illegal schematic variable(s) on rhs"];
   192 
   193     val dup_lhs_tfrees =
   194       (case duplicates (op =) lhs_tfrees of [] => []
   195       | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
   196 
   197     val extra_rhs_tfrees =
   198       (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => []
   199       | extras => ["Extra type variables on rhs: " ^ show_names extras]);
   200 
   201     val illegal_frees =
   202       (case term_frees set of [] => []
   203       | xs => ["Illegal variables on rhs: " ^ show_names (map dest_Free xs)]);
   204 
   205     val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
   206     val _ = if null errs then () else error (cat_lines errs);
   207 
   208     (*test theory errors now!*)
   209     val test_thy = Theory.copy thy;
   210     val _ = test_thy
   211       |> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal);
   212 
   213   in (set, goal, goal_pat, typedef_result) end
   214   handle ERROR msg => err_in_typedef msg name;
   215 
   216 
   217 (* add_typedef interfaces *)
   218 
   219 local
   220 
   221 fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
   222   let
   223     val name = the_default (#1 typ) opt_name;
   224     val (set, goal, _, typedef_result) =
   225       prepare_typedef prep_term def name typ set opt_morphs thy;
   226     val non_empty = Goal.prove_global thy [] [] goal (K tac)
   227       handle ERROR msg => cat_error msg
   228         ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
   229   in typedef_result non_empty thy end;
   230 
   231 in
   232 
   233 val add_typedef = gen_typedef Syntax.read_term;
   234 val add_typedef_i = gen_typedef Syntax.check_term;
   235 
   236 end;
   237 
   238 
   239 (* Isar typedef interface *)
   240 
   241 local
   242 
   243 fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy =
   244   let
   245     val (_, goal, goal_pat, typedef_result) =
   246       prepare_typedef prep_term def name typ set opt_morphs thy;
   247     fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
   248   in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end;
   249 
   250 in
   251 
   252 val typedef = gen_typedef Syntax.read_term;
   253 val typedef_i = gen_typedef Syntax.check_term;
   254 
   255 end;
   256 
   257 
   258 
   259 (** outer syntax **)
   260 
   261 local structure P = OuterParse and K = OuterKeyword in
   262 
   263 val _ = OuterKeyword.keyword "morphisms";
   264 
   265 val typedef_decl =
   266   Scan.optional (P.$$$ "(" |--
   267       ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
   268         --| P.$$$ ")") (true, NONE) --
   269     (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
   270     Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
   271 
   272 fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
   273   typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
   274 
   275 val _ =
   276   OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
   277     (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
   278 
   279 val setup = TypedefInterpretation.init;
   280 
   281 end;
   282 
   283 end;