13 type pcpo_info = |
13 type pcpo_info = |
14 { Rep_strict: thm, Abs_strict: thm, |
14 { Rep_strict: thm, Abs_strict: thm, |
15 Rep_bottom_iff: thm, Abs_bottom_iff: thm } |
15 Rep_bottom_iff: thm, Abs_bottom_iff: thm } |
16 |
16 |
17 val add_podef: binding * (string * sort) list * mixfix -> |
17 val add_podef: binding * (string * sort) list * mixfix -> |
18 term -> (binding * binding) option -> (Proof.context -> tactic) -> theory -> |
18 term -> Typedef.bindings option -> (Proof.context -> tactic) -> theory -> |
19 (Typedef.info * thm) * theory |
19 (Typedef.info * thm) * theory |
20 val add_cpodef: binding * (string * sort) list * mixfix -> |
20 val add_cpodef: binding * (string * sort) list * mixfix -> |
21 term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) -> |
21 term -> Typedef.bindings option -> (Proof.context -> tactic) * (Proof.context -> tactic) -> |
22 theory -> (Typedef.info * cpo_info) * theory |
22 theory -> (Typedef.info * cpo_info) * theory |
23 val add_pcpodef: binding * (string * sort) list * mixfix -> |
23 val add_pcpodef: binding * (string * sort) list * mixfix -> |
24 term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) -> |
24 term -> Typedef.bindings option -> (Proof.context -> tactic) * (Proof.context -> tactic) -> |
25 theory -> (Typedef.info * cpo_info * pcpo_info) * theory |
25 theory -> (Typedef.info * cpo_info * pcpo_info) * theory |
26 |
26 |
27 val cpodef_proof: |
27 val cpodef_proof: |
28 (binding * (string * sort) list * mixfix) * term |
28 (binding * (string * sort) list * mixfix) * term |
29 * (binding * binding) option -> theory -> Proof.state |
29 * Typedef.bindings option -> theory -> Proof.state |
30 val cpodef_proof_cmd: |
30 val cpodef_proof_cmd: |
31 (binding * (string * string option) list * mixfix) * string |
31 (binding * (string * string option) list * mixfix) * string |
32 * (binding * binding) option -> theory -> Proof.state |
32 * Typedef.bindings option -> theory -> Proof.state |
33 val pcpodef_proof: |
33 val pcpodef_proof: |
34 (binding * (string * sort) list * mixfix) * term |
34 (binding * (string * sort) list * mixfix) * term |
35 * (binding * binding) option -> theory -> Proof.state |
35 * Typedef.bindings option -> theory -> Proof.state |
36 val pcpodef_proof_cmd: |
36 val pcpodef_proof_cmd: |
37 (binding * (string * string option) list * mixfix) * string |
37 (binding * (string * string option) list * mixfix) * string |
38 * (binding * binding) option -> theory -> Proof.state |
38 * Typedef.bindings option -> theory -> Proof.state |
39 end |
39 end |
40 |
40 |
41 structure Cpodef : CPODEF = |
41 structure Cpodef : CPODEF = |
42 struct |
42 struct |
43 |
43 |
61 (* proving class instances *) |
61 (* proving class instances *) |
62 |
62 |
63 fun prove_cpo |
63 fun prove_cpo |
64 (name: binding) |
64 (name: binding) |
65 (newT: typ) |
65 (newT: typ) |
66 (Rep_name: binding, Abs_name: binding) |
66 opt_bindings |
67 (type_definition: thm) (* type_definition Rep Abs A *) |
67 (type_definition: thm) (* type_definition Rep Abs A *) |
68 (below_def: thm) (* op << == %x y. Rep x << Rep y *) |
68 (below_def: thm) (* op << == %x y. Rep x << Rep y *) |
69 (admissible: thm) (* adm (%x. x : set) *) |
69 (admissible: thm) (* adm (%x. x : set) *) |
70 (thy: theory) |
70 (thy: theory) |
71 = |
71 = |
72 let |
72 let |
|
73 val {Rep_name, Abs_name, ...} = Typedef.make_bindings name opt_bindings; |
73 val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible] |
74 val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible] |
74 val (full_tname, Ts) = dest_Type newT |
75 val (full_tname, Ts) = dest_Type newT |
75 val lhs_sorts = map (snd o dest_TFree) Ts |
76 val lhs_sorts = map (snd o dest_TFree) Ts |
76 fun tac ctxt = resolve_tac ctxt [@{thm typedef_cpo} OF cpo_thms] 1 |
77 fun tac ctxt = resolve_tac ctxt [@{thm typedef_cpo} OF cpo_thms] 1 |
77 val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy |
78 val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy |
100 end |
101 end |
101 |
102 |
102 fun prove_pcpo |
103 fun prove_pcpo |
103 (name: binding) |
104 (name: binding) |
104 (newT: typ) |
105 (newT: typ) |
105 (Rep_name: binding, Abs_name: binding) |
106 opt_bindings |
106 (type_definition: thm) (* type_definition Rep Abs A *) |
107 (type_definition: thm) (* type_definition Rep Abs A *) |
107 (below_def: thm) (* op << == %x y. Rep x << Rep y *) |
108 (below_def: thm) (* op << == %x y. Rep x << Rep y *) |
108 (bottom_mem: thm) (* bottom : set *) |
109 (bottom_mem: thm) (* bottom : set *) |
109 (thy: theory) |
110 (thy: theory) |
110 = |
111 = |
111 let |
112 let |
|
113 val {Rep_name, Abs_name, ...} = Typedef.make_bindings name opt_bindings; |
112 val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem] |
114 val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem] |
113 val (full_tname, Ts) = dest_Type newT |
115 val (full_tname, Ts) = dest_Type newT |
114 val lhs_sorts = map (snd o dest_TFree) Ts |
116 val lhs_sorts = map (snd o dest_TFree) Ts |
115 fun tac ctxt = resolve_tac ctxt [@{thm typedef_pcpo} OF pcpo_thms] 1 |
117 fun tac ctxt = resolve_tac ctxt [@{thm typedef_pcpo} OF pcpo_thms] 1 |
116 val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy |
118 val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy |
153 |
155 |
154 (*lhs*) |
156 (*lhs*) |
155 val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt') raw_args |
157 val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt') raw_args |
156 val full_tname = Sign.full_name thy tname |
158 val full_tname = Sign.full_name thy tname |
157 val newT = Type (full_tname, map TFree lhs_tfrees) |
159 val newT = Type (full_tname, map TFree lhs_tfrees) |
158 |
160 in |
159 val morphs = opt_morphs |
161 (newT, oldT, set) |
160 |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) |
162 end |
161 in |
163 |
162 (newT, oldT, set, morphs) |
164 fun add_podef typ set opt_bindings tac thy = |
163 end |
|
164 |
|
165 fun add_podef typ set opt_morphs tac thy = |
|
166 let |
165 let |
167 val name = #1 typ |
166 val name = #1 typ |
168 val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy |
167 val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy |
169 |> Typedef.add_typedef_global false typ set opt_morphs tac |
168 |> Typedef.add_typedef_global typ set opt_bindings tac |
170 val oldT = #rep_type (#1 info) |
169 val oldT = #rep_type (#1 info) |
171 val newT = #abs_type (#1 info) |
170 val newT = #abs_type (#1 info) |
172 val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) |
171 val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) |
173 |
172 |
174 val RepC = Const (Rep_name, newT --> oldT) |
173 val RepC = Const (Rep_name, newT --> oldT) |
187 |
186 |
188 fun prepare_cpodef |
187 fun prepare_cpodef |
189 (prep_term: Proof.context -> 'a -> term) |
188 (prep_term: Proof.context -> 'a -> term) |
190 (typ: binding * (string * sort) list * mixfix) |
189 (typ: binding * (string * sort) list * mixfix) |
191 (raw_set: 'a) |
190 (raw_set: 'a) |
192 (opt_morphs: (binding * binding) option) |
191 opt_bindings |
193 (thy: theory) |
192 (thy: theory) |
194 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = |
193 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = |
195 let |
194 let |
196 val name = #1 typ |
195 val name = #1 typ |
197 val (newT, oldT, set, morphs) = |
196 val (newT, oldT, set) = prepare prep_term name typ raw_set thy |
198 prepare prep_term name typ raw_set opt_morphs thy |
|
199 |
197 |
200 val goal_nonempty = |
198 val goal_nonempty = |
201 HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
199 HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
202 val goal_admissible = |
200 val goal_admissible = |
203 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
201 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
204 |
202 |
205 fun cpodef_result nonempty admissible thy = |
203 fun cpodef_result nonempty admissible thy = |
206 let |
204 let |
207 val ((info as (_, {type_definition, ...}), below_def), thy) = thy |
205 val ((info as (_, {type_definition, ...}), below_def), thy) = thy |
208 |> add_podef typ set opt_morphs (fn ctxt => resolve_tac ctxt [nonempty] 1) |
206 |> add_podef typ set opt_bindings (fn ctxt => resolve_tac ctxt [nonempty] 1) |
209 val (cpo_info, thy) = thy |
207 val (cpo_info, thy) = thy |
210 |> prove_cpo name newT morphs type_definition below_def admissible |
208 |> prove_cpo name newT opt_bindings type_definition below_def admissible |
211 in |
209 in |
212 ((info, cpo_info), thy) |
210 ((info, cpo_info), thy) |
213 end |
211 end |
214 in |
212 in |
215 (goal_nonempty, goal_admissible, cpodef_result) |
213 (goal_nonempty, goal_admissible, cpodef_result) |
219 |
217 |
220 fun prepare_pcpodef |
218 fun prepare_pcpodef |
221 (prep_term: Proof.context -> 'a -> term) |
219 (prep_term: Proof.context -> 'a -> term) |
222 (typ: binding * (string * sort) list * mixfix) |
220 (typ: binding * (string * sort) list * mixfix) |
223 (raw_set: 'a) |
221 (raw_set: 'a) |
224 (opt_morphs: (binding * binding) option) |
222 opt_bindings |
225 (thy: theory) |
223 (thy: theory) |
226 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = |
224 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = |
227 let |
225 let |
228 val name = #1 typ |
226 val name = #1 typ |
229 val (newT, oldT, set, morphs) = |
227 val (newT, oldT, set) = prepare prep_term name typ raw_set thy |
230 prepare prep_term name typ raw_set opt_morphs thy |
|
231 |
228 |
232 val goal_bottom_mem = |
229 val goal_bottom_mem = |
233 HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name bottom}, oldT), set)) |
230 HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name bottom}, oldT), set)) |
234 |
231 |
235 val goal_admissible = |
232 val goal_admissible = |
237 |
234 |
238 fun pcpodef_result bottom_mem admissible thy = |
235 fun pcpodef_result bottom_mem admissible thy = |
239 let |
236 let |
240 fun tac ctxt = resolve_tac ctxt [exI] 1 THEN resolve_tac ctxt [bottom_mem] 1 |
237 fun tac ctxt = resolve_tac ctxt [exI] 1 THEN resolve_tac ctxt [bottom_mem] 1 |
241 val ((info as (_, {type_definition, ...}), below_def), thy) = thy |
238 val ((info as (_, {type_definition, ...}), below_def), thy) = thy |
242 |> add_podef typ set opt_morphs tac |
239 |> add_podef typ set opt_bindings tac |
243 val (cpo_info, thy) = thy |
240 val (cpo_info, thy) = thy |
244 |> prove_cpo name newT morphs type_definition below_def admissible |
241 |> prove_cpo name newT opt_bindings type_definition below_def admissible |
245 val (pcpo_info, thy) = thy |
242 val (pcpo_info, thy) = thy |
246 |> prove_pcpo name newT morphs type_definition below_def bottom_mem |
243 |> prove_pcpo name newT opt_bindings type_definition below_def bottom_mem |
247 in |
244 in |
248 ((info, cpo_info, pcpo_info), thy) |
245 ((info, cpo_info, pcpo_info), thy) |
249 end |
246 end |
250 in |
247 in |
251 (goal_bottom_mem, goal_admissible, pcpodef_result) |
248 (goal_bottom_mem, goal_admissible, pcpodef_result) |
254 cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print (#1 typ)) |
251 cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print (#1 typ)) |
255 |
252 |
256 |
253 |
257 (* tactic interface *) |
254 (* tactic interface *) |
258 |
255 |
259 fun add_cpodef typ set opt_morphs (tac1, tac2) thy = |
256 fun add_cpodef typ set opt_bindings (tac1, tac2) thy = |
260 let |
257 let |
261 val (goal1, goal2, cpodef_result) = |
258 val (goal1, goal2, cpodef_result) = |
262 prepare_cpodef Syntax.check_term typ set opt_morphs thy |
259 prepare_cpodef Syntax.check_term typ set opt_bindings thy |
263 val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context) |
260 val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context) |
264 handle ERROR msg => cat_error msg |
261 handle ERROR msg => cat_error msg |
265 ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
262 ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
266 val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context) |
263 val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context) |
267 handle ERROR msg => cat_error msg |
264 handle ERROR msg => cat_error msg |
268 ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) |
265 ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) |
269 in cpodef_result thm1 thm2 thy end |
266 in cpodef_result thm1 thm2 thy end |
270 |
267 |
271 fun add_pcpodef typ set opt_morphs (tac1, tac2) thy = |
268 fun add_pcpodef typ set opt_bindings (tac1, tac2) thy = |
272 let |
269 let |
273 val (goal1, goal2, pcpodef_result) = |
270 val (goal1, goal2, pcpodef_result) = |
274 prepare_pcpodef Syntax.check_term typ set opt_morphs thy |
271 prepare_pcpodef Syntax.check_term typ set opt_bindings thy |
275 val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context) |
272 val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context) |
276 handle ERROR msg => cat_error msg |
273 handle ERROR msg => cat_error msg |
277 ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
274 ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) |
278 val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context) |
275 val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context) |
279 handle ERROR msg => cat_error msg |
276 handle ERROR msg => cat_error msg |
284 (* proof interface *) |
281 (* proof interface *) |
285 |
282 |
286 local |
283 local |
287 |
284 |
288 fun gen_cpodef_proof prep_term prep_constraint |
285 fun gen_cpodef_proof prep_term prep_constraint |
289 ((b, raw_args, mx), set, opt_morphs) thy = |
286 ((b, raw_args, mx), set, opt_bindings) thy = |
290 let |
287 let |
291 val ctxt = Proof_Context.init_global thy |
288 val ctxt = Proof_Context.init_global thy |
292 val args = map (apsnd (prep_constraint ctxt)) raw_args |
289 val args = map (apsnd (prep_constraint ctxt)) raw_args |
293 val (goal1, goal2, make_result) = |
290 val (goal1, goal2, make_result) = |
294 prepare_cpodef prep_term (b, args, mx) set opt_morphs thy |
291 prepare_cpodef prep_term (b, args, mx) set opt_bindings thy |
295 fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) |
292 fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) |
296 | after_qed _ = raise Fail "cpodef_proof" |
293 | after_qed _ = raise Fail "cpodef_proof" |
297 in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
294 in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
298 |
295 |
299 fun gen_pcpodef_proof prep_term prep_constraint |
296 fun gen_pcpodef_proof prep_term prep_constraint |
300 ((b, raw_args, mx), set, opt_morphs) thy = |
297 ((b, raw_args, mx), set, opt_bindings) thy = |
301 let |
298 let |
302 val ctxt = Proof_Context.init_global thy |
299 val ctxt = Proof_Context.init_global thy |
303 val args = map (apsnd (prep_constraint ctxt)) raw_args |
300 val args = map (apsnd (prep_constraint ctxt)) raw_args |
304 val (goal1, goal2, make_result) = |
301 val (goal1, goal2, make_result) = |
305 prepare_pcpodef prep_term (b, args, mx) set opt_morphs thy |
302 prepare_pcpodef prep_term (b, args, mx) set opt_bindings thy |
306 fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) |
303 fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) |
307 | after_qed _ = raise Fail "pcpodef_proof" |
304 | after_qed _ = raise Fail "pcpodef_proof" |
308 in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
305 in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end |
309 |
306 |
310 in |
307 in |
319 |
316 |
320 |
317 |
321 |
318 |
322 (** outer syntax **) |
319 (** outer syntax **) |
323 |
320 |
324 val typedef_proof_decl = |
321 local |
|
322 |
|
323 fun cpodef pcpo = |
325 (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- |
324 (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- |
326 (@{keyword "="} |-- Parse.term) -- |
325 (@{keyword "="} |-- Parse.term) -- |
327 Scan.option |
326 Scan.option |
328 (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) |
327 (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) |
329 |
328 >> (fn ((((args, t), mx), A), morphs) => |
330 fun mk_pcpodef_proof pcpo ((((args, t), mx), A), morphs) = |
329 Toplevel.theory_to_proof |
331 (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) |
330 ((if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) |
332 ((t, args, mx), A, morphs) |
331 ((t, args, mx), A, SOME (Typedef.make_morphisms t morphs)))) |
|
332 |
|
333 in |
333 |
334 |
334 val _ = |
335 val _ = |
335 Outer_Syntax.command @{command_keyword pcpodef} |
336 Outer_Syntax.command @{command_keyword pcpodef} |
336 "HOLCF type definition (requires admissibility proof)" |
337 "HOLCF type definition (requires admissibility proof)" |
337 (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof true)) |
338 (cpodef true) |
338 |
339 |
339 val _ = |
340 val _ = |
340 Outer_Syntax.command @{command_keyword cpodef} |
341 Outer_Syntax.command @{command_keyword cpodef} |
341 "HOLCF type definition (requires admissibility proof)" |
342 "HOLCF type definition (requires admissibility proof)" |
342 (typedef_proof_decl >> (Toplevel.theory_to_proof o mk_pcpodef_proof false)) |
343 (cpodef false) |
343 |
344 |
344 end |
345 end |
|
346 |
|
347 end |