author  wenzelm 
Wed, 24 Jul 2002 00:11:24 +0200  
changeset 13413  0b60b9e18a26 
parent 12876  a70df1e5bf10 
child 13443  1c3327c348b3 
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 
11822  13 
val add_typedef_x: string > bstring * string list * mixfix > 
4866  14 
string > string list > thm list > tactic option > theory > theory 
11827  15 
val add_typedef: bool > string option > bstring * string list * mixfix > 
11822  16 
string > (bstring * bstring) option > tactic > theory > theory * 
17 
{type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, 

18 
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, 

19 
Rep_induct: thm, Abs_induct: thm} 

11827  20 
val add_typedef_i: bool > string option > bstring * string list * mixfix > 
11822  21 
term > (bstring * bstring) option > tactic > theory > theory * 
22 
{type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, 

23 
Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, 

24 
Rep_induct: thm, Abs_induct: thm} 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

25 
val typedef_proof: string * (bstring * string list * mixfix) * string * (string * string) option 
6690  26 
> bool > theory > ProofHistory.T 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

27 
val typedef_proof_i: string * (bstring * string list * mixfix) * term * (string * string) option 
6690  28 
> bool > theory > ProofHistory.T 
4866  29 
end; 
30 

31 
structure TypedefPackage: TYPEDEF_PACKAGE = 

32 
struct 

33 

34 

10280  35 
(** theory context references **) 
36 

11608  37 
val type_definitionN = "Typedef.type_definition"; 
10280  38 

13413  39 
val Rep = thm "type_definition.Rep"; 
40 
val Rep_inverse = thm "type_definition.Rep_inverse"; 

41 
val Abs_inverse = thm "type_definition.Abs_inverse"; 

42 
val Rep_inject = thm "type_definition.Rep_inject"; 

43 
val Abs_inject = thm "type_definition.Abs_inject"; 

44 
val Rep_cases = thm "type_definition.Rep_cases"; 

45 
val Abs_cases = thm "type_definition.Abs_cases"; 

46 
val Rep_induct = thm "type_definition.Rep_induct"; 

47 
val Abs_induct = thm "type_definition.Abs_induct"; 

10280  48 

49 

50 

5104  51 
(** type declarations **) 
52 

53 
fun add_typedecls decls thy = 

54 
let 

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

56 

57 
fun arity_of (raw_name, args, mx) = 

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

58 
(full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.typeS, HOLogic.typeS); 
5104  59 
in 
8141  60 
if can (Theory.assert_super HOL.thy) thy then 
61 
thy 

62 
> PureThy.add_typedecls decls 

63 
> Theory.add_arities_i (map arity_of decls) 

64 
else thy > PureThy.add_typedecls decls 

5104  65 
end; 
66 

67 

68 

69 
(** type definitions **) 

70 

5697  71 
(* messages *) 
72 

73 
val quiet_mode = ref false; 

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

75 

76 

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

77 
(* prove_nonempty  tactical version *) (*exception ERROR*) 
4866  78 

11827  79 
fun prove_nonempty thy cset goal (witn1_tac, witn_names, witn_thms, witn2_tac) = 
6383  80 
let 
81 
val is_def = Logic.is_equals o #prop o Thm.rep_thm; 

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

4866  83 
val tac = 
11827  84 
witn1_tac THEN 
4866  85 
TRY (rewrite_goals_tac (filter is_def thms)) THEN 
86 
TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN 

