78 val thy = ProofContext.theory_of ctxt |
78 val thy = ProofContext.theory_of ctxt |
79 val eqv_ty = fastype_of R2 --> HOLogic.boolT |
79 val eqv_ty = fastype_of R2 --> HOLogic.boolT |
80 val eqv_goal = HOLogic.mk_Trueprop |
80 val eqv_goal = HOLogic.mk_Trueprop |
81 (Const (@{const_name "equivp"}, eqv_ty) $ R2) |
81 (Const (@{const_name "equivp"}, eqv_ty) $ R2) |
82 val eqv_prem = Goal.prove ctxt [] [] eqv_goal (fn _ => equiv_tac ctxt 1) |
82 val eqv_prem = Goal.prove ctxt [] [] eqv_goal (fn _ => equiv_tac ctxt 1) |
83 val thm = (@{thm eq_reflection} OF [ball_bex_thm OF [eqv_prem]]) |
83 val thm = ball_bex_thm OF [eqv_prem] |
84 val thmi = Drule.instantiate' [] [SOME (cterm_of thy R1)] thm |
84 val thmi = Drule.instantiate' [] [SOME (cterm_of thy R1)] thm |
85 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex |
85 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex |
86 val thm2 = Drule.instantiate inst thmi |
86 val thm2 = Drule.instantiate inst thmi |
87 in |
87 in |
88 SOME thm2 |
88 SOME thm2 |
96 val ctxt = Simplifier.the_context ss |
96 val ctxt = Simplifier.the_context ss |
97 in |
97 in |
98 case redex of |
98 case redex of |
99 (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
99 (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
100 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
100 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
101 calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 |
101 calculate_instance ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2 |
102 |
102 |
103 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
103 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
104 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
104 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
105 calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 |
105 calculate_instance ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 |
106 | _ => NONE |
106 | _ => NONE |
107 end |
107 end |
108 |
108 |
109 (* test whether DETERM makes any difference *) |
109 (* test whether DETERM makes any difference *) |
110 fun quotient_tac ctxt = SOLVES' |
110 fun quotient_tac ctxt = SOLVES' |
454 val thy = ProofContext.theory_of ctxt |
454 val thy = ProofContext.theory_of ctxt |
455 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
455 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
456 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
456 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
457 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
457 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
458 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
458 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
459 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
459 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
460 val te = @{thm eq_reflection} OF [solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)] |
460 val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) |
461 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
461 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
462 val make_inst = if ty_c = ty_d then make_inst_id else make_inst |
462 val make_inst = if ty_c = ty_d then make_inst_id else make_inst |
463 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
463 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
464 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
464 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
465 in |
465 in |