wenzelm@4866
|
1 |
(* Title: HOL/Tools/typedef_package.ML
|
wenzelm@4866
|
2 |
ID: $Id$
|
wenzelm@4866
|
3 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@9230
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
wenzelm@4866
|
5 |
|
wenzelm@6357
|
6 |
Gordon/HOL-style type definitions.
|
wenzelm@4866
|
7 |
*)
|
wenzelm@4866
|
8 |
|
wenzelm@4866
|
9 |
signature TYPEDEF_PACKAGE =
|
wenzelm@4866
|
10 |
sig
|
wenzelm@5697
|
11 |
val quiet_mode: bool ref
|
wenzelm@5104
|
12 |
val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
|
wenzelm@11822
|
13 |
val add_typedef_x: string -> bstring * string list * mixfix ->
|
wenzelm@4866
|
14 |
string -> string list -> thm list -> tactic option -> theory -> theory
|
wenzelm@11827
|
15 |
val add_typedef: bool -> string option -> bstring * string list * mixfix ->
|
wenzelm@11822
|
16 |
string -> (bstring * bstring) option -> tactic -> theory -> theory *
|
wenzelm@11822
|
17 |
{type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
|
wenzelm@11822
|
18 |
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
|
wenzelm@11822
|
19 |
Rep_induct: thm, Abs_induct: thm}
|
wenzelm@11827
|
20 |
val add_typedef_i: bool -> string option -> bstring * string list * mixfix ->
|
wenzelm@11822
|
21 |
term -> (bstring * bstring) option -> tactic -> theory -> theory *
|
wenzelm@11822
|
22 |
{type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
|
wenzelm@11822
|
23 |
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
|
wenzelm@11822
|
24 |
Rep_induct: thm, Abs_induct: thm}
|
wenzelm@13443
|
25 |
val typedef_proof: (bool * string) * (bstring * string list * mixfix) * string
|
wenzelm@13443
|
26 |
* (string * string) option -> bool -> theory -> ProofHistory.T
|
wenzelm@13443
|
27 |
val typedef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
|
wenzelm@13443
|
28 |
* (string * string) option -> bool -> theory -> ProofHistory.T
|
wenzelm@4866
|
29 |
end;
|
wenzelm@4866
|
30 |
|
wenzelm@4866
|
31 |
structure TypedefPackage: TYPEDEF_PACKAGE =
|
wenzelm@4866
|
32 |
struct
|
wenzelm@4866
|
33 |
|
wenzelm@4866
|
34 |
|
wenzelm@10280
|
35 |
(** theory context references **)
|
wenzelm@10280
|
36 |
|
wenzelm@11608
|
37 |
val type_definitionN = "Typedef.type_definition";
|
wenzelm@10280
|
38 |
|
wenzelm@13413
|
39 |
val Rep = thm "type_definition.Rep";
|
wenzelm@13413
|
40 |
val Rep_inverse = thm "type_definition.Rep_inverse";
|
wenzelm@13413
|
41 |
val Abs_inverse = thm "type_definition.Abs_inverse";
|
wenzelm@13413
|
42 |
val Rep_inject = thm "type_definition.Rep_inject";
|
wenzelm@13413
|
43 |
val Abs_inject = thm "type_definition.Abs_inject";
|
wenzelm@13413
|
44 |
val Rep_cases = thm "type_definition.Rep_cases";
|
wenzelm@13413
|
45 |
val Abs_cases = thm "type_definition.Abs_cases";
|
wenzelm@13413
|
46 |
val Rep_induct = thm "type_definition.Rep_induct";
|
wenzelm@13413
|
47 |
val Abs_induct = thm "type_definition.Abs_induct";
|
wenzelm@10280
|
48 |
|
wenzelm@10280
|
49 |
|
wenzelm@10280
|
50 |
|
wenzelm@5104
|
51 |
(** type declarations **)
|
wenzelm@5104
|
52 |
|
wenzelm@5104
|
53 |
fun add_typedecls decls thy =
|
wenzelm@5104
|
54 |
let
|
wenzelm@5104
|
55 |
val full = Sign.full_name (Theory.sign_of thy);
|
wenzelm@5104
|
56 |
|
wenzelm@5104
|
57 |
fun arity_of (raw_name, args, mx) =
|
wenzelm@12338
|
58 |
(full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS);
|
wenzelm@5104
|
59 |
in
|
wenzelm@8141
|
60 |
if can (Theory.assert_super HOL.thy) thy then
|
wenzelm@8141
|
61 |
thy
|
wenzelm@8141
|
62 |
|> PureThy.add_typedecls decls
|
wenzelm@8141
|
63 |
|> Theory.add_arities_i (map arity_of decls)
|
wenzelm@8141
|
64 |
else thy |> PureThy.add_typedecls decls
|
wenzelm@5104
|
65 |
end;
|
wenzelm@5104
|
66 |
|
wenzelm@5104
|
67 |
|
wenzelm@5104
|
68 |
|
wenzelm@5104
|
69 |
(** type definitions **)
|
wenzelm@5104
|
70 |
|
wenzelm@5697
|
71 |
(* messages *)
|
wenzelm@5697
|
72 |
|
wenzelm@5697
|
73 |
val quiet_mode = ref false;
|
wenzelm@5697
|
74 |
fun message s = if ! quiet_mode then () else writeln s;
|
wenzelm@5697
|
75 |
|
wenzelm@5697
|
76 |
|
wenzelm@11426
|
77 |
(* prove_nonempty -- tactical version *) (*exception ERROR*)
|
wenzelm@4866
|
78 |
|
wenzelm@11827
|
79 |
fun prove_nonempty thy cset goal (witn1_tac, witn_names, witn_thms, witn2_tac) =
|
wenzelm@6383
|
80 |
let
|
wenzelm@6383
|
81 |
val is_def = Logic.is_equals o #prop o Thm.rep_thm;
|
wenzelm@6383
|
82 |
val thms = PureThy.get_thmss thy witn_names @ witn_thms;
|
wenzelm@4866
|
83 |
val tac =
|
wenzelm@11827
|
84 |
witn1_tac THEN
|
wenzelm@4866
|
85 |
TRY (rewrite_goals_tac (filter is_def thms)) THEN
|
wenzelm@4866
|
86 |
TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN
|
wenzelm@11827
|
87 |
if_none witn2_tac (TRY (ALLGOALS (CLASET' blast_tac)));
|
wenzelm@4866
|
88 |
in
|
wenzelm@6383
|
89 |
message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
|
wenzelm@11968
|
90 |
Tactic.prove (Theory.sign_of thy) [] [] goal (K tac)
|
wenzelm@6383
|
91 |
end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
|
wenzelm@4866
|
92 |
|
wenzelm@4866
|
93 |
|
wenzelm@6383
|
94 |
(* prepare_typedef *)
|
wenzelm@4866
|
95 |
|
wenzelm@6383
|
96 |
fun read_term sg used s =
|
wenzelm@12338
|
97 |
#1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.typeT));
|
wenzelm@6383
|
98 |
|
wenzelm@6383
|
99 |
fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg;
|
wenzelm@6383
|
100 |
|
wenzelm@6383
|
101 |
fun err_in_typedef name =
|
wenzelm@6383
|
102 |
error ("The error(s) above occurred in typedef " ^ quote name);
|
wenzelm@6383
|
103 |
|
wenzelm@11822
|
104 |
fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
|
wenzelm@4866
|
105 |
let
|
wenzelm@11608
|
106 |
val _ = Theory.requires thy "Typedef" "typedefs";
|
wenzelm@6383
|
107 |
val sign = Theory.sign_of thy;
|
wenzelm@10280
|
108 |
val full = Sign.full_name sign;
|
wenzelm@4866
|
109 |
|
wenzelm@4866
|
110 |
(*rhs*)
|
wenzelm@10280
|
111 |
val full_name = full name;
|
wenzelm@6383
|
112 |
val cset = prep_term sign vs raw_set;
|
wenzelm@6383
|
113 |
val {T = setT, t = set, ...} = Thm.rep_cterm cset;
|
wenzelm@4866
|
114 |
val rhs_tfrees = term_tfrees set;
|
wenzelm@4866
|
115 |
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
|
wenzelm@4866
|
116 |
error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT));
|
wenzelm@11426
|
117 |
fun mk_nonempty A =
|
wenzelm@11426
|
118 |
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
|
wenzelm@11426
|
119 |
val goal = mk_nonempty set;
|
wenzelm@11744
|
120 |
val vname = take_suffix Symbol.is_digit (Symbol.explode name)
|
wenzelm@11744
|
121 |
|> apfst implode |> apsnd (#1 o Term.read_int);
|
wenzelm@11744
|
122 |
val goal_pat = mk_nonempty (Var (vname, setT));
|
wenzelm@4866
|
123 |
|
wenzelm@4866
|
124 |
(*lhs*)
|
wenzelm@12338
|
125 |
val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.typeS)) vs;
|
wenzelm@4866
|
126 |
val tname = Syntax.type_name t mx;
|
wenzelm@10280
|
127 |
val full_tname = full tname;
|
wenzelm@10280
|
128 |
val newT = Type (full_tname, map TFree lhs_tfrees);
|
wenzelm@4866
|
129 |
|
wenzelm@11744
|
130 |
val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name);
|
wenzelm@10280
|
131 |
val setC = Const (full_name, setT);
|
wenzelm@10280
|
132 |
val RepC = Const (full Rep_name, newT --> oldT);
|
wenzelm@10280
|
133 |
val AbsC = Const (full Abs_name, oldT --> newT);
|
wenzelm@4866
|
134 |
val x_new = Free ("x", newT);
|
wenzelm@4866
|
135 |
val y_old = Free ("y", oldT);
|
wenzelm@4866
|
136 |
|
wenzelm@11822
|
137 |
val set' = if def then setC else set;
|
wenzelm@10280
|
138 |
|
wenzelm@10280
|
139 |
val typedef_name = "type_definition_" ^ name;
|
wenzelm@10280
|
140 |
val typedefC =
|
wenzelm@10280
|
141 |
Const (type_definitionN, (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
|
wenzelm@11426
|
142 |
val typedef_prop =
|
wenzelm@11426
|
143 |
Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
|
wenzelm@4866
|
144 |
|
wenzelm@11822
|
145 |
fun typedef_result (theory, nonempty) =
|
wenzelm@6383
|
146 |
theory
|
wenzelm@6383
|
147 |
|> add_typedecls [(t, vs, mx)]
|
wenzelm@6383
|
148 |
|> Theory.add_consts_i
|
wenzelm@11822
|
149 |
((if def then [(name, setT, NoSyn)] else []) @
|
wenzelm@6383
|
150 |
[(Rep_name, newT --> oldT, NoSyn),
|
wenzelm@6383
|
151 |
(Abs_name, oldT --> newT, NoSyn)])
|
wenzelm@11822
|
152 |
|> (if def then (apsnd (Some o hd) oo (PureThy.add_defs_i false o map Thm.no_attributes))
|
wenzelm@11822
|
153 |
[Logic.mk_defpair (setC, set)]
|
wenzelm@11822
|
154 |
else rpair None)
|
wenzelm@14570
|
155 |
|>>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
|
wenzelm@11727
|
156 |
[apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
|
wenzelm@14570
|
157 |
|>> Theory.add_finals_i false [RepC, AbsC]
|
wenzelm@14570
|
158 |
|> (fn (theory', (set_def, [type_definition])) =>
|
wenzelm@11822
|
159 |
let
|
wenzelm@11822
|
160 |
fun make th = Drule.standard (th OF [type_definition]);
|
wenzelm@11822
|
161 |
val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
|
wenzelm@11822
|
162 |
Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
|
wenzelm@12338
|
163 |
theory'
|
wenzelm@12338
|
164 |
|> Theory.add_path name
|
wenzelm@12338
|
165 |
|> PureThy.add_thms
|
wenzelm@11822
|
166 |
([((Rep_name, make Rep), []),
|
wenzelm@11822
|
167 |
((Rep_name ^ "_inverse", make Rep_inverse), []),
|
wenzelm@11822
|
168 |
((Abs_name ^ "_inverse", make Abs_inverse), []),
|
wenzelm@11822
|
169 |
((Rep_name ^ "_inject", make Rep_inject), []),
|
wenzelm@11822
|
170 |
((Abs_name ^ "_inject", make Abs_inject), []),
|
wenzelm@11822
|
171 |
((Rep_name ^ "_cases", make Rep_cases),
|
wenzelm@11822
|
172 |
[RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]),
|
wenzelm@11822
|
173 |
((Abs_name ^ "_cases", make Abs_cases),
|
wenzelm@11822
|
174 |
[RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
|
wenzelm@11822
|
175 |
((Rep_name ^ "_induct", make Rep_induct),
|
wenzelm@11822
|
176 |
[RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
|
wenzelm@11822
|
177 |
((Abs_name ^ "_induct", make Abs_induct),
|
wenzelm@12338
|
178 |
[RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])
|
wenzelm@12338
|
179 |
|>> Theory.parent_path;
|
wenzelm@11822
|
180 |
val result = {type_definition = type_definition, set_def = set_def,
|
wenzelm@11822
|
181 |
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
|
wenzelm@11822
|
182 |
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
|
wenzelm@11822
|
183 |
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
|
wenzelm@11822
|
184 |
in ((theory'', type_definition), result) end);
|
wenzelm@6383
|
185 |
|
wenzelm@4866
|
186 |
|
wenzelm@4866
|
187 |
(* errors *)
|
wenzelm@4866
|
188 |
|
wenzelm@4866
|
189 |
fun show_names pairs = commas_quote (map fst pairs);
|
wenzelm@4866
|
190 |
|
wenzelm@4866
|
191 |
val illegal_vars =
|
wenzelm@4866
|
192 |
if null (term_vars set) andalso null (term_tvars set) then []
|
wenzelm@4866
|
193 |
else ["Illegal schematic variable(s) on rhs"];
|
wenzelm@4866
|
194 |
|
wenzelm@4866
|
195 |
val dup_lhs_tfrees =
|
wenzelm@4866
|
196 |
(case duplicates lhs_tfrees of [] => []
|
wenzelm@4866
|
197 |
| dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
|
wenzelm@4866
|
198 |
|
wenzelm@4866
|
199 |
val extra_rhs_tfrees =
|
wenzelm@4866
|
200 |
(case gen_rems (op =) (rhs_tfrees, lhs_tfrees) of [] => []
|
wenzelm@4866
|
201 |
| extras => ["Extra type variables on rhs: " ^ show_names extras]);
|
wenzelm@4866
|
202 |
|
wenzelm@4866
|
203 |
val illegal_frees =
|
wenzelm@4866
|
204 |
(case term_frees set of [] => []
|
wenzelm@4866
|
205 |
| xs => ["Illegal variables on rhs: " ^ show_names (map dest_Free xs)]);
|
wenzelm@4866
|
206 |
|
wenzelm@4866
|
207 |
val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
|
wenzelm@11426
|
208 |
val _ = if null errs then () else error (cat_lines errs);
|
wenzelm@11426
|
209 |
|
wenzelm@11426
|
210 |
(*test theory errors now!*)
|
wenzelm@11426
|
211 |
val test_thy = Theory.copy thy;
|
wenzelm@11727
|
212 |
val _ = (test_thy,
|
wenzelm@11822
|
213 |
setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result;
|
wenzelm@11426
|
214 |
|
wenzelm@11822
|
215 |
in (cset, goal, goal_pat, typedef_result) end
|
wenzelm@11426
|
216 |
handle ERROR => err_in_typedef name;
|
wenzelm@4866
|
217 |
|
wenzelm@4866
|
218 |
|
wenzelm@6383
|
219 |
(* add_typedef interfaces *)
|
wenzelm@4866
|
220 |
|
wenzelm@11827
|
221 |
fun gen_typedef prep_term def name typ set opt_morphs tac1 names thms tac2 thy =
|
wenzelm@6383
|
222 |
let
|
wenzelm@11822
|
223 |
val (cset, goal, _, typedef_result) =
|
wenzelm@11822
|
224 |
prepare_typedef prep_term def name typ set opt_morphs thy;
|
wenzelm@11827
|
225 |
val non_empty = prove_nonempty thy cset goal (tac1, names, thms, tac2);
|
wenzelm@11822
|
226 |
val ((thy', _), result) = (thy, non_empty) |> typedef_result;
|
wenzelm@11822
|
227 |
in (thy', result) end;
|
wenzelm@4866
|
228 |
|
wenzelm@11827
|
229 |
fun sane_typedef prep_term def opt_name typ set opt_morphs tac =
|
wenzelm@11827
|
230 |
gen_typedef prep_term def
|
wenzelm@11827
|
231 |
(if_none opt_name (#1 typ)) typ set opt_morphs all_tac [] [] (Some tac);
|
wenzelm@11822
|
232 |
|
wenzelm@11822
|
233 |
fun add_typedef_x name typ set names thms tac =
|
wenzelm@11827
|
234 |
#1 o gen_typedef read_term true name typ set None (Tactic.rtac exI 1) names thms tac;
|
wenzelm@11822
|
235 |
|
wenzelm@11822
|
236 |
val add_typedef = sane_typedef read_term;
|
wenzelm@11822
|
237 |
val add_typedef_i = sane_typedef cert_term;
|
wenzelm@4866
|
238 |
|
wenzelm@4866
|
239 |
|
wenzelm@6383
|
240 |
(* typedef_proof interface *)
|
wenzelm@6357
|
241 |
|
wenzelm@13443
|
242 |
fun gen_typedef_proof prep_term ((def, name), typ, set, opt_morphs) int thy =
|
wenzelm@11822
|
243 |
let
|
wenzelm@11822
|
244 |
val (_, goal, goal_pat, att_result) =
|
wenzelm@13443
|
245 |
prepare_typedef prep_term def name typ set opt_morphs thy;
|
wenzelm@11822
|
246 |
val att = #1 o att_result;
|
wenzelm@12876
|
247 |
in thy |> IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([goal_pat], []))) int end;
|
wenzelm@6383
|
248 |
|
wenzelm@6383
|
249 |
val typedef_proof = gen_typedef_proof read_term;
|
wenzelm@6383
|
250 |
val typedef_proof_i = gen_typedef_proof cert_term;
|
wenzelm@6383
|
251 |
|
wenzelm@6383
|
252 |
|
wenzelm@6383
|
253 |
|
wenzelm@6383
|
254 |
(** outer syntax **)
|
wenzelm@6383
|
255 |
|
wenzelm@6723
|
256 |
local structure P = OuterParse and K = OuterSyntax.Keyword in
|
wenzelm@6357
|
257 |
|
wenzelm@6357
|
258 |
val typedeclP =
|
wenzelm@12624
|
259 |
OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl
|
wenzelm@12876
|
260 |
(P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) =>
|
wenzelm@6357
|
261 |
Toplevel.theory (add_typedecls [(t, vs, mx)])));
|
wenzelm@6357
|
262 |
|
wenzelm@6723
|
263 |
|
wenzelm@6383
|
264 |
val typedef_proof_decl =
|
wenzelm@13443
|
265 |
Scan.optional (P.$$$ "(" |-- P.!!!
|
wenzelm@13443
|
266 |
(((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, Some s)))
|
wenzelm@13443
|
267 |
--| P.$$$ ")")) (true, None) --
|
wenzelm@11744
|
268 |
(P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
|
wenzelm@12876
|
269 |
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
|
wenzelm@6357
|
270 |
|
wenzelm@13443
|
271 |
fun mk_typedef_proof ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
|
wenzelm@13443
|
272 |
typedef_proof ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
|
wenzelm@6357
|
273 |
|
wenzelm@6357
|
274 |
val typedefP =
|
wenzelm@6723
|
275 |
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
|
wenzelm@6383
|
276 |
(typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof)));
|
wenzelm@6357
|
277 |
|
wenzelm@6723
|
278 |
|
wenzelm@11744
|
279 |
val _ = OuterSyntax.add_keywords ["morphisms"];
|
wenzelm@6357
|
280 |
val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
|
wenzelm@6357
|
281 |
|
wenzelm@4866
|
282 |
end;
|
wenzelm@6383
|
283 |
|
wenzelm@6383
|
284 |
end;
|