117 by (simp) |
117 by (simp) |
118 |
118 |
119 ML {* val qty = @{typ "my_int"} *} |
119 ML {* val qty = @{typ "my_int"} *} |
120 ML {* val ty_name = "my_int" *} |
120 ML {* val ty_name = "my_int" *} |
121 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
121 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
122 ML {* val t_defs = @{thms PLUS_def} *} |
122 ML {* val defs = @{thms PLUS_def} *} |
123 |
123 |
124 ML {* |
124 ML {* |
125 fun lift_thm_my_int lthy t = |
125 fun lift_thm_my_int lthy t = |
126 lift_thm lthy qty ty_name rsp_thms t_defs t |
126 lift_thm lthy qty ty_name rsp_thms defs t |
127 *} |
127 *} |
128 |
128 |
129 ML {* |
129 ML {* |
130 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty; |
130 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty; |
131 *} |
131 *} |
148 |
148 |
149 |
149 |
150 |
150 |
151 |
151 |
152 text {* Below is the construction site code used if things do not work *} |
152 text {* Below is the construction site code used if things do not work *} |
153 |
153 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "my_int" *} |
154 |
|
155 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
154 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
156 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
155 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
157 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
156 ML {* val defs_sym = add_lower_defs @{context} defs *} |
158 |
157 ML {* val consts = lookup_quot_consts defs *} |
159 |
|
160 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
158 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
161 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
159 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
162 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
160 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
163 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
161 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
164 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
162 ML {* val t_a = simp_allex_prs quot [] t_l *} |
165 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *} |
163 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} |
166 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
164 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
167 ML {* ObjectLogic.rulify t_r *} |
165 ML {* ObjectLogic.rulify t_r *} |
168 |
166 |
|
167 thm FORALL_PRS |
169 |
168 |
170 |
|