equal
deleted
inserted
replaced
867 |
867 |
868 (** theorems **) |
868 (** theorems **) |
869 |
869 |
870 (* fact_tac *) |
870 (* fact_tac *) |
871 |
871 |
|
872 local |
|
873 |
|
874 fun comp_hhf_tac th i st = |
|
875 PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = true} |
|
876 (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st; |
|
877 |
872 fun comp_incr_tac [] _ = no_tac |
878 fun comp_incr_tac [] _ = no_tac |
873 | comp_incr_tac (th :: ths) i = |
879 | comp_incr_tac (th :: ths) i = |
874 (fn st => Goal.compose_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i; |
880 (fn st => comp_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i; |
|
881 |
|
882 in |
875 |
883 |
876 fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts; |
884 fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts; |
877 |
885 |
878 fun potential_facts ctxt prop = |
886 fun potential_facts ctxt prop = |
879 Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop); |
887 Facts.could_unify (facts_of ctxt) (Term.strip_all_body prop); |
880 |
888 |
881 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i); |
889 fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i); |
|
890 |
|
891 end; |
882 |
892 |
883 |
893 |
884 (* get_thm(s) *) |
894 (* get_thm(s) *) |
885 |
895 |
886 local |
896 local |