1 (* Title: HOLCF/Tools/cpodef.ML |
|
2 Author: Brian Huffman |
|
3 |
|
4 Primitive domain definitions for HOLCF, similar to Gordon/HOL-style |
|
5 typedef (see also ~~/src/HOL/Tools/typedef.ML). |
|
6 *) |
|
7 |
|
8 signature CPODEF = |
|
9 sig |
|
10 type cpo_info = |
|
11 { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
|
12 is_lub: thm, lub: thm, compact: thm } |
|
13 type pcpo_info = |
|
14 { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm, |
|
15 Rep_defined: thm, Abs_defined: thm } |
|
16 |
|
17 val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix -> |
|
18 term -> (binding * binding) option -> tactic -> theory -> |
|
19 (Typedef.info * thm) * theory |
|
20 val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix -> |
|
21 term -> (binding * binding) option -> tactic * tactic -> theory -> |
|
22 (Typedef.info * cpo_info) * theory |
|
23 val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix -> |
|
24 term -> (binding * binding) option -> tactic * tactic -> theory -> |
|
25 (Typedef.info * cpo_info * pcpo_info) * theory |
|
26 |
|
27 val cpodef_proof: (bool * binding) |
|
28 * (binding * (string * sort) list * mixfix) * term |
|
29 * (binding * binding) option -> theory -> Proof.state |
|
30 val cpodef_proof_cmd: (bool * binding) |
|
31 * (binding * (string * string option) list * mixfix) * string |
|
32 * (binding * binding) option -> theory -> Proof.state |
|
33 val pcpodef_proof: (bool * binding) |
|
34 * (binding * (string * sort) list * mixfix) * term |
|
35 * (binding * binding) option -> theory -> Proof.state |
|
36 val pcpodef_proof_cmd: (bool * binding) |
|
37 * (binding * (string * string option) list * mixfix) * string |
|
38 * (binding * binding) option -> theory -> Proof.state |
|
39 end; |
|
40 |
|
41 structure Cpodef :> CPODEF = |
|
42 struct |
|
43 |
|
44 (** type definitions **) |
|
45 |
|
46 type cpo_info = |
|
47 { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, |
|
48 is_lub: thm, lub: thm, compact: thm } |
|
49 |
|
50 type pcpo_info = |
|
51 { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm, |
|
52 Rep_defined: thm, Abs_defined: thm } |
|
53 |
|
54 (* building terms *) |
|
55 |
|
56 fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT); |
|
57 fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); |
|
58 |
|
59 fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT); |
|
60 |
|
61 (* manipulating theorems *) |
|
62 |
|
63 fun fold_adm_mem thm NONE = thm |
|
64 | fold_adm_mem thm (SOME set_def) = |
|
65 let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp} |
|
66 in rule OF [set_def, thm] end; |
|
67 |
|
68 fun fold_UU_mem thm NONE = thm |
|
69 | fold_UU_mem thm (SOME set_def) = |
|
70 let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp} |
|
71 in rule OF [set_def, thm] end; |
|
72 |
|
73 (* proving class instances *) |
|
74 |
|
75 fun prove_cpo |
|
76 (name: binding) |
|
77 (newT: typ) |
|
78 (Rep_name: binding, Abs_name: binding) |
|
79 (type_definition: thm) (* type_definition Rep Abs A *) |
|
80 (set_def: thm option) (* A == set *) |
|
81 (below_def: thm) (* op << == %x y. Rep x << Rep y *) |
|
82 (admissible: thm) (* adm (%x. x : set) *) |
|
83 (thy: theory) |
|
84 = |
|
85 let |
|
86 val admissible' = fold_adm_mem admissible set_def; |
|
87 val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible']; |
|
88 val (full_tname, Ts) = dest_Type newT; |
|
89 val lhs_sorts = map (snd o dest_TFree) Ts; |
|
90 val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1; |
|
91 val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy; |
|
92 (* transfer thms so that they will know about the new cpo instance *) |
|
93 val cpo_thms' = map (Thm.transfer thy) cpo_thms; |
|
94 fun make thm = Drule.zero_var_indexes (thm OF cpo_thms'); |
|
95 val cont_Rep = make @{thm typedef_cont_Rep}; |
|
96 val cont_Abs = make @{thm typedef_cont_Abs}; |
|
97 val is_lub = make @{thm typedef_is_lub}; |
|
98 val lub = make @{thm typedef_lub}; |
|
99 val compact = make @{thm typedef_compact}; |
|
100 val (_, thy) = |
|
101 thy |
|
102 |> Sign.add_path (Binding.name_of name) |
|
103 |> Global_Theory.add_thms |
|
104 ([((Binding.prefix_name "adm_" name, admissible'), []), |
|
105 ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), |
|
106 ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), |
|
107 ((Binding.prefix_name "is_lub_" name, is_lub ), []), |
|
108 ((Binding.prefix_name "lub_" name, lub ), []), |
|
109 ((Binding.prefix_name "compact_" name, compact ), [])]) |
|
110 ||> Sign.parent_path; |
|
111 val cpo_info : cpo_info = |
|
112 { below_def = below_def, adm = admissible', cont_Rep = cont_Rep, |
|
113 cont_Abs = cont_Abs, is_lub = is_lub, lub = lub, compact = compact }; |
|
114 in |
|
115 (cpo_info, thy) |
|
116 end; |
|
117 |
|
118 fun prove_pcpo |
|
119 (name: binding) |
|
120 (newT: typ) |
|
121 (Rep_name: binding, Abs_name: binding) |
|
122 (type_definition: thm) (* type_definition Rep Abs A *) |
|
123 (set_def: thm option) (* A == set *) |
|
124 (below_def: thm) (* op << == %x y. Rep x << Rep y *) |
|
125 (UU_mem: thm) (* UU : set *) |
|
126 (thy: theory) |
|
127 = |
|
128 let |
|
129 val UU_mem' = fold_UU_mem UU_mem set_def; |
|
130 val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem']; |
|
131 val (full_tname, Ts) = dest_Type newT; |
|
132 val lhs_sorts = map (snd o dest_TFree) Ts; |
|
133 val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1; |
|
134 val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy; |
|
135 val pcpo_thms' = map (Thm.transfer thy) pcpo_thms; |
|
136 fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms'); |
|
137 val Rep_strict = make @{thm typedef_Rep_strict}; |
|
138 val Abs_strict = make @{thm typedef_Abs_strict}; |
|
139 val Rep_bottom_iff = make @{thm typedef_Rep_bottom_iff}; |
|
140 val Abs_bottom_iff = make @{thm typedef_Abs_bottom_iff}; |
|
141 val Rep_defined = make @{thm typedef_Rep_defined}; |
|
142 val Abs_defined = make @{thm typedef_Abs_defined}; |
|
143 val (_, thy) = |
|
144 thy |
|
145 |> Sign.add_path (Binding.name_of name) |
|
146 |> Global_Theory.add_thms |
|
147 ([((Binding.suffix_name "_strict" Rep_name, Rep_strict), []), |
|
148 ((Binding.suffix_name "_strict" Abs_name, Abs_strict), []), |
|
149 ((Binding.suffix_name "_bottom_iff" Rep_name, Rep_bottom_iff), []), |
|
150 ((Binding.suffix_name "_bottom_iff" Abs_name, Abs_bottom_iff), []), |
|
151 ((Binding.suffix_name "_defined" Rep_name, Rep_defined), []), |
|
152 ((Binding.suffix_name "_defined" Abs_name, Abs_defined), [])]) |
|
153 ||> Sign.parent_path; |
|
154 val pcpo_info = |
|
155 { Rep_strict = Rep_strict, Abs_strict = Abs_strict, |
|
156 Rep_bottom_iff = Rep_bottom_iff, Abs_bottom_iff = Abs_bottom_iff, |
|
157 Rep_defined = Rep_defined, Abs_defined = Abs_defined }; |
|
158 in |
|
159 (pcpo_info, thy) |
|
160 end; |
|
161 |
|
162 (* prepare_cpodef *) |
|
163 |
|
164 fun declare_type_name a = |
|
165 Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); |
|
166 |
|
167 fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy = |
|
168 let |
|
169 val _ = Theory.requires thy "Cpodef" "cpodefs"; |
|
170 |
|
171 (*rhs*) |
|
172 val tmp_ctxt = |
|
173 ProofContext.init_global thy |
|
174 |> fold (Variable.declare_typ o TFree) raw_args; |
|
175 val set = prep_term tmp_ctxt raw_set; |
|
176 val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set; |
|
177 |
|
178 val setT = Term.fastype_of set; |
|
179 val oldT = HOLogic.dest_setT setT handle TYPE _ => |
|
180 error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT)); |
|
181 |
|
182 (*lhs*) |
|
183 val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args; |
|
184 val full_tname = Sign.full_name thy tname; |
|
185 val newT = Type (full_tname, map TFree lhs_tfrees); |
|
186 |
|
187 val morphs = opt_morphs |
|
188 |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); |
|
189 in |
|
190 (newT, oldT, set, morphs) |
|
191 end |
|
192 |
|
193 fun add_podef def opt_name typ set opt_morphs tac thy = |
|
194 let |
|
195 val name = the_default (#1 typ) opt_name; |
|
196 val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy |
|
197 |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac; |
|
198 val oldT = #rep_type (#1 info); |
|
199 val newT = #abs_type (#1 info); |
|
200 val lhs_tfrees = map dest_TFree (snd (dest_Type newT)); |
|
201 |
|
202 val RepC = Const (Rep_name, newT --> oldT); |
|
203 val below_eqn = Logic.mk_equals (below_const newT, |
|
204 Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))); |
|
205 val lthy3 = thy2 |
|
206 |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po}); |
|
207 val ((_, (_, below_ldef)), lthy4) = lthy3 |
|
208 |> Specification.definition (NONE, |
|
209 ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn)); |
|
210 val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4); |
|
211 val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef; |
|
212 val thy5 = lthy4 |
|
213 |> Class.prove_instantiation_instance |
|
214 (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1)) |
|
215 |> Local_Theory.exit_global; |
|
216 in ((info, below_def), thy5) end; |
|
217 |
|
218 fun prepare_cpodef |
|
219 (prep_term: Proof.context -> 'a -> term) |
|
220 (def: bool) |
|
221 (name: binding) |
|
222 (typ: binding * (string * sort) list * mixfix) |
|
223 (raw_set: 'a) |
|
224 (opt_morphs: (binding * binding) option) |
|
225 (thy: theory) |
|
226 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = |
|
227 let |
|
228 val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = |
|
229 prepare prep_term name typ raw_set opt_morphs thy; |
|
230 |
|
231 val goal_nonempty = |
|
232 HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); |
|
233 val goal_admissible = |
|
234 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); |
|
235 |
|
236 fun cpodef_result nonempty admissible thy = |
|
237 let |
|
238 val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy |
|
239 |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1); |
|
240 val (cpo_info, thy3) = thy2 |
|
241 |> prove_cpo name newT morphs type_definition set_def below_def admissible; |
|
242 in |
|
243 ((info, cpo_info), thy3) |
|
244 end; |
|
245 in |
|
246 (goal_nonempty, goal_admissible, cpodef_result) |
|
247 end |
|
248 handle ERROR msg => |
|
249 cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name)); |
|
250 |
|
251 fun prepare_pcpodef |
|
252 (prep_term: Proof.context -> 'a -> term) |
|
253 (def: bool) |
|
254 (name: binding) |
|
255 (typ: binding * (string * sort) list * mixfix) |
|
256 (raw_set: 'a) |
|
257 (opt_morphs: (binding * binding) option) |
|
258 (thy: theory) |
|
259 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = |
|
260 let |
|
261 val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = |
|
262 prepare prep_term name typ raw_set opt_morphs thy; |
|
263 |
|
264 val goal_UU_mem = |
|
265 HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)); |
|
266 |
|
267 val goal_admissible = |
|
268 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); |
|
269 |
|
270 fun pcpodef_result UU_mem admissible thy = |
|
271 let |
|
272 val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1; |
|
273 val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy |
|
274 |> add_podef def (SOME name) typ set opt_morphs tac; |
|
275 val (cpo_info, thy3) = thy2 |
|
276 |> prove_cpo name newT morphs type_definition set_def below_def admissible; |
|
277 val (pcpo_info, thy4) = thy3 |
|
278 |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem; |
|
279 in |
|
280 ((info, cpo_info, pcpo_info), thy4) |
|
281 end; |
|
282 in |
|
283 (goal_UU_mem, goal_admissible, pcpodef_result) |
|
284 end |
|
285 handle ERROR msg => |
|
286 cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name)); |
|
287 |
|
288 |
|
289 (* tactic interface *) |
|
290 |
|
291 fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy = |
|
292 let |
|
293 val name = the_default (#1 typ) opt_name; |
|
294 val (goal1, goal2, cpodef_result) = |
|
295 prepare_cpodef Syntax.check_term def name typ set opt_morphs thy; |
|
296 val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) |
|
297 handle ERROR msg => cat_error msg |
|
298 ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); |
|
299 val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) |
|
300 handle ERROR msg => cat_error msg |
|
301 ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)); |
|
302 in cpodef_result thm1 thm2 thy end; |
|
303 |
|
304 fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy = |
|
305 let |
|
306 val name = the_default (#1 typ) opt_name; |
|
307 val (goal1, goal2, pcpodef_result) = |
|
308 prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy; |
|
309 val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) |
|
310 handle ERROR msg => cat_error msg |
|
311 ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)); |
|
312 val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) |
|
313 handle ERROR msg => cat_error msg |
|
314 ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)); |
|
315 in pcpodef_result thm1 thm2 thy end; |
|
316 |
|
317 |
|
318 (* proof interface *) |
|
319 |
|
320 local |
|
321 |
|
322 fun gen_cpodef_proof prep_term prep_constraint |
|
323 ((def, name), (b, raw_args, mx), set, opt_morphs) thy = |
|
324 let |
|
325 val ctxt = ProofContext.init_global thy; |
|
326 val args = map (apsnd (prep_constraint ctxt)) raw_args; |
|
327 val (goal1, goal2, make_result) = |
|
328 prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy; |
|
329 fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) |
|
330 | after_qed _ = raise Fail "cpodef_proof"; |
|
331 in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end; |
|
332 |
|
333 fun gen_pcpodef_proof prep_term prep_constraint |
|
334 ((def, name), (b, raw_args, mx), set, opt_morphs) thy = |
|
335 let |
|
336 val ctxt = ProofContext.init_global thy; |
|
337 val args = map (apsnd (prep_constraint ctxt)) raw_args; |
|
338 val (goal1, goal2, make_result) = |
|
339 prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy; |
|
340 fun after_qed [[th1, th2]] = ProofContext.background_theory (snd o make_result th1 th2) |
|
341 | after_qed _ = raise Fail "pcpodef_proof"; |
|
342 in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end; |
|
343 |
|
344 in |
|
345 |
|
346 fun cpodef_proof x = gen_cpodef_proof Syntax.check_term (K I) x; |
|
347 fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term Typedecl.read_constraint x; |
|
348 |
|
349 fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term (K I) x; |
|
350 fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term Typedecl.read_constraint x; |
|
351 |
|
352 end; |
|
353 |
|
354 |
|
355 |
|
356 (** outer syntax **) |
|
357 |
|
358 val typedef_proof_decl = |
|
359 Scan.optional (Parse.$$$ "(" |-- |
|
360 ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding || |
|
361 Parse.binding >> (fn s => (true, SOME s))) |
|
362 --| Parse.$$$ ")") (true, NONE) -- |
|
363 (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- |
|
364 (Parse.$$$ "=" |-- Parse.term) -- |
|
365 Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)); |
|
366 |
|
367 fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) = |
|
368 (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) |
|
369 ((def, the_default t opt_name), (t, args, mx), A, morphs); |
|
370 |
|
371 val _ = |
|
372 Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" |
|
373 Keyword.thy_goal |
|
374 (typedef_proof_decl >> |
|
375 (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true))); |
|
376 |
|
377 val _ = |
|
378 Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" |
|
379 Keyword.thy_goal |
|
380 (typedef_proof_decl >> |
|
381 (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false))); |
|
382 |
|
383 end; |
|