equal
deleted
inserted
replaced
772 ML {* |
772 ML {* |
773 fun instantiate_tac thm = |
773 fun instantiate_tac thm = |
774 Subgoal.FOCUS (fn {concl, ...} => |
774 Subgoal.FOCUS (fn {concl, ...} => |
775 let |
775 let |
776 val pat = Drule.strip_imp_concl (cprop_of thm) |
776 val pat = Drule.strip_imp_concl (cprop_of thm) |
777 val insts = Thm.match (pat, concl) |
777 val insts = Thm.first_order_match (pat, concl) |
778 in |
778 in |
779 rtac (Drule.instantiate insts thm) 1 |
779 rtac (Drule.instantiate insts thm) 1 |
780 end |
780 end |
781 handle _ => no_tac) |
781 handle _ => no_tac) |
782 *} |
782 *} |
863 case ((HOLogic.dest_Trueprop (term_of concl))) of |
863 case ((HOLogic.dest_Trueprop (term_of concl))) of |
864 ((_ $ (f $ _) $ (_ $ _))) => |
864 ((_ $ (f $ _) $ (_ $ _))) => |
865 let |
865 let |
866 val (asmf, asma) = find_qt_asm (map term_of asms); |
866 val (asmf, asma) = find_qt_asm (map term_of asms); |
867 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
867 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
868 val insts = Thm.match (pat, concl) |
868 val insts = Thm.first_order_match (pat, concl) |
869 in |
869 in |
870 if (fastype_of asmf) = (fastype_of f) |
870 if (fastype_of asmf) = (fastype_of f) |
871 then no_tac |
871 then no_tac |
872 else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
872 else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
873 end |
873 end |
949 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn))) ctxt) i) |
949 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn))) ctxt) i) |
950 *} |
950 *} |
951 |
951 |
952 ML {* fun dest_comb (f $ a) = (f, a) *} |
952 ML {* fun dest_comb (f $ a) = (f, a) *} |
953 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
953 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
954 ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *} |
954 (* TODO: Can this be done easier? *) |
|
955 ML {* |
|
956 fun unlam t = |
|
957 case t of |
|
958 (Abs a) => snd (Term.dest_abs a) |
|
959 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) *} |
955 |
960 |
956 ML {* |
961 ML {* |
957 fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 = |
962 fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 = |
958 (FIRST' [ |
963 (FIRST' [ |
959 (* "cong" rule of the of the relation / transitivity*) |
964 (* "cong" rule of the of the relation / transitivity*) |