renamed subtype.ML to typedef.ML
authorclasohm
Thu Feb 01 13:25:40 1996 +0100 (1996-02-01)
changeset 147049b3e075f124
parent 1469 fb9ccf06dfe8
child 1471 b088c0a1f2bd
renamed subtype.ML to typedef.ML
src/HOL/ROOT.ML
src/HOL/subtype.ML
     1.1 --- a/src/HOL/ROOT.ML	Thu Feb 01 12:08:43 1996 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Thu Feb 01 13:25:40 1996 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4  use_thy "Ord";
     1.5  use_thy "subset";
     1.6  use     "hologic.ML";
     1.7 -use     "subtype.ML";
     1.8 +use     "typedef.ML";
     1.9  use_thy "Prod";
    1.10  use_thy "Sum";
    1.11  use_thy "Gfp";
     2.1 --- a/src/HOL/subtype.ML	Thu Feb 01 12:08:43 1996 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,141 +0,0 @@
     2.4 -(*  Title:      HOL/subtype.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Markus Wenzel, TU Muenchen
     2.7 -
     2.8 -Internal interface for subtype definitions.
     2.9 -*)
    2.10 -
    2.11 -signature SUBTYPE =
    2.12 -sig
    2.13 -  val prove_nonempty: cterm -> thm list -> tactic option -> thm
    2.14 -  val add_subtype: string -> string * string list * mixfix ->
    2.15 -    string -> string list -> thm list -> tactic option -> theory -> theory
    2.16 -  val add_subtype_i: string -> string * string list * mixfix ->
    2.17 -    term -> string list -> thm list -> tactic option -> theory -> theory
    2.18 -end;
    2.19 -
    2.20 -structure Subtype: SUBTYPE =
    2.21 -struct
    2.22 -
    2.23 -open Syntax Logic HOLogic;
    2.24 -
    2.25 -
    2.26 -(* prove non-emptyness of a set *)   (*exception ERROR*)
    2.27 -
    2.28 -val is_def = is_equals o #prop o rep_thm;
    2.29 -
    2.30 -fun prove_nonempty cset thms usr_tac =
    2.31 -  let
    2.32 -    val {T = setT, t = set, maxidx, sign} = rep_cterm cset;
    2.33 -    val T = dest_setT setT;
    2.34 -    val goal =
    2.35 -      cterm_of sign (mk_Trueprop (mk_mem (Var (("x", maxidx + 1), T), set)));
    2.36 -    val tac =
    2.37 -      TRY (rewrite_goals_tac (filter is_def thms)) THEN
    2.38 -      TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN
    2.39 -      if_none usr_tac (TRY (ALLGOALS (fast_tac set_cs)));
    2.40 -  in
    2.41 -    prove_goalw_cterm [] goal (K [tac])
    2.42 -  end
    2.43 -  handle ERROR =>
    2.44 -    error ("Failed to prove non-emptyness of " ^ quote (string_of_cterm cset));
    2.45 -
    2.46 -
    2.47 -(* ext_subtype *)
    2.48 -
    2.49 -fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
    2.50 -  let
    2.51 -    val dummy = require_thy thy "Set" "subtype definitions";
    2.52 -    val sign = sign_of thy;
    2.53 -
    2.54 -    (*rhs*)
    2.55 -    val cset = prep_term sign raw_set;
    2.56 -    val {T = setT, t = set, ...} = rep_cterm cset;
    2.57 -    val rhs_tfrees = term_tfrees set;
    2.58 -    val oldT = dest_setT setT handle TYPE _ =>
    2.59 -      error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT));
    2.60 -
    2.61 -    (*lhs*)
    2.62 -    val lhs_tfrees =
    2.63 -      map (fn v => (v, if_none (assoc (rhs_tfrees, v)) termS)) vs;
    2.64 -
    2.65 -    val tname = type_name t mx;
    2.66 -    val tlen = length vs;
    2.67 -    val newT = Type (tname, map TFree lhs_tfrees);
    2.68 -
    2.69 -    val Rep_name = "Rep_" ^ name;
    2.70 -    val Abs_name = "Abs_" ^ name;
    2.71 -    val setC = Const (name, setT);
    2.72 -    val RepC = Const (Rep_name, newT --> oldT);
    2.73 -    val AbsC = Const (Abs_name, oldT --> newT);
    2.74 -    val x_new = Free ("x", newT);
    2.75 -    val y_old = Free ("y", oldT);
    2.76 -
    2.77 -    (*axioms*)
    2.78 -    val rep_type = mk_Trueprop (mk_mem (RepC $ x_new, setC));
    2.79 -    val rep_type_inv = mk_Trueprop (mk_eq (AbsC $ (RepC $ x_new), x_new));
    2.80 -    val abs_type_inv = mk_implies (mk_Trueprop (mk_mem (y_old, setC)),
    2.81 -      mk_Trueprop (mk_eq (RepC $ (AbsC $ y_old), y_old)));
    2.82 -
    2.83 -
    2.84 -    (* errors *)
    2.85 -
    2.86 -    val show_names = commas_quote o map fst;
    2.87 -
    2.88 -    val illegal_vars =
    2.89 -      if null (term_vars set) andalso null (term_tvars set) then []
    2.90 -      else ["Illegal schematic variable(s) on rhs"];
    2.91 -
    2.92 -    val dup_lhs_tfrees =
    2.93 -      (case duplicates lhs_tfrees of [] => []
    2.94 -      | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
    2.95 -
    2.96 -    val extra_rhs_tfrees =
    2.97 -      (case gen_rems (op =) (rhs_tfrees, lhs_tfrees) of [] => []
    2.98 -      | extras => ["Extra type variables on rhs: " ^ show_names extras]);
    2.99 -
   2.100 -    val illegal_frees =
   2.101 -      (case term_frees set of [] => []
   2.102 -      | xs => ["Illegal variables on rhs: " ^ show_names (map dest_Free xs)]);
   2.103 -
   2.104 -    val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
   2.105 -  in
   2.106 -    if null errs then ()
   2.107 -    else error (cat_lines errs);
   2.108 -
   2.109 -    prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
   2.110 -
   2.111 -    thy
   2.112 -    |> add_types [(t, tlen, mx)]
   2.113 -    |> add_arities
   2.114 -     [(tname, replicate tlen logicS, logicS),
   2.115 -      (tname, replicate tlen termS, termS)]
   2.116 -    |> add_consts_i
   2.117 -     [(name, setT, NoSyn),
   2.118 -      (Rep_name, newT --> oldT, NoSyn),
   2.119 -      (Abs_name, oldT --> newT, NoSyn)]
   2.120 -    |> add_defs_i
   2.121 -     [(name ^ "_def", mk_equals (setC, set))]
   2.122 -    |> add_axioms_i
   2.123 -     [(Rep_name, rep_type),
   2.124 -      (Rep_name ^ "_inverse", rep_type_inv),
   2.125 -      (Abs_name ^ "_inverse", abs_type_inv)]
   2.126 -  end
   2.127 -  handle ERROR =>
   2.128 -    error ("The error(s) above occurred in subtype definition " ^ quote name);
   2.129 -
   2.130 -
   2.131 -(* external interfaces *)
   2.132 -
   2.133 -fun cert_term sg tm =
   2.134 -  cterm_of sg tm handle TERM (msg, _) => error msg;
   2.135 -
   2.136 -fun read_term sg str =
   2.137 -  read_cterm sg (str, termTVar);
   2.138 -
   2.139 -val add_subtype = ext_subtype read_term;
   2.140 -val add_subtype_i = ext_subtype cert_term;
   2.141 -
   2.142 -
   2.143 -end;
   2.144 -