91 val tyenv = Vartab.dest (Envir.type_env env) |
91 val tyenv = Vartab.dest (Envir.type_env env) |
92 in |
92 in |
93 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
93 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
94 end |
94 end |
95 |
95 |
96 (* calculates the instantiations for the lemmas *) |
96 (* Calculates the instantiations for the lemmas: |
97 (* ball_reg_eqv_range and bex_reg_eqv_range *) |
97 ball_reg_eqv_range and bex_reg_eqv_range |
|
98 Since the left-hand-side contains a non-pattern '?P (f ?x)' |
|
99 we rely on unification/instantiation to check whether the |
|
100 theorem applies and return NONE if it doesn't. *) |
98 fun calculate_inst ctxt ball_bex_thm redex R1 R2 = |
101 fun calculate_inst ctxt ball_bex_thm redex R1 R2 = |
99 let |
102 let |
100 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
103 fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm)) |
101 val thy = ProofContext.theory_of ctxt |
104 val thy = ProofContext.theory_of ctxt |
102 val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] |
105 val typ_inst1 = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)] |
103 val trm_inst1 = map (SOME o cterm_of thy) [R2, R1] |
106 val trm_inst1 = map (SOME o cterm_of thy) [R2, R1] |
104 val thm' = Drule.instantiate' typ_inst1 trm_inst1 ball_bex_thm (* raises TYPE *) |
107 in |
105 val inst2 = get_match_inst thy (get_lhs thm') redex |
108 (case try (Drule.instantiate' typ_inst1 trm_inst1) ball_bex_thm of |
106 val thm'' = Drule.instantiate inst2 thm' (* raises THM *) |
109 NONE => NONE |
107 in |
110 | SOME thm' => |
108 SOME thm'' |
111 (case try (get_match_inst thy (get_lhs thm')) redex of |
109 end |
112 NONE => NONE |
110 handle _ => NONE |
113 | SOME inst2 => try (Drule.instantiate inst2) thm') |
111 (* FIXME/TODO: !!!CLEVER CODE!!! *) |
114 ) |
112 (* FIXME/TODO: What are the places where the exceptions are raised, *) |
115 end |
113 (* FIXME/TODO: and which exception is it? *) |
|
114 (* FIXME/TODO: Can one not find out from the types of R1, R2 and redex *) |
|
115 (* FIXME/TODO: when NONE should be returned? *) |
|
116 |
116 |
117 fun ball_bex_range_simproc ss redex = |
117 fun ball_bex_range_simproc ss redex = |
118 let |
118 let |
119 val ctxt = Simplifier.the_context ss |
119 val ctxt = Simplifier.the_context ss |
120 in |
120 in |
220 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) |
220 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) |
221 |
221 |
222 fun dest_comb (f $ a) = (f, a) |
222 fun dest_comb (f $ a) = (f, a) |
223 fun dest_bcomb ((_ $ l) $ r) = (l, r) |
223 fun dest_bcomb ((_ $ l) $ r) = (l, r) |
224 |
224 |
225 (* TODO: Can this be done easier? *) |
|
226 fun unlam t = |
225 fun unlam t = |
227 case t of |
226 case t of |
228 (Abs a) => snd (Term.dest_abs a) |
227 (Abs a) => snd (Term.dest_abs a) |
229 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) |
228 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) |
230 |
229 |
263 |
262 |
264 fun equals_rsp_tac R ctxt = |
263 fun equals_rsp_tac R ctxt = |
265 let |
264 let |
266 val ty = domain_type (fastype_of R); |
265 val ty = domain_type (fastype_of R); |
267 val thy = ProofContext.theory_of ctxt |
266 val thy = ProofContext.theory_of ctxt |
268 val thm = Drule.instantiate' |
267 in |
269 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
268 case try (Drule.instantiate' [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)]) |
270 in |
269 @{thm equals_rsp} of |
271 rtac thm THEN' quotient_tac ctxt |
270 NONE => K no_tac |
272 end |
271 | SOME thm => rtac thm THEN' quotient_tac ctxt |
273 (* TODO: Are they raised by instantiate'? *) |
272 end |
274 (* TODO: Again, can one specify more concretely *) |
273 (* TODO: Again, can one specify more concretely *) |
275 (* TODO: in terms of R when no_tac should be returned? *) |
274 (* TODO: in terms of R when no_tac should be returned? *) |
276 handle THM _ => K no_tac |
|
277 | TYPE _ => K no_tac |
|
278 | TERM _ => K no_tac |
|
279 |
275 |
280 fun rep_abs_rsp_tac ctxt = |
276 fun rep_abs_rsp_tac ctxt = |
281 SUBGOAL (fn (goal, i) => |
277 SUBGOAL (fn (goal, i) => |
282 case (bare_concl goal) of |
278 case (bare_concl goal) of |
283 (rel $ _ $ (rep $ (abs $ _))) => |
279 (rel $ _ $ (rep $ (abs $ _))) => |