54 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
54 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
55 |
55 |
56 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
56 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
57 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
57 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
58 |
58 |
|
59 fun solve_equiv_assm ctxt thm = |
|
60 case Seq.pull (equiv_tac ctxt 1 thm) of |
|
61 SOME (t, _) => t |
|
62 | _ => error "solve_equiv_assm failed." |
|
63 |
|
64 |
|
65 |
59 fun prep_trm thy (x, (T, t)) = |
66 fun prep_trm thy (x, (T, t)) = |
60 (cterm_of thy (Var (x, T)), cterm_of thy t) |
67 (cterm_of thy (Var (x, T)), cterm_of thy t) |
61 |
68 |
62 fun prep_ty thy (x, (S, ty)) = |
69 fun prep_ty thy (x, (S, ty)) = |
63 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
70 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
70 val tyenv = Vartab.dest (Envir.type_env env) |
77 val tyenv = Vartab.dest (Envir.type_env env) |
71 in |
78 in |
72 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
79 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
73 end |
80 end |
74 |
81 |
75 (* calculates the instantiations for ball_reg_eqv_range and bex_reg_eqv_range *) |
82 (* calculates the instantiations for te lemmas *) |
|
83 (* ball_reg_eqv_range and bex_reg_eqv_range *) |
76 fun calculate_instance ctxt ball_bex_thm redex R1 R2 = |
84 fun calculate_instance ctxt ball_bex_thm redex R1 R2 = |
77 let |
85 let |
|
86 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
78 val thy = ProofContext.theory_of ctxt |
87 val thy = ProofContext.theory_of ctxt |
79 val eqv_ty = fastype_of R2 --> HOLogic.boolT |
88 val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] |
80 val eqv_goal = HOLogic.mk_Trueprop |
89 val trm_inst1 = map (SOME o cterm_of thy) [R2, R1] |
81 (Const (@{const_name "equivp"}, eqv_ty) $ R2) |
90 val thm' = Drule.instantiate' typ_inst1 trm_inst1 ball_bex_thm |
82 val eqv_prem = Goal.prove ctxt [] [] eqv_goal (fn _ => equiv_tac ctxt 1) |
91 val inst2 = matching_prs thy (get_lhs thm') redex |
83 val thm = ball_bex_thm OF [eqv_prem] |
92 val thm'' = Drule.instantiate inst2 thm' |
84 val thmi = Drule.instantiate' [] [SOME (cterm_of thy R1)] thm |
93 in |
85 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex |
94 SOME thm'' |
86 val thm2 = Drule.instantiate inst thmi |
95 end |
87 in |
96 handle _ => NONE |
88 SOME thm2 |
97 (* FIXME/TODO: !!!CLEVER CODE!!! *) |
89 end |
98 (* FIXME/TODO: What is the place where the exception is raised, *) |
90 handle _ => NONE |
99 (* FIXME/TODO: and which exception is it? *) |
91 (* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) |
100 (* FIXME/TODO: Can one not find out from the types of R1 or R2, *) |
|
101 (* FIXME/TODO: or from their form, when NONE should be returned? *) |
92 |
102 |
93 |
103 |
94 fun ball_bex_range_simproc ss redex = |
104 fun ball_bex_range_simproc ss redex = |
95 let |
105 let |
96 val ctxt = Simplifier.the_context ss |
106 val ctxt = Simplifier.the_context ss |