author  haftmann 
Fri, 30 Nov 2007 20:13:07 +0100  
changeset 25513  b7de6e23e143 
parent 25495  98f3596bec44 
child 25535  4975b7529a14 
permissions  rwrr 
4866  1 
(* Title: HOL/Tools/typedef_package.ML 
2 
ID: $Id$ 

16458  3 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 
4866  4 

21352  5 
Gordon/HOLstyle type definitions: create a new syntactic type 
6 
represented by a nonempty subset. 

4866  7 
*) 
8 

9 
signature TYPEDEF_PACKAGE = 

10 
sig 

5697  11 
val quiet_mode: bool ref 
19705  12 
type info = 
13 
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, 

14 
type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, 

15 
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, 

16 
Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; 

17 
val get_info: theory > string > info option 

11827  18 
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

19 
string > (bstring * bstring) option > tactic > theory > (string * info) * theory 
11827  20 
val add_typedef_i: bool > string option > bstring * string list * mixfix > 
20483
04aa552a83bc
TypedefPackage.add_typedef_* now yields name of introduced type constructor
haftmann
parents:
20462
diff
changeset

21 
term > (bstring * bstring) option > tactic > theory > (string * info) * theory 
17339  22 
val typedef: (bool * string) * (bstring * string list * mixfix) * string 
23 
* (string * string) option > theory > Proof.state 

24 
val typedef_i: (bool * string) * (bstring * string list * mixfix) * term 

25 
* (string * string) option > theory > Proof.state 

25513  26 
val interpretation: (string > theory > theory) > theory > theory 
4866  27 
end; 
28 

29 
structure TypedefPackage: TYPEDEF_PACKAGE = 

30 
struct 

31 

10280  32 
(** theory context references **) 
33 

11608  34 
val type_definitionN = "Typedef.type_definition"; 
10280  35 

13413  36 
val Rep = thm "type_definition.Rep"; 
37 
val Rep_inverse = thm "type_definition.Rep_inverse"; 

38 
val Abs_inverse = thm "type_definition.Abs_inverse"; 

39 
val Rep_inject = thm "type_definition.Rep_inject"; 

40 
val Abs_inject = thm "type_definition.Abs_inject"; 

41 
val Rep_cases = thm "type_definition.Rep_cases"; 

42 
val Abs_cases = thm "type_definition.Abs_cases"; 

43 
val Rep_induct = thm "type_definition.Rep_induct"; 

44 
val Abs_induct = thm "type_definition.Abs_induct"; 

10280  45 

46 

47 

17922  48 
(** type definitions **) 
49 

50 
(* messages *) 

51 

52 
val quiet_mode = ref false; 

53 
fun message s = if ! quiet_mode then () else writeln s; 

54 

55 

56 
(* theory data *) 

15259  57 

19705  58 
type info = 
59 
{rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, 

60 
type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, 

61 
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, 

62 
Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; 

19459  63 

16458  64 
structure TypedefData = TheoryDataFun 
22846  65 
( 
19705  66 
type T = info Symtab.table; 
15259  67 
val empty = Symtab.empty; 
68 
val copy = I; 

16458  69 
val extend = I; 
19617  70 
fun merge _ tabs : T = Symtab.merge (K true) tabs; 
22846  71 
); 
15259  72 

19705  73 
val get_info = Symtab.lookup o TypedefData.get; 
74 
fun put_info name info = TypedefData.map (Symtab.update (name, info)); 

15259  75 

76 

6383  77 
(* prepare_typedef *) 
78 

18678  79 
fun err_in_typedef msg name = 
80 
cat_error msg ("The error(s) above occurred in typedef " ^ quote name); 

6383  81 

21352  82 
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); 
83 

11822  84 
fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy = 
4866  85 
let 
11608  86 
val _ = Theory.requires thy "Typedef" "typedefs"; 
21352  87 
val ctxt = ProofContext.init thy; 
16458  88 
val full = Sign.full_name thy; 
4866  89 

90 
(*rhs*) 

10280  91 
val full_name = full name; 
21352  92 
val set = prep_term (ctxt > fold declare_type_name vs) raw_set; 
93 
val setT = Term.fastype_of set; 

17280  94 
val rhs_tfrees = Term.add_tfrees set []; 
95 
val rhs_tfreesT = Term.add_tfreesT setT []; 

4866  96 
val oldT = HOLogic.dest_setT setT handle TYPE _ => 
24920  97 
error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

98 
fun mk_nonempty A = 
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

99 
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A))); 
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

100 
val goal = mk_nonempty set; 
19473  101 
val goal_pat = mk_nonempty (Var (the_default (name, 0) (Syntax.read_variable name), setT)); 
4866  102 

103 
(*lhs*) 

