equal
deleted
inserted
replaced
244 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
244 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
245 val qt_asm = find_qt_asm (map term_of asms) |
245 val qt_asm = find_qt_asm (map term_of asms) |
246 in |
246 in |
247 case (bare_concl, qt_asm) of |
247 case (bare_concl, qt_asm) of |
248 (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => |
248 (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => |
249 if (fastype_of qt_fun) = (fastype_of f) |
249 if fastype_of qt_fun = fastype_of f |
250 then no_tac |
250 then no_tac |
251 else |
251 else |
252 let |
252 let |
253 val ty_x = fastype_of x |
253 val ty_x = fastype_of x |
254 val ty_b = fastype_of qt_arg |
254 val ty_b = fastype_of qt_arg |
424 |
424 |
425 (* expands all fun_maps, except in front of the (bound) variables listed in xs *) |
425 (* expands all fun_maps, except in front of the (bound) variables listed in xs *) |
426 fun fun_map_simple_conv xs ctrm = |
426 fun fun_map_simple_conv xs ctrm = |
427 case (term_of ctrm) of |
427 case (term_of ctrm) of |
428 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
428 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
429 if (member (op=) xs h) |
429 if member (op=) xs h |
430 then Conv.all_conv ctrm |
430 then Conv.all_conv ctrm |
431 else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm |
431 else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm |
432 | _ => Conv.all_conv ctrm |
432 | _ => Conv.all_conv ctrm |
433 |
433 |
434 fun fun_map_conv xs ctxt ctrm = |
434 fun fun_map_conv xs ctxt ctrm = |