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