author  wenzelm 
Sat, 13 Oct 2001 21:44:58 +0200  
changeset 11744  3a4625eaead0 
parent 11740  86ac4189a1c1 
child 11807  50a36627e6d6 
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 
11744  19 
val typedef_proof: 
20 
(string * (bstring * string list * mixfix) * string * (string * string) option) * Comment.text 

6690  21 
> bool > theory > ProofHistory.T 
11744  22 
val typedef_proof_i: 
23 
(string * (bstring * string list * mixfix) * term * (string * string) option) * Comment.text 

6690  24 
> bool > theory > ProofHistory.T 
4866  25 
end; 
26 

27 
structure TypedefPackage: TYPEDEF_PACKAGE = 

28 
struct 

29 

30 

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

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

36 
val Rep = thm "Rep"; 

37 
val Rep_inverse = thm "Rep_inverse"; 

38 
val Abs_inverse = thm "Abs_inverse"; 

39 
val Rep_inject = thm "Rep_inject"; 

40 
val Abs_inject = thm "Abs_inject"; 

41 
val Rep_cases = thm "Rep_cases"; 

42 
val Abs_cases = thm "Abs_cases"; 

43 
val Rep_induct = thm "Rep_induct"; 

44 
val Abs_induct = thm "Abs_induct"; 

45 

46 

47 

5104  48 
(** type declarations **) 
49 

50 
fun add_typedecls decls thy = 

51 
let 

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

53 

54 
fun arity_of (raw_name, args, mx) = 

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

56 
in 

8141  57 
if can (Theory.assert_super HOL.thy) thy then 
58 
thy 

59 
> PureThy.add_typedecls decls 

60 
> Theory.add_arities_i (map arity_of decls) 

61 
else thy > PureThy.add_typedecls decls 

5104  62 
end; 
63 

64 

65 

66 
(** type definitions **) 

67 

5697  68 
(* messages *) 
69 

70 
val quiet_mode = ref false; 

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

72 

73 

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

74 
(* prove_nonempty  tactical version *) (*exception ERROR*) 
4866  75 

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

76 
fun prove_nonempty thy cset goal (witn_names, witn_thms, witn_tac) = 
6383  77 
let 
78 
val is_def = Logic.is_equals o #prop o Thm.rep_thm; 

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

4866  80 
val tac = 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

81 
rtac exI 1 THEN 
4866  82 
TRY (rewrite_goals_tac (filter is_def thms)) THEN 
83 
TRY (REPEAT_FIRST (resolve_tac (filter_out is_def thms))) THEN 

6383  84 
if_none witn_tac (TRY (ALLGOALS (CLASET' blast_tac))); 
4866  85 
in 
6383  86 
message ("Proving nonemptiness of set " ^ quote (string_of_cterm cset) ^ " ..."); 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

87 
prove_goalw_cterm [] (cterm_of (sign_of thy) goal) (K [tac]) 
6383  88 
end handle ERROR => error ("Failed to prove nonemptiness of " ^ quote (string_of_cterm cset)); 
4866  89 

90 

6383  91 
(* prepare_typedef *) 
92 

93 
fun read_term sg used s = 

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

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

98 
fun err_in_typedef name = 

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

100 

11744  101 
fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set opt_morphs thy = 
4866  102 
let 
11608  103 
val _ = Theory.requires thy "Typedef" "typedefs"; 
6383  104 
val sign = Theory.sign_of thy; 
10280  105 
val full = Sign.full_name sign; 
4866  106 

107 
(*rhs*) 

10280  108 
val full_name = full name; 
6383  109 
val cset = prep_term sign vs raw_set; 
110 
val {T = setT, t = set, ...} = Thm.rep_cterm cset; 

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

113 
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

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

115 
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

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

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

4866  120 

121 
(*lhs*) 

6383  122 
val lhs_tfrees = map (fn v => (v, if_none (assoc (rhs_tfrees, v)) HOLogic.termS)) vs; 
4866  123 
val tname = Syntax.type_name t mx; 
10280  124 
val full_tname = full tname; 
125 
val newT = Type (full_tname, map TFree lhs_tfrees); 

4866  126 

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

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

4866  131 
val x_new = Free ("x", newT); 
132 
val y_old = Free ("y", oldT); 

10280  133 

10615  134 
val set' = if no_def then set else setC; 
4866  135 

10280  136 
val typedef_name = "type_definition_" ^ name; 
137 
val typedefC = 

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

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

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

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

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

142 
fun typedef_att (theory, nonempty) = 
6383  143 
theory 
144 
> add_typedecls [(t, vs, mx)] 

145 
> Theory.add_consts_i 

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

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

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

9315  149 
> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes)) 
6383  150 
[Logic.mk_defpair (setC, set)]) 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

