14 open Quotient_Info; |
14 open Quotient_Info; |
15 open Quotient_Type; |
15 open Quotient_Type; |
16 open Quotient_Term; |
16 open Quotient_Term; |
17 |
17 |
18 |
18 |
19 (* Since HOL_basic_ss is too "big" for us, *) |
19 (* Since HOL_basic_ss is too "big" for us, we *) |
20 (* we need to set up our own minimal simpset. *) |
20 (* need to set up our own minimal simpset. *) |
21 fun mk_minimal_ss ctxt = |
21 fun mk_minimal_ss ctxt = |
22 Simplifier.context ctxt empty_ss |
22 Simplifier.context ctxt empty_ss |
23 setsubgoaler asm_simp_tac |
23 setsubgoaler asm_simp_tac |
24 setmksimps (mksimps []) |
24 setmksimps (mksimps []) |
25 |
25 |
26 |
26 (* various helper fuctions *) |
27 |
27 |
28 (* various helper functions *) |
28 (* composition of two theorems, used in map *) |
29 fun OF1 thm1 thm2 = thm2 RS thm1 |
29 fun OF1 thm1 thm2 = thm2 RS thm1 |
30 |
30 |
31 (* makes sure a subgoal is solved *) |
31 (* makes sure a subgoal is solved *) |
32 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
32 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) |
33 |
33 |
72 val tyenv = Vartab.dest (Envir.type_env env) |
70 val tyenv = Vartab.dest (Envir.type_env env) |
73 in |
71 in |
74 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
72 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
75 end |
73 end |
76 |
74 |
77 fun calculate_instance ctxt thm redex R1 R2 = |
75 (* calculates the instantiations for ball_reg_eqv_range and bex_reg_eqv_range *) |
|
76 fun calculate_instance ctxt ball_bex_thm redex R1 R2 = |
78 let |
77 let |
79 val thy = ProofContext.theory_of ctxt |
78 val thy = ProofContext.theory_of ctxt |
80 val goal = Const (@{const_name "equivp"}, dummyT) $ R2 |
79 val eqv_ty = fastype_of R2 --> HOLogic.boolT |
81 |> Syntax.check_term ctxt |
80 val eqv_goal = HOLogic.mk_Trueprop |
82 |> HOLogic.mk_Trueprop |
81 (Const (@{const_name "equivp"}, eqv_ty) $ R2) |
83 val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1) |
82 val eqv_prem = Goal.prove ctxt [] [] eqv_goal (fn _ => equiv_tac ctxt 1) |
84 val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) |
83 val thm = (@{thm eq_reflection} OF [ball_bex_thm OF [eqv_prem]]) |
85 val R1c = cterm_of thy R1 |
84 val thmi = Drule.instantiate' [] [SOME (cterm_of thy R1)] thm |
86 val thmi = Drule.instantiate' [] [SOME R1c] thm |
|
87 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 |
88 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) |
86 val thm2 = Drule.instantiate inst thmi |
89 in |
87 in |
90 SOME thm2 |
88 SOME thm2 |
91 end |
89 end |
92 handle _ => NONE |
90 handle _ => NONE |
93 (* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) |
91 (* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) |
|
92 |
94 |
93 |
95 fun ball_bex_range_simproc ss redex = |
94 fun ball_bex_range_simproc ss redex = |
96 let |
95 let |
97 val ctxt = Simplifier.the_context ss |
96 val ctxt = Simplifier.the_context ss |
98 in |
97 in |
114 resolve_tac (quotient_rules_get ctxt)])) |
113 resolve_tac (quotient_rules_get ctxt)])) |
115 |
114 |
116 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
115 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
117 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
116 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
118 |
117 |
119 fun solve_quotient_assum ctxt thm = |
118 fun solve_quotient_assm ctxt thm = |
120 case Seq.pull (quotient_tac ctxt 1 thm) of |
119 case Seq.pull (quotient_tac ctxt 1 thm) of |
121 SOME (t, _) => t |
120 SOME (t, _) => t |
122 | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing" |
121 | _ => error "solve_quotient_assm failed. Maybe a quotient_thm is missing" |
123 |
122 |
124 |
123 |
125 (* 0. preliminary simplification step according to *) |
124 (* 0. preliminary simplification step according to *) |
126 (* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *) |
125 (* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *) |
127 (* ball_reg_eqv_range bex_reg_eqv_range *) |
126 (* ball_reg_eqv_range bex_reg_eqv_range *) |
456 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
455 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
457 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
456 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
458 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] |
459 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)] |
460 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
459 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
461 val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)] |
460 val te = @{thm eq_reflection} OF [solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)] |
462 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
461 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
463 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 |
464 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) |
465 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 |
466 in |
465 in |