src/HOL/Tools/typedef_package.ML
changeset 6383 45bb139e6ceb
parent 6357 12448b8f92fb
child 6690 acbcf8085166
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Mar 17 13:47:34 1999 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Mar 17 13:49:14 1999 +0100
     1.3 @@ -3,22 +3,20 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Gordon/HOL-style type definitions.
     1.7 -
     1.8 -TODO:
     1.9 -  - typedefP: elim witness;
    1.10  *)
    1.11  
    1.12  signature TYPEDEF_PACKAGE =
    1.13  sig
    1.14    val quiet_mode: bool ref
    1.15    val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
    1.16 -  val prove_nonempty: cterm -> thm list -> tactic option -> thm
    1.17    val add_typedef: string -> bstring * string list * mixfix ->
    1.18      string -> string list -> thm list -> tactic option -> theory -> theory
    1.19    val add_typedef_i: string -> bstring * string list * mixfix ->
    1.20      term -> string list -> thm list -> tactic option -> theory -> theory
    1.21    val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
    1.22      term -> string list -> thm list -> tactic option -> theory -> theory
    1.23 +  val typedef_proof: string -> bstring * string list * mixfix -> string -> theory -> ProofHistory.T
    1.24 +  val typedef_proof_i: string -> bstring * string list * mixfix -> term -> theory -> ProofHistory.T
    1.25  end;
    1.26  
    1.27  structure TypedefPackage: TYPEDEF_PACKAGE =
    1.28 @@ -49,44 +47,65 @@
    1.29  fun message s = if ! quiet_mode then () else writeln s;
    1.30  
    1.31  
    1.32 -(* prove non-emptyness of a set *)   (*exception ERROR*)
    1.33 -
    1.34 -val is_def = Logic.is_equals o #prop o rep_thm;
    1.35 +(* non-emptiness of set *)              (*exception ERROR*)
    1.36  
    1.37 -fun prove_nonempty cset thms usr_tac =
    1.38 +fun check_nonempty cset thm =
    1.39    let
    1.40 -    val {T = setT, t = set, maxidx, sign} = rep_cterm cset;
    1.41 +    val {t, sign, maxidx, ...} = Thm.rep_cterm cset;
    1.42 +    val {prop, ...} = Thm.rep_thm (Thm.transfer_sg sign (Drule.standard thm));
    1.43 +    val matches = Pattern.matches (Sign.tsig_of sign);
    1.44 +  in
    1.45 +    (case try (HOLogic.dest_mem o HOLogic.dest_Trueprop) prop of
    1.46 +      None => raise ERROR
    1.47 +    | Some (_, A) => if matches (Logic.incr_indexes ([], maxidx) A, t) then () else raise ERROR)
    1.48 +  end handle ERROR => error ("Bad non-emptiness theorem " ^ Display.string_of_thm thm ^
    1.49 +    "\nfor set " ^ quote (Display.string_of_cterm cset));
    1.50 +
    1.51 +fun goal_nonempty cset =
    1.52 +  let
    1.53 +    val {T = setT, t = A, maxidx, sign} = Thm.rep_cterm cset;
    1.54      val T = HOLogic.dest_setT setT;
    1.55 -    val goal = cterm_of sign
    1.56 -      (HOLogic.mk_Trueprop (HOLogic.mk_mem (Var (("x", maxidx + 1), T), set)));
    1.57 +  in Thm.cterm_of sign (HOLogic.mk_Trueprop (HOLogic.mk_mem (Var (("x", maxidx + 1), T), A))) end;
    1.58 +
    1.59 +fun prove_nonempty thy cset (witn_names, witn_thms, witn_tac) =
    1.60 +  let
    1.61 +    val is_def = Logic.is_equals o #prop o Thm.rep_thm;
    1.62 +    val thms = PureThy.get_thmss thy witn_names @ witn_thms;
    1.63      val tac =
    1.64        TRY (rewrite_goals_tac (filter is_def thms)) THEN
    1.65        TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN
    1.66 -      if_none usr_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.67 +      if_none witn_tac (TRY (ALLGOALS (CLASET' blast_tac)));
    1.68    in
    1.69 -    prove_goalw_cterm [] goal (K [tac])
    1.70 -  end handle ERROR => error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset));
    1.71 +    message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
    1.72 +    prove_goalw_cterm [] (goal_nonempty cset) (K [tac])
    1.73 +  end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    1.74  
    1.75  
    1.76 -(* gen_add_typedef *)
    1.77 +(* prepare_typedef *)
    1.78 +
    1.79 +fun read_term sg used s =
    1.80 +  #1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termTVar));
    1.81  
    1.82 -fun gen_add_typedef prep_term no_def name (t, vs, mx) raw_set thm_names thms usr_tac thy =
    1.83 +fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
    1.84 +
    1.85 +fun err_in_typedef name =
    1.86 +  error ("The error(s) above occurred in typedef " ^ quote name);
    1.87 +
    1.88 +fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy =
    1.89    let
    1.90      val _ = Theory.requires thy "Set" "typedefs";
    1.91 -    val sign = sign_of thy;
    1.92 +    val sign = Theory.sign_of thy;
    1.93      val full_name = Sign.full_name sign;
    1.94  
    1.95      (*rhs*)
    1.96 -    val cset = prep_term sign raw_set;
    1.97 -    val {T = setT, t = set, ...} = rep_cterm cset;
    1.98 +    val cset = prep_term sign vs raw_set;
    1.99 +    val {T = setT, t = set, ...} = Thm.rep_cterm cset;
   1.100      val rhs_tfrees = term_tfrees set;
   1.101      val oldT = HOLogic.dest_setT setT handle TYPE _ =>
   1.102        error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT));
   1.103  
   1.104      (*lhs*)
   1.105 -    val lhs_tfrees =
   1.106 -      map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
   1.107 -
   1.108 +    val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs;
   1.109      val tname = Syntax.type_name t mx;
   1.110      val newT = Type (full_name tname, map TFree lhs_tfrees);
   1.111  
   1.112 @@ -105,6 +124,23 @@
   1.113      val abs_type_inv = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (y_old, set')),
   1.114        HOLogic.mk_Trueprop (HOLogic.mk_eq (RepC $ (AbsC $ y_old), y_old)));
   1.115  
   1.116 +    (*theory extender*)
   1.117 +    fun do_typedef theory =
   1.118 +      theory
   1.119 +      |> Theory.assert_super thy
   1.120 +      |> add_typedecls [(t, vs, mx)]
   1.121 +      |> Theory.add_consts_i
   1.122 +       ((if no_def then [] else [(name, setT, NoSyn)]) @
   1.123 +        [(Rep_name, newT --> oldT, NoSyn),
   1.124 +         (Abs_name, oldT --> newT, NoSyn)])
   1.125 +      |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes)
   1.126 +       [Logic.mk_defpair (setC, set)])
   1.127 +      |> (PureThy.add_axioms_i o map Thm.no_attributes)
   1.128 +       [(Rep_name, rep_type),
   1.129 +        (Rep_name ^ "_inverse", rep_type_inv),
   1.130 +        (Abs_name ^ "_inverse", abs_type_inv)]
   1.131 +      handle ERROR => err_in_typedef name;
   1.132 +
   1.133  
   1.134      (* errors *)
   1.135  
   1.136 @@ -128,65 +164,66 @@
   1.137  
   1.138      val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
   1.139    in
   1.140 -    if null errs then ()
   1.141 -    else error (cat_lines errs);
   1.142 -
   1.143 -    message ("Proving nonemptiness of " ^ quote name ^ " ...");
   1.144 -    prove_nonempty cset (PureThy.get_thmss thy thm_names @ thms) usr_tac;
   1.145 -
   1.146 -    thy
   1.147 -    |> PureThy.add_typedecls [(t, vs, mx)]
   1.148 -    |> Theory.add_arities_i
   1.149 -     [(full_name tname, replicate (length vs) HOLogic.termS, HOLogic.termS)]
   1.150 -    |> Theory.add_consts_i
   1.151 -     ((if no_def then [] else [(name, setT, NoSyn)]) @
   1.152 -      [(Rep_name, newT --> oldT, NoSyn),
   1.153 -       (Abs_name, oldT --> newT, NoSyn)])
   1.154 -    |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes)
   1.155 -     [(name ^ "_def", Logic.mk_equals (setC, set))])
   1.156 -    |> (PureThy.add_axioms_i o map Thm.no_attributes)
   1.157 -     [(Rep_name, rep_type),
   1.158 -      (Rep_name ^ "_inverse", rep_type_inv),
   1.159 -      (Abs_name ^ "_inverse", abs_type_inv)]
   1.160 -  end handle ERROR => error ("The error(s) above occurred in typedef " ^ quote name);
   1.161 +    if null errs then () else error (cat_lines errs);
   1.162 +    (cset, do_typedef)
   1.163 +  end handle ERROR => err_in_typedef name;
   1.164  
   1.165  
   1.166 -(* external interfaces *)
   1.167 +(* add_typedef interfaces *)
   1.168  
   1.169 -fun read_term sg str =
   1.170 -  read_cterm sg (str, HOLogic.termTVar);
   1.171 -
   1.172 -fun cert_term sg tm =
   1.173 -  cterm_of sg tm handle TERM (msg, _) => error msg;
   1.174 +fun gen_add_typedef prep_term no_def name typ set names thms tac thy =
   1.175 +  let
   1.176 +    val (cset, do_typedef) = prepare_typedef prep_term no_def name typ set thy;
   1.177 +    val result = prove_nonempty thy cset (names, thms, tac);
   1.178 +  in check_nonempty cset result; thy |> do_typedef end;
   1.179  
   1.180  val add_typedef = gen_add_typedef read_term false;
   1.181  val add_typedef_i = gen_add_typedef cert_term false;
   1.182  val add_typedef_i_no_def = gen_add_typedef cert_term true;
   1.183  
   1.184  
   1.185 -(* outer syntax *)
   1.186 +(* typedef_proof interface *)
   1.187 +
   1.188 +fun typedef_attribute cset do_typedef (thy, thm) =
   1.189 +  (check_nonempty cset thm; (thy |> do_typedef, thm));
   1.190  
   1.191 -open OuterParse;
   1.192 +fun gen_typedef_proof prep_term name typ set thy =
   1.193 +  let
   1.194 +    val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy;
   1.195 +    val goal = Thm.term_of (goal_nonempty cset);
   1.196 +  in
   1.197 +    thy
   1.198 +    |> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, [])
   1.199 +  end;
   1.200 +
   1.201 +val typedef_proof = gen_typedef_proof read_term;
   1.202 +val typedef_proof_i = gen_typedef_proof cert_term;
   1.203  
   1.204  
   1.205 +
   1.206 +(** outer syntax **)
   1.207 +
   1.208 +local open OuterParse in
   1.209 +
   1.210  val typedeclP =
   1.211 -  OuterSyntax.parser false "typedecl" "HOL type declaration"
   1.212 -    ((type_args -- name -- opt_mixfix) >> (fn ((vs, t), mx) =>
   1.213 +  OuterSyntax.command "typedecl" "HOL type declaration"
   1.214 +    (type_args -- name -- opt_mixfix >> (fn ((vs, t), mx) =>
   1.215        Toplevel.theory (add_typedecls [(t, vs, mx)])));
   1.216  
   1.217 -val opt_witness =
   1.218 -  Scan.optional ($$$ "(" |-- !!! (list1 xname --| $$$ ")")) [];
   1.219 +val typedef_proof_decl =
   1.220 +  Scan.option ($$$ "(" |-- name --| $$$ ")") --
   1.221 +    (type_args -- name) -- opt_infix -- ($$$ "=" |-- term);
   1.222  
   1.223 -val typedef_decl =
   1.224 -  Scan.option ($$$ "(" |-- name --| $$$ ")") --
   1.225 -    (type_args -- name) -- opt_infix -- ($$$ "=" |-- term -- opt_witness);
   1.226 +fun mk_typedef_proof (((opt_name, (vs, t)), mx), A) =
   1.227 +  typedef_proof (if_none opt_name (Syntax.type_name t mx)) (t, vs, mx) A;
   1.228  
   1.229  val typedefP =
   1.230 -  OuterSyntax.parser false "typedef" "HOL type definition"
   1.231 -    (typedef_decl >> (fn (((opt_name, (vs, t)), mx), (A, witn)) =>
   1.232 -      Toplevel.theory (add_typedef (if_none opt_name t) (t, vs, mx) A witn [] None)));
   1.233 -
   1.234 +  OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
   1.235 +    (typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof)));
   1.236  
   1.237  val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
   1.238  
   1.239  end;
   1.240 +
   1.241 +
   1.242 +end;