author  wenzelm 
Thu, 19 Oct 2000 21:25:15 +0200  
changeset 10280  2626d4e37341 
parent 9969  4753185f1dd2 
child 10463  474263d29057 
permissions  rwrr 
4866  1 
(* Title: HOL/Tools/typedef_package.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

9230  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
4866  5 

6357  6 
Gordon/HOLstyle type definitions. 
4866  7 
*) 
8 

9 
signature TYPEDEF_PACKAGE = 

10 
sig 

5697  11 
val quiet_mode: bool ref 
5104  12 
val add_typedecls: (bstring * string list * mixfix) list > theory > theory 
4866  13 
val add_typedef: string > bstring * string list * mixfix > 
14 
string > string list > thm list > tactic option > theory > theory 

15 
val add_typedef_i: string > bstring * string list * mixfix > 

16 
term > string list > thm list > tactic option > theory > theory 

5180
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

17 
val add_typedef_i_no_def: string > bstring * string list * mixfix > 
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

18 
term > string list > thm list > tactic option > theory > theory 
6729  19 
val typedef_proof: (string * (bstring * string list * mixfix) * string) * Comment.text 
6690  20 
> bool > theory > ProofHistory.T 
6729  21 
val typedef_proof_i: (string * (bstring * string list * mixfix) * term) * Comment.text 
6690  22 
> bool > theory > ProofHistory.T 
4866  23 
end; 
24 

25 
structure TypedefPackage: TYPEDEF_PACKAGE = 

26 
struct 

27 

28 

10280  29 
(** theory context references **) 
30 

31 
val type_definitionN = "subset.type_definition"; 

32 
val type_definition_def = thm "type_definition_def"; 

33 

34 
val Rep = thm "Rep"; 

35 
val Rep_inverse = thm "Rep_inverse"; 

36 
val Abs_inverse = thm "Abs_inverse"; 

37 
val Rep_inject = thm "Rep_inject"; 

38 
val Abs_inject = thm "Abs_inject"; 

39 
val Rep_cases = thm "Rep_cases"; 

40 
val Abs_cases = thm "Abs_cases"; 

41 
val Rep_induct = thm "Rep_induct"; 

42 
val Abs_induct = thm "Abs_induct"; 

43 

44 

45 

5104  46 
(** type declarations **) 
47 

48 
fun add_typedecls decls thy = 

49 
let 

50 
val full = Sign.full_name (Theory.sign_of thy); 

51 

52 
fun arity_of (raw_name, args, mx) = 

53 
(full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS); 

54 
in 

8141  55 
if can (Theory.assert_super HOL.thy) thy then 
56 
thy 

57 
> PureThy.add_typedecls decls 

58 
> Theory.add_arities_i (map arity_of decls) 

59 
else thy > PureThy.add_typedecls decls 

5104  60 
end; 
61 

62 

63 

64 
(** type definitions **) 

65 

5697  66 
(* messages *) 
67 

68 
val quiet_mode = ref false; 

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

70 

71 

6383  72 
(* nonemptiness of set *) (*exception ERROR*) 
4866  73 

6383  74 
fun check_nonempty cset thm = 
4866  75 
let 
6383  76 
val {t, sign, maxidx, ...} = Thm.rep_cterm cset; 
77 
val {prop, ...} = Thm.rep_thm (Thm.transfer_sg sign (Drule.standard thm)); 

78 
val matches = Pattern.matches (Sign.tsig_of sign); 

79 
in 

80 
(case try (HOLogic.dest_mem o HOLogic.dest_Trueprop) prop of 

81 
None => raise ERROR 

82 
 Some (_, A) => if matches (Logic.incr_indexes ([], maxidx) A, t) then () else raise ERROR) 

83 
end handle ERROR => error ("Bad nonemptiness theorem " ^ Display.string_of_thm thm ^ 

84 
"\nfor set " ^ quote (Display.string_of_cterm cset)); 

85 

7481  86 
fun goal_nonempty ex cset = 
6383  87 
let 
88 
val {T = setT, t = A, maxidx, sign} = Thm.rep_cterm cset; 

4866  89 
val T = HOLogic.dest_setT setT; 
7481  90 
val tm = 
91 
if ex then HOLogic.mk_exists ("x", T, HOLogic.mk_mem (Free ("x", T), A)) 

