126 ML {* |
127 ML {* |
127 fun lift_thm_my_int lthy t = |
128 fun lift_thm_my_int lthy t = |
128 lift_thm lthy qty ty_name rsp_thms defs t |
129 lift_thm lthy qty ty_name rsp_thms defs t |
129 *} |
130 *} |
130 |
131 |
131 ML {* |
|
132 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty; |
|
133 *} |
|
134 |
|
135 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *} |
132 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *} |
136 |
133 |
137 lemma plus_assoc_pre: |
134 lemma plus_assoc_pre: |
138 shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))" |
135 shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))" |
139 apply (cases i) |
136 apply (cases i) |
149 |
146 |
150 |
147 |
151 |
148 |
152 |
149 |
153 |
150 |
|
151 |
|
152 |
154 text {* Below is the construction site code used if things do not work *} |
153 text {* Below is the construction site code used if things do not work *} |
155 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "my_int" *} |
154 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
155 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" *} |
156 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
156 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
157 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
157 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} |
158 ML {* val defs_sym = add_lower_defs @{context} defs *} |
158 ML {* val defs_sym = add_lower_defs @{context} defs *} |
|
159 (* ML {* val consts = [@{const_name my_plus}] *}*) |
159 ML {* val consts = lookup_quot_consts defs *} |
160 ML {* val consts = lookup_quot_consts defs *} |
160 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
161 ML {* val t_a = atomize_thm @{thm ho_tst} *} |
161 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
162 prove t_r: {* build_regularize_goal t_a rty rel @{context} *} |
162 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
163 ML_prf {* fun tac ctxt = |
163 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
164 (ObjectLogic.full_atomize_tac) THEN' |
164 ML {* val t_a = simp_allex_prs quot [] t_l *} |
165 REPEAT_ALL_NEW (FIRST' [ |
165 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} |
166 rtac rel_refl, |
|
167 atac, |
|
168 rtac @{thm universal_twice}, |
|
169 (rtac @{thm impI} THEN' atac), |
|
170 (*rtac @{thm equality_twice},*) |
|
171 EqSubst.eqsubst_tac ctxt [0] |
|
172 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
173 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
174 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), |
|
175 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
176 ]);*} |
|
177 apply (atomize(full)) |
|
178 apply (tactic {* tac @{context} 1 *}) |
|
179 apply (auto) |
|
180 sorry |
|
181 (*ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}*) |
|
182 ML {* val t_t = Toplevel.program (fn () => repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms) *} |
|
183 ML {* val (alls, exs) = findallex rty qty (prop_of t_a) *} |
|
184 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *} |
|
185 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *} |
|
186 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *} |
|
187 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} |
166 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
188 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
167 ML {* ObjectLogic.rulify t_r *} |
189 ML {* ObjectLogic.rulify t_r *} |
168 |
190 |
169 thm FORALL_PRS |
191 thm FORALL_PRS |
170 |
192 |