191 end |
191 end |
192 |
192 |
193 fun add_podef def opt_name typ set opt_morphs tac thy = |
193 fun add_podef def opt_name typ set opt_morphs tac thy = |
194 let |
194 let |
195 val name = the_default (#1 typ) opt_name; |
195 val name = the_default (#1 typ) opt_name; |
196 val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy |
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; |
197 |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac; |
198 val oldT = #rep_type info; |
198 val oldT = #rep_type (#1 info); |
199 val newT = #abs_type info; |
199 val newT = #abs_type (#1 info); |
200 val lhs_tfrees = map dest_TFree (snd (dest_Type newT)); |
200 val lhs_tfrees = map dest_TFree (snd (dest_Type newT)); |
201 |
201 |
202 val RepC = Const (Rep_name, newT --> oldT); |
202 val RepC = Const (Rep_name, newT --> oldT); |
203 val below_eqn = Logic.mk_equals (below_const newT, |
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)))); |
204 Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))); |
233 val goal_admissible = |
233 val goal_admissible = |
234 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); |
234 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); |
235 |
235 |
236 fun cpodef_result nonempty admissible thy = |
236 fun cpodef_result nonempty admissible thy = |
237 let |
237 let |
238 val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy |
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); |
239 |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1); |
240 val (cpo_info, thy3) = thy2 |
240 val (cpo_info, thy3) = thy2 |
241 |> prove_cpo name newT morphs type_definition set_def below_def admissible; |
241 |> prove_cpo name newT morphs type_definition set_def below_def admissible; |
242 in |
242 in |
243 ((info, cpo_info), thy3) |
243 ((info, cpo_info), thy3) |
268 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); |
268 HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); |
269 |
269 |
270 fun pcpodef_result UU_mem admissible thy = |
270 fun pcpodef_result UU_mem admissible thy = |
271 let |
271 let |
272 val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1; |
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 |
273 val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy |
274 |> add_podef def (SOME name) typ set opt_morphs tac; |
274 |> add_podef def (SOME name) typ set opt_morphs tac; |
275 val (cpo_info, thy3) = thy2 |
275 val (cpo_info, thy3) = thy2 |
276 |> prove_cpo name newT morphs type_definition set_def below_def admissible; |
276 |> prove_cpo name newT morphs type_definition set_def below_def admissible; |
277 val (pcpo_info, thy4) = thy3 |
277 val (pcpo_info, thy4) = thy3 |
278 |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem; |
278 |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem; |