63 fun fold_adm_mem thm NONE = thm |
63 fun fold_adm_mem thm NONE = thm |
64 | fold_adm_mem thm (SOME set_def) = |
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} |
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 |
66 in rule OF [set_def, thm] end |
67 |
67 |
68 fun fold_UU_mem thm NONE = thm |
68 fun fold_bottom_mem thm NONE = thm |
69 | fold_UU_mem thm (SOME set_def) = |
69 | fold_bottom_mem thm (SOME set_def) = |
70 let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp} |
70 let val rule = @{lemma "A == B ==> bottom : B ==> bottom : A" by simp} |
71 in rule OF [set_def, thm] end |
71 in rule OF [set_def, thm] end |
72 |
72 |
73 (* proving class instances *) |
73 (* proving class instances *) |
74 |
74 |
75 fun prove_cpo |
75 fun prove_cpo |
118 (newT: typ) |
118 (newT: typ) |
119 (Rep_name: binding, Abs_name: binding) |
119 (Rep_name: binding, Abs_name: binding) |
120 (type_definition: thm) (* type_definition Rep Abs A *) |
120 (type_definition: thm) (* type_definition Rep Abs A *) |
121 (set_def: thm option) (* A == set *) |
121 (set_def: thm option) (* A == set *) |
122 (below_def: thm) (* op << == %x y. Rep x << Rep y *) |
122 (below_def: thm) (* op << == %x y. Rep x << Rep y *) |
123 (UU_mem: thm) (* UU : set *) |
123 (bottom_mem: thm) (* bottom : set *) |
124 (thy: theory) |
124 (thy: theory) |
125 = |
125 = |
126 let |
126 let |
127 val UU_mem' = fold_UU_mem UU_mem set_def |
127 val bottom_mem' = fold_bottom_mem bottom_mem set_def |
128 val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'] |
128 val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem'] |
129 val (full_tname, Ts) = dest_Type newT |
129 val (full_tname, Ts) = dest_Type newT |
130 val lhs_sorts = map (snd o dest_TFree) Ts |
130 val lhs_sorts = map (snd o dest_TFree) Ts |
131 val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 |
131 val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 |
132 val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy |
132 val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy |
133 val pcpo_thms' = map (Thm.transfer thy) pcpo_thms |
133 val pcpo_thms' = map (Thm.transfer thy) pcpo_thms |
250 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = |
250 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = |
251 let |
251 let |
252 val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = |
252 val (newT, oldT, set, morphs as (Rep_name, Abs_name)) = |
253 prepare prep_term name typ raw_set opt_morphs thy |
253 prepare prep_term name typ raw_set opt_morphs thy |
254 |
254 |
255 val goal_UU_mem = |
255 val goal_bottom_mem = |
256 HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)) |
256 HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name bottom}, oldT), set)) |
257 |
257 |
258 val goal_admissible = |
258 val goal_admissible = |
259 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
259 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))) |
260 |
260 |
261 fun pcpodef_result UU_mem admissible thy = |
261 fun pcpodef_result bottom_mem admissible thy = |
262 let |
262 let |
263 val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1 |
263 val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1 |
264 val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy |
264 val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy |
265 |> add_podef def (SOME name) typ set opt_morphs tac |
265 |> add_podef def (SOME name) typ set opt_morphs tac |
266 val (cpo_info, thy) = thy |
266 val (cpo_info, thy) = thy |
267 |> prove_cpo name newT morphs type_definition set_def below_def admissible |
267 |> prove_cpo name newT morphs type_definition set_def below_def admissible |
268 val (pcpo_info, thy) = thy |
268 val (pcpo_info, thy) = thy |
269 |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem |
269 |> prove_pcpo name newT morphs type_definition set_def below_def bottom_mem |
270 in |
270 in |
271 ((info, cpo_info, pcpo_info), thy) |
271 ((info, cpo_info, pcpo_info), thy) |
272 end |
272 end |
273 in |
273 in |
274 (goal_UU_mem, goal_admissible, pcpodef_result) |
274 (goal_bottom_mem, goal_admissible, pcpodef_result) |
275 end |
275 end |
276 handle ERROR msg => |
276 handle ERROR msg => |
277 cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name)) |
277 cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name)) |
278 |
278 |
279 |
279 |