author | wenzelm |
Thu, 01 Jan 2009 23:31:49 +0100 | |
changeset 29302 | eb782d1dc07c |
parent 29264 | 4ea3358fac3f |
child 29579 | cb520b766e00 |
permissions | -rw-r--r-- |
4866 | 1 |
(* Title: HOL/Tools/typedef_package.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 |
||
8 |
signature TYPEDEF_PACKAGE = |
|
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} |
19705 | 15 |
val get_info: theory -> string -> info option |
11827 | 16 |
val add_typedef: bool -> string option -> bstring * string list * mixfix -> |
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20462
diff
changeset
|
17 |
term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory |
28662 | 18 |
val typedef: (bool * string) * (bstring * string list * mixfix) * term |
17339 | 19 |
* (string * string) option -> theory -> Proof.state |
28662 | 20 |
val typedef_cmd: (bool * string) * (bstring * string list * mixfix) * string |
17339 | 21 |
* (string * string) option -> theory -> Proof.state |
25513 | 22 |
val interpretation: (string -> theory -> theory) -> theory -> theory |
25535 | 23 |
val setup: theory -> theory |
4866 | 24 |
end; |
25 |
||
26 |
structure TypedefPackage: TYPEDEF_PACKAGE = |
|
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 |
||
18678 | 54 |
fun err_in_typedef msg name = |
55 |
cat_error msg ("The error(s) above occurred in typedef " ^ quote name); |
|
6383 | 56 |
|
21352 | 57 |
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); |
58 |
||
25535 | 59 |
structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =); |
60 |
val interpretation = TypedefInterpretation.interpretation; |
|
61 |
||
11822 | 62 |
fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy = |
4866 | 63 |
let |
11608 | 64 |
val _ = Theory.requires thy "Typedef" "typedefs"; |
21352 | 65 |
val ctxt = ProofContext.init thy; |
28965 | 66 |
val full = Sign.full_bname thy; |
4866 | 67 |
|
68 |
(*rhs*) |
|
10280 | 69 |
val full_name = full name; |
21352 | 70 |
val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; |
71 |
val setT = Term.fastype_of set; |
|
17280 | 72 |
val rhs_tfrees = Term.add_tfrees set []; |
73 |
val rhs_tfreesT = Term.add_tfreesT setT []; |
|
4866 | 74 |
val oldT = HOLogic.dest_setT setT handle TYPE _ => |
24920 | 75 |
error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); |
4866 | 76 |
|
77 |
(*lhs*) |
|
17280 | 78 |
val defS = Sign.defaultS thy; |
19473 | 79 |
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; |
17280 | 80 |
val args_setT = lhs_tfrees |
81 |
|> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT)) |
|
82 |
|> map TFree; |
|
83 |
||
4866 | 84 |
val tname = Syntax.type_name t mx; |
10280 | 85 |
val full_tname = full tname; |
86 |
val newT = Type (full_tname, map TFree lhs_tfrees); |
|
4866 | 87 |
|
19473 | 88 |
val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs; |
19391 | 89 |
val setT' = map Term.itselfT args_setT ---> setT; |
17280 | 90 |
val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT); |
10280 | 91 |
val RepC = Const (full Rep_name, newT --> oldT); |
92 |
val AbsC = Const (full Abs_name, oldT --> newT); |
|
93 |
||
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
94 |
(*inhabitance*) |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
95 |
fun mk_inhabited A = |
29054
6f61794f1ff7
logically separate typedef axiomatization from constant definition
krauss
parents:
29053
diff
changeset
|
96 |
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
|
97 |
val set' = if def then setC else set; |
29062 | 98 |
val goal' = mk_inhabited set'; |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
99 |
val goal = mk_inhabited set; |
29062 | 100 |
val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT)); |
4866 | 101 |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
102 |
(*axiomatization*) |
10280 | 103 |
val typedef_name = "type_definition_" ^ name; |
104 |
val typedefC = |
|
29056 | 105 |
Const (@{const_name type_definition}, |
106 |
(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
|
107 |
val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
108 |
val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' []; |
4866 | 109 |
|
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
110 |
(*set definition*) |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
111 |
fun add_def theory = |
29056 | 112 |
if def then |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
113 |
theory |
29053 | 114 |
|> Sign.add_consts_i [(name, setT', NoSyn)] |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
115 |
|> PureThy.add_defs false [Thm.no_attributes ((PrimitiveDefs.mk_defpair (setC, set)))] |
19705 | 116 |
|-> (fn [th] => pair (SOME th)) |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
117 |
else (NONE, theory); |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
118 |
fun contract_def NONE th = th |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
119 |
| contract_def (SOME def_eq) th = |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
120 |
let |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
121 |
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
|
122 |
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
|
123 |
in Drule.standard (Drule.equal_elim_rule2 OF [goal_eq, th]) end; |
18358 | 124 |
|
29056 | 125 |
fun typedef_result inhabited = |
25495 | 126 |
ObjectLogic.typedecl (t, vs, mx) |
25458
ba8f5e4fa336
separated typedecl module, providing typedecl command with interpretation
haftmann
parents:
24926
diff
changeset
|
127 |
#> snd |
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
128 |
#> Sign.add_consts_i |
6383 | 129 |
[(Rep_name, newT --> oldT, NoSyn), |
29053 | 130 |
(Abs_name, oldT --> newT, NoSyn)] |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
131 |
#> add_def |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
132 |
#-> (fn set_def => |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
133 |
PureThy.add_axioms [((typedef_name, typedef_prop), |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
134 |
[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
|
135 |
##>> pair set_def) |
21352 | 136 |
##> Theory.add_deps "" (dest_Const RepC) typedef_deps |
137 |
##> 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
|
138 |
#-> (fn ([type_definition], set_def) => fn thy1 => |
11822 | 139 |
let |
140 |
fun make th = Drule.standard (th OF [type_definition]); |
|
18377 | 141 |
val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, |
19705 | 142 |
Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) = |
143 |
thy1 |
|
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
144 |
|> Sign.add_path name |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12043
diff
changeset
|
145 |
|> PureThy.add_thms |
29056 | 146 |
([((Rep_name, make @{thm type_definition.Rep}), []), |
147 |
((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []), |
|
148 |
((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []), |
|
149 |
((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []), |
|
150 |
((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []), |
|
151 |
((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}), |
|
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24830
diff
changeset
|
152 |
[RuleCases.case_names [Rep_name], Induct.cases_pred full_name]), |
29056 | 153 |
((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}), |
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24712
diff
changeset
|
154 |
[RuleCases.case_names [Abs_name], Induct.cases_type full_tname]), |
29056 | 155 |
((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}), |
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24830
diff
changeset
|
156 |
[RuleCases.case_names [Rep_name], Induct.induct_pred full_name]), |
29056 | 157 |
((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}), |
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24712
diff
changeset
|
158 |
[RuleCases.case_names [Abs_name], Induct.induct_type full_tname])]) |
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset
|
159 |
||> Sign.parent_path; |
19705 | 160 |
val info = {rep_type = oldT, abs_type = newT, |
161 |
Rep_name = full Rep_name, Abs_name = full Abs_name, |
|
28848 | 162 |
inhabited = inhabited, type_definition = type_definition, set_def = set_def, |
19705 | 163 |
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, |
164 |
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, |
|
11822 | 165 |
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; |
25535 | 166 |
in |
167 |
thy2 |
|
168 |
|> put_info full_tname info |
|
169 |
|> TypedefInterpretation.data full_tname |
|
170 |
|> pair (full_tname, info) |
|
171 |
end); |
|
6383 | 172 |
|
29056 | 173 |
|
4866 | 174 |
(* errors *) |
175 |
||
176 |
fun show_names pairs = commas_quote (map fst pairs); |
|
177 |
||
178 |
val illegal_vars = |
|
29264 | 179 |
if null (Term.add_vars set []) andalso null (Term.add_tvars set []) then [] |
4866 | 180 |
else ["Illegal schematic variable(s) on rhs"]; |
181 |
||
182 |
val dup_lhs_tfrees = |
|
18964 | 183 |
(case duplicates (op =) lhs_tfrees of [] => [] |
4866 | 184 |
| dups => ["Duplicate type variables on lhs: " ^ show_names dups]); |
185 |
||
186 |
val extra_rhs_tfrees = |
|
17280 | 187 |
(case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => [] |
4866 | 188 |
| extras => ["Extra type variables on rhs: " ^ show_names extras]); |
189 |
||
190 |
val illegal_frees = |
|
29264 | 191 |
(case Term.add_frees set [] of [] => [] |
192 |
| xs => ["Illegal variables on rhs: " ^ show_names xs]); |
|
4866 | 193 |
|
194 |
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
|
195 |
val _ = if null errs then () else error (cat_lines errs); |
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
196 |
|
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
197 |
(*test theory errors now!*) |
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
198 |
val test_thy = Theory.copy thy; |
21352 | 199 |
val _ = test_thy |
19342
094a1c071c8e
added functions for definitional code generation
haftmann
parents:
18964
diff
changeset
|
200 |
|> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal); |
11426
f280d4b29a2c
abtract non-emptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset
|
201 |
|
29062 | 202 |
in (set, goal, goal_pat, typedef_result) end |
18678 | 203 |
handle ERROR msg => err_in_typedef msg name; |
4866 | 204 |
|
205 |
||
29056 | 206 |
(* add_typedef: tactic interface *) |
4866 | 207 |
|
28662 | 208 |
fun add_typedef def opt_name typ set opt_morphs tac thy = |
6383 | 209 |
let |
17922 | 210 |
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
|
211 |
val (set, goal, _, typedef_result) = |
28662 | 212 |
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
|
213 |
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
|
214 |
handle ERROR msg => cat_error msg |
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted --
wenzelm
parents:
29059
diff
changeset
|
215 |
("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
|
216 |
in typedef_result inhabited thy end; |
4866 | 217 |
|
17339 | 218 |
|
29056 | 219 |
(* typedef: proof interface *) |
6383 | 220 |
|
17339 | 221 |
local |
222 |
||
223 |
fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy = |
|
11822 | 224 |
let |
29062 | 225 |
val (_, goal, goal_pat, typedef_result) = |
13443 | 226 |
prepare_typedef prep_term def name typ set opt_morphs thy; |
21352 | 227 |
fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th); |
29062 | 228 |
in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end; |
17339 | 229 |
|
230 |
in |
|
6383 | 231 |
|
28662 | 232 |
val typedef = gen_typedef Syntax.check_term; |
233 |
val typedef_cmd = gen_typedef Syntax.read_term; |
|
17339 | 234 |
|
19705 | 235 |
end; |
15259 | 236 |
|
237 |
||
238 |
||
6383 | 239 |
(** outer syntax **) |
240 |
||
29056 | 241 |
local structure P = OuterParse in |
6383 | 242 |
|
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26939
diff
changeset
|
243 |
val _ = OuterKeyword.keyword "morphisms"; |
24867 | 244 |
|
17339 | 245 |
val typedef_decl = |
16126
3ba9eb7ea366
fixed outer syntax: allow type_args with parentheses;
wenzelm
parents:
15570
diff
changeset
|
246 |
Scan.optional (P.$$$ "(" |-- |
3ba9eb7ea366
fixed outer syntax: allow type_args with parentheses;
wenzelm
parents:
15570
diff
changeset
|
247 |
((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s))) |
3ba9eb7ea366
fixed outer syntax: allow type_args with parentheses;
wenzelm
parents:
15570
diff
changeset
|
248 |
--| P.$$$ ")") (true, NONE) -- |
11744 | 249 |
(P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset
|
250 |
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)); |
6357 | 251 |
|
17339 | 252 |
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = |
28662 | 253 |
typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs); |
6357 | 254 |
|
24867 | 255 |
val _ = |
29056 | 256 |
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" |
257 |
OuterKeyword.thy_goal |
|
17339 | 258 |
(typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef))); |
6357 | 259 |
|
29056 | 260 |
end; |
261 |
||
262 |
||
25535 | 263 |
val setup = TypedefInterpretation.init; |
264 |
||
4866 | 265 |
end; |