[isabelle-dev] "Subgoal" command and meta-conjunctions

[Daniel Matichuk]

In Isabelle2016-RC4 I’ve noticed that there is a small but significant issue with how the “subgoal” command handles meta-conjuncts.

I have a method which folds subgoals into meta conjunctions, which is effectively the reverse of Goal.conjunction_tac. The intention is that you can collapse several subgoals into one for the purposes of discharging them with “subgoal”.

Example:

lemma
  assumes A: A and B: B and C: C
  shows
  "A ∧ B ∧ C"
  apply (intro conjI)
  apply fold_subgoals[2]
  subgoal by (auto intro: A B)
  apply (rule C)
  done


This worked in my old implementation of subgoal, but I have recently discovered that “subgoal” (Isabelle2016) is introducing the conjunction before focusing. This results in only focusing on the first conjunct, instead of the entire meta-conjunct.

The obvious solution from my end is to have “fold_subgoals” use a custom meta-connective that needs to be explicitly introduced after the “subgoal”, but I was wondering if it would be possible to postpone the meta-conjuction introduction until after the subgoal focus.

-Dan

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.