768 end |
768 end |
769 *} |
769 *} |
770 |
770 |
771 section {* RepAbs Injection Tactic *} |
771 section {* RepAbs Injection Tactic *} |
772 |
772 |
773 ML {* |
|
774 fun stripped_term_of ct = |
|
775 ct |> term_of |> HOLogic.dest_Trueprop |
|
776 *} |
|
777 |
|
778 (* TODO: check if it still works with first_order_match *) |
773 (* TODO: check if it still works with first_order_match *) |
779 ML {* |
774 ML {* |
780 fun instantiate_tac thm = |
775 fun instantiate_tac thm = |
781 Subgoal.FOCUS (fn {concl, ...} => |
776 Subgoal.FOCUS (fn {concl, ...} => |
782 let |
777 let |
804 shows "(R1 ===> R2) f g" |
799 shows "(R1 ===> R2) f g" |
805 using a by simp |
800 using a by simp |
806 |
801 |
807 ML {* |
802 ML {* |
808 val lambda_res_tac = |
803 val lambda_res_tac = |
809 Subgoal.FOCUS (fn {concl, ...} => |
804 SUBGOAL (fn (goal, i) => |
810 case (stripped_term_of concl) of |
805 case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of |
811 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} 1 |
806 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i |
812 | _ => no_tac) |
807 | _ => no_tac) |
813 *} |
808 *} |
814 |
809 |
815 ML {* |
810 ML {* |
816 val weak_lambda_res_tac = |
811 val weak_lambda_res_tac = |
817 Subgoal.FOCUS (fn {concl, ...} => |
812 SUBGOAL (fn (goal, i) => |
818 case (stripped_term_of concl) of |
813 case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of |
819 (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1 |
814 (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1 |
820 | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1 |
815 | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1 |
821 | _ => no_tac) |
816 | _ => no_tac) |
822 *} |
817 *} |
823 |
818 |
824 ML {* |
819 ML {* |
825 val ball_rsp_tac = |
820 val ball_rsp_tac = |
826 Subgoal.FOCUS (fn {concl, ...} => |
821 SUBGOAL (fn (goal, i) => |
827 case (stripped_term_of concl) of |
822 case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of |
828 (_ $ (Const (@{const_name Ball}, _) $ _) |
823 (_ $ (Const (@{const_name Ball}, _) $ _) |
829 $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1 |
824 $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1 |
830 |_ => no_tac) |
825 |_ => no_tac) |
831 *} |
826 *} |
832 |
827 |
833 ML {* |
828 ML {* |
834 val bex_rsp_tac = |
829 val bex_rsp_tac = |
835 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
830 SUBGOAL (fn (goal, i) => |
836 case (stripped_term_of concl) of |
831 case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of |
837 (_ $ (Const (@{const_name Bex}, _) $ _) |
832 (_ $ (Const (@{const_name Bex}, _) $ _) |
838 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1 |
833 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1 |
839 | _ => no_tac) |
834 | _ => no_tac) |
840 *} |
835 *} |
841 |
836 |
845 Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) |
840 Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) |
846 | _ => false |
841 | _ => false |
847 |
842 |
848 *} |
843 *} |
849 |
844 |
|
845 |
|
846 |
|
847 |
850 ML {* |
848 ML {* |
851 fun APPLY_RSP_TAC rty = |
849 fun APPLY_RSP_TAC rty = |
852 Subgoal.FOCUS (fn {concl, ...} => |
850 Subgoal.FOCUS (fn {concl, ...} => |
853 case (stripped_term_of concl) of |
851 case HOLogic.dest_Trueprop (term_of concl) of |
854 (_ $ (f $ _) $ (_ $ _)) => |
852 (_ $ (f $ _) $ (_ $ _)) => |
855 let |
853 let |
856 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
854 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
857 val insts = Thm.match (pat, concl) |
855 val insts = Thm.match (pat, concl) |
858 in |
856 in |