I want to prove that if one implication is true (b --> c), then it follows that some other implication is also true (a --> c), given that there is an appropriate relation between the a and b.
Here is a concrete toy example that I'm trying to prove:
theory Prop imports Main
begin
lemma
fixes func1 :: "'a => 'a"
and func2 :: "'a => 'a"
and func3 :: "'a => 'a"
assumes "∀ x y. func1 x = func1 y --> func3 x = func3 y"
and "∀ x. func1 x = func2 x"
shows "∀ x y. func2 x = func2 y --> func3 x = func3 y"
proof -
from assms show ?thesis by auto
qed
end
The prove does not succed, Isabelle 2018 keeps running and the "by auto" part is colored purple. How should I go about proving this kind of lemmas?
It seems that your problem makes the simplifier (which is part of auto) loop. I don't really see why, but these things do happen occasionally.
When this happens, it can sometimes help to run try0 (which just tries a couple of common automatic proof methods and returns those that succeed) or sledgehammer (which tries to translate the problem into a simpler form and give it to external provers; if they can prove it, it then tries to translate the proof back to Isabelle).
In this case, both try0 and sledgehammer find that a simple apply metis can do the job. Methods like auto and simp do lots of things, including, most notably, ‘stupid’ rewriting with a pre-defined set of rules. metis is a bit more clever in what it does, but you need to manually give it every fact that it is supposed to use, and it is less adapted to Isabelle/HOL.
However, since this problem is simple first-order logic, metis can easily solve them by itself with no explicitly given facts, and it manages to avoid whatever pitfall causes auto and simp to diverge.