96 we rely on unification/instantiation to check whether the |
96 we rely on unification/instantiation to check whether the |
97 theorem applies and return NONE if it doesn't. |
97 theorem applies and return NONE if it doesn't. |
98 *) |
98 *) |
99 fun calculate_inst ctxt ball_bex_thm redex R1 R2 = |
99 fun calculate_inst ctxt ball_bex_thm redex R1 R2 = |
100 let |
100 let |
|
101 val thy = ProofContext.theory_of ctxt |
101 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
102 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
102 val thy = ProofContext.theory_of ctxt |
103 val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] |
103 val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] |
104 val trm_inst = map (SOME o cterm_of thy) [R2, R1] |
104 val trm_inst1 = map (SOME o cterm_of thy) [R2, R1] |
105 in |
105 in |
106 case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of |
106 case try (Drule.instantiate' typ_inst1 trm_inst1) ball_bex_thm of |
|
107 NONE => NONE |
107 NONE => NONE |
108 | SOME thm' => |
108 | SOME thm' => |
109 (case try (get_match_inst thy (get_lhs thm')) redex of |
109 (case try (get_match_inst thy (get_lhs thm')) redex of |
110 NONE => NONE |
110 NONE => NONE |
111 | SOME inst2 => try (Drule.instantiate inst2) thm') |
111 | SOME inst2 => try (Drule.instantiate inst2) thm') |
423 |
423 |
424 |
424 |
425 |
425 |
426 (*** Cleaning of the Theorem ***) |
426 (*** Cleaning of the Theorem ***) |
427 |
427 |
428 (* expands all fun_maps, except in front of the bound variables listed in xs *) |
428 (* expands all fun_maps, except in front of the (bound) variables listed in xs *) |
429 fun fun_map_simple_conv xs ctrm = |
429 fun fun_map_simple_conv xs ctrm = |
430 case (term_of ctrm) of |
430 case (term_of ctrm) of |
431 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
431 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
432 if (member (op=) xs h) |
432 if (member (op=) xs h) |
433 then Conv.all_conv ctrm |
433 then Conv.all_conv ctrm |
441 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
441 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
442 | _ => Conv.all_conv ctrm |
442 | _ => Conv.all_conv ctrm |
443 |
443 |
444 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
444 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
445 |
445 |
446 |
446 (* custom matching functions *) |
447 fun mk_abs u i t = |
447 fun mk_abs u i t = |
448 if incr_boundvars i u aconv t then Bound i |
448 if incr_boundvars i u aconv t then Bound i |
449 else (case t of |
449 else (case t of |
450 t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) |
450 t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) |
451 | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
451 | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
482 val thy = ProofContext.theory_of ctxt |
482 val thy = ProofContext.theory_of ctxt |
483 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
483 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
484 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
484 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
485 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
485 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
486 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
486 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
487 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
487 val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
488 val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) |
488 val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1) |
489 val ts = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} te |
489 val thm3 = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2 |
490 val (insp, inst) = |
490 val (insp, inst) = |
491 if ty_c = ty_d |
491 if ty_c = ty_d |
492 then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm) |
492 then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm) |
493 else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
493 else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm) |
494 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
494 val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3 |
495 in |
495 in |
496 Conv.rewr_conv ti ctrm |
496 Conv.rewr_conv thm4 ctrm |
497 end |
497 end |
498 | _ => Conv.all_conv ctrm |
498 | _ => Conv.all_conv ctrm |
499 |
499 |
500 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt |
500 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt |
501 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
501 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
502 |
502 |
503 |
503 |
504 (* Cleaning consists of: |
504 (* Cleaning consists of: |
505 |
505 |
506 1. unfolding of ---> in front of everything, except |
506 1. unfolding of ---> in front of everything, except |
507 bound variables |
507 bound variables (this prevents lambda_prs from |
508 (this prevents lambda_prs from becoming stuck) |
508 becoming stuck) |
509 |
509 |
510 2. simplification with lambda_prs |
510 2. simplification with lambda_prs |
511 |
511 |
512 3. simplification with Quotient_abs_rep Quotient_rel_rep id_simps |
512 3. simplification with: |
513 folding of definitions and preservation lemmas; |
513 |
514 and simplification with babs_prs all_prs ex_prs ex1_prs |
514 - Quotient_abs_rep Quotient_rel_rep |
|
515 babs_prs all_prs ex_prs ex1_prs |
|
516 - id_simps |
|
517 |
|
518 and folding of definitions and preservation lemmas |
515 |
519 |
516 4. test for refl |
520 4. test for refl |
517 *) |
521 *) |
518 fun clean_tac lthy = |
522 fun clean_tac lthy = |
519 let |
523 let |
520 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest lthy) |
524 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest lthy) |
521 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
525 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
522 val prs = prs_rules_get lthy |
526 val prs = prs_rules_get lthy |
523 val ids = id_simps_get lthy |
527 val ids = id_simps_get lthy |
524 |
528 val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs |
525 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
529 |
526 val ss = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs) |
530 val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
527 in |
531 in |
528 EVERY' [fun_map_tac lthy, |
532 EVERY' [fun_map_tac lthy, |
529 lambda_prs_tac lthy, |
533 lambda_prs_tac lthy, |
530 simp_tac ss, |
534 simp_tac ss, |
531 TRY o rtac refl] |
535 TRY o rtac refl] |