equal
deleted
inserted
replaced
714 *} |
714 *} |
715 |
715 |
716 section {* RepAbs Injection Tactic *} |
716 section {* RepAbs Injection Tactic *} |
717 |
717 |
718 (* TODO: check if it still works with first_order_match *) |
718 (* TODO: check if it still works with first_order_match *) |
|
719 (* FIXME/TODO: do not handle everything *)x |
719 ML {* |
720 ML {* |
720 fun instantiate_tac thm = |
721 fun instantiate_tac thm = |
721 Subgoal.FOCUS (fn {concl, ...} => |
722 Subgoal.FOCUS (fn {concl, ...} => |
722 let |
723 let |
723 val pat = Drule.strip_imp_concl (cprop_of thm) |
724 val pat = Drule.strip_imp_concl (cprop_of thm) |
767 SUBGOAL (fn (goal, i) => |
768 SUBGOAL (fn (goal, i) => |
768 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
769 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
769 (_ $ (Const (@{const_name Bex}, _) $ _) |
770 (_ $ (Const (@{const_name Bex}, _) $ _) |
770 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i |
771 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i |
771 | _ => no_tac) |
772 | _ => no_tac) |
772 *} |
|
773 |
|
774 ML {* (* Legacy *) |
|
775 fun needs_lift (rty as Type (rty_s, _)) ty = |
|
776 case ty of |
|
777 Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) |
|
778 | _ => false |
|
779 |
|
780 *} |
773 *} |
781 |
774 |
782 definition |
775 definition |
783 "QUOT_TRUE x \<equiv> True" |
776 "QUOT_TRUE x \<equiv> True" |
784 |
777 |