Stylistic choice, rule vs. erule · Beginner Questions

Should you only use erule when the rule does not change the goal? In other words, should it be used as a method to split the state of the assumptions or can it be used to perform a forward and backward step at once while splitting the goal cases?

A bit of background. Many elimination rules are set up to apply to arbitrary goal states. E.g.: conjE:

apply (erule inv_maintained) (* or *) apply (rule inv_maintained) apply assumption (* or *) apply (rule inv_maintained, assumption) (* What is a good stylistic choice? *)

context
  fixes P Q P1 P2 P3 P4 P5 P6 P7 P8 Q1 Q2 Q3 Q4 Q5
    and P_inv
    and Q_inv::"('a × 'a) ⇒ bool"
    and f::"('a × 'a) ⇒ ('a × 'a)"
    and g::"'a ⇒ 'a"
  assumes PD: "P x ⟹ P_inv x"
              "P x ⟹ P3 x"
              "P x ⟹ P4 x"
              "P x ⟹ P5 x"
              "P x ⟹ P6 x"
              "P x ⟹ P7 x"
              "P x ⟹ P8 x"
    and P_invD: "P_inv x ⟹ P1 x"
                "P_inv x ⟹ P2 x"
    and Q_invI: "Q1 x ⟹ Q2 x ⟹ Q_inv x"
  and QI: "Q_inv x ⟹ Q3 x ⟹ Q4 x ⟹ Q5 x ⟹ Q x"
begin

lemma provable_trivial:
  assumes "fst x = fst x'"
  shows
    "P1 x ⟹ Q1 x'"
    "P2 x ⟹ Q2 x'"
  sorry

lemma provable_non_trivial:
  "P1 x ⟹ Q1 (f x)"
  "P2 x ⟹ Q2 (f x)"
  "P3 x ⟹ P4 x ⟹ Q3 (f x)"
  "P4 x ⟹ P5 x ⟹ Q4 (f x)"
  "P6 x ⟹ P7 x ⟹ P8 x ⟹ Q5 (f x)"
  sorry

lemma PE:
  assumes "P x"
    and "P_inv x ⟹ P3 x ⟹ P4 x ⟹ P5 x ⟹ P6 x ⟹ P7 x ⟹ P8 x ⟹ thesis"
  shows thesis
  using assms PD P_invD by auto

lemma P_invE:
  assumes "P_inv x"
    and "P1 x ⟹ P2 x ⟹ thesis"
  shows thesis using P_invD assms by auto

lemma goal: "P x ⟹ Q (f x)"
  apply (rule QI)
    apply (rule Q_invI)
  subgoal
    apply (erule PE)
    apply (erule P_invE)
    by (rule provable_non_trivial)
  subgoal
    apply (erule PE)
    apply (erule P_invE)
    by (rule provable_non_trivial)
  subgoal
    apply (erule PE)
    by (rule provable_non_trivial)
  subgoal
    apply (erule PE)
    by (rule provable_non_trivial)
  subgoal
    apply (erule PE)
    apply (rule provable_non_trivial)
    by simp+
  done

lemma inv_maintained:
  assumes "P_inv x"
      and "P1 x ⟹ Q1 x'"
          "P2 x ⟹ Q2 x'"
    shows "Q_inv x'"
  using P_invD Q_invI assms by blast

lemma goal':
  assumes fa: "f = (λ(x, y). (x, g y))"
    shows "P x ⟹ Q (f x)"
  apply (rule QI)
  subgoal
    apply (drule PD(1))
    apply (erule inv_maintained) (* or *) apply (rule inv_maintained) apply assumption (* or *) apply (rule inv_maintained, assumption) (* What is a good stylistic choice? *)
    subgoal apply (rule provable_trivial[rotated], assumption) (* okay *)
      apply (cases x)
      by (simp add: fa)+
    subgoal apply (erule provable_trivial[rotated]) (* probably not clean *)
      apply (cases x)
      by (simp add: fa)+
  done
  subgoal
    apply (frule PD(2))
    apply (drule PD(3))
    by (rule provable_non_trivial)
  subgoal
    apply (frule PD(3))
    apply (drule PD(4))
    by (rule provable_non_trivial)
  subgoal
    apply (frule PD(5))
    apply (frule PD(6))
    apply (drule PD(7))
    by (rule provable_non_trivial)
  done

end

Another stylistic note. The following is also a possibility for proving the subgoals of goal'. Is it bad practice to use defer and prefer?

    subgoal apply (rule provable_trivial)
     prefer 2
      apply assumption
      apply (cases x)
      by (simp add: fa)+

Mathias Fleury (Jun 11 2025 at 10:42):

Mathias Fleury (Jun 11 2025 at 10:43):

David Wang (Jun 11 2025 at 10:59):

To use apply scripts is a deliberate choice in this case. Some terms in the actual (non-example) theories became very large and were related to some other terms. Binding variables and adding assumptions in context blocks helped to some extent, but assumptions became hard to keep track of.

Stream: Beginner Questions

Topic: Stylistic choice, rule vs. erule

David Wang (Jun 11 2025 at 10:34):

Mathias Fleury (Jun 11 2025 at 10:42):

Mathias Fleury (Jun 11 2025 at 10:43):

David Wang (Jun 11 2025 at 10:59):

David Wang (Jun 12 2025 at 14:22):