src/HOL/Tools/typedef_package.ML
changeset 10280 2626d4e37341
parent 9969 4753185f1dd2
child 10463 474263d29057
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Oct 19 21:23:47 2000 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Oct 19 21:25:15 2000 +0200
     1.3 @@ -26,6 +26,23 @@
     1.4  struct
     1.5  
     1.6  
     1.7 +(** theory context references **)
     1.8 +
     1.9 +val type_definitionN = "subset.type_definition";
    1.10 +val type_definition_def = thm "type_definition_def";
    1.11 +
    1.12 +val Rep = thm "Rep";
    1.13 +val Rep_inverse = thm "Rep_inverse";
    1.14 +val Abs_inverse = thm "Abs_inverse";
    1.15 +val Rep_inject = thm "Rep_inject";
    1.16 +val Abs_inject = thm "Abs_inject";
    1.17 +val Rep_cases = thm "Rep_cases";
    1.18 +val Abs_cases = thm "Abs_cases";
    1.19 +val Rep_induct = thm "Rep_induct";
    1.20 +val Abs_induct = thm "Abs_induct";
    1.21 +
    1.22 +
    1.23 +
    1.24  (** type declarations **)
    1.25  
    1.26  fun add_typedecls decls thy =
    1.27 @@ -101,36 +118,40 @@
    1.28  
    1.29  fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy =
    1.30    let
    1.31 -    val _ = Theory.requires thy "Set" "typedefs";
    1.32 +    val _ = Theory.requires thy "subset" "typedefs";
    1.33      val sign = Theory.sign_of thy;
    1.34 -    val full_name = Sign.full_name sign;
    1.35 +    val full = Sign.full_name sign;
    1.36  
    1.37      (*rhs*)
    1.38 +    val full_name = full name;
    1.39      val cset = prep_term sign vs raw_set;
    1.40      val {T = setT, t = set, ...} = Thm.rep_cterm cset;
    1.41      val rhs_tfrees = term_tfrees set;
    1.42      val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    1.43        error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT));
    1.44 +    val cset_pat = Thm.cterm_of sign (Var ((name, 0), setT));
    1.45  
    1.46      (*lhs*)
    1.47      val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
    1.48      val tname = Syntax.type_name t mx;
    1.49 -    val newT = Type (full_name tname, map TFree lhs_tfrees);
    1.50 +    val full_tname = full tname;
    1.51 +    val newT = Type (full_tname, map TFree lhs_tfrees);
    1.52  
    1.53      val Rep_name = "Rep_" ^ name;
    1.54      val Abs_name = "Abs_" ^ name;
    1.55 -    val setC = Const (full_name name, setT);
    1.56 -    val RepC = Const (full_name Rep_name, newT --> oldT);
    1.57 -    val AbsC = Const (full_name Abs_name, oldT --> newT);
    1.58 +
    1.59 +    val setC = Const (full_name, setT);
    1.60 +    val RepC = Const (full Rep_name, newT --> oldT);
    1.61 +    val AbsC = Const (full Abs_name, oldT --> newT);
    1.62      val x_new = Free ("x", newT);
    1.63      val y_old = Free ("y", oldT);
    1.64 -    val set' = if no_def then set else setC;
    1.65 +
    1.66 +    val set' = if no_def then set else setC;    (* FIXME !?? *)
    1.67  
    1.68 -    (*axioms*)
    1.69 -    val rep_type = HOLogic.mk_Trueprop (HOLogic.mk_mem (RepC $ x_new, set'));
    1.70 -    val rep_type_inv = HOLogic.mk_Trueprop (HOLogic.mk_eq (AbsC $ (RepC $ x_new), x_new));
    1.71 -    val abs_type_inv = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (y_old, set')),
    1.72 -      HOLogic.mk_Trueprop (HOLogic.mk_eq (RepC $ (AbsC $ y_old), y_old)));
    1.73 +    val typedef_name = "type_definition_" ^ name;
    1.74 +    val typedefC =
    1.75 +      Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
    1.76 +    val typedef_prop = HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set');
    1.77  
    1.78      (*theory extender*)
    1.79      fun do_typedef theory =
    1.80 @@ -143,10 +164,26 @@
    1.81           (Abs_name, oldT --> newT, NoSyn)])
    1.82        |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes))
    1.83         [Logic.mk_defpair (setC, set)])
    1.84 -      |> (#1 oo (PureThy.add_axioms_i o map Thm.no_attributes))
    1.85 -       [(Rep_name, rep_type),
    1.86 -        (Rep_name ^ "_inverse", rep_type_inv),
    1.87 -        (Abs_name ^ "_inverse", abs_type_inv)]
    1.88 +      |> PureThy.add_axioms_i [((typedef_name, typedef_prop), [])]
    1.89 +      |> (fn (theory', typedef_ax) =>
    1.90 +        let fun make th = standard (th OF typedef_ax) in
    1.91 +          theory'
    1.92 +          |> (#1 oo PureThy.add_thms)
    1.93 +            ([((Rep_name, make Rep), []),
    1.94 +              ((Rep_name ^ "_inverse", make Rep_inverse), []),
    1.95 +              ((Abs_name ^ "_inverse", make Abs_inverse), [])] @
    1.96 +            (if no_def then [] else
    1.97 +             [((Rep_name ^ "_inject", make Rep_inject), []),
    1.98 +              ((Abs_name ^ "_inject", make Abs_inject), []),
    1.99 +              ((Rep_name ^ "_cases", make Rep_cases),
   1.100 +                [RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]),
   1.101 +              ((Abs_name ^ "_cases", make Abs_cases),
   1.102 +                [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
   1.103 +              ((Rep_name ^ "_induct", make Rep_induct),
   1.104 +                [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
   1.105 +              ((Abs_name ^ "_induct", make Abs_induct),
   1.106 +                [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]))
   1.107 +        end)
   1.108        handle ERROR => err_in_typedef name;
   1.109  
   1.110  
   1.111 @@ -173,7 +210,7 @@
   1.112      val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
   1.113    in
   1.114      if null errs then () else error (cat_lines errs);
   1.115 -    (cset, do_typedef)
   1.116 +    (cset, cset_pat, do_typedef)
   1.117    end handle ERROR => err_in_typedef name;
   1.118  
   1.119  
   1.120 @@ -181,7 +218,7 @@
   1.121  
   1.122  fun gen_add_typedef prep_term no_def name typ set names thms tac thy =
   1.123    let
   1.124 -    val (cset, do_typedef) = prepare_typedef prep_term no_def name typ set thy;
   1.125 +    val (cset, _, do_typedef) = prepare_typedef prep_term no_def name typ set thy;
   1.126      val result = prove_nonempty thy cset (names, thms, tac);
   1.127    in check_nonempty cset result; thy |> do_typedef end;
   1.128  
   1.129 @@ -197,11 +234,13 @@
   1.130  
   1.131  fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
   1.132    let
   1.133 -    val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy;
   1.134 +    val (cset, cset_pat, do_typedef) = prepare_typedef prep_term false name typ set thy;
   1.135      val goal = Thm.term_of (goal_nonempty true cset);
   1.136 +    val goal_pat = Thm.term_of (goal_nonempty true cset_pat);
   1.137    in
   1.138      thy
   1.139 -    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, ([], []))), comment) int
   1.140 +    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef],
   1.141 +      (goal, ([goal_pat], []))), comment) int
   1.142    end;
   1.143  
   1.144  val typedef_proof = gen_typedef_proof read_term;