src/HOL/Tools/typedef_package.ML
changeset 13443 1c3327c348b3
parent 13413 0b60b9e18a26
child 14570 0bf4e84bf51d
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Aug 02 11:12:34 2002 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Aug 02 11:49:55 2002 +0200
     1.3 @@ -22,10 +22,10 @@
     1.4      {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
     1.5        Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
     1.6        Rep_induct: thm, Abs_induct: thm}
     1.7 -  val typedef_proof: string * (bstring * string list * mixfix) * string * (string * string) option
     1.8 -    -> bool -> theory -> ProofHistory.T
     1.9 -  val typedef_proof_i: string * (bstring * string list * mixfix) * term * (string * string) option
    1.10 -    -> bool -> theory -> ProofHistory.T
    1.11 +  val typedef_proof: (bool * string) * (bstring * string list * mixfix) * string
    1.12 +    * (string * string) option -> bool -> theory -> ProofHistory.T
    1.13 +  val typedef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
    1.14 +    * (string * string) option -> bool -> theory -> ProofHistory.T
    1.15  end;
    1.16  
    1.17  structure TypedefPackage: TYPEDEF_PACKAGE =
    1.18 @@ -238,10 +238,10 @@
    1.19  
    1.20  (* typedef_proof interface *)
    1.21  
    1.22 -fun gen_typedef_proof prep_term (name, typ, set, opt_morphs) int thy =
    1.23 +fun gen_typedef_proof prep_term ((def, name), typ, set, opt_morphs) int thy =
    1.24    let
    1.25      val (_, goal, goal_pat, att_result) =
    1.26 -      prepare_typedef prep_term true name typ set opt_morphs thy;
    1.27 +      prepare_typedef prep_term def name typ set opt_morphs thy;
    1.28      val att = #1 o att_result;
    1.29    in thy |> IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([goal_pat], []))) int end;
    1.30  
    1.31 @@ -261,12 +261,14 @@
    1.32  
    1.33  
    1.34  val typedef_proof_decl =
    1.35 -  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
    1.36 +  Scan.optional (P.$$$ "(" |-- P.!!!
    1.37 +      (((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, Some s)))
    1.38 +        --| P.$$$ ")")) (true, None) --
    1.39      (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
    1.40      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
    1.41  
    1.42 -fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), morphs) =
    1.43 -  typedef_proof (if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs);
    1.44 +fun mk_typedef_proof ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
    1.45 +  typedef_proof ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
    1.46  
    1.47  val typedefP =
    1.48    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal