Applying the results obtained by "try" · Beginner Questions

lemma KGproof_APPEND: "KGproof Γ p2 ⟹ (KGproof Γ p1 ⟹ KGproof Γ (p1 @ p2))"
proof (induction p2 arbitrary: p1 rule:KGproof.induct)
  try0

qed

proof (state)
goal (7 subgoals):
 1. ⋀G p1. KGproof G p1 ⟹ KGproof G (p1 @ [])
 2. ⋀G p f1 f2 p1.
       (KGproof G p ∧ (∀x. KGproof G x ⟶ KGproof G (x @ p))) ∧
       List.member p (f1 → f2) ∧ List.member p f1 ⟹
       KGproof G p1 ⟹ KGproof G (p1 @ p @ [f2])
 3. ⋀G p f σ p1.
       (KGproof G p ∧ (∀x. KGproof G x ⟶ KGproof G (x @ p))) ∧ List.member p f ⟹
       KGproof G p1 ⟹ KGproof G (p1 @ p @ [subst σ f])
 4. ⋀G p f p1.
       (KGproof G p ∧ (∀x. KGproof G x ⟶ KGproof G (x @ p))) ∧ List.member p f ⟹
       KGproof G p1 ⟹ KGproof G (p1 @ p @ [BOX f])
 5. ⋀G p form p1.
       KGproof G p ⟹
       (⋀p1. KGproof G p1 ⟹ KGproof G (p1 @ p)) ⟹
       KGproof G p1 ⟹ KGproof G (p1 @ p @ [DIAM form → NOT (BOX (NOT form))])
 6. ⋀G p f p1.
       (KGproof G p ∧ (∀x. KGproof G x ⟶ KGproof G (x @ p))) ∧ ptaut f ⟹
       KGproof G p1 ⟹ KGproof G (p1 @ p @ [f])
 7. ⋀G p f p1.
       (KGproof G p ∧ (∀x. KGproof G x ⟶ KGproof G (x @ p))) ∧ f ∈ G ⟹
       KGproof G p1 ⟹ KGproof G (p1 @ p @ [f])

Trying "simp", "auto", "blast", "metis", "argo", "linarith", "presburger", "algebra", "fast", "fastforce", "force", "meson", "satx", and "order"...
Found proof: apply simp (0 ms)
Found proof: apply auto[1] (0 ms)
Found proof: apply fastforce (0 ms)
Found proof: apply force (0 ms)
Try this: apply simp (0 ms)

I only find in documentations the descriptions about the function of "try", it will try the tactics on the goal, and I am taught by the tutorial that "apply" attacks all the existing subgoals. May I please ask how to use the result other than:

have "" ... by (something obtained by try)
have "" ... by (something obtained by try, again)

And, without some "have" and "show", I cannot write "apply" when 7 subgoals are displayed on the interactive window. Previously I just copy and paste what try gives me to each subgoal, but now they are 7 of them, so it becomes a bit labor-taking. Is the "one-by-one" approach the best we can do? (I will not be supervised too much if the answer is yes... My impression is Isar is forbidding anything that breaks the readability of a proof.)

Yiming Xu (Sep 17 2024 at 13:22):

I wrote the expanded proof of the example. But note that this question remains unsolved, even partially. I will (greatly!) appreciate comments on the shortcuts I should take. There is many repetition.

lemma KGproof_APPEND: "KGproof Γ p2 ⟹ (KGproof Γ p1 ⟹ KGproof Γ (p1 @ p2))"
proof (induction p2 arbitrary: p1 rule:KGproof.induct)
  case (1 G)
  then show ?case by simp
next
  case (2 G p f1 f2)
  then show ?case
  proof -
    have a1: "KGproof G (p1 @ p)" using 2 by auto
    have a2: "List.member (p1 @ p) (f1 → f2)" using 2
      by (simp add: member_def)
    have a3: "List.member (p1 @ p) f1" using 2
      by (simp add: member_def)
    from a1 a2 a3 show ?case
    by (metis KGproof.intros(2) append.assoc)
  qed
next
  case (3 G p f σ)
  then show ?case
  proof -
  have a1: "KGproof G (p1 @ p)" using 3 by auto
    have a2: "List.member (p1 @ p) (f)" using 3
      by (simp add: member_def)
    from a1 a2 show ?case
    by (metis KGproof.intros(3) append.assoc)
qed
next
  case (4 G p f)
  then show ?case
  proof -
  have a1: "KGproof G (p1 @ p)" using 4 by auto
    have a2: "List.member (p1 @ p) (f)" using 4
      by (simp add: member_def)
    from a1 a2 show ?case
    by (metis KGproof.intros(4) append.assoc)
  qed
next
  case (5 G p form)
  then show ?case
  proof -
    have a1: "KGproof G (p1 @ p)" using 5 by auto
    from a1 show ?case
    by (metis KGproof.intros(5) append.assoc)
  qed
next
  case (6 G p f)
  then show ?case
  proof -
    have a1: "KGproof G (p1 @ p)" using 6 by auto
    from a1 6 show ?case
    by (metis KGproof.intros(6) append.assoc)
  qed
next
  case (7 G p f)
  then show ?case
  proof -
    have a1: "KGproof G (p1 @ p)" using 7 by auto
    from a1 7 show ?case
    by (metis KGproof.intros(7) append.assoc)
  qed
qed

Mathias Fleury (Sep 17 2024 at 17:41):

  case (7 G p f)
  then show ?case
  proof -
    have a1: "KGproof G (p1 @ p)" using 7 by auto
    from a1 7 show ?case
    by (metis KGproof.intros(7) append.assoc)
  qed

->


  case (7 G p f)
   have a1: "KGproof G (p1 @ p)" using 7 by auto
   with 7 show ?case
      by (metis KGproof.intros(7) append.assoc)

Yiming Xu (Sep 17 2024 at 17:52):

Thanks! I will try it now. So may I please confirm: it does not make sense to do proof - and then immediately try0?

Mathias Fleury (Sep 17 2024 at 17:56):

Yiming Xu (Sep 17 2024 at 17:57):

I do not intend to fight Isabelle. Sometimes I am irritated by what it gives me. I will make attempts to get used to it. I am irritated when I do not know how to proceed if I cannot change the appearance of the goal. I do believe I will appreciate Isar after some days.

Yiming Xu (Sep 17 2024 at 17:57):

But in this case, if it does give something, can I tell which goal does it apply?

Mathias Fleury (Sep 17 2024 at 17:57):

For completeness: I am aware that using try0 the way you are doing can help to populate the ... in qed ..., but I do not like that syntax because it is basically apply style

Mathias Fleury (Sep 17 2024 at 17:58):