Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving implication (a --> c) from (b --> c) g...

Email Gateway (Aug 22 2022 at 18:08):

From: Miha Marolt <miham@beyondsemi.com>
Hi,

I need some help. 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?

Email Gateway (Aug 22 2022 at 18:08):

From: Miha Marolt <miham@beyondsemi.com>
Hi,

I already received answer on StackOverflow: https://stackoverflow.com/q/52073140/6393996. Sorry for the noise.

Email Gateway (Aug 22 2022 at 18:08):

From: Manuel Eberl <eberlm@in.tum.de>
For context:
https://stackoverflow.com/questions/52073140/proving-implication-a-c-from-b-c-given-relation-between-a-and-b/52084855#52084855

Last updated: Nov 21 2024 at 12:39 UTC