284 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
284 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
285 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
285 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
286 in |
286 in |
287 if rel' = rel then rtrm else raise exc |
287 if rel' = rel then rtrm else raise exc |
288 end |
288 end |
|
289 |
289 | (_, Const (s, Type(st, _))) => |
290 | (_, Const (s, Type(st, _))) => |
290 let |
291 let |
291 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
292 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
292 | same_name _ _ = false |
293 | same_name _ _ = false |
293 in |
294 in |
294 (* TODO/FIXME: This test is not enough *) |
295 (* TODO/FIXME: This test is not enough. *) |
|
296 (* Why? *) |
295 if same_name rtrm qtrm then rtrm |
297 if same_name rtrm qtrm then rtrm |
296 else |
298 else |
297 let |
299 let |
298 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
300 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
299 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |
301 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |
300 val thy = ProofContext.theory_of lthy |
302 val thy = ProofContext.theory_of lthy |
301 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
303 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
302 in |
304 in |
303 if Pattern.matches thy (rtrm', rtrm) then rtrm else |
305 if Pattern.matches thy (rtrm', rtrm) |
304 let |
306 then rtrm else raise exc2 |
305 val _ = tracing ("rtrm := " ^ Syntax.string_of_term @{context} rtrm); |
|
306 val _ = tracing ("rtrm':= " ^ Syntax.string_of_term @{context} rtrm'); |
|
307 in raise exc2 end |
|
308 end |
307 end |
309 end |
308 end |
310 |
309 |
311 | (t1 $ t2, t1' $ t2') => |
310 | (t1 $ t2, t1' $ t2') => |
312 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
311 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
318 | (Bound i, Bound i') => |
317 | (Bound i, Bound i') => |
319 if i = i' then rtrm |
318 if i = i' then rtrm |
320 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
319 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
321 |
320 |
322 | (rt, qt) => |
321 | (rt, qt) => |
323 let val (rts, qts) = (Syntax.string_of_term lthy rt, Syntax.string_of_term lthy qt) in |
322 let |
324 raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")")) |
323 val rts = Syntax.string_of_term lthy rt |
|
324 val qts = Syntax.string_of_term lthy qt |
|
325 in |
|
326 raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")")) |
325 end |
327 end |
326 *} |
328 *} |
327 |
329 |
328 section {* Regularize Tactic *} |
330 section {* Regularize Tactic *} |
329 |
331 |
393 |
395 |
394 lemma eq_imp_rel: |
396 lemma eq_imp_rel: |
395 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
397 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
396 by (simp add: equivp_reflp) |
398 by (simp add: equivp_reflp) |
397 |
399 |
398 (* Regularize Tactic *) |
400 ML {* |
|
401 fun quotient_tac ctxt = |
|
402 REPEAT_ALL_NEW (FIRST' |
|
403 [rtac @{thm identity_quotient}, |
|
404 resolve_tac (quotient_rules_get ctxt)]) |
|
405 |
|
406 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
|
407 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
|
408 *} |
399 |
409 |
400 (* 0. preliminary simplification step according to *) |
410 (* 0. preliminary simplification step according to *) |
401 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) |
411 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) |
402 ball_reg_eqv_range bex_reg_eqv_range |
412 ball_reg_eqv_range bex_reg_eqv_range |
403 (* 1. eliminating simple Ball/Bex instances*) |
413 (* 1. eliminating simple Ball/Bex instances*) |
404 thm ball_reg_right bex_reg_left |
414 thm ball_reg_right bex_reg_left |
405 (* 2. monos *) |
415 (* 2. monos *) |
406 (* 3. commutation rules for ball and bex *) |
416 (* 3. commutation rules for ball and bex *) |
407 thm ball_all_comm bex_ex_comm |
417 thm ball_all_comm bex_ex_comm |
408 (* 4. then rel-equality (which need to be instantiated to avoid loops *) |
418 (* 4. then rel-equality (which need to be instantiated to avoid loops) *) |
409 thm eq_imp_rel |
419 thm eq_imp_rel |
410 (* 5. then simplification like 0 *) |
420 (* 5. then simplification like 0 *) |
411 (* finally jump back to 1 *) |
421 (* finally jump back to 1 *) |
412 |
|
413 ML {* |
|
414 fun quotient_tac ctxt = |
|
415 REPEAT_ALL_NEW (FIRST' |
|
416 [rtac @{thm identity_quotient}, |
|
417 resolve_tac (quotient_rules_get ctxt)]) |
|
418 |
|
419 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
|
420 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
|
421 *} |
|
422 |
422 |
423 ML {* |
423 ML {* |
424 fun regularize_tac ctxt = |
424 fun regularize_tac ctxt = |
425 let |
425 let |
426 val thy = ProofContext.theory_of ctxt |
426 val thy = ProofContext.theory_of ctxt |
515 if T = T' then rtrm |
515 if T = T' then rtrm |
516 else mk_repabs lthy (T, T') rtrm |
516 else mk_repabs lthy (T, T') rtrm |
517 |
517 |
518 | (_, Const (@{const_name "op ="}, _)) => rtrm |
518 | (_, Const (@{const_name "op ="}, _)) => rtrm |
519 |
519 |
520 (* FIXME: check here that rtrm is the corresponding definition for the const *) |
|
521 (* Hasn't it already been checked in regularize? *) |
|
522 | (_, Const (_, T')) => |
520 | (_, Const (_, T')) => |
523 let |
521 let |
524 val rty = fastype_of rtrm |
522 val rty = fastype_of rtrm |
525 in |
523 in |
526 if rty = T' then rtrm |
524 if rty = T' then rtrm |
856 *} |
854 *} |
857 |
855 |
858 ML {* |
856 ML {* |
859 fun lambda_prs_simple_conv ctxt ctrm = |
857 fun lambda_prs_simple_conv ctxt ctrm = |
860 case (term_of ctrm) of |
858 case (term_of ctrm) of |
861 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
859 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
862 (let |
860 (let |
863 val thy = ProofContext.theory_of ctxt |
861 val thy = ProofContext.theory_of ctxt |
864 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
862 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
865 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
863 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
866 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
864 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
912 |
910 |
913 (* 1. folding of definitions and preservation lemmas; *) |
911 (* 1. folding of definitions and preservation lemmas; *) |
914 (* and simplification with *) |
912 (* and simplification with *) |
915 thm babs_prs all_prs ex_prs |
913 thm babs_prs all_prs ex_prs |
916 (* 2. unfolding of ---> in front of everything, except *) |
914 (* 2. unfolding of ---> in front of everything, except *) |
917 (* bound variables *) |
915 (* bound variables (this prevents lambda_prs from *) |
|
916 (* becoming stuck *) |
918 thm fun_map.simps |
917 thm fun_map.simps |
919 (* 3. simplification with *) |
918 (* 3. simplification with *) |
920 thm lambda_prs |
919 thm lambda_prs |
921 (* 4. simplification with *) |
920 (* 4. simplification with *) |
922 thm Quotient_abs_rep Quotient_rel_rep id_simps |
921 thm Quotient_abs_rep Quotient_rel_rep id_simps |