equal
deleted
inserted
replaced
788 (** term bindings **) |
788 (** term bindings **) |
789 |
789 |
790 (* simult_matches *) |
790 (* simult_matches *) |
791 |
791 |
792 fun simult_matches ctxt (t, pats) = |
792 fun simult_matches ctxt (t, pats) = |
793 (case Seq.pull (Unify.matchers (theory_of ctxt) (map (rpair t) pats)) of |
793 (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of |
794 NONE => error "Pattern match failed!" |
794 NONE => error "Pattern match failed!" |
795 | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []); |
795 | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []); |
796 |
796 |
797 |
797 |
798 (* bind_terms *) |
798 (* bind_terms *) |
896 |
896 |
897 (* fact_tac *) |
897 (* fact_tac *) |
898 |
898 |
899 local |
899 local |
900 |
900 |
901 fun comp_hhf_tac th i st = |
901 fun comp_hhf_tac ctxt th i st = |
902 PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = true} |
902 PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true} |
903 (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st; |
903 (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st; |
904 |
904 |
905 fun comp_incr_tac [] _ = no_tac |
905 fun comp_incr_tac _ [] _ = no_tac |
906 | comp_incr_tac (th :: ths) i = |
906 | comp_incr_tac ctxt (th :: ths) i = |
907 (fn st => comp_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i; |
907 (fn st => comp_hhf_tac ctxt (Drule.incr_indexes st th) i st) APPEND |
|
908 comp_incr_tac ctxt ths i; |
908 |
909 |
909 in |
910 in |
910 |
911 |
911 fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac facts; |
912 fun fact_tac ctxt facts = Goal.norm_hhf_tac ctxt THEN' comp_incr_tac ctxt facts; |
912 |
913 |
913 fun potential_facts ctxt prop = |
914 fun potential_facts ctxt prop = |
914 Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop); |
915 Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop); |
915 |
916 |
916 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i); |
917 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac ctxt (potential_facts ctxt goal) i); |