113 fun add_typecopy_default_code tyco thy = |
113 fun add_typecopy_default_code tyco thy = |
114 let |
114 let |
115 val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs, |
115 val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs, |
116 typ = raw_ty_rep, ... } = get_info thy tyco; |
116 typ = raw_ty_rep, ... } = get_info thy tyco; |
117 val inst_meet = Sorts.meet_sort_typ (Sign.classes_of thy) |
117 val inst_meet = Sorts.meet_sort_typ (Sign.classes_of thy) |
118 (Logic.varifyT raw_ty_rep, [HOLogic.class_eq]); |
118 (Logic.varifyT raw_ty_rep, [HOLogic.class_eq]) handle Sorts.CLASS_ERROR _ => I; |
119 val ty_inst = Logic.varifyT |
119 val ty_inst = Logic.unvarifyT o inst_meet o Logic.varifyT; |
120 #> inst_meet |
|
121 #> Logic.unvarifyT; |
|
122 val vs = (map dest_TFree o snd o dest_Type o ty_inst) |
120 val vs = (map dest_TFree o snd o dest_Type o ty_inst) |
123 (Type (tyco, map TFree raw_vs)); |
121 (Type (tyco, map TFree raw_vs)); |
124 val ty_rep = ty_inst raw_ty_rep; |
122 val ty_rep = ty_inst raw_ty_rep; |
125 val SOME { Rep_inject = proj_inject, ... } = TypedefPackage.get_info thy tyco; |
123 val SOME { Rep_inject = proj_inject, ... } = TypedefPackage.get_info thy tyco; |
126 val ty_constr = Logic.unvarifyT (Sign.the_const_type thy constr_name); |
124 val ty_constr = Logic.unvarifyT (Sign.the_const_type thy constr_name); |
129 fun mk_eq ty t_x t_y = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT) |
127 fun mk_eq ty t_x t_y = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT) |
130 $ t_x $ t_y; |
128 $ t_x $ t_y; |
131 fun mk_proj t = Const (proj, ty --> ty_rep) $ t; |
129 fun mk_proj t = Const (proj, ty --> ty_rep) $ t; |
132 val (t_x, t_y) = (Free ("x", ty), Free ("y", ty)); |
130 val (t_x, t_y) = (Free ("x", ty), Free ("y", ty)); |
133 val def_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
131 val def_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) |
134 (mk_eq ty t_x t_y, mk_eq ty_rep (mk_proj t_x) (mk_proj t_y)); |
132 (mk_eq ty t_x t_y, HOLogic.mk_eq (mk_proj t_x, mk_proj t_y)); |
135 fun mk_eq_refl thy = @{thm HOL.eq_refl} |
133 fun mk_eq_refl thy = @{thm HOL.eq_refl} |
136 |> Thm.instantiate |
134 |> Thm.instantiate |
137 ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []) |
135 ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT ty)], []) |
138 |> AxClass.unoverload thy; |
136 |> AxClass.unoverload thy; |
139 in |
137 in |
153 |-> (fn def_thm => Code.add_eqn def_thm) |
151 |-> (fn def_thm => Code.add_eqn def_thm) |
154 |> `(fn thy => mk_eq_refl thy) |
152 |> `(fn thy => mk_eq_refl thy) |
155 |-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm) |
153 |-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm) |
156 end; |
154 end; |
157 |
155 |
158 fun perhaps_add_typecopy_default_code tyco thy = |
|
159 add_typecopy_default_code tyco thy handle Sorts.CLASS_ERROR _ => thy; |
|
160 |
|
161 val setup = |
156 val setup = |
162 TypecopyInterpretation.init |
157 TypecopyInterpretation.init |
163 #> interpretation perhaps_add_typecopy_default_code |
158 #> interpretation add_typecopy_default_code |
164 |
159 |
165 end; |
160 end; |