Rewrting `subgoal_tac` in Isar · Beginner Questions

I wonder how to introduce a subgoal in Isar (or, proof(state) mode) like the tactic subgoal_tac did, in an elegant way:upside_down:.
Here is the example, commented existing apply ... steps, as well as my current attempt:

 lemma gen_obj_refs_subset:
  "(gen_obj_refs cap ⊆ gen_obj_refs cap')
       = (obj_refs cap ⊆ obj_refs cap'
             ∧ cap_irqs cap ⊆ cap_irqs cap'
             ∧ arch_gen_refs cap ⊆ arch_gen_refs cap')"
  apply (simp add: gen_obj_refs_def)
(*    apply (subgoal_tac "∀x y. Inl x ≠ Inr y") *)
(*   apply blast
  apply simp *)
proof -
  have a: "(∀x y. Inl x ≠ Inr y) ⟹ ((ObjRef ` obj_refs cap ⊆ ObjRef ` obj_refs cap' ∪ IRQRef ` cap_irqs cap' ∪ ArchRef ` arch_gen_refs cap' ∧
     IRQRef ` cap_irqs cap ⊆ ObjRef ` obj_refs cap' ∪ IRQRef ` cap_irqs cap' ∪ ArchRef ` arch_gen_refs cap' ∧
     ArchRef ` arch_gen_refs cap ⊆ ObjRef ` obj_refs cap' ∪ IRQRef ` cap_irqs cap' ∪ ArchRef ` arch_gen_refs cap') =
    (obj_refs cap ⊆ obj_refs cap' ∧ cap_irqs cap ⊆ cap_irqs cap' ∧ arch_gen_refs cap ⊆ arch_gen_refs cap'))" by blast
  have b: "∀x y. Inl x ≠ Inr y" by simp
  show "(ObjRef ` obj_refs cap ⊆ ObjRef ` obj_refs cap' ∪ IRQRef ` cap_irqs cap' ∪ ArchRef ` arch_gen_refs cap' ∧
     IRQRef ` cap_irqs cap ⊆ ObjRef ` obj_refs cap' ∪ IRQRef ` cap_irqs cap' ∪ ArchRef ` arch_gen_refs cap' ∧
     ArchRef ` arch_gen_refs cap ⊆ ObjRef ` obj_refs cap' ∪ IRQRef ` cap_irqs cap' ∪ ArchRef ` arch_gen_refs cap') =
    (obj_refs cap ⊆ obj_refs cap' ∧ cap_irqs cap ⊆ cap_irqs cap' ∧ arch_gen_refs cap ⊆ arch_gen_refs cap')"
    apply (simp add: a b)
    done
qed

(ObjRef ` obj_refs cap ⊆ ... is just copied from the IDE output and its meaning does not matter.

irvin (Oct 29 2025 at 12:00):

In this case "∀x y. Inl x ≠ Inr y" is already a theorem and you can just do using Sum_type.Inl_not_Inr by blast

David Wang (Oct 29 2025 at 19:18):

I don't know exactly how subgoal tac works, but this looks like something you could do with presume:

lemma assumes p: P
  and pq: "P ⟹ Q"
  and pr: "P ⟹ R"
  and rqs: "R ⟹ Q ⟹ S"
  and st: "S ⟹ T"
shows T
proof -
  presume S
  thus T using st by simp
next
  presume "R ∧ Q"
  thus S using rqs by simp
next
  show "R ∧ Q" using pr pq p by simp
qed

lemma assumes p: P
  and pq: "P ⟹ Q"
  and pr: "P ⟹ R"
  and rqs: "R ⟹ Q ⟹ S"
  and st: "S ⟹ T"
shows T
  apply (subgoal_tac "S")
   apply (rule st, assumption)
  apply (subgoal_tac "R ∧ Q")
   apply (rule rqs)
    apply (erule conjE, assumption)
   apply (erule conjE, assumption)
  apply (rule conjI)
   apply (rule pr)
   apply (rule p)
  apply (rule pq)
  by (rule p)

Stream: Beginner Questions

Topic: Rewrting `subgoal_tac` in Isar

ws (Oct 29 2025 at 06:15):

irvin (Oct 29 2025 at 12:00):

David Wang (Oct 29 2025 at 19:18):

ws (Oct 30 2025 at 01:37):