151 
> PureThy.add_axioms_i [((typedef_name, typedef_prop), 
11727
a27150cc8fa5
test: use SkipProof.make_thm instead of Thm.assume;
wenzelm
parents:
11608
diff
changeset

152 
[apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])] 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

153 
> (fn (theory', axm) => 
11727
a27150cc8fa5
test: use SkipProof.make_thm instead of Thm.assume;
wenzelm
parents:
11608
diff
changeset

154 
let fun make th = Drule.standard (th OF axm) in 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

155 
rpair (hd axm) (theory' 
10280  156 
> (#1 oo PureThy.add_thms) 
157 
([((Rep_name, make Rep), []), 

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

10615  159 
((Abs_name ^ "_inverse", make Abs_inverse), []), 
160 
((Rep_name ^ "_inject", make Rep_inject), []), 

10280  161 
((Abs_name ^ "_inject", make Abs_inject), []), 
162 
((Rep_name ^ "_cases", make Rep_cases), 

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

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

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

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

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

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

10675
0b40c19f09f3
'typedef': present result theorem "type_definition Rep Abs A";
wenzelm
parents:
10615
diff
changeset

169 
[RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])])) 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

170 
end); 
6383  171 

4866  172 

173 
(* errors *) 

174 

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

176 

177 
val illegal_vars = 

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

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

180 

181 
val dup_lhs_tfrees = 

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

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

184 

185 
val extra_rhs_tfrees = 

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

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

188 

189 
val illegal_frees = 

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

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

192 

193 
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

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

195 

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

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

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

198 
val _ = (test_thy, 
a27150cc8fa5
test: use SkipProof.make_thm instead of Thm.assume;
wenzelm
parents:
11608
diff
changeset

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

200 

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

201 
in (cset, goal, goal_pat, typedef_att) end 
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

202 
handle ERROR => err_in_typedef name; 
4866  203 

204 

6383  205 
(* add_typedef interfaces *) 
4866  206 

6383  207 
fun gen_add_typedef prep_term no_def name typ set names thms tac thy = 
208 
let 

11744  209 
val (cset, goal, _, typedef_att) = prepare_typedef prep_term no_def name typ set None thy; 
11426
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

210 
val result = prove_nonempty thy cset goal (names, thms, tac); 
f280d4b29a2c
abtract nonemptiness statements (no longer use Eps);
wenzelm
parents:
10697
diff
changeset

211 
in (thy, result) > typedef_att > #1 end; 
4866  212 

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

213 
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

214 
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

215 
val add_typedef_i_no_def = gen_add_typedef cert_term true; 
4866  216 

217 

6383  218 
(* typedef_proof interface *) 
219 

11744  220 
fun gen_typedef_proof prep_term ((name, typ, set, opt_morphs), comment) int thy = 
221 
let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set opt_morphs thy in 

222 
thy > 

223 
IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int 

11740  224 
end; 
6383  225 

226 
val typedef_proof = gen_typedef_proof read_term; 

227 
val typedef_proof_i = gen_typedef_proof cert_term; 

6357  228 

229 

6383  230 

231 
(** outer syntax **) 

232 

6723  233 
local structure P = OuterParse and K = OuterSyntax.Keyword in 
6383  234 

6357  235 
val typedeclP = 
6723  236 
OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl 
7152  237 
(P.type_args  P.name  P.opt_infix  P.marg_comment >> (fn ((vs, t), mx) => 
6357  238 
Toplevel.theory (add_typedecls [(t, vs, mx)]))); 
239 

6723  240 

6383  241 
val typedef_proof_decl = 
6723  242 
Scan.option (P.$$$ "("  P.name  P.$$$ ")")  
11744  243 
(P.type_args  P.name)  P.opt_infix  (P.$$$ "="  P.term)  
244 
Scan.option (P.$$$ "morphisms"  P.!!! (P.name  P.name))  

245 
P.marg_comment; 

6357  246 

11744  247 
fun mk_typedef_proof (((((opt_name, (vs, t)), mx), A), morphs), comment) = 
248 
typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs), comment); 

6357  249 

250 
val typedefP = 

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

6723  254 

11744  255 
val _ = OuterSyntax.add_keywords ["morphisms"]; 
6357  256 
val _ = OuterSyntax.add_parsers [typedeclP, typedefP]; 
257 

4866  258 
end; 
6383  259 

260 

261 
end; 