author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29579  cb520b766e00 
child 30345  76fd85bbf139 
permissions  rwrr 
4866  1 
(* Title: HOL/Tools/typedef_package.ML 
16458  2 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 
4866  3 

21352  4 
Gordon/HOLstyle type definitions: create a new syntactic type 
5 
represented by a nonempty 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)] 
29579  115 
> PureThy.add_defs false [Thm.no_attributes (apfst (Binding.name) 
116 
(PrimitiveDefs.mk_defpair (setC, set)))] 

19705  117 
> (fn [th] => pair (SOME th)) 
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

118 
else (NONE, theory); 
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

119 
fun contract_def NONE th = th 
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

120 
 contract_def (SOME def_eq) th = 
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

121 
let 
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

122 
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

123 
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

124 
in Drule.standard (Drule.equal_elim_rule2 OF [goal_eq, th]) end; 
18358  125 

29056  126 
fun typedef_result inhabited = 
25495  127 
ObjectLogic.typedecl (t, vs, mx) 
25458
ba8f5e4fa336
separated typedecl module, providing typedecl command with interpretation
haftmann
parents:
24926
diff
changeset

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

129 
#> Sign.add_consts_i 
6383  130 
[(Rep_name, newT > oldT, NoSyn), 
29053  131 
(Abs_name, oldT > newT, NoSyn)] 
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

132 
#> add_def 
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

133 
#> (fn set_def => 
29579  134 
PureThy.add_axioms [((Binding.name typedef_name, typedef_prop), 
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

135 
[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

136 
##>> pair set_def) 
21352  137 
##> Theory.add_deps "" (dest_Const RepC) typedef_deps 
138 
##> 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

139 
#> (fn ([type_definition], set_def) => fn thy1 => 
11822  140 
let 
141 
fun make th = Drule.standard (th OF [type_definition]); 

18377  142 
val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, 
19705  143 
Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) = 
144 
thy1 

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

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

146 
> PureThy.add_thms 
29579  147 
((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []), 
29056  148 
((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []), 
149 
((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []), 

150 
((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []), 

151 
((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []), 

152 
((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}), 

24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24830
diff
changeset

153 
[RuleCases.case_names [Rep_name], Induct.cases_pred full_name]), 
29056  154 
((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

155 
[RuleCases.case_names [Abs_name], Induct.cases_type full_tname]), 
29056  156 
((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}), 
24861
cc669ca5f382
tuned Induct interface: prefer pred'' over set'';
wenzelm
parents:
24830
diff
changeset

157 
[RuleCases.case_names [Rep_name], Induct.induct_pred full_name]), 
29056  158 
((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

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

160 
> Sign.parent_path; 
19705  161 
val info = {rep_type = oldT, abs_type = newT, 
162 
Rep_name = full Rep_name, Abs_name = full Abs_name, 

28848  163 
inhabited = inhabited, type_definition = type_definition, set_def = set_def, 
19705  164 
Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, 
165 
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, 

11822  166 
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}; 
25535  167 
in 
168 
thy2 

169 
> put_info full_tname info 

170 
> TypedefInterpretation.data full_tname 

171 
> pair (full_tname, info) 

172 
end); 

6383  173 

29056  174 

4866  175 
(* errors *) 
176 

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

178 

179 
val illegal_vars = 

29264  180 
if null (Term.add_vars set []) andalso null (Term.add_tvars set []) then [] 
4866  181 
else ["Illegal schematic variable(s) on rhs"]; 
182 

183 
val dup_lhs_tfrees = 

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

187 
val extra_rhs_tfrees = 

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

191 
val illegal_frees = 

29264  192 
(case Term.add_frees set [] of [] => [] 
193 
 xs => ["Illegal variables on rhs: " ^ show_names xs]); 

4866  194 

195 
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

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

197 

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

198 
(*test theory errors now!*) 
29061
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

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

201 
> 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

202 

29062  203 
in (set, goal, goal_pat, typedef_result) end 
18678  204 
handle ERROR msg => err_in_typedef msg name; 
4866  205 

206 

29056  207 
(* add_typedef: tactic interface *) 
4866  208 

28662  209 
fun add_typedef def opt_name typ set opt_morphs tac thy = 
6383  210 
let 
17922  211 
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

212 
val (set, goal, _, typedef_result) = 
28662  213 
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

214 
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

215 
handle ERROR msg => cat_error msg 
c67cc9402ba9
inhabitance goal is now stated in original form and result contracted 
wenzelm
parents:
29059
diff
changeset

216 
("Failed to prove nonemptiness 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

217 
in typedef_result inhabited thy end; 
4866  218 

17339  219 

29056  220 
(* typedef: proof interface *) 
6383  221 

17339  222 
local 
223 

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

11822  225 
let 
29062  226 
val (_, goal, goal_pat, typedef_result) = 
13443  227 
prepare_typedef prep_term def name typ set opt_morphs thy; 
21352  228 
fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th); 
29062  229 
in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end; 
17339  230 

231 
in 

6383  232 

28662  233 
val typedef = gen_typedef Syntax.check_term; 
234 
val typedef_cmd = gen_typedef Syntax.read_term; 

17339  235 

19705  236 
end; 
15259  237 

238 

239 

6383  240 
(** outer syntax **) 
241 

29056  242 
local structure P = OuterParse in 
6383  243 

27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
26939
diff
changeset

244 
val _ = OuterKeyword.keyword "morphisms"; 
24867  245 

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

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

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

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

251 
Scan.option (P.$$$ "morphisms"  P.!!! (P.name  P.name)); 
6357  252 

17339  253 
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) = 
28662  254 
typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs); 
6357  255 

24867  256 
val _ = 
29056  257 
OuterSyntax.command "typedef" "HOL type definition (requires nonemptiness proof)" 
258 
OuterKeyword.thy_goal 

17339  259 
(typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef))); 
6357  260 

29056  261 
end; 
262 

263 

25535  264 
val setup = TypedefInterpretation.init; 
265 

4866  266 
end; 