173 fun replace_bnd0 (trm, Abs (x, T, t)) = |
173 fun replace_bnd0 (trm, Abs (x, T, t)) = |
174 Abs (x, T, subst_bound (trm, t)) |
174 Abs (x, T, subst_bound (trm, t)) |
175 *} |
175 *} |
176 |
176 |
177 ML {* |
177 ML {* |
178 fun inj_REPABS_aux lthy (rtrm, qtrm) = |
178 fun inj_REPABS lthy (rtrm, qtrm) = |
179 let |
179 let |
180 val rty = fastype_of rtrm |
180 val rty = fastype_of rtrm |
181 val qty = fastype_of qtrm |
181 val qty = fastype_of qtrm |
182 in |
182 in |
183 case (rtrm, qtrm) of |
183 case (rtrm, qtrm) of |
184 (Abs (x, T, t), Abs (x', T', t')) => |
184 (Abs (x, T, t), Abs (x', T', t')) => |
185 let |
185 let |
186 val (y, s) = Term.dest_abs (x, T, t) |
186 val (y, s) = Term.dest_abs (x, T, t) |
187 val (y', s') = Term.dest_abs (x', T', t') |
187 val (y', s') = Term.dest_abs (x', T', t') |
188 val yvar = Free (y, T) |
188 val yvar = Free (y, T) |
189 val res = lambda yvar (inj_REPABS_aux lthy (s, s')) |
189 val res = lambda yvar (inj_REPABS lthy (s, s')) |
190 in |
190 in |
191 if T = T' |
191 if T = T' |
192 then res |
192 then res |
193 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
193 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
194 end |
194 end |
195 (* FIXME: Does one havae to look at the abstraction or go under the lambda. *) |
195 (* FIXME: Does one havae to look at the abstraction or go under the lambda. *) |
196 | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
196 | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
197 Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS_aux lthy (t, t')) |
197 Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t')) |
198 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
198 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
199 Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS_aux lthy (t, t')) |
199 Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t')) |
200 | (rtrm as _ $ _, qtrm as _ $ _) => |
200 | (rtrm as _ $ _, qtrm as _ $ _) => |
201 let |
201 let |
202 val (rhead, rargs) = Term.strip_comb rtrm |
202 val (rhead, rargs) = Term.strip_comb rtrm |
203 val (qhead, qargs) = Term.strip_comb qtrm |
203 val (qhead, qargs) = Term.strip_comb qtrm |
204 val rhead' = inj_REPABS_aux lthy (rhead, qhead) |
204 val rhead' = inj_REPABS lthy (rhead, qhead) |
205 val rargs' = map (inj_REPABS_aux lthy) (rargs ~~ qargs) |
205 val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs) |
206 val res = list_comb (rhead', rargs') |
206 val res = list_comb (rhead', rargs') |
207 in |
207 in |
208 if rty = qty |
208 if rty = qty |
209 then res |
209 then res |
210 else mk_repabs lthy (rty, qty) res |
210 else mk_repabs lthy (rty, qty) res |
244 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
242 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
245 done |
243 done |
246 |
244 |
247 ML {* @{thm testtest} OF [arthm] *} |
245 ML {* @{thm testtest} OF [arthm] *} |
248 |
246 |
249 ML {* |
247 ML {* val reg_atrm = prop_of (@{thm testtest} OF [arthm]) *} |
250 val reg_atrm = prop_of (@{thm testtest} OF [arthm]); |
248 |
251 *} |
249 ML {* |
|
250 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
|
251 (REPEAT1 o FIRST1) |
|
252 [rtac trans_thm, |
|
253 LAMBDA_RES_TAC ctxt, |
|
254 ball_rsp_tac ctxt, |
|
255 bex_rsp_tac ctxt, |
|
256 FIRST' (map rtac rsp_thms), |
|
257 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
|
258 rtac refl, |
|
259 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
260 Cong_Tac.cong_tac @{thm cong}, |
|
261 rtac @{thm ext}, |
|
262 rtac reflex_thm, |
|
263 atac, |
|
264 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
|
265 WEAK_LAMBDA_RES_TAC ctxt, |
|
266 CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))] |
|
267 *} |
|
268 |
|
269 ML {* |
|
270 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
|
271 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
|
272 val consts = lookup_quot_consts defs |
|
273 *} |
|
274 |
|
275 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *} |
|
276 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
277 (* does not work *) |
|
278 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms *}) |
|
279 |
252 |
280 |
253 ML {* |
281 ML {* |
254 inj_REPABS @{context} (reg_atrm, aqtrm) |
282 inj_REPABS @{context} (reg_atrm, aqtrm) |
255 |> Syntax.string_of_term @{context} |
283 |> Syntax.string_of_term @{context} |
256 |> writeln |
284 |> writeln |