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

Makarius makarius at sketis.net
Fri Feb 12 16:52:41 CET 2016

```On Thu, 11 Feb 2016, Daniel Matichuk wrote:

> 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.

There is already a relatively long history of the 'subgoal' command
outside and inside the Isabelle repository. In the official repository the
relevant change is this:

changeset:   60626:5d13babbb3f6
user:        wenzelm
date:        Wed Jul 01 22:37:49 2015 +0200
files:       src/Pure/subgoal.ML
description:
split multi-goals as usual (outermost Pure.conjunction only);

It means that the internal Pure.conjunction is treated as in normal proof
method application: like multiple subgoals. Thus it is formally canonical,
but it still needs to be proven or disproven in actual use.

An example application is this proof pattern for multiple structured
goals:

lemma "A x ⟹ B x"
and "X u ⟹ Y u"
subgoal premises using ‹A x› sorry
subgoal premises using ‹X u› sorry
done

This replaces slightly awkward (is "?A ==> ?B") in the goal statement from
the past. I have already changed a few existing proofs in that respect.

Certain "raw" proof methods do it differently, e.g. the "induct" family.
The Pure.conjunction is preserved an somehow internalized into the
reasoning step. There could be some syntax for 'subgoal' to mean that, but
details need to be worked out.

> 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.

Note that there is something new introduced here that goes beyond plain
multi-goals A and B and C: the result of fold_subgoals is !!x. P x ==> A x
&& B x && C x with a prefix of goal parameters and premises.

It requires routine inspection if and how that affects existing uses of
Pure.conjunction. The changeset above says "outermost Pure.conjunction
only", which means I did not go into this question at that point.

BTW, the change above is from Jul-2015. A discussion like that started a
few months earlier could have had an impact on the Isabelle2016 release,
but now the train is already departed.

Makarius
```