author | wenzelm |
Sat, 17 Oct 2009 16:58:03 +0200 | |
changeset 32970 | fbd2bb2489a8 |
parent 32966 | 5b21661fe618 |
child 33314 | 53d49370f7af |
permissions | -rw-r--r-- |
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30345
diff
changeset
|
1 |
(* Title: HOL/Tools/typedef.ML |
16458 | 2 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
4866 | 3 |
|
21352 | 4 |
Gordon/HOL-style type definitions: create a new syntactic type |
5 |
represented by a non-empty subset. |
|
4866 | 6 |
*) |
7 |
||
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30345
diff
changeset
|
8 |
signature TYPEDEF = |
4866 | 9 |
sig |
19705 | 10 |
type info = |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
11 |
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
12 |
type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
13 |
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
14 |
Rep_induct: thm, Abs_induct: thm} |
30345 | 15 |
val add_typedef: bool -> binding option -> binding * string list * mixfix -> |
16 |
term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory |
|
17 |
val typedef: (bool * binding) * (binding * string list * mixfix) * term |
|
18 |
* (binding * binding) option -> theory -> Proof.state |
|
19 |
val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string |
|
20 |
* (binding * binding) option -> theory -> Proof.state |
|
31735 | 21 |
val get_info: theory -> string -> info option |
25513 | 22 |
val interpretation: (string -> theory -> theory) -> theory -> theory |
25535 | 23 |
val setup: theory -> theory |
4866 | 24 |
end; |
25 |
||
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
30345
diff
changeset
|
26 |
structure Typedef: TYPEDEF = |
4866 | 27 |
struct |
28 |
||
17922 | 29 |
(** type definitions **) |
30 |
||
31 |
(* theory data *) |
|
15259 | 32 |
|
19705 | 33 |
type info = |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
34 |
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
35 |
type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
36 |
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
37 |
Rep_induct: thm, Abs_induct: thm}; |
19459 | 38 |
|
16458 | 39 |
structure TypedefData = TheoryDataFun |
22846 | 40 |
( |
19705 | 41 |
type T = info Symtab.table; |
15259 | 42 |
val empty = Symtab.empty; |
43 |
val copy = I; |
|
16458 | 44 |
val extend = I; |
19617 | 45 |
fun merge _ tabs : T = Symtab.merge (K true) tabs; |
22846 | 46 |
); |
15259 | 47 |
|
19705 | 48 |
val get_info = Symtab.lookup o TypedefData.get; |
49 |
fun put_info name info = TypedefData.map (Symtab.update (name, info)); |
|
15259 | 50 |
|
51 |
||
6383 | 52 |
(* prepare_typedef *) |
53 |
||
21352 | 54 |
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); |
55 |
||
25535 | 56 |
structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =); |
57 |
val interpretation = TypedefInterpretation.interpretation; |
|
58 |
||
11822 | 59 |
fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy = |
4866 | 60 |
let |
11608 | 61 |
val _ = Theory.requires thy "Typedef" "typedefs"; |
21352 | 62 |
val ctxt = ProofContext.init thy; |
30345 | 63 |
|
64 |
val full = Sign.full_name thy; |
|
65 |
val full_name = full name; |
|
66 |
val bname = Binding.name_of name; |
|
4866 | 67 |
|
68 |
(*rhs*) |
|
21352 | 69 |
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; |
70 |
val setT = Term.fastype_of set; |
|
17280 | 71 |
val rhs_tfrees = Term.add_tfrees set []; |
72 |
val rhs_tfreesT = Term.add_tfreesT setT []; |
|
4866 | 73 |
val oldT = HOLogic.dest_setT setT handle TYPE _ => |
24920 | 74 |
error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); |
4866 | 75 |
|
76 |
(*lhs*) |
|
17280 | 77 |
val defS = Sign.defaultS thy; |
19473 | 78 |
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; |
17280 | 79 |
val args_setT = lhs_tfrees |
80 |
|> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT)) |
|
81 |
|> map TFree; |
|
82 |
||
30345 | 83 |
val tname = Binding.map_name (Syntax.type_name mx) t; |
10280 | 84 |
val full_tname = full tname; |
85 |
val newT = Type (full_tname, map TFree lhs_tfrees); |
|
4866 | 86 |
|
30345 | 87 |
val (Rep_name, Abs_name) = |
88 |
(case opt_morphs of |
|
89 |
NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) |
|
90 |
| SOME morphs => morphs); |
|
19391 | 91 |
val setT' = map Term.itselfT args_setT ---> setT; |
17280 | 92 |
val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT); |
10280 | 93 |
val RepC = Const (full Rep_name, newT --> oldT); |
94 |
val AbsC = Const (full Abs_name, oldT --> newT); |
|
95 |
||
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
96 |
(*inhabitance*) |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
97 |
fun mk_inhabited A = |
29054
6f61794f1ff7
logically separate typedef axiomatization from constant definition
krauss
parents:
29053
diff
changeset
|
98 |
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A))); |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
99 |
val set' = if def then setC else set; |
29062 | 100 |
val goal' = mk_inhabited set'; |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
101 |
val goal = mk_inhabited set; |
30345 | 102 |
val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT)); |
4866 | 103 |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
104 |
(*axiomatization*) |
30345 | 105 |
val typedef_name = Binding.prefix_name "type_definition_" name; |
10280 | 106 |
val typedefC = |
29056 | 107 |
Const (@{const_name type_definition}, |
108 |
(newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT); |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
109 |
val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); |
30345 | 110 |
val typedef_deps = Term.add_consts set' []; |
4866 | 111 |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
112 |
(*set definition*) |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
113 |
fun add_def theory = |
29056 | 114 |
if def then |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
115 |
theory |
29053 | 116 |
|> Sign.add_consts_i [(name, setT', NoSyn)] |
29579 | 117 |
|> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name) |
118 |
(PrimitiveDefs.mk_defpair (setC, set)))] |
|
19705 | 119 |
|-> (fn [th] => pair (SOME th)) |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
120 |
else (NONE, theory); |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
121 |
fun contract_def NONE th = th |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
122 |
| contract_def (SOME def_eq) th = |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
123 |
let |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
124 |
val cert = Thm.cterm_of (Thm.theory_of_thm def_eq); |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
125 |
val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal'); |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
126 |
in Drule.standard (Drule.equal_elim_rule2 OF [goal_eq, th]) end; |
18358 | 127 |
|
29056 | 128 |
fun typedef_result inhabited = |
25495 | 129 |
ObjectLogic.typedecl (t, vs, mx) |
25458
ba8f5e4fa336
separated typedecl module, providing typedecl command with interpretation
haftmann
parents:
24926
diff
changeset
|
130 |
#> snd |
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
131 |
#> Sign.add_consts_i |
6383 | 132 |
[(Rep_name, newT --> oldT, NoSyn), |
29053 | 133 |
(Abs_name, oldT --> newT, NoSyn)] |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
134 |
#> add_def |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
135 |
#-> (fn set_def => |
30345 | 136 |
PureThy.add_axioms [((typedef_name, typedef_prop), |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
137 |
[Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])] |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
138 |
##>> pair set_def) |
21352 | 139 |
##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
140 |
##> Theory.add_deps "" (dest_Const AbsC) typedef_deps |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
141 |
#-> (fn ([type_definition], set_def) => fn thy1 => |
11822 | 142 |
let |
143 |
fun make th = Drule.standard (th OF [type_definition]); |
|
18377 | 144 |
val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, |
19705 | 145 |
Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) = |
146 |
thy1 |
|
30345 | 147 |
|> Sign.add_path (Binding.name_of name) |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12043
diff
changeset
|
148 |
|> PureThy.add_thms |
30345 | 149 |
[((Rep_name, make @{thm type_definition.Rep}), []), |
150 |
((Binding.suffix_name "_inverse" Rep_name, make @{thm type_definition.Rep_inverse}), []), |
|
151 |
((Binding.suffix_name "_inverse" Abs_name, make @{thm type_definition.Abs_inverse}), []), |
|
152 |
((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []), |
|
153 |
((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []), |
|
154 |
((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}), |
|
155 |
[RuleCases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]), |
|
156 |
((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}), |
|
157 |
[RuleCases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]), |
|
158 |
((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}), |
|
159 |
[RuleCases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]), |
|
160 |
((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}), |
|
161 |
[RuleCases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])] |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
162 |
||> Sign.parent_path; |
19705 | 163 |
val info = {rep_type = oldT, abs_type = newT, |
164 |
Rep_name = full Rep_name, Abs_name = full Abs_name, |
|
28848 | 165 |
inhabited = inhabited, type_definition = type_definition, set_def = set_def, |
19705 | 166 |
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, |
167 |
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, |
|
11822 | 168 |
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; |
25535 | 169 |
in |
170 |
thy2 |
|
171 |
|> put_info full_tname info |
|
172 |
|> TypedefInterpretation.data full_tname |
|
173 |
|> pair (full_tname, info) |
|
174 |
end); |
|
6383 | 175 |
|
29056 | 176 |
|
4866 | 177 |
(* errors *) |
178 |
||
179 |
fun show_names pairs = commas_quote (map fst pairs); |
|
180 |
||
181 |
val illegal_vars = |
|
29264 | 182 |
if null (Term.add_vars set []) andalso null (Term.add_tvars set []) then [] |
4866 | 183 |
else ["Illegal schematic variable(s) on rhs"]; |
184 |
||
185 |
val dup_lhs_tfrees = |
|
18964 | 186 |
(case duplicates (op =) lhs_tfrees of [] => [] |
4866 | 187 |
| dups => ["Duplicate type variables on lhs: " ^ show_names dups]); |
188 |
||
189 |
val extra_rhs_tfrees = |
|
17280 | 190 |
(case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => [] |
4866 | 191 |
| extras => ["Extra type variables on rhs: " ^ show_names extras]); |
192 |
||
193 |
val illegal_frees = |
|
29264 | 194 |
(case Term.add_frees set [] of [] => [] |
195 |
| xs => ["Illegal variables on rhs: " ^ show_names xs]); |
|
4866 | 196 |
|
197 |
val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees; |
|
11426
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
198 |
val _ = if null errs then () else error (cat_lines errs); |
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
199 |
|
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
200 |
(*test theory errors now!*) |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
201 |
val test_thy = Theory.copy thy; |
32970
fbd2bb2489a8
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
wenzelm
parents:
32966
diff
changeset
|
202 |
val _ = typedef_result (Skip_Proof.make_thm test_thy goal) test_thy; |
11426
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
203 |
|
29062 | 204 |
in (set, goal, goal_pat, typedef_result) end |
30345 | 205 |
handle ERROR msg => |
206 |
cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name)); |
|
4866 | 207 |
|
208 |
||
29056 | 209 |
(* add_typedef: tactic interface *) |
4866 | 210 |
|
28662 | 211 |
fun add_typedef def opt_name typ set opt_morphs tac thy = |
6383 | 212 |
let |
17922 | 213 |
val name = the_default (#1 typ) opt_name; |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
214 |
val (set, goal, _, typedef_result) = |
28662 | 215 |
prepare_typedef Syntax.check_term def name typ set opt_morphs thy; |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
216 |
val inhabited = Goal.prove_global thy [] [] goal (K tac) |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
217 |
handle ERROR msg => cat_error msg |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
218 |
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
219 |
in typedef_result inhabited thy end; |
4866 | 220 |
|
17339 | 221 |
|
29056 | 222 |
(* typedef: proof interface *) |
6383 | 223 |
|
17339 | 224 |
local |
225 |
||
226 |
fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy = |
|
11822 | 227 |
let |
29062 | 228 |
val (_, goal, goal_pat, typedef_result) = |
13443 | 229 |
prepare_typedef prep_term def name typ set opt_morphs thy; |
21352 | 230 |
fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th); |
29062 | 231 |
in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end; |
17339 | 232 |
|
233 |
in |
|
6383 | 234 |
|
28662 | 235 |
val typedef = gen_typedef Syntax.check_term; |
236 |
val typedef_cmd = gen_typedef Syntax.read_term; |
|
17339 | 237 |
|
19705 | 238 |
end; |
15259 | 239 |
|
240 |
||
241 |
||
6383 | 242 |
(** outer syntax **) |
243 |
||
29056 | 244 |
local structure P = OuterParse in |
6383 | 245 |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26939
diff
changeset
|
246 |
val _ = OuterKeyword.keyword "morphisms"; |
24867 | 247 |
|
17339 | 248 |
val typedef_decl = |
16126
3ba9eb7ea366
fixed outer syntax: allow type_args with parentheses;
wenzelm
parents:
15570
diff
changeset
|
249 |
Scan.optional (P.$$$ "(" |-- |
30345 | 250 |
((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s))) |
16126
3ba9eb7ea366
fixed outer syntax: allow type_args with parentheses;
wenzelm
parents:
15570
diff
changeset
|
251 |
--| P.$$$ ")") (true, NONE) -- |
30345 | 252 |
(P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- |
253 |
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)); |
|
6357 | 254 |
|
17339 | 255 |
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = |
30345 | 256 |
typedef_cmd ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), |
257 |
(t, vs, mx), A, morphs); |
|
6357 | 258 |
|
24867 | 259 |
val _ = |
29056 | 260 |
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" |
261 |
OuterKeyword.thy_goal |
|
17339 | 262 |
(typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef))); |
6357 | 263 |
|
29056 | 264 |
end; |
265 |
||
266 |
||
25535 | 267 |
val setup = TypedefInterpretation.init; |
268 |
||
4866 | 269 |
end; |