src/HOL/Tools/typedef_package.ML
changeset 11744 3a4625eaead0
parent 11740 86ac4189a1c1
child 11807 50a36627e6d6
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Oct 13 21:43:00 2001 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Oct 13 21:44:58 2001 +0200
     1.3 @@ -16,9 +16,11 @@
     1.4      term -> string list -> thm list -> tactic option -> theory -> theory
     1.5    val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
     1.6      term -> string list -> thm list -> tactic option -> theory -> theory
     1.7 -  val typedef_proof: (string * (bstring * string list * mixfix) * string) * Comment.text
     1.8 +  val typedef_proof:
     1.9 +    (string * (bstring * string list * mixfix) * string * (string * string) option) * Comment.text
    1.10      -> bool -> theory -> ProofHistory.T
    1.11 -  val typedef_proof_i: (string * (bstring * string list * mixfix) * term) * Comment.text
    1.12 +  val typedef_proof_i:
    1.13 +    (string * (bstring * string list * mixfix) * term * (string * string) option) * Comment.text
    1.14      -> bool -> theory -> ProofHistory.T
    1.15  end;
    1.16  
    1.17 @@ -96,7 +98,7 @@
    1.18  fun err_in_typedef name =
    1.19    error ("The error(s) above occurred in typedef " ^ quote name);
    1.20  
    1.21 -fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy =
    1.22 +fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set opt_morphs thy =
    1.23    let
    1.24      val _ = Theory.requires thy "Typedef" "typedefs";
    1.25      val sign = Theory.sign_of thy;
    1.26 @@ -112,7 +114,9 @@
    1.27      fun mk_nonempty A =
    1.28        HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
    1.29      val goal = mk_nonempty set;
    1.30 -    val goal_pat = mk_nonempty (Var ((name, 0), setT));
    1.31 +    val vname = take_suffix Symbol.is_digit (Symbol.explode name)
    1.32 +      |> apfst implode |> apsnd (#1 o Term.read_int);
    1.33 +    val goal_pat = mk_nonempty (Var (vname, setT));
    1.34  
    1.35      (*lhs*)
    1.36      val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
    1.37 @@ -120,9 +124,7 @@
    1.38      val full_tname = full tname;
    1.39      val newT = Type (full_tname, map TFree lhs_tfrees);
    1.40  
    1.41 -    val Rep_name = "Rep_" ^ name;
    1.42 -    val Abs_name = "Abs_" ^ name;
    1.43 -
    1.44 +    val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name);
    1.45      val setC = Const (full_name, setT);
    1.46      val RepC = Const (full Rep_name, newT --> oldT);
    1.47      val AbsC = Const (full Abs_name, oldT --> newT);
    1.48 @@ -204,7 +206,7 @@
    1.49  
    1.50  fun gen_add_typedef prep_term no_def name typ set names thms tac thy =
    1.51    let
    1.52 -    val (cset, goal, _, typedef_att) = prepare_typedef prep_term no_def name typ set thy;
    1.53 +    val (cset, goal, _, typedef_att) = prepare_typedef prep_term no_def name typ set None thy;
    1.54      val result = prove_nonempty thy cset goal (names, thms, tac);
    1.55    in (thy, result) |> typedef_att |> #1 end;
    1.56  
    1.57 @@ -215,10 +217,10 @@
    1.58  
    1.59  (* typedef_proof interface *)
    1.60  
    1.61 -fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
    1.62 -  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set thy in
    1.63 -    thy
    1.64 -    |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
    1.65 +fun gen_typedef_proof prep_term ((name, typ, set, opt_morphs), comment) int thy =
    1.66 +  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set opt_morphs thy in
    1.67 +    thy |>
    1.68 +    IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
    1.69    end;
    1.70  
    1.71  val typedef_proof = gen_typedef_proof read_term;
    1.72 @@ -238,16 +240,19 @@
    1.73  
    1.74  val typedef_proof_decl =
    1.75    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
    1.76 -    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- P.marg_comment;
    1.77 +    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
    1.78 +    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)) --
    1.79 +    P.marg_comment;
    1.80  
    1.81 -fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), comment) =
    1.82 -  typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A), comment);
    1.83 +fun mk_typedef_proof (((((opt_name, (vs, t)), mx), A), morphs), comment) =
    1.84 +  typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs), comment);
    1.85  
    1.86  val typedefP =
    1.87    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
    1.88      (typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof)));
    1.89  
    1.90  
    1.91 +val _ = OuterSyntax.add_keywords ["morphisms"];
    1.92  val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
    1.93  
    1.94  end;