17280  104 
val defS = Sign.defaultS thy; 
19473  105 
val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; 
17280  106 
val args_setT = lhs_tfrees 
107 
> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT)) 

108 
> map TFree; 

109 

4866  110 
val tname = Syntax.type_name t mx; 
10280  111 
val full_tname = full tname; 
112 
val newT = Type (full_tname, map TFree lhs_tfrees); 

4866  113 

19473  114 
val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs; 
19391  115 
val setT' = map Term.itselfT args_setT > setT; 
17280  116 
val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT); 
10280  117 
val RepC = Const (full Rep_name, newT > oldT); 
118 
val AbsC = Const (full Abs_name, oldT > newT); 

4866  119 
val x_new = Free ("x", newT); 
120 
val y_old = Free ("y", oldT); 

10280  121 

11822  122 
val set' = if def then setC else set; 
4866  123 

10280  124 
val typedef_name = "type_definition_" ^ name; 
125 
val typedefC = 

126 
Const (type_definitionN, (newT > oldT) > (oldT > newT) > setT > HOLogic.boolT); 

11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

127 
val typedef_prop = 
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

128 
Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); 
19705  129 
val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c  _ => I) set' []; 
4866  130 

19705  131 
fun add_def eq thy = 
132 
if def then 

18358  133 
thy 
19705  134 
> PureThy.add_defs_i false [Thm.no_attributes eq] 
135 
> (fn [th] => pair (SOME th)) 

136 
else (NONE, thy); 

18358  137 

21352  138 
fun typedef_result nonempty = 
25495  139 
ObjectLogic.typedecl (t, vs, mx) 
25458
ba8f5e4fa336
separated typedecl module, providing typedecl command with interpretation
haftmann
parents:
24926
diff
changeset

140 
#> snd 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset

141 
#> Sign.add_consts_i 
17280  142 
((if def then [(name, setT', NoSyn)] else []) @ 
6383  143 
[(Rep_name, newT > oldT, NoSyn), 
144 
(Abs_name, oldT > newT, NoSyn)]) 

24255  145 
#> add_def (PrimitiveDefs.mk_defpair (setC, set)) 
21352  146 
##>> PureThy.add_axioms_i [((typedef_name, typedef_prop), 
20046  147 
[apsnd (fn cond_axm => nonempty RS cond_axm)])] 
21352  148 
##> Theory.add_deps "" (dest_Const RepC) typedef_deps 
149 
##> Theory.add_deps "" (dest_Const AbsC) typedef_deps 

150 
#> (fn (set_def, [type_definition]) => fn thy1 => 

11822  151 
let 
152 
fun make th = Drule.standard (th OF [type_definition]); 

19342
094a1c071c8e
added functions for definitional code generation
haftmann
parents:
18964
diff
changeset

153 
val abs_inject = make Abs_inject; 
094a1c071c8e
added functions for definitional code generation
haftmann
parents:
18964
diff
changeset

154 
val abs_inverse = make Abs_inverse; 
18377  155 
val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, 
19705  156 
Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) = 
157 
thy1 

24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset

158 
> Sign.add_path name 
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12043
diff
changeset

159 
> PureThy.add_thms 
11822  160 
([((Rep_name, make Rep), []), 
161 
((Rep_name ^ "_inverse", make Rep_inverse), []), 

19342
094a1c071c8e
added functions for definitional code generation
haftmann
parents:
18964
diff
changeset

162 
((Abs_name ^ "_inverse", abs_inverse), []), 
11822  163 
((Rep_name ^ "_inject", make Rep_inject), []), 
19342
094a1c071c8e
added functions for definitional code generation
haftmann
parents:
18964
diff
changeset

164 
((Abs_name ^ "_inject", abs_inject), []), 
11822  165 
((Rep_name ^ "_cases", make Rep_cases), 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24830
diff
changeset

166 
[RuleCases.case_names [Rep_name], Induct.cases_pred full_name]), 
11822  167 
((Abs_name ^ "_cases", make Abs_cases), 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24712
diff
changeset

168 
[RuleCases.case_names [Abs_name], Induct.cases_type full_tname]), 
11822  169 
((Rep_name ^ "_induct", make Rep_induct), 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24830
diff
changeset

170 
[RuleCases.case_names [Rep_name], Induct.induct_pred full_name]), 
11822  171 
((Abs_name ^ "_induct", make Abs_induct), 
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24712
diff
changeset

172 
[RuleCases.case_names [Abs_name], Induct.induct_type full_tname])]) 
24712
64ed05609568
proper Sign operations instead of Theory aliases;
wenzelm
parents:
24509
diff
changeset

173 
> Sign.parent_path; 
19705  174 
val info = {rep_type = oldT, abs_type = newT, 
175 
Rep_name = full Rep_name, Abs_name = full Abs_name, 

176 
type_definition = type_definition, set_def = set_def, 

177 
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, 

178 
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, 

11822  179 
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; 
19705  180 
val thy3 = thy2 > put_info full_tname info; 
21352  181 
in ((full_tname, info), thy3) end); 
6383  182 