92 
else HOLogic.mk_mem (Var (("x", maxidx + 1), T), A); (*oldstyle version*) 

93 
in Thm.cterm_of sign (HOLogic.mk_Trueprop tm) end; 

6383  94 

95 
fun prove_nonempty thy cset (witn_names, witn_thms, witn_tac) = 

96 
let 

97 
val is_def = Logic.is_equals o #prop o Thm.rep_thm; 

98 
val thms = PureThy.get_thmss thy witn_names @ witn_thms; 

4866  99 
val tac = 
100 
TRY (rewrite_goals_tac (filter is_def thms)) THEN 

101 
TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN 

6383  102 
if_none witn_tac (TRY (ALLGOALS (CLASET' blast_tac))); 
4866  103 
in 
6383  104 
message ("Proving nonemptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); 
7481  105 
prove_goalw_cterm [] (goal_nonempty false cset) (K [tac]) 
6383  106 
end handle ERROR => error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset)); 
4866  107 

108 

6383  109 
(* prepare_typedef *) 
110 

111 
fun read_term sg used s = 

8100  112 
#1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.termT)); 
4866  113 

6383  114 
fun cert_term sg _ t = Thm.cterm_of sg t handle TERM (msg, _) => error msg; 
115 

116 
fun err_in_typedef name = 

117 
error ("The error(s) above occurred in typedef " ^ quote name); 

118 

119 
fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set thy = 

4866  120 
let 
10280  121 
val _ = Theory.requires thy "subset" "typedefs"; 
6383  122 
val sign = Theory.sign_of thy; 
10280  123 
val full = Sign.full_name sign; 
4866  124 

125 
(*rhs*) 

10280  126 
val full_name = full name; 
6383  127 
val cset = prep_term sign vs raw_set; 
128 
val {T = setT, t = set, ...} = Thm.rep_cterm cset; 

4866  129 
val rhs_tfrees = term_tfrees set; 
130 
val oldT = HOLogic.dest_setT setT handle TYPE _ => 

131 
error ("Not a set type: " ^ quote (Sign.string_of_typ sign setT)); 

10280  132 
val cset_pat = Thm.cterm_of sign (Var ((name, 0), setT)); 
4866  133 

134 
(*lhs*) 

6383  135 
val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs; 
4866  136 
val tname = Syntax.type_name t mx; 
10280  137 
val full_tname = full tname; 
138 
val newT = Type (full_tname, map TFree lhs_tfrees); 

4866  139 

140 
val Rep_name = "Rep_" ^ name; 

141 
val Abs_name = "Abs_" ^ name; 

10280  142 

143 
val setC = Const (full_name, setT); 

144 
val RepC = Const (full Rep_name, newT > oldT); 

145 
val AbsC = Const (full Abs_name, oldT > newT); 

4866  146 
val x_new = Free ("x", newT); 
147 
val y_old = Free ("y", oldT); 

10280  148 

149 
val set' = if no_def then set else setC; (* FIXME !?? *) 

4866  150 

10280  151 
val typedef_name = "type_definition_" ^ name; 
152 
val typedefC = 

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

154 
val typedef_prop = HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'); 

4866  155 

6383  156 
(*theory extender*) 
157 
fun do_typedef theory = 

158 
theory 

159 
> Theory.assert_super thy 

160 
> add_typedecls [(t, vs, mx)] 

161 
> Theory.add_consts_i 

162 
((if no_def then [] else [(name, setT, NoSyn)]) @ 

163 
[(Rep_name, newT > oldT, NoSyn), 

164 
(Abs_name, oldT > newT, NoSyn)]) 

9315  165 
> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes)) 
6383  166 
[Logic.mk_defpair (setC, set)]) 
10280  167 
> PureThy.add_axioms_i [((typedef_name, typedef_prop), [])] 
168 
> (fn (theory', typedef_ax) => 

169 
let fun make th = standard (th OF typedef_ax) in 

170 
theory' 

171 
> (#1 oo PureThy.add_thms) 

172 
([((Rep_name, make Rep), []), 

173 
((Rep_name ^ "_inverse", make Rep_inverse), []), 

174 
((Abs_name ^ "_inverse", make Abs_inverse), [])] @ 

175 
(if no_def then [] else 

176 
[((Rep_name ^ "_inject", make Rep_inject), []), 

177 
((Abs_name ^ "_inject", make Abs_inject), []), 

178 
((Rep_name ^ "_cases", make Rep_cases), 

179 
[RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]), 

180 
((Abs_name ^ "_cases", make Abs_cases), 

181 
[RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]), 

182 
((Rep_name ^ "_induct", make Rep_induct), 

183 
[RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]), 

184 
((Abs_name ^ "_induct", make Abs_induct), 

185 
[RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])) 

186 
end) 

6383  187 
handle ERROR => err_in_typedef name; 
188 

4866  189 

190 
(* errors *) 

191 

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

193 

194 
val illegal_vars = 

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

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

197 

198 
val dup_lhs_tfrees = 

199 
(case duplicates lhs_tfrees of [] => [] 

200 
 dups => ["Duplicate type variables on lhs: " ^ show_names dups]); 

201 

202 
val extra_rhs_tfrees = 

203 
(case gen_rems (op =) (rhs_tfrees, lhs_tfrees) of [] => [] 

204 
 extras => ["Extra type variables on rhs: " ^ show_names extras]); 

205 

206 
val illegal_frees = 

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

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

209 

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

211 
in 

6383  212 
if null errs then () else error (cat_lines errs); 
10280  213 
(cset, cset_pat, do_typedef) 
6383  214 
end handle ERROR => err_in_typedef name; 
4866  215 

216 

6383  217 
(* add_typedef interfaces *) 
4866  218 

6383  219 
fun gen_add_typedef prep_term no_def name typ set names thms tac thy = 
220 
let 

10280  221 
val (cset, _, do_typedef) = prepare_typedef prep_term no_def name typ set thy; 
6383  222 
val result = prove_nonempty thy cset (names, thms, tac); 
223 
in check_nonempty cset result; thy > do_typedef end; 

4866  224 

5180
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

225 
val add_typedef = gen_add_typedef read_term false; 
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

226 
val add_typedef_i = gen_add_typedef cert_term false; 
d82a70766af0
Added new function add_typedef_i_no_def which doesn't add
berghofe
parents:
5104
diff
changeset

227 
val add_typedef_i_no_def = gen_add_typedef cert_term true; 
4866  228 

229 

6383  230 
(* typedef_proof interface *) 
231 

232 
fun typedef_attribute cset do_typedef (thy, thm) = 

9969  233 
(check_nonempty cset (thm RS (some_eq_ex RS iffD2)); (thy > do_typedef, thm)); 
6357  234 

6729  235 
fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy = 
6383  236 
let 
10280  237 
val (cset, cset_pat, do_typedef) = prepare_typedef prep_term false name typ set thy; 
7481  238 
val goal = Thm.term_of (goal_nonempty true cset); 
10280  239 
val goal_pat = Thm.term_of (goal_nonempty true cset_pat); 
6383  240 
in 
241 
thy 

10280  242 
> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], 
243 
(goal, ([goal_pat], []))), comment) int 

6383  244 
end; 
245 

246 
val typedef_proof = gen_typedef_proof read_term; 

247 
val typedef_proof_i = gen_typedef_proof cert_term; 

6357  248 

249 

6383  250 

251 
(** outer syntax **) 

252 

6723  253 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6383  254 

6357  255 
val typedeclP = 
6723  256 
OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl 
7152  257 
(P.type_args  P.name  P.opt_infix  P.marg_comment >> (fn ((vs, t), mx) => 
6357  258 
Toplevel.theory (add_typedecls [(t, vs, mx)]))); 
259 

6723  260 

6383  261 
val typedef_proof_decl = 
6723  262 
Scan.option (P.$$$ "("  P.name  P.$$$ ")")  
6729  263 
(P.type_args  P.name)  P.opt_infix  (P.$$$ "="  P.term)  P.marg_comment; 
6357  264 

6729  265 
fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), comment) = 
266 
typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A), comment); 

6357  267 

268 
val typedefP = 

6723  269 
OuterSyntax.command "typedef" "HOL type definition (requires nonemptiness proof)" K.thy_goal 
6383  270 
(typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof))); 
6357  271 

6723  272 

6357  273 
val _ = OuterSyntax.add_parsers [typedeclP, typedefP]; 
274 

4866  275 
end; 
6383  276 

277 

278 
end; 