src/HOL/Tools/typedef_package.ML
changeset 6357 12448b8f92fb
parent 6092 d9db67970c73
child 6383 45bb139e6ceb
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Mar 11 21:56:22 1999 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Mar 11 21:57:34 1999 +0100
     1.3 @@ -2,7 +2,10 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Gordon/HOL style type definitions.
     1.8 +Gordon/HOL-style type definitions.
     1.9 +
    1.10 +TODO:
    1.11 +  - typedefP: elim witness;
    1.12  *)
    1.13  
    1.14  signature TYPEDEF_PACKAGE =
    1.15 @@ -62,14 +65,12 @@
    1.16        if_none usr_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.17    in
    1.18      prove_goalw_cterm [] goal (K [tac])
    1.19 -  end
    1.20 -  handle ERROR =>
    1.21 -    error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset));
    1.22 +  end handle ERROR => error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset));
    1.23  
    1.24  
    1.25  (* gen_add_typedef *)
    1.26  
    1.27 -fun gen_add_typedef prep_term no_def name (t, vs, mx) raw_set axms thms usr_tac thy =
    1.28 +fun gen_add_typedef prep_term no_def name (t, vs, mx) raw_set thm_names thms usr_tac thy =
    1.29    let
    1.30      val _ = Theory.requires thy "Set" "typedefs";
    1.31      val sign = sign_of thy;
    1.32 @@ -131,7 +132,7 @@
    1.33      else error (cat_lines errs);
    1.34  
    1.35      message ("Proving nonemptiness of " ^ quote name ^ " ...");
    1.36 -    prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
    1.37 +    prove_nonempty cset (PureThy.get_thmss thy thm_names @ thms) usr_tac;
    1.38  
    1.39      thy
    1.40      |> PureThy.add_typedecls [(t, vs, mx)]
    1.41 @@ -147,9 +148,7 @@
    1.42       [(Rep_name, rep_type),
    1.43        (Rep_name ^ "_inverse", rep_type_inv),
    1.44        (Abs_name ^ "_inverse", abs_type_inv)]
    1.45 -  end
    1.46 -  handle ERROR =>
    1.47 -    error ("The error(s) above occurred in typedef " ^ quote name);
    1.48 +  end handle ERROR => error ("The error(s) above occurred in typedef " ^ quote name);
    1.49  
    1.50  
    1.51  (* external interfaces *)
    1.52 @@ -165,4 +164,29 @@
    1.53  val add_typedef_i_no_def = gen_add_typedef cert_term true;
    1.54  
    1.55  
    1.56 +(* outer syntax *)
    1.57 +
    1.58 +open OuterParse;
    1.59 +
    1.60 +
    1.61 +val typedeclP =
    1.62 +  OuterSyntax.parser false "typedecl" "HOL type declaration"
    1.63 +    ((type_args -- name -- opt_mixfix) >> (fn ((vs, t), mx) =>
    1.64 +      Toplevel.theory (add_typedecls [(t, vs, mx)])));
    1.65 +
    1.66 +val opt_witness =
    1.67 +  Scan.optional ($$$ "(" |-- !!! (list1 xname --| $$$ ")")) [];
    1.68 +
    1.69 +val typedef_decl =
    1.70 +  Scan.option ($$$ "(" |-- name --| $$$ ")") --
    1.71 +    (type_args -- name) -- opt_infix -- ($$$ "=" |-- term -- opt_witness);
    1.72 +
    1.73 +val typedefP =
    1.74 +  OuterSyntax.parser false "typedef" "HOL type definition"
    1.75 +    (typedef_decl >> (fn (((opt_name, (vs, t)), mx), (A, witn)) =>
    1.76 +      Toplevel.theory (add_typedef (if_none opt_name t) (t, vs, mx) A witn [] None)));
    1.77 +
    1.78 +
    1.79 +val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
    1.80 +
    1.81  end;