798 using a by simp |
798 using a by simp |
799 |
799 |
800 ML {* |
800 ML {* |
801 val lambda_res_tac = |
801 val lambda_res_tac = |
802 SUBGOAL (fn (goal, i) => |
802 SUBGOAL (fn (goal, i) => |
803 case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of |
803 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
804 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i |
804 (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i |
805 | _ => no_tac) |
805 | _ => no_tac) |
806 *} |
806 *} |
807 |
807 |
808 ML {* |
808 ML {* |
809 val weak_lambda_res_tac = |
809 val weak_lambda_res_tac = |
810 SUBGOAL (fn (goal, i) => |
810 SUBGOAL (fn (goal, i) => |
811 case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of |
811 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
812 (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i |
812 (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i |
813 | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i |
813 | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i |
814 | _ => no_tac) |
814 | _ => no_tac) |
815 *} |
815 *} |
816 |
816 |
817 ML {* |
817 ML {* |
818 val ball_rsp_tac = |
818 val ball_rsp_tac = |
819 SUBGOAL (fn (goal, i) => |
819 SUBGOAL (fn (goal, i) => |
820 case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of |
820 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
821 (_ $ (Const (@{const_name Ball}, _) $ _) |
821 (_ $ (Const (@{const_name Ball}, _) $ _) |
822 $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i |
822 $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i |
823 |_ => no_tac) |
823 |_ => no_tac) |
824 *} |
824 *} |
825 |
825 |
826 ML {* |
826 ML {* |
827 val bex_rsp_tac = |
827 val bex_rsp_tac = |
828 SUBGOAL (fn (goal, i) => |
828 SUBGOAL (fn (goal, i) => |
829 case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of |
829 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
830 (_ $ (Const (@{const_name Bex}, _) $ _) |
830 (_ $ (Const (@{const_name Bex}, _) $ _) |
831 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i |
831 $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i |
832 | _ => no_tac) |
832 | _ => no_tac) |
833 *} |
833 *} |
834 |
834 |
911 fun find_fun trm = |
911 fun find_fun trm = |
912 case trm of |
912 case trm of |
913 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
913 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
914 | _ => false |
914 | _ => false |
915 in |
915 in |
916 case find_first find_fun (Logic.strip_imp_prems gl) of |
916 case find_first find_fun (Logic.strip_assums_hyp gl) of |
917 SOME (_ $ (_ $ x)) => |
917 SOME (_ $ (_ $ x)) => |
918 let |
918 let |
919 val fx = fnctn x; |
919 val fx = fnctn x; |
920 val ctrm1 = cterm_of thy x; |
920 val ctrm1 = cterm_of thy x; |
921 val cty1 = ctyp_of thy (fastype_of x); |
921 val cty1 = ctyp_of thy (fastype_of x); |