src/HOL/Tools/typedef_package.ML
changeset 4866 72a46bd00c8d
child 4932 c90411dde8e8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Apr 29 11:39:52 1998 +0200
     1.3 @@ -0,0 +1,140 @@
     1.4 +(*  Title:      HOL/Tools/typedef_package.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Gordon/HOL style type definitions.
     1.9 +*)
    1.10 +
    1.11 +signature TYPEDEF_PACKAGE =
    1.12 +sig
    1.13 +  val prove_nonempty: cterm -> thm list -> tactic option -> thm
    1.14 +  val add_typedef: string -> bstring * string list * mixfix ->
    1.15 +    string -> string list -> thm list -> tactic option -> theory -> theory
    1.16 +  val add_typedef_i: string -> bstring * string list * mixfix ->
    1.17 +    term -> string list -> thm list -> tactic option -> theory -> theory
    1.18 +end;
    1.19 +
    1.20 +structure TypedefPackage: TYPEDEF_PACKAGE =
    1.21 +struct
    1.22 +
    1.23 +
    1.24 +(* prove non-emptyness of a set *)   (*exception ERROR*)
    1.25 +
    1.26 +val is_def = Logic.is_equals o #prop o rep_thm;
    1.27 +
    1.28 +fun prove_nonempty cset thms usr_tac =
    1.29 +  let
    1.30 +    val {T = setT, t = set, maxidx, sign} = rep_cterm cset;
    1.31 +    val T = HOLogic.dest_setT setT;
    1.32 +    val goal = cterm_of sign
    1.33 +      (HOLogic.mk_Trueprop (HOLogic.mk_mem (Var (("x", maxidx + 1), T), set)));
    1.34 +    val tac =
    1.35 +      TRY (rewrite_goals_tac (filter is_def thms)) THEN
    1.36 +      TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN
    1.37 +      if_none usr_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.38 +  in
    1.39 +    prove_goalw_cterm [] goal (K [tac])
    1.40 +  end
    1.41 +  handle ERROR =>
    1.42 +    error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset));
    1.43 +
    1.44 +
    1.45 +(* gen_add_typedef *)
    1.46 +
    1.47 +fun gen_add_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
    1.48 +  let
    1.49 +    val _ = Theory.require thy "Set" "typedefs";
    1.50 +    val sign = sign_of thy;
    1.51 +    val full_name = Sign.full_name sign;
    1.52 +
    1.53 +    (*rhs*)
    1.54 +    val cset = prep_term sign raw_set;
    1.55 +    val {T = setT, t = set, ...} = rep_cterm cset;
    1.56 +    val rhs_tfrees = term_tfrees set;
    1.57 +    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
    1.58 +      error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT));
    1.59 +
    1.60 +    (*lhs*)
    1.61 +    val lhs_tfrees =
    1.62 +      map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
    1.63 +
    1.64 +    val tname = Syntax.type_name t mx;
    1.65 +    val tlen = length vs;
    1.66 +    val newT = Type (full_name tname, map TFree lhs_tfrees);
    1.67 +
    1.68 +    val Rep_name = "Rep_" ^ name;
    1.69 +    val Abs_name = "Abs_" ^ name;
    1.70 +    val setC = Const (full_name name, setT);
    1.71 +    val RepC = Const (full_name Rep_name, newT --> oldT);
    1.72 +    val AbsC = Const (full_name Abs_name, oldT --> newT);
    1.73 +    val x_new = Free ("x", newT);
    1.74 +    val y_old = Free ("y", oldT);
    1.75 +
    1.76 +    (*axioms*)
    1.77 +    val rep_type = HOLogic.mk_Trueprop (HOLogic.mk_mem (RepC $ x_new, setC));
    1.78 +    val rep_type_inv = HOLogic.mk_Trueprop (HOLogic.mk_eq (AbsC $ (RepC $ x_new), x_new));
    1.79 +    val abs_type_inv = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (y_old, setC)),
    1.80 +      HOLogic.mk_Trueprop (HOLogic.mk_eq (RepC $ (AbsC $ y_old), y_old)));
    1.81 +
    1.82 +
    1.83 +    (* errors *)
    1.84 +
    1.85 +    fun show_names pairs = commas_quote (map fst pairs);
    1.86 +
    1.87 +    val illegal_vars =
    1.88 +      if null (term_vars set) andalso null (term_tvars set) then []
    1.89 +      else ["Illegal schematic variable(s) on rhs"];
    1.90 +
    1.91 +    val dup_lhs_tfrees =
    1.92 +      (case duplicates lhs_tfrees of [] => []
    1.93 +      | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
    1.94 +
    1.95 +    val extra_rhs_tfrees =
    1.96 +      (case gen_rems (op =) (rhs_tfrees, lhs_tfrees) of [] => []
    1.97 +      | extras => ["Extra type variables on rhs: " ^ show_names extras]);
    1.98 +
    1.99 +    val illegal_frees =
   1.100 +      (case term_frees set of [] => []
   1.101 +      | xs => ["Illegal variables on rhs: " ^ show_names (map dest_Free xs)]);
   1.102 +
   1.103 +    val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
   1.104 +  in
   1.105 +    if null errs then ()
   1.106 +    else error (cat_lines errs);
   1.107 +
   1.108 +    writeln("Proving nonemptiness of " ^ quote name ^ " ...");
   1.109 +    prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
   1.110 +
   1.111 +    thy
   1.112 +    |> Theory.add_types [(t, tlen, mx)]
   1.113 +    |> Theory.add_arities_i
   1.114 +     [(full_name tname, replicate tlen logicS, logicS),
   1.115 +      (full_name tname, replicate tlen HOLogic.termS, HOLogic.termS)]
   1.116 +    |> Theory.add_consts_i
   1.117 +     [(name, setT, NoSyn),
   1.118 +      (Rep_name, newT --> oldT, NoSyn),
   1.119 +      (Abs_name, oldT --> newT, NoSyn)]
   1.120 +    |> (PureThy.add_defs_i o map Attribute.none)
   1.121 +     [(name ^ "_def", Logic.mk_equals (setC, set))]
   1.122 +    |> (PureThy.add_axioms_i o map Attribute.none)
   1.123 +     [(Rep_name, rep_type),
   1.124 +      (Rep_name ^ "_inverse", rep_type_inv),
   1.125 +      (Abs_name ^ "_inverse", abs_type_inv)]
   1.126 +  end
   1.127 +  handle ERROR =>
   1.128 +    error ("The error(s) above occurred in typedef " ^ quote name);
   1.129 +
   1.130 +
   1.131 +(* external interfaces *)
   1.132 +
   1.133 +fun read_term sg str =
   1.134 +  read_cterm sg (str, HOLogic.termTVar);
   1.135 +
   1.136 +fun cert_term sg tm =
   1.137 +  cterm_of sg tm handle TERM (msg, _) => error msg;
   1.138 +
   1.139 +val add_typedef = gen_add_typedef read_term;
   1.140 +val add_typedef_i = gen_add_typedef cert_term;
   1.141 +
   1.142 +
   1.143 +end;