99 | Const (@{const_name part_equivp}, _) $ rel => |
99 | Const (@{const_name part_equivp}, _) $ rel => |
100 HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph) |
100 HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph) |
101 | _ => error "unsupported equivalence theorem" |
101 | _ => error "unsupported equivalence theorem" |
102 ) |
102 ) |
103 val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body)); |
103 val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body)); |
104 val qty_name = (fst o dest_Type) qty |
104 val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty |
105 val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name) |
105 val cr_rel_name = Binding.prefix_name "cr_" qty_name |
106 val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy |
106 val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy |
107 val ((_, (_ , def_thm)), lthy'') = |
107 val ((_, (_ , def_thm)), lthy'') = |
108 Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy' |
108 Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy' |
109 in |
109 in |
110 (def_thm, lthy'') |
110 (def_thm, lthy'') |
113 fun setup_lifting_package gen_code quot3_thm equiv_thm lthy = |
113 fun setup_lifting_package gen_code quot3_thm equiv_thm lthy = |
114 let |
114 let |
115 val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm |
115 val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm |
116 val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy |
116 val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy |
117 val (rty, qty) = (dest_funT o fastype_of) abs_fun |
117 val (rty, qty) = (dest_funT o fastype_of) abs_fun |
118 val qty_name = (fst o dest_Type) qty |
118 val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty |
119 val quotient_thm_name = Binding.prefix_name "Quotient_" (Binding.qualified_name qty_name) |
119 val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name |
120 val (reflp_thm, quot_thm) = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of |
120 val (reflp_thm, quot_thm) = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of |
121 Const (@{const_name equivp}, _) $ _ => |
121 Const (@{const_name equivp}, _) $ _ => |
122 (SOME (equiv_thm RS @{thm equivp_reflp2}), |
122 (SOME (equiv_thm RS @{thm equivp_reflp2}), |
123 [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}) |
123 [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}) |
124 | Const (@{const_name part_equivp}, _) $ _ => |
124 | Const (@{const_name part_equivp}, _) $ _ => |