[isabelle-dev] "Subgoal" command and meta-conjunctions
Daniel.Matichuk at nicta.com.au
Thu Feb 11 05:10:43 CET 2016
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”.
assumes A: A and B: B and C: C
"A ∧ B ∧ C"
apply (intro conjI)
subgoal by (auto intro: A B)
apply (rule C)
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.
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.
More information about the isabelle-dev