4866  183 

184 
(* errors *) 

185 

186 
fun show_names pairs = commas_quote (map fst pairs); 

187 

188 
val illegal_vars = 

189 
if null (term_vars set) andalso null (term_tvars set) then [] 

190 
else ["Illegal schematic variable(s) on rhs"]; 

191 

192 
val dup_lhs_tfrees = 

18964  193 
(case duplicates (op =) lhs_tfrees of [] => [] 
4866  194 
 dups => ["Duplicate type variables on lhs: " ^ show_names dups]); 
195 

196 
val extra_rhs_tfrees = 

17280  197 
(case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => [] 
4866  198 
 extras => ["Extra type variables on rhs: " ^ show_names extras]); 
199 

200 
val illegal_frees = 

201 
(case term_frees set of [] => [] 

202 
 xs => ["Illegal variables on rhs: " ^ show_names (map dest_Free xs)]); 

203 

204 
val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees; 

11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

205 
val _ = if null errs then () else error (cat_lines errs); 
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

206 

f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

207 
(*test theory errors now!*) 
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

208 
val test_thy = Theory.copy thy; 
21352  209 
val _ = test_thy 
19342
094a1c071c8e
added functions for definitional code generation
haftmann
parents:
18964
diff
changeset

210 
> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal); 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

211 

21352  212 
in (set, goal, goal_pat, typedef_result) end 
18678  213 
handle ERROR msg => err_in_typedef msg name; 
4866  214 

215 

6383  216 
(* add_typedef interfaces *) 
4866  217 

25513  218 
structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =); 
219 
val interpretation = TypedefInterpretation.interpretation; 

220 

17339  221 
local 
222 

17922  223 
fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy = 
6383  224 
let 
24920  225 
val string_of_term = Sign.string_of_term thy; 
17922  226 
val name = the_default (#1 typ) opt_name; 
21352  227 
val (set, goal, _, typedef_result) = 
11822  228 
prepare_typedef prep_term def name typ set opt_morphs thy; 
21352  229 
val _ = message ("Proving nonemptiness of set " ^ quote (string_of_term set) ^ " ..."); 
20046  230 
val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg => 
21352  231 
cat_error msg ("Failed to prove nonemptiness of " ^ quote (string_of_term set)); 
25513  232 
in 
233 
thy 

234 
> typedef_result non_empty 

235 
> (fn (a, info) => TypedefInterpretation.data a #> pair (a, info)) 

236 
end; 

4866  237 

17339  238 
in 
239 

24509
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24255
diff
changeset

240 
val add_typedef = gen_typedef Syntax.read_term; 
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24255
diff
changeset

241 
val add_typedef_i = gen_typedef Syntax.check_term; 
4866  242 

17339  243 
end; 
4866  244 

17339  245 

246 
(* Isar typedef interface *) 

6383  247 

17339  248 
local 
249 

250 
fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy = 

11822  251 
let 
19705  252 
val (_, goal, goal_pat, typedef_result) = 
13443  253 
prepare_typedef prep_term def name typ set opt_morphs thy; 
21352  254 
fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th); 
21434  255 
in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end; 
17339  256 

257 
in 

6383  258 

24509
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24255
diff
changeset

259 
val typedef = gen_typedef Syntax.read_term; 
23ee6b7788c2
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents:
24255
diff
changeset

260 
val typedef_i = gen_typedef Syntax.check_term; 
17339  261 

19705  262 
end; 
15259  263 

264 

265 

6383  266 
(** outer syntax **) 
267 

17057  268 
local structure P = OuterParse and K = OuterKeyword in 
6383  269 

24867  270 
val _ = OuterSyntax.keywords ["morphisms"]; 
271 

17339  272 
val typedef_decl = 
16126
3ba9eb7ea366
fixed outer syntax: allow type_args with parentheses;
wenzelm
parents:
15570
diff
changeset

273 
Scan.optional (P.$$$ "("  
3ba9eb7ea366
fixed outer syntax: allow type_args with parentheses;
wenzelm
parents:
15570
diff
changeset

274 
((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

275 
 P.$$$ ")") (true, NONE)  
11744  276 
(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

277 
Scan.option (P.$$$ "morphisms"  P.!!! (P.name  P.name)); 
6357  278 

17339  279 
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = 
19473  280 
typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs); 
6357  281 

24867  282 
val _ = 
6723  283 
OuterSyntax.command "typedef" "HOL type definition (requires nonemptiness proof)" K.thy_goal 
17339  284 
(typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef))); 
6357  285 

4866  286 
end; 
6383  287 

288 
end; 