11827  87 
if_none witn2_tac (TRY (ALLGOALS (CLASET' blast_tac))); 
4866  88 
in 
6383  89 
message ("Proving nonemptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); 
11968  90 
Tactic.prove (Theory.sign_of thy) [] [] goal (K tac) 
6383  91 
end handle ERROR => error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset)); 
4866  92 

93 

6383  94 
(* prepare_typedef *) 
95 

96 
fun read_term sg used s = 

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

97 
#1 (Thm.read_def_cterm (sg, K None, K None) used true (s, HOLogic.typeT)); 
4866  98 

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

101 
fun err_in_typedef name = 

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

103 

11822  104 
fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy = 
4866  105 
let 
11608  106 
val _ = Theory.requires thy "Typedef" "typedefs"; 
6383  107 
val sign = Theory.sign_of thy; 
10280  108 
val full = Sign.full_name sign; 
4866  109 

110 
(*rhs*) 

10280  111 
val full_name = full name; 
6383  112 
val cset = prep_term sign vs raw_set; 
113 
val {T = setT, t = set, ...} = Thm.rep_cterm cset; 

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

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

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

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

118 
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

119 
val goal = mk_nonempty set; 
11744  120 
val vname = take_suffix Symbol.is_digit (Symbol.explode name) 
121 
> apfst implode > apsnd (#1 o Term.read_int); 

122 
val goal_pat = mk_nonempty (Var (vname, setT)); 

4866  123 

124 
(*lhs*) 

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

125 
val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.typeS)) vs; 
4866  126 
val tname = Syntax.type_name t mx; 
10280  127 
val full_tname = full tname; 
128 
val newT = Type (full_tname, map TFree lhs_tfrees); 

4866  129 

11744  130 
val (Rep_name, Abs_name) = if_none opt_morphs ("Rep_" ^ name, "Abs_" ^ name); 
10280  131 
val setC = Const (full_name, setT); 
132 
val RepC = Const (full Rep_name, newT > oldT); 

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

4866  134 
val x_new = Free ("x", newT); 
135 
val y_old = Free ("y", oldT); 

10280  136 

11822  137 
val set' = if def then setC else set; 
4866  138 

10280  139 
val typedef_name = "type_definition_" ^ name; 
140 
val typedefC = 

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

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

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

143 
Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set')); 
4866  144 

11822  145 
fun typedef_result (theory, nonempty) = 
6383  146 
theory 
147 
> add_typedecls [(t, vs, mx)] 

148 
> Theory.add_consts_i 

11822  149 
((if def then [(name, setT, NoSyn)] else []) @ 
6383  150 
[(Rep_name, newT > oldT, NoSyn), 
151 
(Abs_name, oldT > newT, NoSyn)]) 

11822  152 
> (if def then (apsnd (Some o hd) oo (PureThy.add_defs_i false o map Thm.no_attributes)) 
153 
[Logic.mk_defpair (setC, set)] 

154 
else rpair None) 

155 
>> PureThy.add_axioms_i [((typedef_name, typedef_prop), 

11727
a27150cc8fa5
test: use SkipProof.make_thm instead of Thm.assume;
wenzelm
parents:
11608
diff
changeset

156 
[apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])] 
11822  157 
> (fn ((theory', [type_definition]), set_def) => 
158 
let 

159 
fun make th = Drule.standard (th OF [type_definition]); 

160 
val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, 

161 
Rep_cases, Abs_cases, Rep_induct, Abs_induct]) = 

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

162 
theory' 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12043
diff
changeset

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

164 
> PureThy.add_thms 
11822  165 
([((Rep_name, make Rep), []), 
166 
((Rep_name ^ "_inverse", make Rep_inverse), []), 

167 
((Abs_name ^ "_inverse", make Abs_inverse), []), 

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

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

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

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

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

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

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

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

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

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

177 
[RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]) 
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12043
diff
changeset

178 
>> Theory.parent_path; 
11822  179 
val result = {type_definition = type_definition, set_def = set_def, 
180 
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, 

181 
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, 

182 
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; 

183 
in ((theory'', type_definition), result) end); 

6383  184 

4866  185 

186 
(* errors *) 

187 

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

189 

190 
val illegal_vars = 

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

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

193 

194 
val dup_lhs_tfrees = 

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

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

197 

198 
val extra_rhs_tfrees = 

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

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

201 

202 
val illegal_frees = 

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

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

205 

206 
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

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

208 

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

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

210 
val test_thy = Theory.copy thy; 
11727
a27150cc8fa5
test: use SkipProof.make_thm instead of Thm.assume;
wenzelm
parents:
11608
diff
changeset

211 
val _ = (test_thy, 
11822  212 
setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) > typedef_result; 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

213 

11822  214 
in (cset, goal, goal_pat, typedef_result) end 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

215 
handle ERROR => err_in_typedef name; 
4866  216 

217 

6383  218 
(* add_typedef interfaces *) 
4866  219 

11827  220 
fun gen_typedef prep_term def name typ set opt_morphs tac1 names thms tac2 thy = 
6383  221 
let 
11822  222 
val (cset, goal, _, typedef_result) = 
223 
prepare_typedef prep_term def name typ set opt_morphs thy; 

11827  224 
val non_empty = prove_nonempty thy cset goal (tac1, names, thms, tac2); 
11822  225 
val ((thy', _), result) = (thy, non_empty) > typedef_result; 
226 
in (thy', result) end; 

4866  227 

11827  228 
fun sane_typedef prep_term def opt_name typ set opt_morphs tac = 
229 
gen_typedef prep_term def 

230 
(if_none opt_name (#1 typ)) typ set opt_morphs all_tac [] [] (Some tac); 

11822  231 

232 
fun add_typedef_x name typ set names thms tac = 

11827  233 
#1 o gen_typedef read_term true name typ set None (Tactic.rtac exI 1) names thms tac; 
11822  234 

235 
val add_typedef = sane_typedef read_term; 

236 
val add_typedef_i = sane_typedef cert_term; 

4866  237 

238 

6383  239 
(* typedef_proof interface *) 
240 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

241 
fun gen_typedef_proof prep_term (name, typ, set, opt_morphs) int thy = 
11822  242 
let 
243 
val (_, goal, goal_pat, att_result) = 

244 
prepare_typedef prep_term true name typ set opt_morphs thy; 

245 
val att = #1 o att_result; 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

246 
in thy > IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([goal_pat], []))) int end; 
6383  247 

248 
val typedef_proof = gen_typedef_proof read_term; 

249 
val typedef_proof_i = gen_typedef_proof cert_term; 

6357  250 

251 

6383  252 

253 
(** outer syntax **) 

254 

6723  255 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6383  256 

6357  257 
val typedeclP = 
12624  258 
OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl 
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

259 
(P.type_args  P.name  P.opt_infix >> (fn ((vs, t), mx) => 
6357  260 
Toplevel.theory (add_typedecls [(t, vs, mx)]))); 
261 

6723  262 

6383  263 
val typedef_proof_decl = 
6723  264 
Scan.option (P.$$$ "("  P.name  P.$$$ ")")  
11744  265 
(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

266 
Scan.option (P.$$$ "morphisms"  P.!!! (P.name  P.name)); 
6357  267 

12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

268 
fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), morphs) = 
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12694
diff
changeset

269 
typedef_proof (if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs); 
6357  270 

271 
val typedefP = 

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

6723  275 

11744  276 
val _ = OuterSyntax.add_keywords ["morphisms"]; 
6357  277 
val _ = OuterSyntax.add_parsers [typedeclP, typedefP]; 
278 

4866  279 
end; 
6383  280 

281 
end; 