Stream: Beginner Questions

Topic: Postpone Goals

Jakob Schulz (Jan 16 2023 at 15:13):

Hi :) I am currently doing proofs in which similar goals are generated multiple times. As a simplified example, let's say I have the following code:

context cring begin

definition inc where
"inc x ≡ x ⊕ 𝟭"

lemma inc_closed[simp]: "x ∈ carrier R ⟹ inc x ∈ carrier R"
  unfolding inc_def by simp

lemma
  assumes "x ∈ carrier R"
  shows "x ⊗ (inc (inc x)) ∈ carrier R"
  apply (intro m_closed)

Then, the application of introleaves these two subgoals:

goal (2 subgoals):
 1. x ∈ carrier R
 2. inc (inc x) ∈ carrier R

I could now prove the first subgoal by writing using assms apply simpdirectly, but if I would start proving the second subgoal by apply (intro inc_closed), this would generate exactly the same as the first subgoal. So, is there a way to postpone the first subgoal, so that I can simplify the second subgoal first and then solve the remaining equal goals at once?

Lukas Stevens (Jan 16 2023 at 15:37):

You can use defer but that is not good style.

Lukas Stevens (Jan 16 2023 at 15:39):

I think apply(intro m_closed; (intro inc_closed)?) should work

Last updated: Apr 27 2024 at 20:14 UTC