Stream: Beginner Questions

Topic: Making use of premises in Isar without "assumes"

Chengsong Tan (Feb 08 2024 at 13:17):

I am trying to finish a proof of the following shape:

lemma mwe: "⟦a = 1+1 ∧ b = 2+1 ∧ c = 3+1 ⟧ ⟹ a = 2 ∧ b = 3 ∧ c = 4"
(is "?asmps ⟹ ?concls")
  apply(elim conjE)
proof(intro conjI)
  show "a = 2"
    sorry
next
  show "b = 3"
    sorry
next
  show "c = 4"
    sorry
qed

In each subgoal's proof the premises are all lost. How do I avoid that?
I know that the idiomatic way to use Isar is to use "assumes...shows...", however
in this proof I have a rather large conjunction (~100 conjuncts) as premise and therefore
would like to not fully expand that in the lemma statement, but break that down later using
apply(elim conjE) so that individual clauses can be picked up as needed by ATPs later for individual subgoal proofs.

Thanks a lot!

Best wishes,
Chengsong

Balazs Toth (Feb 08 2024 at 13:51):

You said you don't wanna use "assumes...shows...", but wouldn't something like this exactly solve your problem?

lemma mwe:
  assumes "a = 1+1 ∧ b = 2+1 ∧ c = 3+1 "
  shows "a = 2 ∧ b = 3 ∧ c = 4"
proof(intro conjI)
  show "a = 2"
    using assms
    apply(elim conjE)
    sorry
next
  show "b = 3"
    sorry
next
  show "c = 4"
    sorry
qed

Chengsong Tan (Feb 08 2024 at 14:26):

Balazs Toth said:

You said you don't wanna use "assumes...shows...", but wouldn't something like this exactly solve your problem?

lemma mwe:
  assumes "a = 1+1 ∧ b = 2+1 ∧ c = 3+1 "
  shows "a = 2 ∧ b = 3 ∧ c = 4"
proof(intro conjI)
  show "a = 2"
    using assms
    apply(elim conjE)
    sorry
next
  show "b = 3"
    sorry
next
  show "c = 4"
    sorry
qed

Yes it does! Thanks for the nice solution!

Chengsong Tan (Feb 08 2024 at 14:30):

Balazs Toth said:

You said you don't wanna use "assumes...shows...", but wouldn't something like this exactly solve your problem?

lemma mwe:
  assumes "a = 1+1 ∧ b = 2+1 ∧ c = 3+1 "
  shows "a = 2 ∧ b = 3 ∧ c = 4"
proof(intro conjI)
  show "a = 2"
    using assms
    apply(elim conjE)
    sorry
next
  show "b = 3"
    sorry
next
  show "c = 4"
    sorry
qed

Something like this also works:

lemma mwe: "⟦a = 1+1 ∧ b = 2+1 ∧ c = 3+1 ⟧ ⟹ a = 2 ∧ b = 3 ∧ c = 4"
(is "?asmps ⟹ ?concls")
proof(intro conjI)
  assume "?asmps"
  thus "a = 2"
    apply(elim conjE)
    by simp
next
  assume "?asmps"
  thus "b = 3"
    apply(elim conjE)
    by simp
next
  show "c = 4"
    sorry
qed

Last updated: Dec 21 2024 at 16:20 UTC